The LYM inequality using probability theory #

This file proves the LYM inequality using (very elementary) probability theory.

References #

This proof formalizes Section 1.2 of Prof. Yufei Zhao's lecture notes for MIT 18.226:

A video of Prof. Zhao's lecture is available on YouTube:

The proof of Theorem 1.10, Lecture 3 in the Cambridge lecture notes on combinatorics:

is basically the same proof, except without using probability theory.

theorem LYM_inequality {α : Type u_1} [Fintype α] {𝒜 : Finset (Finset α)} (h𝒜 : IsAntichain (fun (x1 x2 : Finset α) => x1 ⊆ x2) ↑𝒜) :

∑ s ∈ 𝒜, (↑((Fintype.card α).choose s.card))⁻¹ ≤ 1

The Lubell-Yamamoto-Meshalkin inequality, proved using the Katona circle method.