Reimer's inequality for an increasing and a decreasing event

TheoremHarris–FKG inequality for increasing events#✓fully proved

The Harris–FKG inequality for a product probability weight: increasing events are positively correlated.

theorem wprob_fkg_pos [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 : IsIncreasing A) (hB : IsIncreasing B) :
    wprob φ A * wprob φ B ≤ wprob φ (A ∩ B)

Uses 9 · Used by 1

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

Proof usesFKG lattice condition · Log-modular weights satisfy the FKG lattice condition · FKG inequality for increasing events · Product weight of a configuration · Nonnegativity of the product weight · Product probability weight has total mass one

Used byHarris–FKG inequality for an increasing and a decreasing event

TheoremHarris–FKG inequality for an increasing and a decreasing event#✓fully proved

The Harris–FKG inequality for an increasing and a decreasing event: they are negatively correlated.

theorem wprob_fkg_neg [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 : IsIncreasing A) (hB : IsDecreasing B) :
    wprob φ (A ∩ B) ≤ wprob φ A * wprob φ B

Uses 8 · Used by 1

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

Proof usesComplement of a decreasing event is increasing · Product weight of a configuration · Product probability weight has total mass one · Harris–FKG inequality for increasing events

Used byReimer's inequality for mixed monotone events, product weights

TheoremDisjoint occurrence of an increasing and a decreasing event#✓fully proved

For A increasing and B decreasing, A □ B = A ∩ B.

theorem disjointOccurrence_eq_inter_of_mixed {A B : Set (ConfigSpace E)}
    (hA : IsIncreasing A) (hB : IsDecreasing B) :
    disjointOccurrence A B = A ∩ B

Uses 7 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Decreasing event · Increasing event · Disjoint occurrence of events

Proof usesOccurrence of an event on a coordinate set · Agreement of configurations on a set · Disjoint occurrence lies in the intersection

Used byReimer's inequality for mixed monotone events, product weights

TheoremReimer's inequality for mixed monotone events, product weights#✓fully proved

Reimer's inequality for an increasing and a decreasing event under a product probability weight.

theorem reimerMixed_wprob [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 : IsIncreasing A) (hB : IsDecreasing B) :
    wprob φ (disjointOccurrence A B) ≤ wprob φ A * wprob φ B

Uses 7 · Used by 1

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

Proof usesDisjoint occurrence of an increasing and a decreasing event · Harris–FKG inequality for an increasing and a decreasing event

Used byReimer's inequality for mixed monotone events, Bernoulli measure

TheoremReimer's inequality for mixed monotone events, Bernoulli measure#✓fully proved

Reimer's inequality for an increasing and a decreasing event under the product Bernoulli measure.

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

Statement usesConfiguration space of a statistical-mechanics model · Decreasing event · Increasing 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 · Reimer's inequality for mixed monotone events, product weights · Weighted probability of an event

5 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.