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.sum_card_slice_div_choose_le_one, 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

• R. Ahlswede, Z. Zhang, An identity in combinatorial extremal theory
• D. T. Tru, An AZ-style identity and Bollobás deficiency

Truncated supremum, truncated infimum

def Finset.truncatedSup {α : Type u_1} [SemilatticeSup α] [OrderTop α] [DecidableRel fun (x x_1 : α) => x ≤ x_1] (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 (Finset.filter (fun (b : α) => a ≤ b) s).sup' ⋯ id else ⊤

theorem Finset.truncatedSup_of_mem {α : Type u_1} [SemilatticeSup α] [OrderTop α] [DecidableRel fun (x x_1 : α) => x ≤ x_1] {s : Finset α} {a : α} (h : a ∈ lowerClosure ↑s) : s.truncatedSup a = (Finset.filter (fun (b : α) => a ≤ b) s).sup' ⋯ id

theorem Finset.truncatedSup_of_not_mem {α : Type u_1} [SemilatticeSup α] [OrderTop α] [DecidableRel fun (x x_1 : α) => x ≤ x_1] {s : Finset α} {a : α} (h : a ∉ lowerClosure ↑s) : s.truncatedSup a = ⊤

@[simp]

theorem Finset.truncatedSup_empty {α : Type u_1} [SemilatticeSup α] [OrderTop α] [DecidableRel fun (x x_1 : α) => x ≤ x_1] (a : α) : ∅.truncatedSup a = ⊤

@[simp]

theorem Finset.truncatedSup_singleton {α : Type u_1} [SemilatticeSup α] [OrderTop α] [DecidableRel fun (x x_1 : α) => x ≤ x_1] (b : α) (a : α) : {b}.truncatedSup a = if a ≤ b then b else ⊤

theorem Finset.le_truncatedSup {α : Type u_1} [SemilatticeSup α] [OrderTop α] [DecidableRel fun (x x_1 : α) => x ≤ x_1] {s : Finset α} {a : α} : a ≤ s.truncatedSup a

theorem Finset.map_truncatedSup {α : Type u_1} {β : Type u_2} [SemilatticeSup α] [OrderTop α] [DecidableRel fun (x x_1 : α) => x ≤ x_1] [SemilatticeSup β] [BoundedOrder β] [DecidableRel fun (x x_1 : β) => x ≤ x_1] (e : α ≃o β) (s : Finset α) (a : α) : e (s.truncatedSup a) = (Finset.map e.toEmbedding s).truncatedSup (e a)

theorem Finset.truncatedSup_union {α : Type u_1} [SemilatticeSup α] [OrderTop α] [DecidableRel fun (x x_1 : α) => x ≤ x_1] {s : Finset α} {t : Finset α} {a : α} [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 α] [OrderTop α] [DecidableRel fun (x x_1 : α) => x ≤ x_1] {s : Finset α} {t : Finset α} {a : α} [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 α] [OrderTop α] [DecidableRel fun (x x_1 : α) => x ≤ x_1] {s : Finset α} {t : Finset α} {a : α} [DecidableEq α] (hs : a ∉ lowerClosure ↑s) (ht : a ∈ lowerClosure ↑t) : (s ∪ t).truncatedSup a = t.truncatedSup a

theorem Finset.truncatedSup_union_of_not_mem {α : Type u_1} [SemilatticeSup α] [OrderTop α] [DecidableRel fun (x x_1 : α) => x ≤ x_1] {s : Finset α} {t : Finset α} {a : α} [DecidableEq α] (hs : a ∉ lowerClosure ↑s) (ht : a ∉ lowerClosure ↑t) : (s ∪ t).truncatedSup a = ⊤

theorem Finset.truncatedSup_of_isAntichain {α : Type u_1} [SemilatticeSup α] [OrderTop α] [DecidableRel fun (x x_1 : α) => x ≤ x_1] {s : Finset α} {a : α} (hs : IsAntichain (fun (x x_1 : α) => x ≤ x_1) ↑s) (ha : a ∈ s) : s.truncatedSup a = a

def Finset.truncatedInf {α : Type u_1} [SemilatticeInf α] [BoundedOrder α] [DecidableRel fun (x x_1 : α) => x ≤ x_1] (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 (Finset.filter (fun (x : α) => x ≤ a) s).inf' ⋯ id else ⊥

theorem Finset.truncatedInf_of_mem {α : Type u_1} [SemilatticeInf α] [BoundedOrder α] [DecidableRel fun (x x_1 : α) => x ≤ x_1] {s : Finset α} {a : α} (h : a ∈ upperClosure ↑s) : s.truncatedInf a = (Finset.filter (fun (x : α) => x ≤ a) s).inf' ⋯ id

theorem Finset.truncatedInf_of_not_mem {α : Type u_1} [SemilatticeInf α] [BoundedOrder α] [DecidableRel fun (x x_1 : α) => x ≤ x_1] {s : Finset α} {a : α} (h : a ∉ upperClosure ↑s) : s.truncatedInf a = ⊥

theorem Finset.truncatedInf_le {α : Type u_1} [SemilatticeInf α] [BoundedOrder α] [DecidableRel fun (x x_1 : α) => x ≤ x_1] {s : Finset α} {a : α} : s.truncatedInf a ≤ a

@[simp]

theorem Finset.truncatedInf_empty {α : Type u_1} [SemilatticeInf α] [BoundedOrder α] [DecidableRel fun (x x_1 : α) => x ≤ x_1] (a : α) : ∅.truncatedInf a = ⊥

@[simp]

theorem Finset.truncatedInf_singleton {α : Type u_1} [SemilatticeInf α] [BoundedOrder α] [DecidableRel fun (x x_1 : α) => x ≤ x_1] (b : α) (a : α) : {b}.truncatedInf a = if b ≤ a then b else ⊥

theorem Finset.map_truncatedInf {α : Type u_1} {β : Type u_2} [SemilatticeInf α] [BoundedOrder α] [DecidableRel fun (x x_1 : α) => x ≤ x_1] [SemilatticeInf β] [BoundedOrder β] [DecidableRel fun (x x_1 : β) => x ≤ x_1] (e : α ≃o β) (s : Finset α) (a : α) : e (s.truncatedInf a) = (Finset.map e.toEmbedding s).truncatedInf (e a)

theorem Finset.truncatedInf_union {α : Type u_1} [SemilatticeInf α] [BoundedOrder α] [DecidableRel fun (x x_1 : α) => x ≤ x_1] {s : Finset α} {t : Finset α} {a : α} [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 α] [BoundedOrder α] [DecidableRel fun (x x_1 : α) => x ≤ x_1] {s : Finset α} {t : Finset α} {a : α} [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 α] [BoundedOrder α] [DecidableRel fun (x x_1 : α) => x ≤ x_1] {s : Finset α} {t : Finset α} {a : α} [DecidableEq α] (hs : a ∉ upperClosure ↑s) (ht : a ∈ upperClosure ↑t) : (s ∪ t).truncatedInf a = t.truncatedInf a

theorem Finset.truncatedInf_union_of_not_mem {α : Type u_1} [SemilatticeInf α] [BoundedOrder α] [DecidableRel fun (x x_1 : α) => x ≤ x_1] {s : Finset α} {t : Finset α} {a : α} [DecidableEq α] (hs : a ∉ upperClosure ↑s) (ht : a ∉ upperClosure ↑t) : (s ∪ t).truncatedInf a = ⊥

theorem Finset.truncatedInf_of_isAntichain {α : Type u_1} [SemilatticeInf α] [BoundedOrder α] [DecidableRel fun (x x_1 : α) => x ≤ x_1] {s : Finset α} {a : α} (hs : IsAntichain (fun (x x_1 : α) => x ≤ x_1) ↑s) (ha : a ∈ s) : s.truncatedInf a = a

theorem Finset.truncatedSup_infs {α : Type u_1} [DistribLattice α] [BoundedOrder α] [DecidableEq α] [DecidableRel fun (x x_1 : α) => x ≤ x_1] {s : Finset α} {t : Finset α} {a : α} (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 α] [BoundedOrder α] [DecidableEq α] [DecidableRel fun (x x_1 : α) => x ≤ x_1] {s : Finset α} {t : Finset α} {a : α} (hs : a ∈ upperClosure ↑s) (ht : a ∈ upperClosure ↑t) : (s ⊻ t).truncatedInf a = s.truncatedInf a ⊔ t.truncatedInf a

theorem Finset.truncatedSup_infs_of_not_mem {α : Type u_1} [DistribLattice α] [BoundedOrder α] [DecidableEq α] [DecidableRel fun (x x_1 : α) => x ≤ x_1] {s : Finset α} {t : Finset α} {a : α} (ha : a ∉ lowerClosure ↑s ⊓ lowerClosure ↑t) : (s ⊼ t).truncatedSup a = ⊤

theorem Finset.truncatedInf_sups_of_not_mem {α : Type u_1} [DistribLattice α] [BoundedOrder α] [DecidableEq α] [DecidableRel fun (x x_1 : α) => x ≤ x_1] {s : Finset α} {t : Finset α} {a : α} (ha : a ∉ upperClosure ↑s ⊔ upperClosure ↑t) : (s ⊻ t).truncatedInf a = ⊥

@[simp]

theorem Finset.compl_truncatedSup {α : Type u_1} [BooleanAlgebra α] [DecidableRel fun (x x_1 : α) => x ≤ x_1] (s : Finset α) (a : α) : (s.truncatedSup a)ᶜ = s.compls.truncatedInf aᶜ

@[simp]

theorem Finset.compl_truncatedInf {α : Type u_1} [BooleanAlgebra α] [DecidableRel fun (x x_1 : α) => x ≤ x_1] (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 α)) (ℬ : 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 α)) (ℬ : 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))

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))

