English
A division form of the local LYM inequality comparing divided shadow sizes.
Русский
Деление локального неравенства LYM сравнивает размеры теней по делению.
LaTeX
$$$|\mathcal{A}|/\binom{|\alpha|}{r} \le |∂\mathcal{A}|/\binom{|\alpha|}{r-1}$$$
Lean4
/-- The downward **local LYM inequality**. `𝒜` takes up less of `α^(r)` (the finsets of card `r`)
than `∂𝒜` takes up of `α^(r - 1)`. -/
theorem local_lubell_yamamoto_meshalkin_inequality_div (hr : r ≠ 0) (h𝒜 : (𝒜 : Set (Finset α)).Sized r) :
(#𝒜 : 𝕜) / (Fintype.card α).choose r ≤ #(∂ 𝒜) / (Fintype.card α).choose (r - 1) :=
by
obtain hr' | hr' := lt_or_ge (Fintype.card α) r
· rw [choose_eq_zero_of_lt hr', cast_zero, div_zero]
exact div_nonneg (cast_nonneg _) (cast_nonneg _)
replace h𝒜 := local_lubell_yamamoto_meshalkin_inequality_mul h𝒜
rw [div_le_div_iff₀] <;> norm_cast
· rcases r with - | r
· exact (hr rfl).elim
rw [tsub_add_eq_add_tsub hr', add_tsub_add_eq_tsub_right] at h𝒜
apply le_of_mul_le_mul_right _ (pos_iff_ne_zero.2 hr)
convert Nat.mul_le_mul_right ((Fintype.card α).choose r) h𝒜 using 1
· simpa [mul_assoc, Nat.choose_succ_right_eq] using Or.inl (mul_comm _ _)
· simp only [mul_assoc, choose_succ_right_eq, mul_eq_mul_left_iff]
exact Or.inl (mul_comm _ _)
· exact Nat.choose_pos hr'
· exact Nat.choose_pos (r.pred_le.trans hr')
