Special cases of Reimer's inequality

DefinitionNegatively correlated events#✓fully proved

A and B are negatively correlated under the weight φ: wprob φ (A ∩ B) ≤ wprob φ A * wprob φ B.

def NegativelyCorrelated [Fintype E] [DecidableEq E] (φ : E → Bool → ℝ)
    (A B : Set (ConfigSpace E)) : Prop :=
  wprob φ (A ∩ B) ≤ wprob φ A * wprob φ B

Uses 2 · Used by 2

Statement usesConfiguration space of a statistical-mechanics model · Weighted probability of an event

Used byReimer's inequality for disjoint events · Reimer's inequality for negatively correlated events

TheoremReimer's inequality for negatively correlated events#✓fully proved

Reimer's inequality for negatively correlated events (since A □ B ⊆ A ∩ B).

theorem reimer_wprob_of_negCorr [Fintype E] [DecidableEq E] {φ : E → Bool → ℝ}
    (hφ0 : ∀ x b, 0 ≤ φ x b) {A B : Set (ConfigSpace E)} (h : NegativelyCorrelated φ A B) :
    wprob φ (disjointOccurrence A B) ≤ wprob φ A * wprob φ B

Uses 6 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Negatively correlated events · Disjoint occurrence of events · Weighted probability of an event

Proof usesDisjoint occurrence lies in the intersection · Monotonicity of the weighted probability

Used byReimer's inequality for disjoint events

TheoremReimer's inequality for disjoint events#✓fully proved

Reimer's inequality for disjoint events under the product Bernoulli measure: both sides are compared with P(A □ B) = 0.

theorem reimer_inequality_of_inter_empty [Fintype E] [DecidableEq E] {p : ℝ≥0} (hp : p ≤ 1)
    {A B : Set (ConfigSpace E)} (h : A ∩ B = ∅) :
    (bernoulliProductMeasure (E := E) p hp).real (disjointOccurrence A B)
      ≤ (bernoulliProductMeasure (E := E) p hp).real A
        * (bernoulliProductMeasure (E := E) p hp).real B

Uses 10 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Bernoulli product measure on configuration space · Disjoint occurrence of events

Proof usesNegatively correlated events · Bernoulli distribution on the Booleans · Bernoulli product measure as a weighted probability · Product weight of a configuration · Nonnegativity of the product weight · Reimer's inequality for negatively correlated events · Weighted probability of an event

Used byReimer's inequality for the XOR and XNOR events

DefinitionEvent that two coordinates differ#✓fully proved

The event ω 0 ≠ ω 1 on two coordinates.

def evXor : Set (ConfigSpace (Fin 2)) := {ω | ω 0 ≠ ω 1}

Uses 1 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model

Used byReimer's inequality for the XOR and XNOR events

DefinitionEvent that two coordinates agree#✓fully proved

The event ω 0 = ω 1 on two coordinates.

def evXnor : Set (ConfigSpace (Fin 2)) := {ω | ω 0 = ω 1}

Uses 1 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model

Used byReimer's inequality for the XOR and XNOR events

TheoremReimer's inequality for the XOR and XNOR events#✓fully proved

Reimer's inequality for evXor and evXnor, which are neither increasing nor decreasing (and are disjoint).

theorem reimer_xor_xnor_inequality {p : ℝ≥0} (hp : p ≤ 1) :
    (bernoulliProductMeasure (E := Fin 2) p hp).real (disjointOccurrence evXor evXnor)
      ≤ (bernoulliProductMeasure (E := Fin 2) p hp).real evXor
        * (bernoulliProductMeasure (E := Fin 2) p hp).real evXnor

Uses 6

Statement usesConfiguration space of a statistical-mechanics model · Bernoulli product measure on configuration space · Disjoint occurrence of events · Event that two coordinates agree · Event that two coordinates differ

Proof usesReimer's inequality for disjoint events

TheoremSlice inequalities in the one-coordinate BK induction step#✓fully proved

The slice inequalities of the one-coordinate BK induction step, with A₀, A₁, B₀, B₁ the slices at the first coordinate: P(A₀ □ B₀) ≤ P((A₀ □ B₁) ∩ (A₁ □ B₀)) and P((A₀ □ B₁) ∪ (A₁ □ B₀)) ≤ P(A₁) P(B₁), for increasing events A, B.

theorem slice_disjointOccurrence_le_of_isIncreasing (n : ℕ) (ψ : Fin n → Bool → ℝ)
    (hψ0 : ∀ i b, 0 ≤ ψ i b) (hψ1 : ∀ i, ψ i false + ψ i true = 1)
    (A B : Set (ConfigSpace (Fin (n + 1)))) (hA : IsIncreasing A) (hB : IsIncreasing B) :
    wprob ψ (disjointOccurrence (slice A false) (slice B false))
        ≤ wprob ψ (disjointOccurrence (slice A false) (slice B true)
                    ∩ disjointOccurrence (slice A true) (slice B false))
    ∧ wprob ψ (disjointOccurrence (slice A false) (slice B true)
                ∪ disjointOccurrence (slice A true) (slice B false))
        ≤ wprob ψ (slice A true) * wprob ψ (slice B true)

Uses 10

Statement usesConfiguration space of a statistical-mechanics model · Increasing event · Disjoint occurrence of events · Slice of an event at the first coordinate · Weighted probability of an event

Proof usesBK inequality for product weights on \(n\) ordered coordinates · Disjoint occurrence is monotone in both events · False slice of an increasing event lies in the true slice · Slices of an increasing event are increasing · Monotonicity of the weighted probability

7 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.