theorem AhlswedeZhang.supSum_union_add_supSum_infs {α : Type u_1} [Fintype α] [DecidableEq α] (𝒜 : Finset (Finset α)) (ℬ : Finset (Finset α)) : AhlswedeZhang.supSum (𝒜 ∪ ℬ) + AhlswedeZhang.supSum (𝒜 ⊼ ℬ) = AhlswedeZhang.supSum 𝒜 + AhlswedeZhang.supSum ℬ

theorem AhlswedeZhang.infSum_union_add_infSum_sups {α : Type u_1} [Fintype α] [DecidableEq α] (𝒜 : Finset (Finset α)) (ℬ : Finset (Finset α)) : AhlswedeZhang.infSum (𝒜 ∪ ℬ) + AhlswedeZhang.infSum (𝒜 ⊻ ℬ) = AhlswedeZhang.infSum 𝒜 + AhlswedeZhang.infSum ℬ

theorem AhlswedeZhang.IsAntichain.le_infSum {α : Type u_1} [Fintype α] [DecidableEq α] {𝒜 : Finset (Finset α)} (h𝒜 : IsAntichain (fun (x x_1 : Finset α) => x ⊆ x_1) ↑𝒜) (h𝒜₀ : ∅ ∉ 𝒜) : ∑ s ∈ 𝒜, (↑((Fintype.card α).choose s.card))⁻¹ ≤ AhlswedeZhang.infSum 𝒜

