English
Kruskal-Katona theorem bounding the shadow: Given a family of r-sets and an initial segment 𝒞 of the same size, the shadow of 𝒞 is no larger than the shadow of the original family 𝒜.
Русский
Теорема Крускал-Катона ограничивает тень: дано семейство r-множест на равной размерности; тень начального сегмента не превосходит тени исходного семейства.
LaTeX
$$$|\partial 𝒞| \le |\partial 𝒜| \quad\text{under appropriate size conditions}$$$
Lean4
/-- **Kleitman's theorem**. An intersecting family on `n` elements contains at most `2ⁿ⁻¹` sets, and
each further intersecting family takes at most half of the sets that are in no previous family. -/
theorem card_biUnion_le_of_intersecting (s : Finset ι) (f : ι → Finset (Finset α))
(hf : ∀ i ∈ s, (f i : Set (Finset α)).Intersecting) :
#(s.biUnion f) ≤ 2 ^ Fintype.card α - 2 ^ (Fintype.card α - #s) :=
by
have : DecidableEq ι := by classical infer_instance
obtain hs | hs := le_total (Fintype.card α) #s
· rw [tsub_eq_zero_of_le hs, pow_zero]
refine
(card_le_card <|
biUnion_subset.2 fun i hi a ha ↦ mem_compl.2 <| notMem_singleton.2 <| (hf _ hi).ne_bot ha).trans_eq
?_
rw [card_compl, Fintype.card_finset, card_singleton]
induction s using Finset.cons_induction generalizing f with
| empty => simp
| cons i s hi
ih =>
set f' : ι → Finset (Finset α) := fun j ↦ if hj : j ∈ cons i s hi then (hf j hj).exists_card_eq.choose else ∅
have hf₁ :
∀ j, j ∈ cons i s hi → f j ⊆ f' j ∧ 2 * #(f' j) = 2 ^ Fintype.card α ∧ (f' j : Set (Finset α)).Intersecting :=
by
rintro j hj
simp_rw [f', dif_pos hj, ← Fintype.card_finset]
exact Classical.choose_spec (hf j hj).exists_card_eq
have hf₂ : ∀ j, j ∈ cons i s hi → IsUpperSet (f' j : Set (Finset α)) :=
by
refine fun j hj ↦ (hf₁ _ hj).2.2.isUpperSet' ((hf₁ _ hj).2.2.is_max_iff_card_eq.2 ?_)
rw [Fintype.card_finset]
exact (hf₁ _ hj).2.1
refine (card_le_card <| biUnion_mono fun j hj ↦ (hf₁ _ hj).1).trans ?_
nth_rw 1 [cons_eq_insert i]
rw [biUnion_insert]
refine (card_mono <| @le_sup_sdiff _ _ _ <| f' i).trans ((card_union_le _ _).trans ?_)
rw [union_sdiff_left, sdiff_eq_inter_compl]
refine le_of_mul_le_mul_left ?_ (pow_pos (zero_lt_two' ℕ) <| Fintype.card α + 1)
rw [pow_succ, mul_add, mul_assoc, mul_comm _ 2, mul_assoc]
refine
(add_le_add ((mul_le_mul_iff_right₀ <| pow_pos (zero_lt_two' ℕ) _).2 (hf₁ _ <| mem_cons_self _ _).2.2.card_le) <|
(mul_le_mul_iff_right₀ <| zero_lt_two' ℕ).2 <| IsUpperSet.card_inter_le_finset ?_ ?_).trans
?_
· rw [coe_biUnion]
exact isUpperSet_iUnion₂ fun i hi ↦ hf₂ _ <| subset_cons _ hi
· rw [coe_compl]
exact (hf₂ _ <| mem_cons_self _ _).compl
rw [mul_tsub, card_compl, Fintype.card_finset, mul_left_comm, mul_tsub, (hf₁ _ <| mem_cons_self _ _).2.1, two_mul,
add_tsub_cancel_left, ← mul_tsub, ← mul_two, mul_assoc, ← add_mul, mul_comm]
refine mul_le_mul_left' ?_ _
refine
(add_le_add_left (ih _ (fun i hi ↦ (hf₁ _ <| subset_cons _ hi).2.2) ((card_le_card <| subset_cons _).trans hs))
_).trans
?_
rw [mul_tsub, two_mul, ← pow_succ', ←
add_tsub_assoc_of_le (pow_right_mono₀ (one_le_two : (1 : ℕ) ≤ 2) tsub_le_self), tsub_add_eq_add_tsub hs,
card_cons, add_tsub_add_eq_tsub_right]
