English
The downward LYM inequality for Finset families: the size of an r-shadow is controlled by the size of the (r-1)-shadow under suitable conditions.
Русский
Локальное неравенство LYM в нисходящем направлении для семей множеств: размер r-тени управляется размером (r-1)-тени.
LaTeX
$$$|\mathcal{A}| \cdot r \le |∂\mathcal{A}| \cdot (|\alpha| - r + 1)$$$
Lean4
/-- The downward **local LYM inequality**, with cancelled denominators. `𝒜` takes up less of `α^(r)`
(the finsets of card `r`) than `∂𝒜` takes up of `α^(r - 1)`. -/
theorem local_lubell_yamamoto_meshalkin_inequality_mul (h𝒜 : (𝒜 : Set (Finset α)).Sized r) :
#𝒜 * r ≤ #(∂ 𝒜) * (Fintype.card α - r + 1) :=
by
let i : DecidableRel ((· ⊆ ·) : Finset α → Finset α → Prop) := fun _ _ => Classical.dec _
refine card_mul_le_card_mul' (· ⊆ ·) (fun s hs => ?_) (fun s hs => ?_)
· rw [← h𝒜 hs, ← card_image_of_injOn s.erase_injOn]
refine card_le_card ?_
simp_rw [image_subset_iff, mem_bipartiteBelow]
exact fun a ha => ⟨erase_mem_shadow hs ha, erase_subset _ _⟩
refine le_trans ?_ tsub_tsub_le_tsub_add
rw [← (Set.Sized.shadow h𝒜) hs, ← card_compl, ← card_image_of_injOn (insert_inj_on' _)]
refine card_le_card fun t ht => ?_
rw [mem_bipartiteAbove] at ht
have : ∅ ∉ 𝒜 := by
rw [← mem_coe, h𝒜.empty_mem_iff, coe_eq_singleton]
rintro rfl
rw [shadow_singleton_empty] at hs
exact notMem_empty s hs
have h :=
exists_eq_insert_iff.2
⟨ht.2, by rw [(sized_shadow_iff this).1 (Set.Sized.shadow h𝒜) ht.1, (Set.Sized.shadow h𝒜) hs]⟩
rcases h with ⟨a, ha, rfl⟩
exact mem_image_of_mem _ (mem_compl.2 ha)
