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 𝒜, the Ahlswede-Zhang identity states that the sum of
|⋂ B ∈ 𝒜, B ⊆ A, B|/(|A| * n.choose |A|) is exactly 1.
Main declarations #
finset.truncated_sup:s.truncated_sup ais the supremum of allb ≤ ain𝒜if there are some, or⊤if there are none.finset.truncated_infs.truncated_inf ais the infimum of allb ≥ ain𝒜if there are some, or⊥if there are none.
References #
Truncated supremum, truncated infimum #
def
finset.truncated_sup
{α : Type u_1}
[semilattice_sup α]
[order_top α]
[decidable_rel has_le.le]
(s : finset α)
(a : α) :
α
The infimum of the elements of s less than a if there are some, otherwise ⊤.
Equations
- s.truncated_sup a = dite (a ∈ lower_closure ↑s) (λ (h : a ∈ lower_closure ↑s), (finset.filter (λ (b : α), a ≤ b) s).sup' _ id) (λ (h : a ∉ lower_closure ↑s), ⊤)
theorem
finset.truncated_sup_of_mem
{α : Type u_1}
[semilattice_sup α]
[order_top α]
[decidable_rel has_le.le]
{s : finset α}
{a : α}
(h : a ∈ lower_closure ↑s) :
s.truncated_sup a = (finset.filter (λ (b : α), a ≤ b) s).sup' _ id
theorem
finset.truncated_sup_of_not_mem
{α : Type u_1}
[semilattice_sup α]
[order_top α]
[decidable_rel has_le.le]
{s : finset α}
{a : α}
(h : a ∉ lower_closure ↑s) :
s.truncated_sup a = ⊤
@[simp]
theorem
finset.truncated_sup_empty
{α : Type u_1}
[semilattice_sup α]
[order_top α]
[decidable_rel has_le.le]
(a : α) :
∅.truncated_sup a = ⊤
theorem
finset.le_truncated_sup
{α : Type u_1}
[semilattice_sup α]
[order_top α]
[decidable_rel has_le.le]
{s : finset α}
{a : α} :
a ≤ s.truncated_sup a
theorem
finset.map_truncated_sup
{α : Type u_1}
{β : Type u_2}
[semilattice_sup α]
[order_top α]
[decidable_rel has_le.le]
[semilattice_sup β]
[bounded_order β]
[decidable_rel has_le.le]
(e : α ≃o β)
(s : finset α)
(a : α) :
⇑e (s.truncated_sup a) = (finset.map e.to_equiv.to_embedding s).truncated_sup (⇑e a)
theorem
finset.truncated_sup_union
{α : Type u_1}
[semilattice_sup α]
[order_top α]
[decidable_rel has_le.le]
{s t : finset α}
{a : α}
[decidable_eq α]
(hs : a ∈ lower_closure ↑s)
(ht : a ∈ lower_closure ↑t) :
(s ∪ t).truncated_sup a = s.truncated_sup a ⊔ t.truncated_sup a
theorem
finset.truncated_sup_union_left
{α : Type u_1}
[semilattice_sup α]
[order_top α]
[decidable_rel has_le.le]
{s t : finset α}
{a : α}
[decidable_eq α]
(hs : a ∈ lower_closure ↑s)
(ht : a ∉ lower_closure ↑t) :
(s ∪ t).truncated_sup a = s.truncated_sup a
theorem
finset.truncated_sup_union_right
{α : Type u_1}
[semilattice_sup α]
[order_top α]
[decidable_rel has_le.le]
{s t : finset α}
{a : α}
[decidable_eq α]
(hs : a ∉ lower_closure ↑s)
(ht : a ∈ lower_closure ↑t) :
(s ∪ t).truncated_sup a = t.truncated_sup a
theorem
finset.truncated_sup_union_of_not_mem
{α : Type u_1}
[semilattice_sup α]
[order_top α]
[decidable_rel has_le.le]
{s t : finset α}
{a : α}
[decidable_eq α]
(hs : a ∉ lower_closure ↑s)
(ht : a ∉ lower_closure ↑t) :
(s ∪ t).truncated_sup a = ⊤
def
finset.truncated_inf
{α : Type u_1}
[semilattice_inf α]
[bounded_order α]
[decidable_rel has_le.le]
(s : finset α)
(a : α) :
α
The infimum of the elements of s less than a if there are some, otherwise ⊥.
Equations
- s.truncated_inf a = dite (a ∈ upper_closure ↑s) (λ (h : a ∈ upper_closure ↑s), (finset.filter (λ (b : α), b ≤ a) s).inf' _ id) (λ (h : a ∉ upper_closure ↑s), ⊥)
theorem
finset.truncated_inf_of_mem
{α : Type u_1}
[semilattice_inf α]
[bounded_order α]
[decidable_rel has_le.le]
{s : finset α}
{a : α}
(h : a ∈ upper_closure ↑s) :
s.truncated_inf a = (finset.filter (λ (b : α), b ≤ a) s).inf' _ id
theorem
finset.truncated_inf_of_not_mem
{α : Type u_1}
[semilattice_inf α]
[bounded_order α]
[decidable_rel has_le.le]
{s : finset α}
{a : α}
(h : a ∉ upper_closure ↑s) :
s.truncated_inf a = ⊥
theorem
finset.truncated_inf_le
{α : Type u_1}
[semilattice_inf α]
[bounded_order α]
[decidable_rel has_le.le]
(s : finset α)
(a : α) :
s.truncated_inf a ≤ a
@[simp]
theorem
finset.truncated_inf_empty
{α : Type u_1}
[semilattice_inf α]
[bounded_order α]
[decidable_rel has_le.le]
(a : α) :
∅.truncated_inf a = ⊥
theorem
finset.map_truncated_inf
{α : Type u_1}
{β : Type u_2}
[semilattice_inf α]
[bounded_order α]
[decidable_rel has_le.le]
[semilattice_inf β]
[bounded_order β]
[decidable_rel has_le.le]
(e : α ≃o β)
(s : finset α)
(a : α) :
⇑e (s.truncated_inf a) = (finset.map e.to_equiv.to_embedding s).truncated_inf (⇑e a)
theorem
finset.truncated_inf_union
{α : Type u_1}
[semilattice_inf α]
[bounded_order α]
[decidable_rel has_le.le]
{s t : finset α}
{a : α}
[decidable_eq α]
(hs : a ∈ upper_closure ↑s)
(ht : a ∈ upper_closure ↑t) :
(s ∪ t).truncated_inf a = s.truncated_inf a ⊓ t.truncated_inf a
theorem
finset.truncated_inf_union_left
{α : Type u_1}
[semilattice_inf α]
[bounded_order α]
[decidable_rel has_le.le]
{s t : finset α}
{a : α}
[decidable_eq α]
(hs : a ∈ upper_closure ↑s)
(ht : a ∉ upper_closure ↑t) :
(s ∪ t).truncated_inf a = s.truncated_inf a
theorem
finset.truncated_inf_union_right
{α : Type u_1}
[semilattice_inf α]
[bounded_order α]
[decidable_rel has_le.le]
{s t : finset α}
{a : α}
[decidable_eq α]
(hs : a ∉ upper_closure ↑s)
(ht : a ∈ upper_closure ↑t) :
(s ∪ t).truncated_inf a = t.truncated_inf a
theorem
finset.truncated_inf_union_of_not_mem
{α : Type u_1}
[semilattice_inf α]
[bounded_order α]
[decidable_rel has_le.le]
{s t : finset α}
{a : α}
[decidable_eq α]
(hs : a ∉ upper_closure ↑s)
(ht : a ∉ upper_closure ↑t) :
(s ∪ t).truncated_inf a = ⊥
theorem
finset.truncated_sup_infs
{α : Type u_1}
[distrib_lattice α]
[bounded_order α]
[decidable_eq α]
[decidable_rel has_le.le]
{s t : finset α}
{a : α}
(hs : a ∈ lower_closure ↑s)
(ht : a ∈ lower_closure ↑t) :
(s ⊼ t).truncated_sup a = s.truncated_sup a ⊓ t.truncated_sup a
theorem
finset.truncated_inf_sups
{α : Type u_1}
[distrib_lattice α]
[bounded_order α]
[decidable_eq α]
[decidable_rel has_le.le]
{s t : finset α}
{a : α}
(hs : a ∈ upper_closure ↑s)
(ht : a ∈ upper_closure ↑t) :
(s ⊻ t).truncated_inf a = s.truncated_inf a ⊔ t.truncated_inf a
theorem
finset.truncated_sup_infs_of_not_mem
{α : Type u_1}
[distrib_lattice α]
[bounded_order α]
[decidable_eq α]
[decidable_rel has_le.le]
{s t : finset α}
{a : α}
(ha : a ∉ lower_closure ↑s ⊓ lower_closure ↑t) :
(s ⊼ t).truncated_sup a = ⊤
theorem
finset.truncated_inf_sups_of_not_mem
{α : Type u_1}
[distrib_lattice α]
[bounded_order α]
[decidable_eq α]
[decidable_rel has_le.le]
{s t : finset α}
{a : α}
(ha : a ∉ upper_closure ↑s ⊔ upper_closure ↑t) :
(s ⊻ t).truncated_inf a = ⊥
@[simp]
theorem
finset.compl_truncated_sup
{α : Type u_1}
[boolean_algebra α]
[decidable_rel has_le.le]
(s : finset α)
(a : α) :
(s.truncated_sup a)ᶜ = (finset.map {to_fun := has_compl.compl (boolean_algebra.to_has_compl α), inj' := _} s).truncated_inf aᶜ
@[simp]
theorem
finset.compl_truncated_inf
{α : Type u_1}
[boolean_algebra α]
[decidable_rel has_le.le]
(s : finset α)
(a : α) :
(s.truncated_inf a)ᶜ = (finset.map {to_fun := has_compl.compl (boolean_algebra.to_has_compl α), inj' := _} s).truncated_sup aᶜ
theorem
finset.card_truncated_sup_union_add_card_truncated_sup_infs
{α : Type u_1}
[decidable_eq α]
[fintype α]
(𝒜 ℬ : finset (finset α))
(s : finset α) :
((𝒜 ∪ ℬ).truncated_sup s).card + ((𝒜 ⊼ ℬ).truncated_sup s).card = (𝒜.truncated_sup s).card + (ℬ.truncated_sup s).card