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) : (initSeg s).shadow = 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₁ : IsInitSeg 𝒜 r) : 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 U 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 ℬ) : 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))} (h𝒜r : Set.Sized r ↑𝒜) (h𝒞𝒜 : 𝒞.card ≤ 𝒜.card) (h𝒞 : 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))} (h₁ : Set.Sized r ↑𝒜) (h₂ : 𝒞.card ≤ 𝒜.card) (h₃ : Colex.IsInitSeg 𝒞 r) : (shadow^[k] 𝒞).card ≤ (shadow^[k] 𝒜).card

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

theorem Finset.kruskal_katona_lovasz_form {n r k i : ℕ} {𝒜 : Finset (Finset (Fin n))} (hir : i ≤ r) (hrk : r ≤ k) (hkn : k ≤ n) (h₁ : Set.Sized r ↑𝒜) (h₂ : k.choose r ≤ 𝒜.card) : k.choose (r - i) ≤ (shadow^[i] 𝒜).card

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 Finset.erdos_ko_rado {n : ℕ} {𝒜 : Finset (Finset (Fin n))} {r : ℕ} (h𝒜 : (↑𝒜).Intersecting) (h₂ : Set.Sized r ↑𝒜) (h₃ : r ≤ n / 2) : 𝒜.card ≤ (n - 1).choose (r - 1)

The Erdős–Ko–Rado theorem.

The maximum size of an intersecting family in α where all sets have size r is bounded by (card α - 1).choose (r - 1). This bound is sharp.