Documentation

Mathlib.Combinatorics.SetFamily.LYM

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 #

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 #

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.card_div_choose_le_card_shadow_div_choose {𝕜 : Type u_1} {α : Type u_2} [LinearOrderedField 𝕜] [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 α)) :

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

Equations
Instances For
    theorem Finset.mem_falling {α : Type u_2} [DecidableEq α] {k : } {𝒜 : Finset (Finset α)} {s : Finset α} :
    s Finset.falling k 𝒜 (∃ t𝒜, s t) s.card = k
    theorem Finset.sized_falling {α : Type u_2} [DecidableEq α] (k : ) (𝒜 : Finset (Finset α)) :
    theorem Finset.slice_subset_falling {α : Type u_2} [DecidableEq α] (k : ) (𝒜 : Finset (Finset α)) :
    𝒜.slice k Finset.falling k 𝒜
    theorem Finset.falling_zero_subset {α : Type u_2} [DecidableEq α] (𝒜 : Finset (Finset α)) :
    theorem Finset.slice_union_shadow_falling_succ {α : Type u_2} [DecidableEq α] (k : ) (𝒜 : Finset (Finset α)) :
    𝒜.slice k (Finset.falling (k + 1) 𝒜).shadow = Finset.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) (Finset.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} [LinearOrderedField 𝕜] [DecidableEq α] {k : } {𝒜 : Finset (Finset α)} [Fintype α] (hk : k Fintype.card α) (h𝒜 : IsAntichain (fun (x1 x2 : Finset α) => x1 x2) 𝒜) :
    rFinset.range (k + 1), (𝒜.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 𝒜.

    theorem Finset.sum_card_slice_div_choose_le_one {𝕜 : Type u_1} {α : Type u_2} [LinearOrderedField 𝕜] {𝒜 : Finset (Finset α)} [Fintype α] (h𝒜 : IsAntichain (fun (x1 x2 : Finset α) => x1 x2) 𝒜) :
    rFinset.range (Fintype.card α + 1), (𝒜.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 #

    theorem Finset.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.