Reimer's inequality

Reimer's inequality for arbitrary events and its proof machinery: configurations as finsets, down-compression, doubled ground sets, disjoint-pair counts and weighted pair sums, and special and mixed-monotone cases.

TheoremReimer's inequality#●ready to prove

Reimer's inequality (van den Berg–Kesten conjecture). For every n, every product probability weight φ on {0, 1}^n (φ i b ≥ 0, φ i false + φ i true = 1) and all events A, B ⊆ {0, 1}^n, P(A □ B) ≤ P(A) P(B), where A □ B is the event that A and B occur on disjoint sets of coordinates.

public theorem_wanted reimer_inequality :
    ∀ (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

Sources

• D. Reimer, Proof of the van den Berg–Kesten conjecture, Combin. Probab. Comput. 9 (2000), 27–32.

Uses 3

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

• Reimer's inequality: statement, reductions, and the monotone cases
• Reimer's inequality for an increasing and a decreasing event
• Special cases of Reimer's inequality
• Families of finsets as events
• Weighted disjoint-pair sums
• Doubled ground set in Reimer's proof
• Down-compression and disjoint pairs
• Events determined by disjoint coordinate sets

TheoremReimer's inequality, ported hypothesis form#●ready to prove

Reimer's inequality in the form of the ported hypothesis StatMech.ReimerWprobCore (definitionally reimer_inequality).

public theorem_wanted reimer_wprob_core : ReimerWprobCore

Sources

• D. Reimer, Proof of the van den Berg–Kesten conjecture, Combin. Probab. Comput. 9 (2000), 27–32.

Uses 1

Statement usesReimer's inequality

2 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.