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

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 𝒜.
is_antichain.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 #

Tags #

shadow, lym, slice, sperner, antichain

Local LYM inequality #

source

theorem finset.card_mul_le_card_shadow_mul {α : Type u_2} [decidable_eq α] [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).

source

theorem finset.card_div_choose_le_card_shadow_div_choose {𝕜 : Type u_1} {α : Type u_2} [linear_ordered_field 𝕜] [decidable_eq α] [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 #

source

def finset.falling {α : Type u_2} [decidable_eq α] (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.powerset_len k)

source

theorem finset.mem_falling {α : Type u_2} [decidable_eq α] {k : ℕ} {𝒜 : finset (finset α)} {s : finset α} :

s ∈ finset.falling k 𝒜 ↔ (∃ (t : finset α) (H : t ∈ 𝒜), s ⊆ t) ∧ s.card = k

source

theorem finset.sized_falling {α : Type u_2} [decidable_eq α] (k : ℕ) (𝒜 : finset (finset α)) :

set.sized k ↑(finset.falling k 𝒜)

source

theorem finset.slice_subset_falling {α : Type u_2} [decidable_eq α] (k : ℕ) (𝒜 : finset (finset α)) :

𝒜.slice k ⊆ finset.falling k 𝒜

source

theorem finset.falling_zero_subset {α : Type u_2} [decidable_eq α] (𝒜 : finset (finset α)) :

finset.falling 0 𝒜 ⊆ {∅}

source

theorem finset.slice_union_shadow_falling_succ {α : Type u_2} [decidable_eq α] (k : ℕ) (𝒜 : finset (finset α)) :

𝒜.slice k ∪ (finset.falling (k + 1) 𝒜).shadow = finset.falling k 𝒜

source

theorem is_antichain.disjoint_slice_shadow_falling {α : Type u_2} [decidable_eq α] {𝒜 : finset (finset α)} {m n : ℕ} (h𝒜 : is_antichain has_subset.subset ↑𝒜) :

disjoint (𝒜.slice m) (finset.falling n 𝒜).shadow

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

source

theorem finset.le_card_falling_div_choose {𝕜 : Type u_1} {α : Type u_2} [linear_ordered_field 𝕜] [decidable_eq α] {k : ℕ} {𝒜 : finset (finset α)} [fintype α] (hk : k ≤ fintype.card α) (h𝒜 : is_antichain has_subset.subset ↑𝒜) :

(finset.range (k + 1)).sum (λ (r : ℕ), ↑((𝒜.slice (fintype.card α - r)).card) / ↑((fintype.card α).choose (fintype.card α - r))) ≤ ↑((finset.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 𝒜.

source

theorem finset.sum_card_slice_div_choose_le_one {𝕜 : Type u_1} {α : Type u_2} [linear_ordered_field 𝕜] {𝒜 : finset (finset α)} [fintype α] (h𝒜 : is_antichain has_subset.subset ↑𝒜) :

(finset.range (fintype.card α + 1)).sum (λ (r : ℕ), ↑((𝒜.slice r).card) / ↑((fintype.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 #

source

theorem is_antichain.sperner {α : Type u_2} [fintype α] {𝒜 : finset (finset α)} (h𝒜 : is_antichain has_subset.subset ↑𝒜) :

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