English
For a finite α with n = |α| and antichain 𝒜, summing certain normalized layer sizes up to k yields a bound controlled by the remaining shadow at level n−k.
Русский
Для конечного α с n = |α| и антицепи 𝒜 сумма нормированных размеров слоёв до уровня k удовлетворяет ограничению, зависящему от падения на уровне n−k.
LaTeX
$$$$ \\sum_{r=0}^{k} \\frac{|(𝒜 \\# (n-r))|}{\\binom{n}{n-r}} \\le \\frac{|falling (n-k) 𝒜|}{\\binom{n}{n-k}} $$$$
Lean4
/-- A bound on any top part of the sum in LYM in terms of the size of `falling k 𝒜`. -/
theorem le_card_falling_div_choose [Fintype α] (hk : k ≤ Fintype.card α)
(h𝒜 : IsAntichain (· ⊆ ·) (𝒜 : Set (Finset α))) :
(∑ r ∈ range (k + 1), (#(𝒜 #(Fintype.card α - r)) : 𝕜) / (Fintype.card α).choose (Fintype.card α - r)) ≤
(falling (Fintype.card α - k) 𝒜).card / (Fintype.card α).choose (Fintype.card α - k) :=
by
induction k with
|
zero =>
simp only [tsub_zero, cast_one, cast_le, sum_singleton, div_one, choose_self, range_one, zero_add, range_one,
sum_singleton, tsub_zero, choose_self, cast_one, div_one, cast_le]
exact card_le_card (slice_subset_falling _ _)
| succ k
ih =>
rw [sum_range_succ, ← slice_union_shadow_falling_succ,
card_union_of_disjoint (IsAntichain.disjoint_slice_shadow_falling h𝒜), cast_add, _root_.add_div, add_comm]
rw [← tsub_tsub, tsub_add_cancel_of_le (le_tsub_of_add_le_left hk)]
exact
add_le_add_left
((ih <| le_of_succ_le hk).trans <|
local_lubell_yamamoto_meshalkin_inequality_div (tsub_pos_iff_lt.2 <| Nat.succ_le_iff.1 hk).ne' <|
sized_falling _ _)
_
