• What is this?
• How can I install this package?
• Why did you choose this bit of maths to formalise?
• What's the Kruskal-Katona theorem?
  • What form do you prove it in?
• Can I contribute?
• Where did you get the proofs from?
• What's in this package?
  • to_mathlib.lean
  • basic.lean
  • shadows.lean
  • colex.lean
  • compressions/*.lean
  • kruskal_katona.lean
• Doesn't some of this belong in mathlib?

A Lean package formalising some combinatorics of finite sets, in particular the Kruskal-Katona theorem and some related results.

First install Lean and mathlib using the instructions here, and then

git clone https://github.com/b-mehta/combinatorics.git
cd combinatorics
leanpkg configure
update-mathlib

Combinatorics tends to have problems which are easy to state but hard to prove. In particular, the difficulty is usually in the proofs rather than in complicated definitions, so I thought to get to grips with Lean it'd be a good idea to formalise some of these proofs. The main goal was to formalise the Kruskal-Katona theorem, but along the way I also formalised the local LYM inequality and LYM inequality, Sperner's theorem and a consequence of the Kruskal-Katona theorem called the Erdős-Ko-Rado theorem.

In brief, the Kruskal-Katona theorem tells us the minimum possible size of the shadow of certain set families. Picking apart what this means, a set family is just a collection (set) of subsets of a fixed finite 'universe' of elements - typically write [n] := {0,...,n-1}. Kruskal-Katona is concerned particular with set families in which every element has the same size, for instance

A = { {0,1,2}, {0,1,3}, {0,2,3}, {0,2,4} }.

Each set in here would be called a 3-set, since each set has three elements.

The shadow of such a set family is everything we can get by removing an element from each set, and it's written ∂. In our example,

∂A = { {0,1}, {0,2}, {0,3}, {0,4}, {1,2}, {1,3}, {2,3}, {2,4} }.

A question we could ask about shadows is

If A is a set of r-sets, and the number of sets in A is fixed, how small can we make the shadow of A?

Ultimately, this is asking "How tightly can we pack some r-sets?". In particular, we'll say that we've fixed r and fixed n, so we can only take elements from [n] = {0,...,n-1}.

If we fix the size of A to be C(k, r) (the binomial coefficient) for some k, it seems reasonable that the best A would be all r-sets taking elements from [k].

Kruskal-Katona says that this is the minimum, in particular if |A| = C(k, r), then |∂A| ≥ C(k, r-1). Actually, Kruskal-Katona gives a stronger result: for any value of |A| it gives the minimum value of |∂A| (although in this package, we don't prove it in this exact form).

To write the Kruskal-Katona theorem in more general form in which it's formalised here, let's first define an ordering on r-sets called the colexicographic ordering, or colex for short. The colex ordering effectively tries to avoid large numbers. For r = 2, it starts like this:

{0,1}, {0,2}, {1,2}, {0,3}, {1,3}, {2,3}, {0,4}, {1,4}, {2,4}, {3,4}, ...

Notice how it reached {2,3} before {1,4}, because it tried to avoid getting 4. Also, observe that the first three sets above gives all 2-sets from [3], the first six sets give all 2-sets from [4], and so on, which were our guess for the minimum shadow families.

The Kruskal-Katona theorem then says

If A is a family of r-sets, and C is the first |A| r-sets in colex, then |∂A| ≥ |∂C|.

Yes! Take a look at the issues tab of the repository, there's a couple of things that could be added. Pull requests are very welcome.

The proofs are adapted from my notes of Imre Leader's Cambridge Part III Combinatorics course in 2018.

A fair few lemmas came up along the way, and some of them seemed like they ought to have already been in mathlib, so I've collected them in to_mathlib.lean. In my opinion they belong in mathlib, but I haven't yet got round to making the PRs myself. Feel free to do this if you'd like to help.

We first set up some basic definitions and lemmas for general combinatorics in basic.lean such as the definition of an antichain. An antichain is a set family in which no set is contained in another, for instance

{ {0}, {4,6,7}, {2,4,5,6} }

In shadows.lean, we define the basic notion of a shadow. An important theorem relating to shadows is the local LYM theorem, which is then used to prove the LYM (Lubell-Yamamoto-Meshalkin) inequality:

If A is an antichain, then

Finally, this inequality is used to prove Sperner's theorem:

If A is an antichain, then

Defines the colex ordering and proves a couple of properties and lemmas relating to it.

To prove the Kruskal-Katona theorem, it is useful to use compressions (sometimes called shifting operators). The idea of a compression to "squash" a set family into something which might have a smaller shadow, but the same size. An i,j-compression does reduce the shadow of a set family, so an idea might be to keep applying them until we can't any more, and hope this gives the minimum shadow. Unfortunately this doesn't exactly work, but i,j-compressions are defined anyway in compressions/ij.lean, along with a proof that they do decrease the shadow.

One (not the only) approach to fixing this argument is to use more general U,V-compressions, defined in compressions/UV.lean. They can be a bit more drastic, and it turns out that if a set family is fully U,V-compressed, it is an initial segment of colex. The drawback to this approach is that U,V-compressions only decrease the shadow under certain conditions. So, the general idea of the proof is to apply these U,V-compressions in just the right order, until we can't apply any. Then the resultant family has a smaller shadow, and it's an initial segment of colex, which is what we wanted.

In kruskal_katona.lean we prove the Kruskal-Katona theorem! Here's the statement (X is notation for fin n, i.e. {0,...,n-1}):

theorem kruskal_katona {r : ℕ} {𝒜 𝒞 : finset (finset X)}
  (h₁ : all_sized 𝒜 r) (h₂ : 𝒜.card = 𝒞.card) (h₃ : is_init_seg_of_colex 𝒞 r) :
(∂𝒞).card ≤ (∂𝒜).card :=

We also prove some generalisations: strengthened is the same statement, but h₂ is relaxed to 𝒞.card ≤ 𝒜.card.

One can also show that the shadow of an initial segment of colex is also an initial segment of colex, so the theorem can be iterated to show that the repeated shadow is also minimsed by colex:

theorem iterated {r k : ℕ} {𝒜 𝒞 : finset (finset X)}
  (h₁ : all_sized 𝒜 r) (h₂ : 𝒞.card ≤ 𝒜.card) (h₃ : is_init_seg_of_colex 𝒞 r) : 
(shadow^[k] 𝒞).card ≤ (shadow^[k] 𝒜).card :=

Finally we can get the Kruskal-Katona theorem in the form it was mentioned all the way at the top, provided all the sizes (hidden in the [...]) work:

theorem lovasz_form {r k i : ℕ} {𝒜 : finset (finset X)} [...] 
  (h₁ : all_sized 𝒜 r) (h₂ : choose k r ≤ 𝒜.card) : 
choose k (r-i) ≤ (shadow^[i] 𝒜).card :=

Using this, we can prove the Erdős-Ko-Rado theorem. It says that if A is a collection of r-sets for r ≤ n/2, and every two sets in A are not disjoint (A is intersecting), then A can't be too large:

theorem EKR {𝒜 : finset (finset X)} {r : ℕ} 
  (h₁ : intersecting 𝒜) (h₂ : all_sized 𝒜 r) (h₃ : r ≤ n/2) : 
𝒜.card ≤ choose (n-1) (r-1) :=

Possibly! Some parts might not follow mathlib conventions, although in most places I tried to get reasonably close.