le_card_inter_finset' — Mathlib

English

Harris-Kleitman inequality for lower sets: for two downward-closed families of Finsets, a bound involves 2^|S| and the intersection.

Русский

Неравенство Харриса–Клейтмана для нисходящих множеств: для двух downward-closed семейств конечных множеств существует оценка через 2^{|S|} и пересечение.

LaTeX

$$$$|\\mathcal{A}|\\cdot|\\mathcal{B}| \\le 2^{|\\mathsf{X}|}\\;|\\mathcal{A}\\cap\\mathcal{B}|$$$$

Lean4

/-- **Harris-Kleitman inequality**: Any two lower sets of finsets correlate. -/
theorem le_card_inter_finset' (h𝒜 : IsLowerSet (𝒜 : Set (Finset α))) (hℬ : IsLowerSet (ℬ : Set (Finset α)))
    (h𝒜s : ∀ t ∈ 𝒜, t ⊆ s) (hℬs : ∀ t ∈ ℬ, t ⊆ s) : #𝒜 * #ℬ ≤ 2 ^ #s * #(𝒜 ∩ ℬ) := by
  induction s using Finset.induction generalizing 𝒜 ℬ with
  | empty =>
    simp_rw [subset_empty, ← subset_singleton_iff', subset_singleton_iff] at h𝒜s hℬs
    obtain rfl | rfl := h𝒜s
    · simp only [card_empty, zero_mul, empty_inter, mul_zero, le_refl]
    obtain rfl | rfl := hℬs
    · simp only [card_empty, inter_empty, mul_zero, le_refl]
    · simp only [card_empty, pow_zero, inter_singleton_of_mem, mem_singleton, card_singleton, le_refl]
  | insert a s hs
    ih =>
    rw [card_insert_of_notMem hs, ← card_memberSubfamily_add_card_nonMemberSubfamily a 𝒜, ←
      card_memberSubfamily_add_card_nonMemberSubfamily a ℬ, add_mul, mul_add, mul_add, add_comm (_ * _),
      add_add_add_comm]
    refine
      (add_le_add_right
            (mul_add_mul_le_mul_add_mul (card_le_card h𝒜.memberSubfamily_subset_nonMemberSubfamily) <|
              card_le_card hℬ.memberSubfamily_subset_nonMemberSubfamily)
            _).trans
        ?_
    rw [← two_mul, pow_succ', mul_assoc]
    have h₀ : ∀ 𝒞 : Finset (Finset α), (∀ t ∈ 𝒞, t ⊆ insert a s) → ∀ t ∈ 𝒞.nonMemberSubfamily a, t ⊆ s :=
      by
      rintro 𝒞 h𝒞 t ht
      rw [mem_nonMemberSubfamily] at ht
      exact (subset_insert_iff_of_notMem ht.2).1 (h𝒞 _ ht.1)
    have h₁ : ∀ 𝒞 : Finset (Finset α), (∀ t ∈ 𝒞, t ⊆ insert a s) → ∀ t ∈ 𝒞.memberSubfamily a, t ⊆ s :=
      by
      rintro 𝒞 h𝒞 t ht
      rw [mem_memberSubfamily] at ht
      exact (subset_insert_iff_of_notMem ht.2).1 ((subset_insert _ _).trans <| h𝒞 _ ht.1)
    refine mul_le_mul_left' ?_ _
    refine
      (add_le_add (ih h𝒜.memberSubfamily hℬ.memberSubfamily (h₁ _ h𝒜s) <| h₁ _ hℬs) <|
            ih h𝒜.nonMemberSubfamily hℬ.nonMemberSubfamily (h₀ _ h𝒜s) <| h₀ _ hℬs).trans_eq
        ?_
    rw [← mul_add, ← memberSubfamily_inter, ← nonMemberSubfamily_inter,
      card_memberSubfamily_add_card_nonMemberSubfamily]

Похожие утверждения