Proof of the LYM inequality using probability theory

Stream: maths

[Ching-Tsun Chou]

Just for fun, I formalized a proof of the LYM inequality using (very elementary) probability theory:

https://github.com/ctchou/my_lean/blob/main/MyLean/ProbLYM.lean

The informal proof on which my formalization is based is in sec.1.2 of these lecture notes:

https://yufeizhao.com/pm/probmethod_notes.pdf

A lecture video on the proof can be found here:

https://youtu.be/exBXHYl4po8?si=aW8hhJ6zBrvWT1T0

I am very grateful to @Chris Wong, who came up with a much more elegant definition of Numbering than the one I had that reduced the proof size of the cardinality of SetPrefixby about 150 lines of code. So I have included him as a co-author of the file. (The proof of is_prefix_equiv is basically Chris's verbatim.) The relevant discussion can be found in this thread:

#new members > How to reason about Fin type

The proof of the lemma aux_1 is due to @Aaron Liu. I also benefited greatly from the answers I got on Zulip.

Your comments will be greatly appreciated.

[Ching-Tsun Chou]

PS. I do know that the proof of the LYM inequality already exists in mathlib. The above is just for my own edification.

[Yaël Dillies]

Nice! This is also the proof done in the Cambridge combinatorics lecture notes (Theorem 1.10, Lecture 3). Would you like to contribute your proof to LeanCamCombi?

[Chris Wong]

Glad to hear I could help! I second Yaël's suggestion. They give very good feedback.

[Ching-Tsun Chou]

@Yaël Dillies, how do you want me to contribute? The proof under theorem 1.10 of the Cambridge lecture seems to be the proof I formalized but with probability stripped out. Do you want my proof as it is currently formulated, or with probability stripped out?

[Yaël Dillies]

Both versions are close enough in my mind that I won't bother you with it :smile:

[Ching-Tsun Chou]

In which directory should I place my file?
BTW, I don't really know much combinatorics. Why does the proof use "Katona's circle method"?

[Ching-Tsun Chou]

PR: https://github.com/YaelDillies/LeanCamCombi/pull/42

[Ching-Tsun Chou]

Just to update that the proof is now in:
https://github.com/YaelDillies/LeanCamCombi/commit/da0f82e05a2791ec928bac015672c40563f35c5e
Most of the improvements are due to @Yaël Dillies, including:
(1) NumberingOn s is removed in favor of Numberings s, which is equal to Numbering {x // x ∈ s}.
(2) Mathlib.Data.Finset.Densityis used instead of the heavy-duty probability theory.
Reading Yaël's code is a great education!

[Chris Wong]

TIL about docs#Finset.dens . This would be useful for my own project too!