@[simp]

theorem AhlswedeZhang.supSum_singleton {α : Type u_1} [Fintype α] [DecidableEq α] {s : Finset α} [Nonempty α] (hs : s ≠ Finset.univ) : AhlswedeZhang.supSum {s} = ↑(Fintype.card α) * ∑ k ∈ Finset.range (Fintype.card α), (↑k)⁻¹

theorem AhlswedeZhang.infSum_compls_add_supSum {α : Type u_1} [Fintype α] [DecidableEq α] [Nonempty α] (𝒜 : Finset (Finset α)) : AhlswedeZhang.infSum 𝒜.compls + AhlswedeZhang.supSum 𝒜 = ↑(Fintype.card α) * ∑ k ∈ Finset.range (Fintype.card α), (↑k)⁻¹ + 1

The Ahlswede-Zhang Identity.

theorem AhlswedeZhang.supSum_of_not_univ_mem {α : Type u_1} [Fintype α] [DecidableEq α] {𝒜 : Finset (Finset α)} [Nonempty α] (h𝒜₁ : 𝒜.Nonempty) (h𝒜₂ : Finset.univ ∉ 𝒜) : AhlswedeZhang.supSum 𝒜 = ↑(Fintype.card α) * ∑ k ∈ Finset.range (Fintype.card α), (↑k)⁻¹

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

The Ahlswede-Zhang Identity.