FKG and Holley inequalities

TheoremFKG inequality#✓fully proved

The FKG inequality (Fortuin, Kasteleyn, Ginibre 1971). Let π be a probability weight on ConfigSpace E (π ≥ 0, ∑ π = 1) satisfying the FKG lattice condition. Then any two monotone functions f g : ConfigSpace E → ℝ are positively correlated: E_π[f] * E_π[g] ≤ E_π[f * g].

See also Mathlib's fkg, which assumes f, g ≥ 0 and does not normalize π; this version removes the sign condition by shifting f and g by their values at ⊥.

theorem fkg_inequality [Fintype E] [DecidableEq E] {π : ConfigSpace E → ℝ}
    (hπ₀ : 0 ≤ π) (hnorm : ∑ ω, π ω = 1) (hπ : FKGLatticeCondition π)
    {f g : ConfigSpace E → ℝ} (hf : Monotone f) (hg : Monotone g) :
    (∑ ω, π ω * f ω) * (∑ ω, π ω * g ω) ≤ ∑ ω, π ω * (f ω * g ω)

Uses 2 · Used by 7

Statement usesConfiguration space of a statistical-mechanics model · FKG lattice condition

Used byFKG inequality for increasing events · Griffiths–Hurst–Sherman inequality · Griffiths–Hurst–Sherman inequality · Griffiths–Hurst–Sherman inequality · FKG inequality · FKG inequality for the random-cluster measure, \(q \ge 1\) · FKG inequality for the random-cluster model

TheoremFKG inequality for increasing events#✓fully proved

The FKG inequality for events: under a probability weight π satisfying the FKG lattice condition, two increasing events are positively correlated, π(A) * π(B) ≤ π(A ∩ B).

theorem fkg_inequality_events [Fintype E] [DecidableEq E] {π : ConfigSpace E → ℝ}
    (hπ₀ : 0 ≤ π) (hnorm : ∑ ω, π ω = 1) (hπ : FKGLatticeCondition π)
    {A B : Set (ConfigSpace E)} (hA : IsIncreasing A) (hB : IsIncreasing B) :
    (∑ ω, π ω * A.indicator (fun _ => (1 : ℝ)) ω)
        * (∑ ω, π ω * B.indicator (fun _ => (1 : ℝ)) ω)
      ≤ ∑ ω, π ω * (A ∩ B).indicator (fun _ => (1 : ℝ)) ω

Uses 5 · Used by 9

Statement usesConfiguration space of a statistical-mechanics model · FKG lattice condition · Increasing event

Proof usesIndicator of an increasing event is monotone · FKG inequality

Used byHarris inequality · Harris–FKG inequality for increasing events · Inf-based and sup-based Ising critical points agree for \(d \ge 2\) · Ergodicity of the plus state · Extremality of the plus state · FKG inequality for increasing random-cluster events · FKG inequality for the wired measure when \(q \ge 1\) · Sharpness of the Ising phase transition on \(\mathbb{Z}^d\), \(d \ge 2\) · Auxiliary critical point \(\tilde\beta_c(d)\) is positive for \(d \ge 2\)

TheoremHolley inequality for increasing events#✓fully proved

The Holley inequality for increasing events (Holley 1974). If μ₁, μ₂ ≥ 0 have equal total mass and satisfy μ₁ a * μ₂ b ≤ μ₁ (a ⊓ b) * μ₂ (a ⊔ b), then μ₁(A) ≤ μ₂(A) for every increasing event A. This is Mathlib's holley applied to the indicator of A.

theorem holley_dominates [Fintype E] [DecidableEq E] {μ₁ μ₂ : ConfigSpace E → ℝ}
    (h₁ : 0 ≤ μ₁) (h₂ : 0 ≤ μ₂) (hsum : ∑ ω, μ₁ ω = ∑ ω, μ₂ ω)
    (hcond : ∀ a b, μ₁ a * μ₂ b ≤ μ₁ (a ⊓ b) * μ₂ (a ⊔ b))
    {A : Set (ConfigSpace E)} (hA : IsIncreasing A) :
    ∑ ω, A.indicator (fun _ => (1 : ℝ)) ω * μ₁ ω
      ≤ ∑ ω, A.indicator (fun _ => (1 : ℝ)) ω * μ₂ ω

Uses 3 · Used by 13

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

Proof usesIndicator of an increasing event is monotone

Used byHolley's inequality · Uniqueness of the Gibbs state · Ergodicity of the plus state · Translation invariance of the plus state · Extremality of the plus state · Monotonicity in \(p\) of free \(q = 2\) edge marginals on a finite graph · Wired law at most the \(q = 1\) law on increasing events, \(q \ge 1\) · Random-cluster comparison of boundary conditions for \(q \ge 1\) · Boundary-graph FK measure increases in \(p\) for \(q \ge 1\) · Conditional measures increase with the wiring for \(q \ge 1\) · Free–wired domination on a finite graph for \(q \ge 1\) · Monotonicity of the random-cluster measure in p · Mean-field lower bound for the spontaneous magnetization

DefinitionFinite measure with prescribed point masses#✓fully proved

