English
If 𝒜 is an antichain of finite subsets of α with n = |α|, then the sum over s ∈ 𝒜 of (C(n, |s|))^{-1} does not exceed 1.
Русский
Если 𝒜 — антицепь конечных подмножеств α, где n = |α|, то сумма по s ∈ 𝒜 из (C(n, |s|))^{-1} не превосходит 1.
LaTeX
$$$$ \\sum_{s \\in 𝒜} \\left( {n \\choose |s| } \\right)^{-1} \\le 1 $$$$
Lean4
/-- The **Lubell-Yamamoto-Meshalkin inequality**, also known as the **LYM inequality**.
If `𝒜` is an antichain, then the sum of `(#α.choose #s)⁻¹` over `s ∈ 𝒜` is less than `1`. -/
theorem lubell_yamamoto_meshalkin_inequality_sum_inv_choose (h𝒜 : IsAntichain (· ⊆ ·) 𝒜.toSet) :
∑ s ∈ 𝒜, ((Fintype.card α).choose #s : 𝕜)⁻¹ ≤ 1 := by
calc
_ = ∑ r ∈ range (Fintype.card α + 1), ∑ s ∈ 𝒜 with #s = r, ((Fintype.card α).choose r : 𝕜)⁻¹ := by
rw [sum_fiberwise_of_maps_to']; simp [Nat.lt_succ_iff, card_le_univ]
_ = ∑ r ∈ range (Fintype.card α + 1), (#(𝒜 #r) / (Fintype.card α).choose r : 𝕜) := by simp [slice, div_eq_mul_inv]
_ ≤ 1 := lubell_yamamoto_meshalkin_inequality_sum_card_div_choose h𝒜
