English
Lovász formulation of Kruskal–Katona: a lower bound on the i-th iterated shadow of a family via the r-choose bounds.
Русский
Формулировка Ловаша теоремы Крускал-Катона: нижняя оценка i-й итерационной тени через биномиальные границы.
LaTeX
$$$k \choose (r-i) \le |(\partial^{[i]} 𝒜)|$ under appropriate hypotheses$$
Lean4
/-- The **Lovasz formulation of the Kruskal-Katona theorem**.
If `|𝒜| ≥ k choose r`, (and everything in `𝒜` has size `r`) then the initial segment we compare to
is just all the subsets of `{0, ..., k - 1}` of size `r`. The `i`-th iterated shadow of this is all
the subsets of `{0, ..., k - 1}` of size `r - i`, so the `i`-th iterated shadow of `𝒜` has at least
`k.choose (r - i)` elements. -/
theorem kruskal_katona_lovasz_form (hir : i ≤ r) (hrk : r ≤ k) (hkn : k ≤ n) (h₁ : (𝒜 : Set (Finset (Fin n))).Sized r)
(h₂ : k.choose r ≤ #𝒜) : k.choose (r - i) ≤ #(∂ ^[i] 𝒜) :=
by
set range'k : Finset (Fin n) := attachFin (range k) fun m ↦ by rw [mem_range]; apply forall_lt_iff_le.2 hkn
set 𝒞 : Finset (Finset (Fin n)) := powersetCard r range'k
have : (𝒞 : Set (Finset (Fin n))).Sized r := Set.sized_powersetCard _ _
calc
k.choose (r - i)
_ = #(powersetCard (r - i) range'k) := by rw [card_powersetCard, card_attachFin, card_range]
_ = #(∂ ^[i] 𝒞) := by
congr!
ext B
rw [mem_powersetCard, mem_shadow_iterate_iff_exists_sdiff]
constructor
· rintro ⟨hBk, hB⟩
have :=
exists_subsuperset_card_eq hBk (Nat.le_add_left _ i) <| by
rwa [hB, card_attachFin, card_range, ← Nat.add_sub_assoc hir, Nat.add_sub_cancel_left]
obtain ⟨C, BsubC, hCrange, hcard⟩ := this
rw [hB, ← Nat.add_sub_assoc hir, Nat.add_sub_cancel_left] at hcard
refine ⟨C, mem_powersetCard.2 ⟨hCrange, hcard⟩, BsubC, ?_⟩
rw [card_sdiff_of_subset BsubC, hcard, hB, Nat.sub_sub_self hir]
· rintro ⟨A, Ah, hBA, card_sdiff_i⟩
rw [mem_powersetCard] at Ah
refine ⟨hBA.trans Ah.1, eq_tsub_of_add_eq ?_⟩
rw [← Ah.2, ← card_sdiff_i, add_comm, card_sdiff_add_card_eq_card hBA]
_ ≤ #(∂ ^[i] 𝒜) := by
refine iterated_kk h₁ ?_ ⟨‹_›, ?_⟩
· rwa [card_powersetCard, card_attachFin, card_range]
simp_rw [𝒞, mem_powersetCard]
rintro A B hA ⟨HB₁, HB₂⟩
refine ⟨fun t ht ↦ ?_, ‹_›⟩
rw [mem_attachFin, mem_range]
have : toColex (image Fin.val B) < toColex (image Fin.val A) := by
rwa [toColex_image_lt_toColex_image Fin.val_strictMono]
apply Colex.forall_lt_mono this.le _ t (mem_image.2 ⟨t, ht, rfl⟩)
simp_rw [mem_image]
rintro _ ⟨a, ha, hab⟩
simpa [range'k, hab] using hA.1 ha
