Documentation

Mathlib.Combinatorics.SetFamily.AhlswedeZhang

The Ahlswede-Zhang identity #

This file proves the Ahlswede-Zhang identity, which is a nontrivial relation between the size of the "truncated unions" of a set family. It sharpens the Lubell-Yamamoto-Meshalkin inequality Finset.lubell_yamamoto_meshalkin_inequality_sum_card_div_choose, by making explicit the correction term.

For a set family 𝒜 over a ground set of size n, the Ahlswede-Zhang identity states that the sum of |⋂ B ∈ 𝒜, B ⊆ A, B|/(|A| * n.choose |A|) over all set A is exactly 1. This implies the LYM inequality since for an antichain 𝒜 and every A ∈ 𝒜 we have |⋂ B ∈ 𝒜, B ⊆ A, B|/(|A| * n.choose |A|) = 1 / n.choose |A|.

Main declarations #

Finset.truncatedSup: s.truncatedSup a is the supremum of all b ≥ a in 𝒜 if there are some, or ⊤ if there are none.
Finset.truncatedInf: s.truncatedInf a is the infimum of all b ≤ a in 𝒜 if there are some, or ⊥ if there are none.
AhlswedeZhang.infSum: LHS of the Ahlswede-Zhang identity.
AhlswedeZhang.le_infSum: The sum of 1 / n.choose |A| over an antichain is less than the RHS of the Ahlswede-Zhang identity.
AhlswedeZhang.infSum_eq_one: Ahlswede-Zhang identity.

References #

Truncated supremum, truncated infimum #

def Finset.truncatedSup {α : Type u_1} [SemilatticeSup α] [DecidableLE α] [OrderTop α] (s : Finset α) (a : α) :

α

The supremum of the elements of s less than a if there are some, otherwise ⊤.

Equations

s.truncatedSup a = if h : a ∈ lowerClosure ↑s then {b ∈ s | a ≤ b}.sup' ⋯ id else ⊤

Instances For

theorem Finset.truncatedSup_of_mem {α : Type u_1} [SemilatticeSup α] {s : Finset α} {a : α} [DecidableLE α] [OrderTop α] (h : a ∈ lowerClosure ↑s) :

s.truncatedSup a = {b ∈ s | a ≤ b}.sup' ⋯ id

theorem Finset.truncatedSup_of_notMem {α : Type u_1} [SemilatticeSup α] {s : Finset α} {a : α} [DecidableLE α] [OrderTop α] (h : a ∉ lowerClosure ↑s) :

s.truncatedSup a = ⊤

@[deprecated Finset.truncatedSup_of_notMem (since := "2025-05-23")]

theorem Finset.truncatedSup_of_not_mem {α : Type u_1} [SemilatticeSup α] {s : Finset α} {a : α} [DecidableLE α] [OrderTop α] (h : a ∉ lowerClosure ↑s) :

s.truncatedSup a = ⊤

Alias of Finset.truncatedSup_of_notMem.

@[simp]

theorem Finset.truncatedSup_empty {α : Type u_1} [SemilatticeSup α] [DecidableLE α] [OrderTop α] (a : α) :

∅.truncatedSup a = ⊤

@[simp]

theorem Finset.truncatedSup_singleton {α : Type u_1} [SemilatticeSup α] [DecidableLE α] [OrderTop α] (b a : α) :

{b}.truncatedSup a = if a ≤ b then b else ⊤

theorem Finset.le_truncatedSup {α : Type u_1} [SemilatticeSup α] {s : Finset α} {a : α} [DecidableLE α] [OrderTop α] :

a ≤ s.truncatedSup a

theorem Finset.map_truncatedSup {α : Type u_1} {β : Type u_2} [SemilatticeSup α] [SemilatticeSup β] [BoundedOrder β] [DecidableLE α] [OrderTop α] [DecidableLE β] (e : α ≃o β) (s : Finset α) (a : α) :

