Families of finsets as events

TheoremLower sets are families closed under erasing an element#✓fully proved

A family of finsets is a lower set iff it is closed under erasing any single element.

theorem isLowerSet_iff_isDownAt_all (𝒜 : Finset (Finset α)) :
    IsLowerSet (𝒜 : Set (Finset α)) ↔ ∀ i, IsDownAtCoord i 𝒜

Uses 1

Statement usesFamily closed under erasing a coordinate

4 fully proved

Bridge

DefinitionEvent of a family of finsets#✓fully proved

The event that the support of a configuration lies in the family 𝒜.

def familyEvent (𝒜 : Finset (Finset α)) : Set (ConfigSpace α) := {ω | cfgSupport ω ∈ 𝒜}

abbrev ConfigSpace (E : Type*) : Type _ := E → Bool

MathlibExt/Probability/Configuration/ConfigSpace.lean:40

def cfgSupport [Fintype E] [DecidableEq E] (ω : ConfigSpace E) : Finset E :=
  Finset.univ.filter (fun i => ω i = true)

MathlibExt/Probability/CorrelationInequalities/ReimerCompression.lean:54

Uses 2 · Used by 3

Statement usesConfiguration space of a statistical-mechanics model · Support of a configuration as a finset

Used byWeighted disjoint pairs as a doubled-weight probability · Reimer's inequality for two lower families · Reimer's inequality for two upper families

Base Case

TheoremReimer's inequality for two lower families#✓fully proved

Reimer's inequality for the events of two lower families (the BK inequality for decreasing events).

theorem reimer_wprob_familyEvent_of_isLowerSet (w : α → Bool → ℝ)
    (hw0 : ∀ x b, 0 ≤ w x b) (hw1 : ∀ x, w x false + w x true = 1)
    {𝒜 ℬ : Finset (Finset α)} (h𝒜 : IsLowerSet (𝒜 : Set (Finset α)))
    (hℬ : IsLowerSet (ℬ : Set (Finset α))) :
    wprob w (disjointOccurrence (familyEvent 𝒜) (familyEvent ℬ))
      ≤ wprob w (familyEvent 𝒜) * wprob w (familyEvent ℬ)

noncomputable def wprob [Fintype E] [DecidableEq E] (φ : E → Bool → ℝ)
    (S : Set (ConfigSpace E)) : ℝ :=
  ∑ ω, S.indicator (fun _ => (1 : ℝ)) ω * pweight φ ω

MathlibExt/Probability/CorrelationInequalities/BK.lean:101

def disjointOccurrence (A B : Set (ConfigSpace E)) : Set (ConfigSpace E) :=
  {ω | ∃ K L : Set E, Disjoint K L ∧ OccursOn A K ω ∧ OccursOn B L ω}

MathlibExt/Probability/CorrelationInequalities/DisjointOccurrence.lean:92

def familyEvent (𝒜 : Finset (Finset α)) : Set (ConfigSpace α) := {ω | cfgSupport ω ∈ 𝒜}

MathlibExt/Probability/CorrelationInequalities/ReimerFamilyEvents.lean:59

Uses 7

Statement usesDisjoint occurrence of events · Event of a family of finsets · Weighted probability of an event

Proof usesConfiguration space of a statistical-mechanics model · Decreasing event · BK inequality for decreasing events under product weights · Support of a configuration as a finset

TheoremReimer's inequality for two upper families#✓fully proved

Reimer's inequality for the events of two upper families (the BK inequality).

theorem reimer_wprob_familyEvent_of_isUpperSet (w : α → Bool → ℝ)
    (hw0 : ∀ x b, 0 ≤ w x b) (hw1 : ∀ x, w x false + w x true = 1)
    {𝒜 ℬ : Finset (Finset α)} (h𝒜 : IsUpperSet (𝒜 : Set (Finset α)))
    (hℬ : IsUpperSet (ℬ : Set (Finset α))) :
    wprob w (disjointOccurrence (familyEvent 𝒜) (familyEvent ℬ))
      ≤ wprob w (familyEvent 𝒜) * wprob w (familyEvent ℬ)

noncomputable def wprob [Fintype E] [DecidableEq E] (φ : E → Bool → ℝ)
    (S : Set (ConfigSpace E)) : ℝ :=
  ∑ ω, S.indicator (fun _ => (1 : ℝ)) ω * pweight φ ω

MathlibExt/Probability/CorrelationInequalities/BK.lean:101

def disjointOccurrence (A B : Set (ConfigSpace E)) : Set (ConfigSpace E) :=
  {ω | ∃ K L : Set E, Disjoint K L ∧ OccursOn A K ω ∧ OccursOn B L ω}

MathlibExt/Probability/CorrelationInequalities/DisjointOccurrence.lean:92

def familyEvent (𝒜 : Finset (Finset α)) : Set (ConfigSpace α) := {ω | cfgSupport ω ∈ 𝒜}

MathlibExt/Probability/CorrelationInequalities/ReimerFamilyEvents.lean:59

Uses 7

Statement usesDisjoint occurrence of events · Event of a family of finsets · Weighted probability of an event

Proof usesConfiguration space of a statistical-mechanics model · Increasing event · BK inequality for product weights on a finite set · Support of a configuration as a finset

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.