The finite measure ∑_ω μ(ω) δ_ω on ConfigSpace E with point masses μ(ω) (negative masses are truncated to 0). For a normalized nonnegative μ it is the measure of the PMF PMF.ofFintype μ; see measOfMass_eq_toMeasure.

noncomputable def measOfMass (μ : ConfigSpace E → ℝ) : Measure (ConfigSpace E) :=
  ∑ ω : ConfigSpace E, (ENNReal.ofReal (μ ω)) • Measure.dirac ω

Uses 1 · Used by 12

Statement usesConfiguration space of a statistical-mechanics model

Used byHolley's coupling theorem · Holley's inequality · Normalized point masses give the probability mass function's measure · FK critical point is less than one for \(d \ge 2\), \(q \ge 1\) · Inf-based and sup-based Ising critical points agree for \(d \ge 2\) · Sup-based \(\beta_c\) equals \(-\tfrac{1}{2}\log(1 - p_c)\) for \(d \ge 2\) · Existence of the Ising phase transition · Comparison inequalities · Random-cluster measure increases stochastically in \(p\) when \(q \ge 1\) · Per-box uniqueness of the random-cluster measures off a countable set · Countable-exception \(q = 2\) uniqueness from one-sided derivative data · Free-energy data give \(q = 2\) box uniqueness off countably many \(t\)

LemmaNormalized point masses give the probability mass function's measure#✓fully proved

For a normalized nonnegative mass function, measOfMass μ is the measure of the PMF PMF.ofFintype (ENNReal.ofReal ∘ μ).

lemma measOfMass_eq_toMeasure (μ : ConfigSpace E → ℝ)
    (h : ∑ ω, ENNReal.ofReal (μ ω) = 1) :
    measOfMass μ = (PMF.ofFintype (fun ω => ENNReal.ofReal (μ ω)) h).toMeasure

Uses 2

Statement usesConfiguration space of a statistical-mechanics model · Finite measure with prescribed point masses

TheoremHolley's inequality#✓fully proved

If μ₁, μ₂ ≥ 0 on {0,1}^E have equal total mass and satisfy the Holley lattice condition μ₁(a) μ₂(b) ≤ μ₁(a ∧ b) μ₂(a ∨ b), then measOfMass μ₁ is stochastically dominated by measOfMass μ₂. Strict positivity, assumed in Holley's paper, is not needed. See R. Holley, Remarks on the FKG inequalities, Comm. Math. Phys. 36 (1974); the real-valued form is StatMech.holley_dominates, from Mathlib's holley.

theorem holley_stochasticallyDominated {μ₁ μ₂ : ConfigSpace E → ℝ}
    (h₁ : 0 ≤ μ₁) (h₂ : 0 ≤ μ₂) (hsum : ∑ ω, μ₁ ω = ∑ ω, μ₂ ω)
    (hcond : ∀ a b, μ₁ a * μ₂ b ≤ μ₁ (a ⊓ b) * μ₂ (a ⊔ b)) :
    measOfMass μ₁ ≼ measOfMass μ₂

Uses 5 · Used by 7

Statement usesConfiguration space of a statistical-mechanics model · Finite measure with prescribed point masses · Stochastic domination of measures on configurations

Proof usesIncreasing event · Holley inequality for increasing events

Used byHolley's coupling theorem · FK critical point is less than one for \(d \ge 2\), \(q \ge 1\) · Inf-based and sup-based Ising critical points agree for \(d \ge 2\) · Sup-based \(\beta_c\) equals \(-\tfrac{1}{2}\log(1 - p_c)\) for \(d \ge 2\) · Existence of the Ising phase transition · Comparison inequalities · Random-cluster measure increases stochastically in \(p\) when \(q \ge 1\)

TheoremHolley's coupling theorem#✓fully proved

If μ₁, μ₂ are strictly positive probability mass functions on {0,1}^E satisfying the Holley lattice condition μ₁(a) μ₂(b) ≤ μ₁(a ∧ b) μ₂(a ∨ b), there is a finite measure on pairs with marginals measOfMass μ₁ and measOfMass μ₂, concentrated on {(a, b) | a ≤ b}. See R. Holley, Remarks on the FKG inequalities, Comm. Math. Phys. 36 (1974), and G. Grimmett, The Random-Cluster Model (2006), Chapter 2.

theorem holley_exists_monotoneCoupling {μ₁ μ₂ : ConfigSpace E → ℝ}
    (h₁ : 0 < μ₁) (h₂ : 0 < μ₂)
    (hn₁ : ∑ ω, μ₁ ω = 1) (hn₂ : ∑ ω, μ₂ ω = 1)
    (hcond : ∀ a b, μ₁ a * μ₂ b ≤ μ₁ (a ⊓ b) * μ₂ (a ⊔ b)) :
    ∃ κ : Measure (ConfigSpace E × ConfigSpace E),
      IsFiniteMeasure κ ∧ MonotoneCoupling (measOfMass μ₁) (measOfMass μ₂) κ

Uses 5

Statement usesConfiguration space of a statistical-mechanics model · Finite measure with prescribed point masses · Monotone coupling of two measures

Proof usesHolley's inequality · Strassen's theorem

7 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.