Documentation

Mathlib.Combinatorics.SetFamily.KruskalKatona

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:

TODO #

References #

Tags #

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

source
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.

source
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.

source
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.

source
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.

source
theorem Finset.kruskal_katona {n r : β„•} {π’œ π’ž : 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.

source
theorem Finset.iterated_kk {n r k : β„•} {π’œ π’ž : 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.

source
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) ≀ (Finset.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.

source
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.