The Aizenman–Barsky–Fernández differential inequality, finite volume

9 fully proved

A. Derivatives of the partition function

DefinitionNegative Hamiltonian of the Ising model#✓fully proved

The negative Hamiltonian ∑_{xy ∈ E} σ_xσ_y + h ∑_x σ_x.

noncomputable def negHam (h : ℝ) (s : ConfigSpace V) : ℝ :=
  (∑ e ∈ G.edgeFinset, bond s e) + h * ∑ x, spin s x

Uses 3 · Used by 2

Statement usesConfiguration space of a statistical-mechanics model · Bond variable of an unordered pair · Spin of a configuration at a site

Used byMean-field lower bound for the spontaneous magnetization · \(\beta\)-derivative of the origin magnetization in a box

B. Covariances

DefinitionTwo-point spin covariance#✓fully proved

The spin covariance Cov(σ_x, σ_y) = ⟨σ_xσ_y⟩ - ⟨σ_x⟩⟨σ_y⟩.

noncomputable def cov2 (β h : ℝ) (x y : V) : ℝ :=
  isingExpectation G β h (fun s => spin s x * spin s y)
    - isingExpectation G β h (fun s => spin s x) * isingExpectation G β h (fun s => spin s y)

Uses 3 · Used by 7

Statement usesConfiguration space of a statistical-mechanics model · Finite-volume Ising expectation · Spin of a configuration at a site

Used byGHS gap on an edge equals the third Ursell function · Griffiths–Hurst–Sherman inequality · GHS concavity of the magnetization in the field · Griffiths–Hurst–Sherman inequality · Mean-field lower bound for the spontaneous magnetization · GHS bound for a bond · Ising susceptibility at a site

DefinitionIsing one-point function#✓fully proved

The one-point function ⟨σ_x⟩.

noncomputable def onePt (β h : ℝ) (x : V) : ℝ := isingExpectation G β h (fun s => spin s x)

Uses 3 · Used by 5

Statement usesConfiguration space of a statistical-mechanics model · Finite-volume Ising expectation · Spin of a configuration at a site

Used byGHS gap on an edge equals the third Ursell function · Griffiths–Hurst–Sherman inequality · GHS concavity of the magnetization in the field · Griffiths–Hurst–Sherman inequality · GHS bound for a bond

DefinitionCovariance of a spin with a bond variable#✓fully proved

The covariance ⟨σ_o σ_x σ_y⟩ - ⟨σ_o⟩⟨σ_x σ_y⟩ of σ_o with the bond variable of e = {x, y}.

noncomputable def cov3sym (β h : ℝ) (o : V) (e : Sym2 V) : ℝ :=
  Sym2.lift ⟨fun x y =>
    isingExpectation G β h (fun s => spin s o * (spin s x * spin s y))
      - isingExpectation G β h (fun s => spin s o)
          * isingExpectation G β h (fun s => spin s x * spin s y), by
    intro a b
    have h1 : (fun s : ConfigSpace V => spin s o * (spin s a * spin s b))
        = (fun s => spin s o * (spin s b * spin s a)) := by funext s; ring
    have h2 : (fun s : ConfigSpace V => spin s a * spin s b)
        = (fun s => spin s b * spin s a) := by funext s; ring
    simp only []; rw [h1, h2]⟩ e

Uses 3 · Used by 7

Statement usesConfiguration space of a statistical-mechanics model · Finite-volume Ising expectation · Spin of a configuration at a site

Used byGHS gap on an edge equals the third Ursell function · Griffiths–Hurst–Sherman inequality · GHS concavity of the magnetization in the field · Griffiths–Hurst–Sherman inequality · Conditional finite-volume Aizenman–Barsky–Fernández inequality · Bond-energy susceptibility · GHS three-point inequality at a site for every edge

DefinitionGHS bound for a bond#✓fully proved

The GHS bound Cov(σ_o, σ_x)⟨σ_y⟩ + Cov(σ_o, σ_y)⟨σ_x⟩ for the bond e = {x, y}.

noncomputable def ghsBoundSym (β h : ℝ) (o : V) (e : Sym2 V) : ℝ :=
  Sym2.lift ⟨fun x y => cov2 G β h o x * onePt G β h y + cov2 G β h o y * onePt G β h x,
    fun a b => by ring⟩ e

Uses 2 · Used by 6

Statement usesTwo-point spin covariance · Ising one-point function

Used byGHS gap on an edge equals the third Ursell function · Griffiths–Hurst–Sherman inequality · GHS concavity of the magnetization in the field · Griffiths–Hurst–Sherman inequality · Conditional finite-volume Aizenman–Barsky–Fernández inequality · GHS three-point inequality at a site for every edge

C. Susceptibilities and the derivative of the magnetization

DefinitionBond-energy susceptibility#✓fully proved

The bond-energy susceptibility ∑_{e ∈ E} Cov(σ_o, σ_e).

noncomputable def bondEnergySusceptibility (β h : ℝ) (o : V) : ℝ :=
  ∑ e ∈ G.edgeFinset, cov3sym G β h o e

Uses 1 · Used by 1

Statement usesCovariance of a spin with a bond variable

Used byConditional finite-volume Aizenman–Barsky–Fernández inequality

DefinitionIsing susceptibility at a site#✓fully proved

The susceptibility χ(o) = ∑_x Cov(σ_o, σ_x).

noncomputable def susceptibility (β h : ℝ) (o : V) : ℝ :=
  ∑ x, cov2 G β h o x

Uses 1 · Used by 1

Statement usesTwo-point spin covariance

Used byConditional finite-volume Aizenman–Barsky–Fernández inequality

D. The GHS-type bound

DefinitionGHS three-point inequality at a site for every edge#✓fully proved

The GHS inequality at o for every edge: cov3sym ≤ ghsBoundSym, equivalently u₃(o, x, y) ≤ 0 for every edge {x, y}.

def GHSThreePointSym (β h : ℝ) (o : V) : Prop :=
  ∀ e ∈ G.edgeFinset, cov3sym G β h o e ≤ ghsBoundSym G β h o e

Uses 2 · Used by 2

Statement usesCovariance of a spin with a bond variable · GHS bound for a bond

Used byGriffiths–Hurst–Sherman inequality · Conditional finite-volume Aizenman–Barsky–Fernández inequality

LemmaConditional finite-volume Aizenman–Barsky–Fernández inequality#✓fully proved

A conditional finite-volume form of the Aizenman–Barsky–Fernández inequality: if the GHS bound holds at o and the GHS bounds sum to J ⟨σ_o⟩ χ(o), then the bond-energy susceptibility is at most J ⟨σ_o⟩ χ(o).

lemma aizenman_barsky_inequality (β h : ℝ) (o : V) (J : ℝ)
    (hghs : GHSThreePointSym G β h o)
    (hfactor : ∑ e ∈ G.edgeFinset, ghsBoundSym G β h o e
        = J * (isingExpectation G β h (fun s => spin s o)) * susceptibility G β h o) :
    bondEnergySusceptibility G β h o
      ≤ J * (isingExpectation G β h (fun s => spin s o)) * susceptibility G β h o

Uses 8

Statement usesConfiguration space of a statistical-mechanics model · GHS three-point inequality at a site for every edge · Bond-energy susceptibility · GHS bound for a bond · Finite-volume Ising expectation · Spin of a configuration at a site · Ising susceptibility at a site

Proof usesCovariance of a spin with a bond variable

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.