English
Let 𝒜 be an antichain in Finset α with α finite and n = |α|. Then the Lubell–Yamamoto–Meshalkin inequality says the weighted sum of layer sizes over all r satisfies ∑_{r=0}^{n} |𝒜 #r| / C(n,r) ≤ 1.
Русский
Пусть 𝒜 — антицепь в Finset α, где α конечно, n = |α|. Тогда неравенство Льюмелла–Ямамото–Мешалкин: сумма по слоям ∑_{r=0}^{n} |𝒜 #r| / C(n,r) ≤ 1.
LaTeX
$$$$ \\sum_{r=0}^{n} \\frac{|𝒜 \\# r|}{\\binom{n}{r}} \\le 1 $$$$
Lean4
/-- The **Lubell-Yamamoto-Meshalkin inequality**, also known as the **LYM inequality**.
If `𝒜` is an antichain, then the sum of the proportion of elements it takes from each layer is less
than `1`. -/
theorem lubell_yamamoto_meshalkin_inequality_sum_card_div_choose (h𝒜 : IsAntichain (· ⊆ ·) (𝒜 : Set (Finset α))) :
∑ r ∈ range (Fintype.card α + 1), (#(𝒜 #r) / (Fintype.card α).choose r : 𝕜) ≤ 1 := by
classical
rw [← sum_flip]
refine (le_card_falling_div_choose le_rfl h𝒜).trans ?_
rw [div_le_iff₀] <;> norm_cast
· simpa only [Nat.sub_self, one_mul, Nat.choose_zero_right, falling] using Set.Sized.card_le (sized_falling 0 𝒜)
· rw [tsub_self, choose_zero_right]
exact zero_lt_one
