English
The shadow of an initial segment is itself an initial segment in the colex order.
Русский
Тень начального сегмента в порядке Colex также является начальным сегментом.
LaTeX
$$$\partial(\text{initSeg } s) = \text{initSeg}(s')$ with appropriate s'$$
Lean4
/-- This is important for iterating Kruskal-Katona: the shadow of an initial segment is also an
initial segment. -/
theorem shadow_initSeg [Fintype α] (hs : s.Nonempty) : ∂ (initSeg s) = initSeg (erase s <| min' s hs) := by
-- This is a pretty painful proof, with lots of cases.
ext t
simp only [mem_shadow_iff_insert_mem, mem_initSeg]
constructor
-- First show that if t ∪ a ≤ s, then t ≤ s - min s
· rintro ⟨a, ha, hst, hts⟩
constructor
· rw [card_erase_of_mem (min'_mem _ _), hst, card_insert_of_notMem ha, add_tsub_cancel_right]
·
simpa [ha] using
erase_le_erase_min' hts hst.ge
(mem_insert_self _ _)
-- Now show that if t ≤ s - min s, there is j such that t ∪ j ≤ s
-- We choose j as the smallest thing not in t
simp_rw [le_iff_eq_or_lt, lt_iff_exists_filter_lt, mem_sdiff, filter_inj, and_assoc]
simp only [toColex_inj, and_imp]
rintro cards'
(rfl | ⟨k, hks, hkt, z⟩)
-- If t = s - min s, then use j = min s so t ∪ j = s
· refine ⟨min' s hs, notMem_erase _ _, ?_⟩
rw [insert_erase (min'_mem _ _)]
exact ⟨rfl, Or.inl rfl⟩
set j :=
min' tᶜ
⟨k, mem_compl.2 hkt⟩
-- Assume first t < s - min s, and take k as the colex witness for this
have hjk : j ≤ k := min'_le _ _ (mem_compl.2 ‹k ∉ t›)
have : j ∉ t := mem_compl.1 (min'_mem _ _)
have hcard : #s = #(insert j t) := by
rw [card_insert_of_notMem ‹j ∉ t›, ← ‹_ = #t›, card_erase_add_one (min'_mem _ _)]
refine
⟨j, ‹_›, hcard, ?_⟩
-- Cases on j < k or j = k
obtain hjk | r₁ := hjk.lt_or_eq
· refine Or.inr ⟨k, mem_of_mem_erase ‹_›, fun hk ↦ hkt <| mem_of_mem_insert_of_ne hk hjk.ne', fun x hx ↦ ?_⟩
simpa only [mem_insert, z hx, (hjk.trans hx).ne', mem_erase, Ne, false_or, and_iff_right_iff_imp] using fun _ ↦
((min'_le _ _ <| mem_of_mem_erase hks).trans_lt hx).ne'
refine Or.inl (eq_of_subset_of_card_le (fun a ha ↦ ?_) hcard.ge).symm
rcases lt_trichotomy k a with (lt | rfl | gt)
· apply mem_insert_of_mem
rw [z lt]
refine mem_erase_of_ne_of_mem (lt_of_le_of_lt ?_ lt).ne' ha
apply min'_le _ _ (mem_of_mem_erase ‹_›)
· rw [r₁]; apply mem_insert_self
· apply mem_insert_of_mem
rw [← r₁] at gt
by_contra
apply (min'_le tᶜ _ _).not_gt gt
rwa [mem_compl]
