English
Let α be a finite set and 𝒜 be a finite antichain of subsets of α with ∅ not in 𝒜. Then the sum over s in 𝒜 of 1 / binom(|α|, |s|) is at most infSum(𝒜).
Русский
Пусть α — конечное множество, а 𝒜 — конечное антицепное семейство подмножеств α, не содержащее пустое множество. Тогда сумма по s∈𝒜 от 1/ C(|α|, |s|) не превосходит infSum(𝒜).
LaTeX
$$$\sum_{s \in 𝒜} {\binom{|\alpha|}{|s|}}^{-1} \le \infSum 𝒜$$$
Lean4
theorem le_infSum (h𝒜 : IsAntichain (· ⊆ ·) (𝒜 : Set (Finset α))) (h𝒜₀ : ∅ ∉ 𝒜) :
∑ s ∈ 𝒜, ((card α).choose #s : ℚ)⁻¹ ≤ infSum 𝒜 :=
by
calc
_ = ∑ s ∈ 𝒜, #(truncatedInf 𝒜 s) / (#s * (card α).choose #s : ℚ) := ?_
_ ≤ _ := sum_le_univ_sum_of_nonneg fun s ↦ by positivity
refine sum_congr rfl fun s hs ↦ ?_
rw [truncatedInf_of_isAntichain h𝒜 hs, div_mul_cancel_left₀]
have := (nonempty_iff_ne_empty.2 <| ne_of_mem_of_not_mem hs h𝒜₀).card_pos
positivity
