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.local_lubell_yamamoto_meshalkin_inequality_div: Local Lubell-Yamamoto-Meshalkin inequality. The shadow of a set 𝒜 in a layer takes a greater proportion of its layer than 𝒜 does.
• Finset.lubell_yamamoto_meshalkin_inequality_sum_card_div_choose: 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 lubell_yamamoto_meshalkin_inequality_sum_card_div_choose.

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

shadow, lym, slice, sperner, antichain

Local LYM inequality

theorem Finset.local_lubell_yamamoto_meshalkin_inequality_mul {α : Type u_2} [DecidableEq α] [Fintype α] {𝒜 : Finset (Finset α)} {r : ℕ} (h𝒜 : Set.Sized r ↑𝒜) : 𝒜.card * r ≤ 𝒜.shadow.card * (Fintype.card α - r + 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_mul_le_card_shadow_mul {α : Type u_2} [DecidableEq α] [Fintype α] {𝒜 : Finset (Finset α)} {r : ℕ} (h𝒜 : Set.Sized r ↑𝒜) : 𝒜.card * r ≤ 𝒜.shadow.card * (Fintype.card α - r + 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.local_lubell_yamamoto_meshalkin_inequality_div {𝕜 : Type u_1} {α : Type u_2} [Semifield 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [DecidableEq α] [Fintype α] {𝒜 : Finset (Finset α)} {r : ℕ} (hr : r ≠ 0) (h𝒜 : Set.Sized r ↑𝒜) : ↑𝒜.card / ↑((Fintype.card α).choose r) ≤ ↑𝒜.shadow.card / ↑((Fintype.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).

theorem Finset.card_div_choose_le_card_shadow_div_choose {𝕜 : Type u_1} {α : Type u_2} [Semifield 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [DecidableEq α] [Fintype α] {𝒜 : Finset (Finset α)} {r : ℕ} (hr : r ≠ 0) (h𝒜 : Set.Sized r ↑𝒜) : ↑𝒜.card / ↑((Fintype.card α).choose r) ≤ ↑𝒜.shadow.card / ↑((Fintype.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} [DecidableEq α] (k : ℕ) (𝒜 : Finset (Finset α)) : Finset (Finset α)

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

Equations

• Finset.falling k 𝒜 = 𝒜.sup (Finset.powersetCard k)

theorem Finset.mem_falling {α : Type u_2} [DecidableEq α] {k : ℕ} {𝒜 : Finset (Finset α)} {s : Finset α} : s ∈ falling k 𝒜 ↔ (∃ t ∈ 𝒜, s ⊆ t) ∧ s.card = k

theorem Finset.sized_falling {α : Type u_2} [DecidableEq α] (k : ℕ) (𝒜 : Finset (Finset α)) : Set.Sized k ↑(falling k 𝒜)

theorem Finset.slice_subset_falling {α : Type u_2} [DecidableEq α] (k : ℕ) (𝒜 : Finset (Finset α)) : 𝒜.slice k ⊆ falling k 𝒜

theorem Finset.falling_zero_subset {α : Type u_2} [DecidableEq α] (𝒜 : Finset (Finset α)) : falling 0 𝒜 ⊆ {∅}

theorem Finset.slice_union_shadow_falling_succ {α : Type u_2} [DecidableEq α] (k : ℕ) (𝒜 : Finset (Finset α)) : 𝒜.slice k ∪ (falling (k + 1) 𝒜).shadow = falling k 𝒜

theorem Finset.IsAntichain.disjoint_slice_shadow_falling {α : Type u_2} [DecidableEq α] {𝒜 : Finset (Finset α)} {m n : ℕ} (h𝒜 : IsAntichain (fun (x1 x2 : Finset α) => x1 ⊆ x2) ↑𝒜) : Disjoint (𝒜.slice m) (falling n 𝒜).shadow

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} [Semifield 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [DecidableEq α] {k : ℕ} {𝒜 : Finset (Finset α)} [Fintype α] (hk : k ≤ Fintype.card α) (h𝒜 : IsAntichain (fun (x1 x2 : Finset α) => x1 ⊆ x2) ↑𝒜) : ∑ r ∈ range (k + 1), ↑(𝒜.slice (Fintype.card α - r)).card / ↑((Fintype.card α).choose (Fintype.card α - r)) ≤ ↑(falling (Fintype.card α - k) 𝒜).card / ↑((Fintype.card α).choose (Fintype.card α - k))

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

theorem Finset.lubell_yamamoto_meshalkin_inequality_sum_card_div_choose {𝕜 : Type u_1} {α : Type u_2} [Semifield 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [Fintype α] {𝒜 : Finset (Finset α)} (h𝒜 : IsAntichain (fun (x1 x2 : Finset α) => x1 ⊆ x2) ↑𝒜) : ∑ r ∈ range (Fintype.card α + 1), ↑(𝒜.slice r).card / ↑((Fintype.card α).choose r) ≤ 1

The Lubell-Yamamoto-Meshalkin inequality, also known as the LYM inequality.

If 𝒜 is an antichain, then the sum of the proportion of elements it takes from each layer is less than 1.

theorem Finset.sum_card_slice_div_choose_le_one {𝕜 : Type u_1} {α : Type u_2} [Semifield 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [Fintype α] {𝒜 : Finset (Finset α)} (h𝒜 : IsAntichain (fun (x1 x2 : Finset α) => x1 ⊆ x2) ↑𝒜) : ∑ r ∈ range (Fintype.card α + 1), ↑(𝒜.slice r).card / ↑((Fintype.card α).choose r) ≤ 1

The Lubell-Yamamoto-Meshalkin inequality, also known as the LYM inequality.

If 𝒜 is an antichain, then the sum of the proportion of elements it takes from each layer is less than 1.

theorem Finset.lubell_yamamoto_meshalkin_inequality_sum_inv_choose {𝕜 : Type u_1} {α : Type u_2} [Semifield 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [Fintype α] {𝒜 : Finset (Finset α)} (h𝒜 : IsAntichain (fun (x1 x2 : Finset α) => x1 ⊆ x2) ↑𝒜) : ∑ s ∈ 𝒜, (↑((Fintype.card α).choose s.card))⁻¹ ≤ 1

The Lubell-Yamamoto-Meshalkin inequality, also known as the LYM inequality.

If 𝒜 is an antichain, then the sum of (#α.choose #s)⁻¹ over s ∈ 𝒜 is less than 1.

Sperner's theorem

theorem IsAntichain.sperner {α : Type u_2} [Fintype α] {𝒜 : Finset (Finset α)} (h𝒜 : IsAntichain (fun (x1 x2 : Finset α) => x1 ⊆ x2) ↑𝒜) : 𝒜.card ≤ (Fintype.card α).choose (Fintype.card α / 2)

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.