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

• Finset.truncatedSup s a = if h : a ∈ lowerClosure ↑s then Finset.sup' (Finset.filter (fun (b : α) => a ≤ b) s) (_ : (Finset.filter (fun (b : α) => a ≤ b) s).Nonempty) 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) : Finset.truncatedSup s a = Finset.sup' (Finset.filter (fun (b : α) => a ≤ b) s) (_ : (Finset.filter (fun (b : α) => a ≤ b) s).Nonempty) 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) : Finset.truncatedSup s a = ⊤

@[simp]

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

@[simp]

theorem Finset.truncatedSup_singleton {α : Type u_1} [SemilatticeSup α] [OrderTop α] [DecidableRel fun (x x_1 : α) => x ≤ x_1] (b : α) (a : α) : Finset.truncatedSup {b} 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 ≤ Finset.truncatedSup s 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 (Finset.truncatedSup s a) = Finset.truncatedSup (Finset.map (Equiv.toEmbedding e.toEquiv) s) (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) : Finset.truncatedSup (s ∪ t) a = Finset.truncatedSup s a ⊔ Finset.truncatedSup t 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) : Finset.truncatedSup (s ∪ t) a = Finset.truncatedSup s 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) : Finset.truncatedSup (s ∪ t) a = Finset.truncatedSup t 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) : Finset.truncatedSup (s ∪ t) 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) : Finset.truncatedSup s 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

• Finset.truncatedInf s a = if h : a ∈ upperClosure ↑s then Finset.inf' (Finset.filter (fun (x : α) => x ≤ a) s) (_ : (Finset.filter (fun (x : α) => x ≤ a) s).Nonempty) 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) : Finset.truncatedInf s a = Finset.inf' (Finset.filter (fun (x : α) => x ≤ a) s) (_ : (Finset.filter (fun (x : α) => x ≤ a) s).Nonempty) 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) : Finset.truncatedInf s a = ⊥

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

@[simp]

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

@[simp]

theorem Finset.truncatedInf_singleton {α : Type u_1} [SemilatticeInf α] [BoundedOrder α] [DecidableRel fun (x x_1 : α) => x ≤ x_1] (b : α) (a : α) : Finset.truncatedInf {b} 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 (Finset.truncatedInf s a) = Finset.truncatedInf (Finset.map (Equiv.toEmbedding e.toEquiv) s) (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) : Finset.truncatedInf (s ∪ t) a = Finset.truncatedInf s a ⊓ Finset.truncatedInf t 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) : Finset.truncatedInf (s ∪ t) a = Finset.truncatedInf s 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) : Finset.truncatedInf (s ∪ t) a = Finset.truncatedInf t 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) : Finset.truncatedInf (s ∪ t) 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) : Finset.truncatedInf s 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) : Finset.truncatedSup (s ⊼ t) a = Finset.truncatedSup s a ⊓ Finset.truncatedSup t 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) : Finset.truncatedInf (s ⊻ t) a = Finset.truncatedInf s a ⊔ Finset.truncatedInf t 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) : Finset.truncatedSup (s ⊼ t) 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) : Finset.truncatedInf (s ⊻ t) a = ⊥

@[simp]

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

@[simp]

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

theorem Finset.card_truncatedSup_union_add_card_truncatedSup_infs {α : Type u_1} [DecidableEq α] [Fintype α] (𝒜 : Finset (Finset α)) (ℬ : Finset (Finset α)) (s : Finset α) : (Finset.truncatedSup (𝒜 ∪ ℬ) s).card + (Finset.truncatedSup (𝒜 ⊼ ℬ) s).card = (Finset.truncatedSup 𝒜 s).card + (Finset.truncatedSup ℬ s).card

theorem Finset.card_truncatedInf_union_add_card_truncatedInf_sups {α : Type u_1} [DecidableEq α] [Fintype α] (𝒜 : Finset (Finset α)) (ℬ : Finset (Finset α)) (s : Finset α) : (Finset.truncatedInf (𝒜 ∪ ℬ) s).card + (Finset.truncatedInf (𝒜 ⊻ ℬ) s).card = (Finset.truncatedInf 𝒜 s).card + (Finset.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 𝒜 = Finset.sum Finset.univ fun (s : Finset α) => ↑(Finset.truncatedInf 𝒜 s).card / (↑s.card * ↑(Nat.choose (Fintype.card α) 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 𝒜 = Finset.sum Finset.univ fun (s : Finset α) => ↑(Finset.truncatedSup 𝒜 s).card / ((↑(Fintype.card α) - ↑s.card) * ↑(Nat.choose (Fintype.card α) 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𝒜₀ : ∅ ∉ 𝒜) : (Finset.sum 𝒜 fun (s : Finset α) => (↑(Nat.choose (Fintype.card α) 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 α) * Finset.sum (Finset.range (Fintype.card α)) fun (k : ℕ) => (↑k)⁻¹

theorem AhlswedeZhang.infSum_compls_add_supSum {α : Type u_1} [Fintype α] [DecidableEq α] [Nonempty α] (𝒜 : Finset (Finset α)) : AhlswedeZhang.infSum (Finset.compls 𝒜) + AhlswedeZhang.supSum 𝒜 = (↑(Fintype.card α) * Finset.sum (Finset.range (Fintype.card α)) fun (k : ℕ) => (↑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 α) * Finset.sum (Finset.range (Fintype.card α)) fun (k : ℕ) => (↑k)⁻¹

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

The Ahlswede-Zhang Identity.