e (s.truncatedSup a) = (map e.toEmbedding s).truncatedSup (e a)

theorem Finset.truncatedSup_of_isAntichain {α : Type u_1} [SemilatticeSup α] {s : Finset α} {a : α} [DecidableLE α] [OrderTop α] (hs : IsAntichain (fun (x1 x2 : α) => x1 ≤ x2) ↑s) (ha : a ∈ s) :

s.truncatedSup a = a

theorem Finset.truncatedSup_union {α : Type u_1} [SemilatticeSup α] {s t : Finset α} {a : α} [DecidableLE α] [OrderTop α] [DecidableEq α] (hs : a ∈ lowerClosure ↑s) (ht : a ∈ lowerClosure ↑t) :

(s ∪ t).truncatedSup a = s.truncatedSup a ⊔ t.truncatedSup a

theorem Finset.truncatedSup_union_left {α : Type u_1} [SemilatticeSup α] {s t : Finset α} {a : α} [DecidableLE α] [OrderTop α] [DecidableEq α] (hs : a ∈ lowerClosure ↑s) (ht : a ∉ lowerClosure ↑t) :

(s ∪ t).truncatedSup a = s.truncatedSup a

theorem Finset.truncatedSup_union_right {α : Type u_1} [SemilatticeSup α] {s t : Finset α} {a : α} [DecidableLE α] [OrderTop α] [DecidableEq α] (hs : a ∉ lowerClosure ↑s) (ht : a ∈ lowerClosure ↑t) :

(s ∪ t).truncatedSup a = t.truncatedSup a

theorem Finset.truncatedSup_union_of_notMem {α : Type u_1} [SemilatticeSup α] {s t : Finset α} {a : α} [DecidableLE α] [OrderTop α] [DecidableEq α] (hs : a ∉ lowerClosure ↑s) (ht : a ∉ lowerClosure ↑t) :

(s ∪ t).truncatedSup a = ⊤

@[deprecated Finset.truncatedSup_union_of_notMem (since := "2025-05-23")]

theorem Finset.truncatedSup_union_of_not_mem {α : Type u_1} [SemilatticeSup α] {s t : Finset α} {a : α} [DecidableLE α] [OrderTop α] [DecidableEq α] (hs : a ∉ lowerClosure ↑s) (ht : a ∉ lowerClosure ↑t) :

(s ∪ t).truncatedSup a = ⊤

Alias of Finset.truncatedSup_union_of_notMem.

def Finset.truncatedInf {α : Type u_1} [SemilatticeInf α] [DecidableLE α] [BoundedOrder α] (s : Finset α) (a : α) :

α

The infimum of the elements of s less than a if there are some, otherwise ⊥.

Equations

s.truncatedInf a = if h : a ∈ upperClosure ↑s then {b ∈ s | b ≤ a}.inf' ⋯ id else ⊥

Instances For

theorem Finset.truncatedInf_of_mem {α : Type u_1} [SemilatticeInf α] {s : Finset α} {a : α} [DecidableLE α] [BoundedOrder α] (h : a ∈ upperClosure ↑s) :

s.truncatedInf a = {b ∈ s | b ≤ a}.inf' ⋯ id

theorem Finset.truncatedInf_of_notMem {α : Type u_1} [SemilatticeInf α] {s : Finset α} {a : α} [DecidableLE α] [BoundedOrder α] (h : a ∉ upperClosure ↑s) :

s.truncatedInf a = ⊥

@[deprecated Finset.truncatedInf_of_notMem (since := "2025-05-23")]

theorem Finset.truncatedInf_of_not_mem {α : Type u_1} [SemilatticeInf α] {s : Finset α} {a : α} [DecidableLE α] [BoundedOrder α] (h : a ∉ upperClosure ↑s) :

s.truncatedInf a = ⊥

Alias of Finset.truncatedInf_of_notMem.

