Kruskal-Katona theorem

This file proves the Kruskal-Katona theorem. This is a sharp statement about how many sets of size k - 1 are covered by a family of sets of size k, given only its size.

Main declarations

The key results proved here are:

• Finset.kruskal_katona: The basic Kruskal-Katona theorem. Given a set family 𝒜 consisting of r-sets, and 𝒞 an initial segment of the colex order of the same size, the shadow of 𝒞 is smaller than the shadow of 𝒜. In particular, this shows that the minimum shadow size is achieved by initial segments of colex.
• Finset.iterated_kruskal_katona: An iterated form of the Kruskal-Katona theorem, stating that the minimum iterated shadow size is given by initial segments of colex.

TODO

• Define the k-cascade representation of a natural and prove the corresponding version of Kruskal-Katona.
• Abstract away from Fin n so that it also applies to ℕ. Probably LocallyFiniteOrderBot will help here.
• Characterise the equality case.

References

• http://b-mehta.github.io/maths-notes/iii/mich/combinatorics.pdf
• http://discretemath.imp.fu-berlin.de/DMII-2015-16/kruskal.pdf

Tags

kruskal-katona, kruskal, katona, shadow, initial segments, intersecting

theorem Finset.Colex.shadow_initSeg {α : Type u_1} [LinearOrder α] {s : Finset α} [Fintype α] (hs : s.Nonempty) : (Finset.Colex.initSeg s).shadow = Finset.Colex.initSeg (s.erase (s.min' hs))

This is important for iterating Kruskal-Katona: the shadow of an initial segment is also an initial segment.

theorem Finset.Colex.IsInitSeg.shadow {α : Type u_1} [LinearOrder α] {𝒜 : Finset (Finset α)} {r : ℕ} [Finite α] (h₁ : Finset.Colex.IsInitSeg 𝒜 r) : Finset.Colex.IsInitSeg 𝒜.shadow (r - 1)

The shadow of an initial segment is also an initial segment.

theorem Finset.UV.toColex_compress_lt_toColex {α : Type u_1} [LinearOrder α] {s : Finset α} {U : Finset α} {V : Finset α} {hU : U.Nonempty} {hV : V.Nonempty} (h : U.max' hU < V.max' hV) (hA : UV.compress U V s ≠ s) : { ofColex := UV.compress U V s } < { ofColex := s }

Applying the compression makes the set smaller in colex. This is intuitive since a portion of the set is being "shifted down" as max U < max V.

theorem Finset.UV.isInitSeg_of_compressed {α : Type u_1} [LinearOrder α] {ℬ : Finset (Finset α)} {r : ℕ} (h₁ : Set.Sized r ↑ℬ) (h₂ : ∀ (U V : Finset α), Finset.UV.UsefulCompression U V → UV.IsCompressed U V ℬ) : Finset.Colex.IsInitSeg ℬ r

If we're compressed by all useful compressions, then we're an initial segment. This is the other key Kruskal-Katona part.

theorem Finset.kruskal_katona {n : ℕ} {r : ℕ} {𝒜 : Finset (Finset (Fin n))} {𝒞 : Finset (Finset (Fin n))} (h𝒜r : Set.Sized r ↑𝒜) (h𝒞𝒜 : 𝒞.card ≤ 𝒜.card) (h𝒞 : Finset.Colex.IsInitSeg 𝒞 r) : 𝒞.shadow.card ≤ 𝒜.shadow.card

The Kruskal-Katona theorem.

Given a set family 𝒜 consisting of r-sets, and 𝒞 an initial segment of the colex order of the same size, the shadow of 𝒞 is smaller than the shadow of 𝒜. In particular, this gives that the minimum shadow size is achieved by initial segments of colex.

theorem Finset.iterated_kk {n : ℕ} {r : ℕ} {k : ℕ} {𝒜 : Finset (Finset (Fin n))} {𝒞 : Finset (Finset (Fin n))} (h₁ : Set.Sized r ↑𝒜) (h₂ : 𝒞.card ≤ 𝒜.card) (h₃ : Finset.Colex.IsInitSeg 𝒞 r) : (Finset.shadow^[k] 𝒞).card ≤ (Finset.shadow^[k] 𝒜).card

An iterated form of the Kruskal-Katona theorem. In particular, the minimum possible iterated shadow size is attained by initial segments.