Reimer's inequality: statement, reductions, and the monotone cases

DefinitionReimer's inequality#✓fully proved

Reimer's inequality (the van den Berg–Kesten conjecture, proved by Reimer 2000) for product probability weights on Fin n: for every n, every weight φ with φ ≥ 0 and φ i false + φ i true = 1, and all events A, B, wprob φ (A □ B) ≤ wprob φ A * wprob φ B.

def ReimerWprobCore : Prop :=
  ∀ (n : ℕ) (φ : Fin n → Bool → ℝ),
    (∀ i b, 0 ≤ φ i b) → (∀ i, φ i false + φ i true = 1) →
    ∀ (A B : Set (ConfigSpace (Fin n))),
      wprob φ (disjointOccurrence A B) ≤ wprob φ A * wprob φ B

Uses 3 · Used by 3

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

Used byReimer's inequality for Bernoulli measures, assuming the core case · Reimer's inequality for product weights, assuming the core case · Reimer's inequality, ported hypothesis form

TheoremReimer's inequality for product weights, assuming the core case#✓fully proved

Reimer's inequality for product probability weights on any finite set, assuming ReimerWprobCore.

theorem reimer_wprob_general_of_core (h : ReimerWprobCore) [Fintype E] [DecidableEq E]
    (φ : E → Bool → ℝ) (hφ0 : ∀ x b, 0 ≤ φ x b) (hφ1 : ∀ x, φ x false + φ x true = 1)
    (A B : Set (ConfigSpace E)) :
    wprob φ (disjointOccurrence A B) ≤ wprob φ A * wprob φ B

Uses 7 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Reimer's inequality · Disjoint occurrence of events · Weighted probability of an event

Proof usesRelabeling configurations along a bijection · Disjoint occurrence commutes with relabeling coordinates · Weighted probability is invariant under relabeling coordinates

Used byReimer's inequality for Bernoulli measures, assuming the core case

TheoremReimer's inequality for Bernoulli measures, assuming the core case#✓fully proved

Reimer's inequality P_p(A □ B) ≤ P_p(A) * P_p(B) for all events under the product Bernoulli measure on a finite set, assuming ReimerWprobCore.

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

Uses 9

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

Proof usesBernoulli distribution on the Booleans · Bernoulli point masses sum to one · Bernoulli product measure as a weighted probability · Reimer's inequality for product weights, assuming the core case · Weighted probability of an event

TheoremReimer's inequality on the one-point configuration space#✓fully proved

Reimer's inequality on the one-point configuration space ConfigSpace (Fin 0).

theorem reimer_wprob_zero (φ : Fin 0 → Bool → ℝ)
    (A B : Set (ConfigSpace (Fin 0))) :
    wprob φ (disjointOccurrence A B) ≤ wprob φ A * wprob φ B

Uses 5

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

Proof usesDisjoint occurrence on a one-point space is the intersection · Product weight of a configuration

DefinitionFlipping every coordinate of a configuration#✓fully proved

The configuration with every coordinate flipped, x ↦ !(ω x).

def flipCfg (ω : ConfigSpace E) : ConfigSpace E := fun x => !(ω x)

Uses 1 · Used by 2

Statement usesConfiguration space of a statistical-mechanics model

Used byBK inequality for decreasing events under product weights · Coordinate flip as an involutive equivalence

DefinitionCoordinate flip as an involutive equivalence#✓fully proved

Flipping all coordinates, as an involutive equivalence of ConfigSpace E.

def flipEquiv : ConfigSpace E ≃ ConfigSpace E where
  toFun := flipCfg
  invFun := flipCfg
  left_inv := flipCfg_flipCfg
  right_inv := flipCfg_flipCfg

Uses 2 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Flipping every coordinate of a configuration

Used byBK inequality for decreasing events under product weights

TheoremBK inequality for decreasing events under product weights#✓fully proved

The BK inequality for two decreasing events under a product probability weight, obtained from StatMech.bk_wprob_general by flipping all coordinates.

theorem bk_wprob_decreasing [Fintype E] [DecidableEq E] (φ : E → Bool → ℝ)
    (hφ0 : ∀ x b, 0 ≤ φ x b) (hφ1 : ∀ x, φ x false + φ x true = 1)
    {A B : Set (ConfigSpace E)} (hA : IsDecreasing A) (hB : IsDecreasing B) :
    wprob φ (disjointOccurrence A B) ≤ wprob φ A * wprob φ B

Uses 12 · Used by 2

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

Proof usesIncreasing event · Occurrence of an event on a coordinate set · Agreement of configurations on a set · BK inequality for product weights on a finite set · Flipping every coordinate of a configuration · Coordinate flip as an involutive equivalence · Membership in a disjoint occurrence · Product weight of a configuration

Used byReimer's inequality for two lower families · BK inequality for decreasing events

TheoremBK inequality for decreasing events#✓fully proved

The BK inequality for decreasing events: under the product Bernoulli(p) measure on a finite set, P_p(A □ B) ≤ P_p(A) * P_p(B) for decreasing A, B.

theorem bk_inequality_decreasing [Fintype E] [DecidableEq E] {p : ℝ≥0} (hp : p ≤ 1)
    {A B : Set (ConfigSpace E)} (hA : IsDecreasing A) (hB : IsDecreasing 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 9

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

Proof usesBernoulli distribution on the Booleans · Bernoulli point masses sum to one · Bernoulli product measure as a weighted probability · BK inequality for decreasing events under product weights · Weighted probability of an event

8 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.