theorem Finset.truncatedInf_le {α : Type u_1} [SemilatticeInf α] {s : Finset α} {a : α} [DecidableLE α] [BoundedOrder α] :

s.truncatedInf a ≤ a

@[simp]

theorem Finset.truncatedInf_empty {α : Type u_1} [SemilatticeInf α] [DecidableLE α] [BoundedOrder α] (a : α) :

∅.truncatedInf a = ⊥

@[simp]

theorem Finset.truncatedInf_singleton {α : Type u_1} [SemilatticeInf α] [DecidableLE α] [BoundedOrder α] (b a : α) :

{b}.truncatedInf a = if b ≤ a then b else ⊥

theorem Finset.map_truncatedInf {α : Type u_1} {β : Type u_2} [SemilatticeInf α] [SemilatticeInf β] [BoundedOrder β] [DecidableLE β] [DecidableLE α] [BoundedOrder α] (e : α ≃o β) (s : Finset α) (a : α) :

e (s.truncatedInf a) = (map e.toEmbedding s).truncatedInf (e a)

theorem Finset.truncatedInf_of_isAntichain {α : Type u_1} [SemilatticeInf α] {s : Finset α} {a : α} [DecidableLE α] [BoundedOrder α] (hs : IsAntichain (fun (x1 x2 : α) => x1 ≤ x2) ↑s) (ha : a ∈ s) :

s.truncatedInf a = a

theorem Finset.truncatedInf_union {α : Type u_1} [SemilatticeInf α] {s t : Finset α} {a : α} [DecidableLE α] [BoundedOrder α] [DecidableEq α] (hs : a ∈ upperClosure ↑s) (ht : a ∈ upperClosure ↑t) :

(s ∪ t).truncatedInf a = s.truncatedInf a ⊓ t.truncatedInf a

theorem Finset.truncatedInf_union_left {α : Type u_1} [SemilatticeInf α] {s t : Finset α} {a : α} [DecidableLE α] [BoundedOrder α] [DecidableEq α] (hs : a ∈ upperClosure ↑s) (ht : a ∉ upperClosure ↑t) :

(s ∪ t).truncatedInf a = s.truncatedInf a

theorem Finset.truncatedInf_union_right {α : Type u_1} [SemilatticeInf α] {s t : Finset α} {a : α} [DecidableLE α] [BoundedOrder α] [DecidableEq α] (hs : a ∉ upperClosure ↑s) (ht : a ∈ upperClosure ↑t) :

(s ∪ t).truncatedInf a = t.truncatedInf a

theorem Finset.truncatedInf_union_of_notMem {α : Type u_1} [SemilatticeInf α] {s t : Finset α} {a : α} [DecidableLE α] [BoundedOrder α] [DecidableEq α] (hs : a ∉ upperClosure ↑s) (ht : a ∉ upperClosure ↑t) :

(s ∪ t).truncatedInf a = ⊥

@[deprecated Finset.truncatedInf_union_of_notMem (since := "2025-05-23")]

theorem Finset.truncatedInf_union_of_not_mem {α : Type u_1} [SemilatticeInf α] {s t : Finset α} {a : α} [DecidableLE α] [BoundedOrder α] [DecidableEq α] (hs : a ∉ upperClosure ↑s) (ht : a ∉ upperClosure ↑t) :

(s ∪ t).truncatedInf a = ⊥

Alias of Finset.truncatedInf_union_of_notMem.

theorem Finset.truncatedSup_infs {α : Type u_1} [DistribLattice α] [DecidableEq α] {s t : Finset α} {a : α} [DecidableLE α] [BoundedOrder α] (hs : a ∈ lowerClosure ↑s) (ht : a ∈ lowerClosure ↑t) :

(s ⊼ t).truncatedSup a = s.truncatedSup a ⊓ t.truncatedSup a

