# Lubell-Yamamoto-Meshalkin inequality and Sperner's theorem #

This file proves the local LYM and LYM inequalities as well as Sperner's theorem.

## Main declarations #

• Finset.card_div_choose_le_card_shadow_div_choose: Local Lubell-Yamamoto-Meshalkin inequality. The shadow of a set 𝒜 in a layer takes a greater proportion of its layer than 𝒜 does.
• Finset.sum_card_slice_div_choose_le_one: Lubell-Yamamoto-Meshalkin inequality. The sum of densities of 𝒜 in each layer is at most 1 for any antichain 𝒜.
• IsAntichain.sperner: Sperner's theorem. The size of any antichain in Finset α is at most the size of the maximal layer of Finset α. It is a corollary of sum_card_slice_div_choose_le_one.

## TODO #

Prove upward local LYM.

Provide equality cases. Local LYM gives that the equality case of LYM and Sperner is precisely when 𝒜 is a middle layer.

falling could be useful more generally in grade orders.

## References #

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

## Tags #

### Local LYM inequality #

theorem Finset.card_mul_le_card_shadow_mul {α : Type u_2} [] [] {𝒜 : Finset ()} {r : } (h𝒜 : Set.Sized r 𝒜) :
𝒜.card * r 𝒜.shadow.card * ( + 1)

The downward local LYM inequality, with cancelled denominators. 𝒜 takes up less of α^(r) (the finsets of card r) than ∂𝒜 takes up of α^(r - 1).

theorem Finset.card_div_choose_le_card_shadow_div_choose {𝕜 : Type u_1} {α : Type u_2} [] [] {𝒜 : Finset ()} {r : } (hr : r 0) (h𝒜 : Set.Sized r 𝒜) :
𝒜.card / (().choose r) 𝒜.shadow.card / (().choose (r - 1))

The downward local LYM inequality. 𝒜 takes up less of α^(r) (the finsets of card r) than ∂𝒜 takes up of α^(r - 1).

### LYM inequality #

def Finset.falling {α : Type u_2} [] (k : ) (𝒜 : Finset ()) :

falling k 𝒜 is all the finsets of cardinality k which are a subset of something in 𝒜.

Equations
• = 𝒜.sup
Instances For
theorem Finset.mem_falling {α : Type u_2} [] {k : } {𝒜 : Finset ()} {s : } :
s (t𝒜, s t) s.card = k
theorem Finset.sized_falling {α : Type u_2} [] (k : ) (𝒜 : Finset ()) :
Set.Sized k ()
theorem Finset.slice_subset_falling {α : Type u_2} [] (k : ) (𝒜 : Finset ()) :
𝒜.slice k
theorem Finset.falling_zero_subset {α : Type u_2} [] (𝒜 : Finset ()) :
{}
theorem Finset.slice_union_shadow_falling_succ {α : Type u_2} [] (k : ) (𝒜 : Finset ()) :
𝒜.slice k (Finset.falling (k + 1) 𝒜).shadow =
theorem Finset.IsAntichain.disjoint_slice_shadow_falling {α : Type u_2} [] {𝒜 : Finset ()} {m : } {n : } (h𝒜 : IsAntichain (fun (x x_1 : ) => x x_1) 𝒜) :

The shadow of falling m 𝒜 is disjoint from the n-sized elements of 𝒜, thanks to the antichain property.

theorem Finset.le_card_falling_div_choose {𝕜 : Type u_1} {α : Type u_2} [] {k : } {𝒜 : Finset ()} [] (hk : ) (h𝒜 : IsAntichain (fun (x x_1 : ) => x x_1) 𝒜) :
((Finset.range (k + 1)).sum fun (r : ) => (𝒜.slice ()).card / (().choose ())) (Finset.falling () 𝒜).card / (().choose ())

A bound on any top part of the sum in LYM in terms of the size of falling k 𝒜.

theorem Finset.sum_card_slice_div_choose_le_one {𝕜 : Type u_1} {α : Type u_2} {𝒜 : Finset ()} [] (h𝒜 : IsAntichain (fun (x x_1 : ) => x x_1) 𝒜) :
((Finset.range ()).sum fun (r : ) => (𝒜.slice r).card / (().choose r)) 1

The Lubell-Yamamoto-Meshalkin inequality. If 𝒜 is an antichain, then the sum of the proportion of elements it takes from each layer is less than 1.

### Sperner's theorem #

theorem Finset.IsAntichain.sperner {α : Type u_2} [] {𝒜 : Finset ()} (h𝒜 : IsAntichain (fun (x x_1 : ) => x x_1) 𝒜) :
𝒜.card ().choose ()

Sperner's theorem. The size of an antichain in Finset α is bounded by the size of the maximal layer in Finset α. This precisely means that Finset α is a Sperner order.