English
An iterated version of Kruskal–Katona: applying shadow multiple times preserves the inequality direction under suitable hypotheses.
Русский
Итерированная версия теоремы Крускала-Катоны: повторное применение тени сохраняет неравенство при подходящих предпосылках.
LaTeX
$$$\#(\partial^{[k]} 𝒜) \le \#(\partial^{[k]} 𝒞)$ under the stated hypotheses$$
Lean4
/-- An iterated form of the Kruskal-Katona theorem. In particular, the minimum possible iterated
shadow size is attained by initial segments. -/
theorem iterated_kk (h₁ : (𝒜 : Set (Finset (Fin n))).Sized r) (h₂ : #𝒞 ≤ #𝒜) (h₃ : IsInitSeg 𝒞 r) :
#(∂ ^[k] 𝒞) ≤ #(∂ ^[k] 𝒜) := by
induction k generalizing r 𝒜 𝒞 with
| zero => simpa
| succ _ ih =>
refine ih h₁.shadow (kruskal_katona h₁ h₂ h₃) ?_
convert h₃.shadow