theorem Finset.truncatedInf_sups {α : Type u_1} [DistribLattice α] [DecidableEq α] {s t : Finset α} {a : α} [DecidableLE α] [BoundedOrder α] (hs : a ∈ upperClosure ↑s) (ht : a ∈ upperClosure ↑t) :

(s ⊻ t).truncatedInf a = s.truncatedInf a ⊔ t.truncatedInf a

theorem Finset.truncatedSup_infs_of_notMem {α : Type u_1} [DistribLattice α] [DecidableEq α] {s t : Finset α} {a : α} [DecidableLE α] [BoundedOrder α] (ha : a ∉ lowerClosure ↑s ⊓ lowerClosure ↑t) :

(s ⊼ t).truncatedSup a = ⊤

@[deprecated Finset.truncatedSup_infs_of_notMem (since := "2025-05-23")]

theorem Finset.truncatedSup_infs_of_not_mem {α : Type u_1} [DistribLattice α] [DecidableEq α] {s t : Finset α} {a : α} [DecidableLE α] [BoundedOrder α] (ha : a ∉ lowerClosure ↑s ⊓ lowerClosure ↑t) :

(s ⊼ t).truncatedSup a = ⊤

Alias of Finset.truncatedSup_infs_of_notMem.

theorem Finset.truncatedInf_sups_of_notMem {α : Type u_1} [DistribLattice α] [DecidableEq α] {s t : Finset α} {a : α} [DecidableLE α] [BoundedOrder α] (ha : a ∉ upperClosure ↑s ⊔ upperClosure ↑t) :

(s ⊻ t).truncatedInf a = ⊥

@[deprecated Finset.truncatedInf_sups_of_notMem (since := "2025-05-23")]

theorem Finset.truncatedInf_sups_of_not_mem {α : Type u_1} [DistribLattice α] [DecidableEq α] {s t : Finset α} {a : α} [DecidableLE α] [BoundedOrder α] (ha : a ∉ upperClosure ↑s ⊔ upperClosure ↑t) :

(s ⊻ t).truncatedInf a = ⊥

Alias of Finset.truncatedInf_sups_of_notMem.

@[simp]

theorem Finset.compl_truncatedSup {α : Type u_1} [BooleanAlgebra α] [DecidableLE α] (s : Finset α) (a : α) :

(s.truncatedSup a)ᶜ = s.compls.truncatedInf aᶜ

@[simp]

theorem Finset.compl_truncatedInf {α : Type u_1} [BooleanAlgebra α] [DecidableLE α] (s : Finset α) (a : α) :

(s.truncatedInf a)ᶜ = s.compls.truncatedSup aᶜ

theorem Finset.card_truncatedSup_union_add_card_truncatedSup_infs {α : Type u_1} [DecidableEq α] [Fintype α] (𝒜 ℬ : Finset (Finset α)) (s : Finset α) :

((𝒜 ∪ ℬ).truncatedSup s).card + ((𝒜 ⊼ ℬ).truncatedSup s).card = (𝒜.truncatedSup s).card + (ℬ.truncatedSup s).card

theorem Finset.card_truncatedInf_union_add_card_truncatedInf_sups {α : Type u_1} [DecidableEq α] [Fintype α] (𝒜 ℬ : Finset (Finset α)) (s : Finset α) :

((𝒜 ∪ ℬ).truncatedInf s).card + ((𝒜 ⊻ ℬ).truncatedInf s).card = (𝒜.truncatedInf s).card + (ℬ.truncatedInf s).card

def AhlswedeZhang.infSum {α : Type u_1} [Fintype α] [DecidableEq α] (𝒜 : Finset (Finset α)) :

Weighted sum of the size of the truncated infima of a set family. Relevant to the Ahlswede-Zhang identity.

Equations

AhlswedeZhang.infSum 𝒜 = ∑ s : Finset α, ↑(𝒜.truncatedInf s).card / (↑s.card * ↑((Fintype.card α).choose s.card))

Instances For

