Set family certificates

This file defines the certificator of two families of sets. If we consider set families 𝒜 and ℬ as probabilistic events, the size of the certificator 𝒜 □ ℬ corresponds to the probability that 𝒜 and ℬ occur "disjointly".

Main declarations

• finset.certificator: Certificator of two elements of a Boolean algebra
• finset.card_certificator_le: The Van den Berg-Kesten-Reimer inequality: The probability that 𝒜 and ℬ occur "disjointly" is less than the product of their probabilities.

References

• D. Reimer, Proof of the Van den Berg–Kesten Conjecture

noncomputable def Finset.certificator {α : Type u_1} [BooleanAlgebra α] (s t : Finset α) : Finset α

Equations

• s.certificator t = {a ∈ s ∩ t | ∃ (x : α) (y : α), IsCompl x y ∧ (∀ ⦃b : α⦄, a ⊓ x = b ⊓ x → b ∈ s) ∧ ∀ ⦃b : α⦄, a ⊓ y = b ⊓ y → b ∈ t}

def FinsetFamily.«term_□_» : Lean.TrailingParserDescr

Equations

• FinsetFamily.«term_□_» = Lean.ParserDescr.trailingNode `FinsetFamily.«term_□_» 70 70 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " □ ") (Lean.ParserDescr.cat `term 71))

@[simp]

theorem Finset.mem_certificator {α : Type u_1} [BooleanAlgebra α] {s t : Finset α} {a : α} : a ∈ s.certificator t ↔ ∃ (x : α) (y : α), IsCompl x y ∧ (∀ ⦃b : α⦄, a ⊓ x = b ⊓ x → b ∈ s) ∧ ∀ ⦃b : α⦄, a ⊓ y = b ⊓ y → b ∈ t

theorem Finset.certificator_subset_inter {α : Type u_1} [BooleanAlgebra α] {s t : Finset α} [DecidableEq α] : s.certificator t ⊆ s ∩ t

theorem Finset.certificator_subset_disjSups {α : Type u_1} [BooleanAlgebra α] {s t : Finset α} : s.certificator t ⊆ s.disjSups t

theorem Finset.certificator_comm {α : Type u_1} [BooleanAlgebra α] (s t : Finset α) : s.certificator t = t.certificator s

theorem Finset.IsUpperSet.certificator_eq_inter {α : Type u_1} [BooleanAlgebra α] (s t : Finset α) [DecidableEq α] (hs : IsUpperSet ↑s) (ht : IsLowerSet ↑t) : s.certificator t = s ∩ t

theorem Finset.IsLowerSet.certificator_eq_inter {α : Type u_1} [BooleanAlgebra α] (s t : Finset α) [DecidableEq α] (hs : IsLowerSet ↑s) (ht : IsUpperSet ↑t) : s.certificator t = s ∩ t

theorem Finset.IsUpperSet.certificator_eq_disjSups {α : Type u_1} [BooleanAlgebra α] (s t : Finset α) (hs : IsUpperSet ↑s) (ht : IsUpperSet ↑t) : s.certificator t = s.disjSups t

theorem Finset.card_certificator_le {α : Type u_1} [DecidableEq α] [Fintype α] {𝒜 ℬ : Finset (Finset α)} : 2 ^ Fintype.card α * (𝒜.certificator ℬ).card ≤ 𝒜.card * ℬ.card

The Van den Berg-Kesten-Reimer Inequality: The probability that 𝒜 and ℬ occur "disjointly" is less than the product of their probabilities.