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.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 #

References #

Truncated supremum, truncated infimum #

def Finset.truncatedSup {α : Type u_1} [SemilatticeSup α] [DecidableRel fun (x1 x2 : α) => x1 x2] [OrderTop α] (s : Finset α) (a : α) :
α

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

Equations
Instances For
    theorem Finset.truncatedSup_of_mem {α : Type u_1} [SemilatticeSup α] {s : Finset α} {a : α} [DecidableRel fun (x1 x2 : α) => x1 x2] [OrderTop α] (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 α] {s : Finset α} {a : α} [DecidableRel fun (x1 x2 : α) => x1 x2] [OrderTop α] (h : alowerClosure s) :
    s.truncatedSup a =
    @[simp]
    theorem Finset.truncatedSup_empty {α : Type u_1} [SemilatticeSup α] [DecidableRel fun (x1 x2 : α) => x1 x2] [OrderTop α] (a : α) :
    .truncatedSup a =
    @[simp]
    theorem Finset.truncatedSup_singleton {α : Type u_1} [SemilatticeSup α] [DecidableRel fun (x1 x2 : α) => x1 x2] [OrderTop α] (b : α) (a : α) :
    {b}.truncatedSup a = if a b then b else
    theorem Finset.le_truncatedSup {α : Type u_1} [SemilatticeSup α] {s : Finset α} {a : α} [DecidableRel fun (x1 x2 : α) => x1 x2] [OrderTop α] :
    a s.truncatedSup a
    theorem Finset.map_truncatedSup {α : Type u_1} {β : Type u_2} [SemilatticeSup α] [SemilatticeSup β] [BoundedOrder β] [DecidableRel fun (x1 x2 : α) => x1 x2] [OrderTop α] [DecidableRel fun (x1 x2 : β) => x1 x2] (e : α ≃o β) (s : Finset α) (a : α) :
    e (s.truncatedSup a) = (Finset.map e.toEmbedding s).truncatedSup (e a)
    theorem Finset.truncatedSup_of_isAntichain {α : Type u_1} [SemilatticeSup α] {s : Finset α} {a : α} [DecidableRel fun (x1 x2 : α) => x1 x2] [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 : Finset α} {t : Finset α} {a : α} [DecidableRel fun (x1 x2 : α) => x1 x2] [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 : Finset α} {t : Finset α} {a : α} [DecidableRel fun (x1 x2 : α) => x1 x2] [OrderTop α] [DecidableEq α] (hs : a lowerClosure s) (ht : alowerClosure t) :
    (s t).truncatedSup a = s.truncatedSup a
    theorem Finset.truncatedSup_union_right {α : Type u_1} [SemilatticeSup α] {s : Finset α} {t : Finset α} {a : α} [DecidableRel fun (x1 x2 : α) => x1 x2] [OrderTop α] [DecidableEq α] (hs : alowerClosure s) (ht : a lowerClosure t) :
    (s t).truncatedSup a = t.truncatedSup a
    theorem Finset.truncatedSup_union_of_not_mem {α : Type u_1} [SemilatticeSup α] {s : Finset α} {t : Finset α} {a : α} [DecidableRel fun (x1 x2 : α) => x1 x2] [OrderTop α] [DecidableEq α] (hs : alowerClosure s) (ht : alowerClosure t) :
    (s t).truncatedSup a =
    def Finset.truncatedInf {α : Type u_1} [SemilatticeInf α] [DecidableRel fun (x1 x2 : α) => x1 x2] [BoundedOrder α] (s : Finset α) (a : α) :
    α

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

    Equations
    Instances For
      theorem Finset.truncatedInf_of_mem {α : Type u_1} [SemilatticeInf α] {s : Finset α} {a : α} [DecidableRel fun (x1 x2 : α) => x1 x2] [BoundedOrder α] (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 α] {s : Finset α} {a : α} [DecidableRel fun (x1 x2 : α) => x1 x2] [BoundedOrder α] (h : aupperClosure s) :
      s.truncatedInf a =
      theorem Finset.truncatedInf_le {α : Type u_1} [SemilatticeInf α] {s : Finset α} {a : α} [DecidableRel fun (x1 x2 : α) => x1 x2] [BoundedOrder α] :
      s.truncatedInf a a
      @[simp]
      theorem Finset.truncatedInf_empty {α : Type u_1} [SemilatticeInf α] [DecidableRel fun (x1 x2 : α) => x1 x2] [BoundedOrder α] (a : α) :
      .truncatedInf a =
      @[simp]
      theorem Finset.truncatedInf_singleton {α : Type u_1} [SemilatticeInf α] [DecidableRel fun (x1 x2 : α) => x1 x2] [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 β] [DecidableRel fun (x1 x2 : β) => x1 x2] [DecidableRel fun (x1 x2 : α) => x1 x2] [BoundedOrder α] (e : α ≃o β) (s : Finset α) (a : α) :
      e (s.truncatedInf a) = (Finset.map e.toEmbedding s).truncatedInf (e a)
      theorem Finset.truncatedInf_of_isAntichain {α : Type u_1} [SemilatticeInf α] {s : Finset α} {a : α} [DecidableRel fun (x1 x2 : α) => x1 x2] [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 : Finset α} {t : Finset α} {a : α} [DecidableRel fun (x1 x2 : α) => x1 x2] [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 : Finset α} {t : Finset α} {a : α} [DecidableRel fun (x1 x2 : α) => x1 x2] [BoundedOrder α] [DecidableEq α] (hs : a upperClosure s) (ht : aupperClosure t) :
      (s t).truncatedInf a = s.truncatedInf a
      theorem Finset.truncatedInf_union_right {α : Type u_1} [SemilatticeInf α] {s : Finset α} {t : Finset α} {a : α} [DecidableRel fun (x1 x2 : α) => x1 x2] [BoundedOrder α] [DecidableEq α] (hs : aupperClosure s) (ht : a upperClosure t) :
      (s t).truncatedInf a = t.truncatedInf a
      theorem Finset.truncatedInf_union_of_not_mem {α : Type u_1} [SemilatticeInf α] {s : Finset α} {t : Finset α} {a : α} [DecidableRel fun (x1 x2 : α) => x1 x2] [BoundedOrder α] [DecidableEq α] (hs : aupperClosure s) (ht : aupperClosure t) :
      (s t).truncatedInf a =
      theorem Finset.truncatedSup_infs {α : Type u_1} [DistribLattice α] [DecidableEq α] {s : Finset α} {t : Finset α} {a : α} [DecidableRel fun (x1 x2 : α) => x1 x2] [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 : Finset α} {t : Finset α} {a : α} [DecidableRel fun (x1 x2 : α) => x1 x2] [BoundedOrder α] (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 α] [DecidableEq α] {s : Finset α} {t : Finset α} {a : α} [DecidableRel fun (x1 x2 : α) => x1 x2] [BoundedOrder α] (ha : alowerClosure s lowerClosure t) :
      (s t).truncatedSup a =
      theorem Finset.truncatedInf_sups_of_not_mem {α : Type u_1} [DistribLattice α] [DecidableEq α] {s : Finset α} {t : Finset α} {a : α} [DecidableRel fun (x1 x2 : α) => x1 x2] [BoundedOrder α] (ha : aupperClosure s upperClosure t) :
      (s t).truncatedInf a =
      @[simp]
      theorem Finset.compl_truncatedSup {α : Type u_1} [BooleanAlgebra α] [DecidableRel fun (x1 x2 : α) => x1 x2] (s : Finset α) (a : α) :
      (s.truncatedSup a) = s.compls.truncatedInf a
      @[simp]
      theorem Finset.compl_truncatedInf {α : Type u_1} [BooleanAlgebra α] [DecidableRel fun (x1 x2 : α) => x1 x2] (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
      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
        Instances For
          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))⁻¹ AhlswedeZhang.infSum 𝒜
          @[simp]
          theorem AhlswedeZhang.supSum_singleton {α : Type u_1} [Fintype α] [DecidableEq α] {s : Finset α} [Nonempty α] (hs : s Finset.univ) :
          theorem AhlswedeZhang.infSum_compls_add_supSum {α : Type u_1} [Fintype α] [DecidableEq α] [Nonempty α] (𝒜 : Finset (Finset α)) :
          AhlswedeZhang.infSum 𝒜.compls + AhlswedeZhang.supSum 𝒜 = (Fintype.card α) * kFinset.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𝒜) :
          theorem AhlswedeZhang.infSum_eq_one {α : Type u_1} [Fintype α] [DecidableEq α] {𝒜 : Finset (Finset α)} [Nonempty α] (h𝒜₁ : 𝒜.Nonempty) (h𝒜₀ : 𝒜) :

          The Ahlswede-Zhang Identity.