def AhlswedeZhang.supSum {α : Type u_1} [Fintype α] [DecidableEq α] (𝒜 : Finset (Finset α)) :

Weighted sum of the size of the truncated suprema of a set family. Relevant to the Ahlswede-Zhang identity.

Equations

AhlswedeZhang.supSum 𝒜 = ∑ s : Finset α, ↑(𝒜.truncatedSup s).card / ((↑(Fintype.card α) - ↑s.card) * ↑((Fintype.card α).choose s.card))

Instances For

theorem AhlswedeZhang.supSum_union_add_supSum_infs {α : Type u_1} [Fintype α] [DecidableEq α] (𝒜 ℬ : Finset (Finset α)) :

supSum (𝒜 ∪ ℬ) + supSum (𝒜 ⊼ ℬ) = supSum 𝒜 + supSum ℬ

theorem AhlswedeZhang.infSum_union_add_infSum_sups {α : Type u_1} [Fintype α] [DecidableEq α] (𝒜 ℬ : Finset (Finset α)) :

infSum (𝒜 ∪ ℬ) + infSum (𝒜 ⊻ ℬ) = infSum 𝒜 + infSum ℬ

theorem AhlswedeZhang.IsAntichain.le_infSum {α : Type u_1} [Fintype α] [DecidableEq α] {𝒜 : Finset (Finset α)} (h𝒜 : IsAntichain (fun (x1 x2 : Finset α) => x1 ⊆ x2) ↑𝒜) (h𝒜₀ : ∅ ∉ 𝒜) :

∑ s ∈ 𝒜, (↑((Fintype.card α).choose s.card))⁻¹ ≤ infSum 𝒜

@[simp]

theorem AhlswedeZhang.supSum_singleton {α : Type u_1} [Fintype α] [DecidableEq α] {s : Finset α} [Nonempty α] (hs : s ≠ Finset.univ) :

supSum {s} = ↑(Fintype.card α) * ∑ k ∈ Finset.range (Fintype.card α), (↑k)⁻¹

theorem AhlswedeZhang.infSum_compls_add_supSum {α : Type u_1} [Fintype α] [DecidableEq α] [Nonempty α] (𝒜 : Finset (Finset α)) :

infSum 𝒜.compls + supSum 𝒜 = ↑(Fintype.card α) * ∑ k ∈ Finset.range (Fintype.card α), (↑k)⁻¹ + 1

The Ahlswede-Zhang Identity.

theorem AhlswedeZhang.supSum_of_univ_notMem {α : Type u_1} [Fintype α] [DecidableEq α] {𝒜 : Finset (Finset α)} [Nonempty α] (h𝒜₁ : 𝒜.Nonempty) (h𝒜₂ : Finset.univ ∉ 𝒜) :

supSum 𝒜 = ↑(Fintype.card α) * ∑ k ∈ Finset.range (Fintype.card α), (↑k)⁻¹

@[deprecated AhlswedeZhang.supSum_of_univ_notMem (since := "2025-05-23")]

theorem AhlswedeZhang.supSum_of_not_univ_mem {α : Type u_1} [Fintype α] [DecidableEq α] {𝒜 : Finset (Finset α)} [Nonempty α] (h𝒜₁ : 𝒜.Nonempty) (h𝒜₂ : Finset.univ ∉ 𝒜) :

supSum 𝒜 = ↑(Fintype.card α) * ∑ k ∈ Finset.range (Fintype.card α), (↑k)⁻¹

Alias of AhlswedeZhang.supSum_of_univ_notMem.

theorem AhlswedeZhang.infSum_eq_one {α : Type u_1} [Fintype α] [DecidableEq α] {𝒜 : Finset (Finset α)} [Nonempty α] (h𝒜₁ : 𝒜.Nonempty) (h𝒜₀ : ∅ ∉ 𝒜) :

infSum 𝒜 = 1

The Ahlswede-Zhang Identity.