PlainCombi: LYM inequality using the Katona circle method

[ctchou]

Per Yaël's suggestion:

https://leanprover.zulipchat.com/#narrow/channel/116395-maths/topic/Proof.20of.20the.20LYM.20inequality.20using.20probability.20theory

I'm contributing this proof. I'm not sure I'm putting the file in the right directory, though. Let me know where I should place it and I'll update the PR.

[YaelDillies]

Thank you for the PR!

Below is a first round of comments, and here are a few general remarks:

• You are not following the naming convention wrt to lowerCamelCasing definitions in lemma names and prefixing head operations (eg foo.card should become card_foo in a lemma name)
• Since it's a result from the Combinatorics course, it should go in the PlainCombi folder.
• All the numbering stuff not specific to antichains is the Katona circle method. Could you move it to a new file? (also in the PlainCombi folder)
• I dislike calling this the "probability theory" proof of LYM: It's neither probabilistic in the sense that it shows some object exists because it exists with positive probability, nor is it the only proof that manipulates probabilities (although I can't remember which other proof I am thinking off). A better description would be that it is a double-counting argument on maximal chains passing through a point of the antichain (note that the Katona circle method is precisely double-counting with maximal chains)
• Nice work! 😁

[ctchou]

@YaelDillies, If I split out the code not related to anti-chains to a different file, what should I call it?

More generally, I may need you write the comments, since I don't know much combinatorics yet. Currently I don't really know what terms like "double counting" and "Katona circle method" mean.

[ctchou]

@YaelDillies, I incorporated most of your comments and changed the naming convention. However, I did not change the definition of NumberIngOn as you suggested, because the proof of the theorem equiv_IsPrefix_Numbering2 (previously is_prefix_equiv) is very fragile and I do not yet know how much impact your suggested definition will have.

[YaelDillies]

If I split out the code not related to anti-chains to a different file, what should I call it?

Keep it in the current file. Split out the rest to PlainCombi.KatonaCircle.

More generally, I may need you write the comments, since I don't know much combinatorics yet. Currently I don't really know what terms like "double counting" and "Katona circle method" mean.

I am happy to do that when I have time.

I did not change the definition of NumberIngOn as you suggested, because the proof of the theorem equiv_IsPrefix_Numbering2 (previously is_prefix_equiv) is very fragile and I do not yet know how much impact your suggested definition will have.

Working on it!

[ctchou]

I can give your NumberingOn suggestion a try today. I didn't have time yesterday.

[ctchou]

@YaelDillies, I just pushed a new commit, in which I tried to use Numbering to define NumberingOn, as you suggested. I was able to fix the first few failures in the proof of equiv_IsPrefix_NumberingOn2, but I got stuck on the failures on lines 100 and 107. Without fixing them, the remaining failures cannot be fixed. Lines 100 and 107 are in the term mode, where I don't know my way around. I need your help on this.

[ctchou]

Instead of fixing each failure in the proof of equiv_IsPrefix_NumberingOn2, I think I'm going to prove the equivalence of the old and new definitions of NumberingOn and connect the old proof with the new definition via the equivalence. This way I don't have to touch the tricky proof. It will take me some time to do this, as I have other commitments.

[YaelDillies]

"Working on it" is usually shorthand for "I have 100 lines of uncommitted edits. Please don't edit simultaneously so that we avoid conflicts" 😅

[ctchou]

OK, I'll revert my commit and wait for you.

[ctchou]

Just pushed the revert. In the meantime, I'll play in the branch personal/ctchou/prob-lym-OLD-*, so that the PR is not impacted.

[ctchou]

In the branch personal/ctchou/prob-lym-OLD-2, NumberingOn is removed altogether. I did not try to fix the proof of equiv_IsPrefix_NumberingOn2, but kept the old proof with its old goal and used that result to prove the new equiv_IsPrefix_Numbering2.

[YaelDillies]

Okay, done. Could you now do the KatonaCircle split?

[ctchou]

I just did the split. I did not touch the comments, which are duplicated in both files. I guess you want to call ProbLYM.lean some other name now.

[ctchou]

I'm a bit mystified by your code: how did you manage to get rid of NumberingOn without invoking the theorem Fintype.card_coe anywhere? I found it necessary to use the theorem in many places in the proof of equiv_IsPrefix_Numbering2 when I tried it.

[YaelDillies]

I'm a bit mystified by your code: how did you manage to get rid of NumberingOn without invoking the theorem Fintype.card_coe anywhere?

🧙 (I used simp)

[YaelDillies]

Not sure how that happened, but you managed to do the exact opposite split to what I had in mind. I've turned it around and golfed your proof to use Finset.dens instead of the much heavier probability theoretic setup (they are wholly equivalent, but the former only imports basic finiteness).

Thanks for everything! Looking forward to the next one.

[ctchou]

Not sure how that happened, but you managed to do the exact opposite split to what I had in mind.

Because of what you wrote above:

[I asked:] If I split out the code not related to anti-chains to a different file, what should I call it?
Keep it in the current file. Split out the rest to PlainCombi.KatonaCircle.

Either I misread your answer, or you misread my question.

[YaelDillies]

Ooh, I had read "related to antichains" instead of "not related to antichains".

[ctchou]

One more question for my education: What is the difference between simps [...] using e and simps [..., e]? I realize that the latter doesn't work in many places where you have used the former, but I don't understand why.

[YaelDillies]

I assume you mean simpa, not simps.

simpa [lemmas] using term is the same as

have hyp := term
simp [lemmas] at hyp ⊢
exact hyp

You can see how this is more powerful than simp [lemmas, term], because it gets to simplify term and also unify up to defeq at the end (instead of just synteq).

[ctchou]

Thanks for the explanation!