Griffiths–Hurst–Sherman inequality

DefinitionCurrent connecting all three site pairs#✓fully proved

The current m connects each of the pairs {x, y}, {o, y}, {o, x}.

def aie_allConn (ends : ι → Sym2 V) (m : Finset ι) (o x y : V) : Prop :=
  connK ends m x y ∧ connK ends m o y ∧ connK ends m o x
Uses 1 · Used by 2
Statement usesConnectivity in a multigraph edge set
Used byDomination condition fails on the triangle · Conditioned domination condition over a set of currents

DefinitionCurrent connecting none of the three site pairs#✓fully proved

The current m connects none of the pairs {x, y}, {o, y}, {o, x}.

def aie_noneConn (ends : ι → Sym2 V) (m : Finset ι) (o x y : V) : Prop :=
  ¬ connK ends m x y ∧ ¬ connK ends m o y ∧ ¬ connK ends m o x
Uses 1 · Used by 2
Statement usesConnectivity in a multigraph edge set
Used byDomination condition fails on the triangle · Conditioned domination condition over a set of currents

DefinitionMass of sub-currents with a given source set#✓fully proved

The total weight ∑ φ(K) of the sub-currents K ⊆ m with source set S.

noncomputable def aie_mass (ends : ι → Sym2 V) (m : Finset ι) (φ : Finset ι → ℝ) (S : Finset V) :
    ℝ :=
  ∑ K ∈ m.powerset.filter (fun K => sources ends K = S), φ K
Uses 1 · Used by 3
Statement usesSources of a multigraph edge set
Used byDomination condition fails on the triangle · GHS gap of a sourced current · Conditioned domination condition over a set of currents

DefinitionGHS gap of a sourced current#✓fully proved

The GHS gap mass(A) - mass(A ∆ {x, y}) - mass(A ∆ {o, y}) - mass(A ∆ {o, x}).

noncomputable def aie_gap (ends : ι → Sym2 V) (m : Finset ι) (φ : Finset ι → ℝ) (A : Finset V)
    (o x y : V) : ℝ :=
  aie_mass ends m φ A - aie_mass ends m φ (A ∆ {x, y})
    - aie_mass ends m φ (A ∆ {o, y}) - aie_mass ends m φ (A ∆ {o, x})
Uses 1
Statement usesMass of sub-currents with a given source set

DefinitionEdges of the triangle on three vertices#✓fully proved

The three edges {0, 1}, {1, 2}, {0, 2} of the triangle on Fin 3.

def ahd_triEnds : Fin 3 → Sym2 (Fin 3)
  | 0 => s(0, 1)
  | 1 => s(1, 2)
  | 2 => s(0, 2)
Used by 1
Used byDomination condition fails on the triangle

LemmaDomination condition fails on the triangle#✓fully proved

The domination condition fails for the single current through all edges of the triangle.

lemma ahd_hdom_refutable :
    ¬ (2 * (∑ m ∈ ({({0, 1, 2} : Finset (Fin 3))} : Finset (Finset (Fin 3))).filter
              (fun m => aie_allConn ahd_triEnds m 0 1 2),
            aie_mass ahd_triEnds m (fun _ => 1)
              (sources ahd_triEnds ({0, 1, 2} : Finset (Fin 3))))
        ≤ ∑ m ∈ ({({0, 1, 2} : Finset (Fin 3))} : Finset (Finset (Fin 3))).filter
              (fun m => aie_noneConn ahd_triEnds m 0 1 2),
            aie_mass ahd_triEnds m (fun _ => 1)
              (sources ahd_triEnds ({0, 1, 2} : Finset (Fin 3))))
Uses 7
Statement usesEdges of the triangle on three vertices · Current connecting all three site pairs · Mass of sub-currents with a given source set · Current connecting none of the three site pairs · Sources of a multigraph edge set
Proof usesAdjacency through an edge of a multigraph edge set · Connectivity in a multigraph edge set

DefinitionThree-site backbone factor#✓fully proved

The three-site backbone factor: 1, 0 or -2 according to how many of the pairs {x, y}, {o, y}, {o, x} the current connects.

noncomputable def asd_ghsBackboneFactor (ends : ι → Sym2 V) (m : Finset ι) (o x y : V) : ℝ :=
  1 - (if connK ends m x y then 1 else 0)
    - (if connK ends m o y then 1 else 0)
    - (if connK ends m o x then 1 else 0)
Uses 1
Statement usesConnectivity in a multigraph edge set

DefinitionBackbone cluster of a site in a current#✓fully proved

The cluster of o in the current m: the sites connected to o by edges of m.

noncomputable def atb_backbone (ends : ι → Sym2 V) (m : Finset ι) (o : V) : Finset V :=
  compK ends m o
Uses 1
Statement usesCluster of a vertex in a multigraph edge set

DefinitionConditioned domination condition over a set of currents#✓fully proved

The domination condition 2 · mass(all connected) ≤ mass(none connected), summed over currents in M.

def atb_conditionedDom (ends : ι → Sym2 V) (M : Finset (Finset ι)) (A : Finset V)
    (o x y : V) (Φ : Finset ι → Finset ι → ℝ) : Prop :=
  2 * (∑ m ∈ M.filter (fun m => aie_allConn ends m o x y), aie_mass ends m (Φ m) A)
    ≤ ∑ m ∈ M.filter (fun m => aie_noneConn ends m o x y), aie_mass ends m (Φ m) A
Uses 3
Statement usesCurrent connecting all three site pairs · Mass of sub-currents with a given source set · Current connecting none of the three site pairs

DefinitionThree-site duplicated-variable factor#✓fully proved

The three-site duplicated-variable factor 1 - σ_x σ_y - σ_o σ_y - σ_o σ_x of the configuration q.

noncomputable def ghsQFactor (q : ConfigSpace V) (o x y : V) : ℝ :=
  1 - spin q x * spin q y - spin q o * spin q y - spin q o * spin q x
Uses 2
Statement usesConfiguration space of a statistical-mechanics model · Spin of a configuration at a site

DefinitionThree-replica Ising expectation#✓fully proved

The expectation of F a b c over three independent copies a, b, c of the Ising Gibbs distribution.

noncomputable def isingExp3 (β h : ℝ)
    (F : ConfigSpace V → ConfigSpace V → ConfigSpace V → ℝ) : ℝ :=
  ∑ a : ConfigSpace V, ∑ b : ConfigSpace V, ∑ c : ConfigSpace V,
    isingProb G β h a * isingProb G β h b * isingProb G β h c * F a b c
Uses 2
Statement usesConfiguration space of a statistical-mechanics model · Gibbs probability of an Ising configuration

DefinitionThree-replica variable \(d_w\)#✓fully proved

The three-replica variable d_w = σ_w(b) + σ_w(c) - 2σ_w(a).

def dvar (a b c : ConfigSpace V) (w : V) : ℝ := spin b w + spin c w - 2 * spin a w
Uses 2
Statement usesConfiguration space of a statistical-mechanics model · Spin of a configuration at a site

DefinitionTwo-replica Ising expectation#✓fully proved

The expectation of F a b over two independent copies a, b of the Ising Gibbs distribution.

noncomputable def isingExp2 (β h : ℝ) (F : ConfigSpace V → ConfigSpace V → ℝ) : ℝ :=
  ∑ a : ConfigSpace V, ∑ b : ConfigSpace V,
    isingProb G β h a * isingProb G β h b * F a b
Uses 2 · Used by 2
Statement usesConfiguration space of a statistical-mechanics model · Gibbs probability of an Ising configuration
Used byGriffiths–Hurst–Sherman inequality · Griffiths–Hurst–Sherman inequality

DefinitionRotated two-replica difference variable \(u_w\)#✓fully proved

The rotated two-replica variable u_w = (σ_w(a) - σ_w(b)) / 2.

noncomputable def uvar (a b : ConfigSpace V) (w : V) : ℝ := (spin a w - spin b w) / 2
Uses 2 · Used by 6
Statement usesConfiguration space of a statistical-mechanics model · Spin of a configuration at a site
Used byGriffiths–Hurst–Sherman inequality · Conditional expectation of \(u_o u_x\) given the agreement · Griffiths–Hurst–Sherman inequality · Inhomogeneous conditional expectation of \(u_o u_x\) · Griffiths–Hurst–Sherman inequality · Fibre factorization property for \(u_o u_x\) and \(t_y\)

DefinitionRotated two-replica sum variable \(t_w\)#✓fully proved

The rotated two-replica variable t_w = (σ_w(a) + σ_w(b)) / 2.

noncomputable def tvar (a b : ConfigSpace V) (w : V) : ℝ := (spin a w + spin b w) / 2
Uses 2 · Used by 6
Statement usesConfiguration space of a statistical-mechanics model · Spin of a configuration at a site
Used byGriffiths–Hurst–Sherman inequality · Conditional expectation of \(t_y\) given the agreement · Griffiths–Hurst–Sherman inequality · Inhomogeneous conditional expectation of \(t_y\) · Griffiths–Hurst–Sherman inequality · Fibre factorization property for \(u_o u_x\) and \(t_y\)

DefinitionEdges of the induced subgraph on a vertex set#✓fully proved

The edges of E with both endpoints in S (the edges of the induced subgraph on S).

def ghsvp_vertexEdges (E : Finset (Sym2 W)) (S : Finset W) : Finset (Sym2 W) :=
  E.filter (Sharpness.edgeInside S)
Uses 1 · Used by 16
Statement usesUnordered pair inside a set
Used byGriffiths–Hurst–Sherman inequality · FKG lattice condition for the agreement law when \(\beta, h \ge 0\) · Agreement-set Boltzmann weight with doubled couplings and field · Zero-field disagreement-set Boltzmann weight · Griffiths–Hurst–Sherman inequality · Inhomogeneous agreement-set Boltzmann weight · Inhomogeneous induced-subgraph partition function with field · Griffiths–Hurst–Sherman inequality · Inhomogeneous zero-field disagreement-set weight · Inhomogeneous zero-field induced-subgraph partition function · Induced-subgraph partition function over the active sites only · Induced-subgraph partition function with doubled coupling and field · Zero-field induced-subgraph partition function with doubled coupling · Zero-field correlation in an induced subgraph · Correlation with field in an induced subgraph · Zero-field partition function of an induced subgraph

DefinitionZero-field partition function of an induced subgraph#✓fully proved

The zero-field partition function of the induced subgraph on S, with couplings J.

noncomputable def ghsvp_vertexZ (E : Finset (Sym2 W)) (J : Sym2 W -> Real)
    (S : Finset W) : Real :=
  ZJ (ghsvp_vertexEdges E S) J (fun _ => 0)
Uses 2 · Used by 6
Statement usesEdges of the induced subgraph on a vertex set · Partition function with inhomogeneous couplings and site fields
Used byGriffiths–Hurst–Sherman inequality · FKG lattice condition for the agreement law when \(\beta, h \ge 0\) · Griffiths–Hurst–Sherman inequality · Inhomogeneous weight of an agreement set · Griffiths–Hurst–Sherman inequality · Weight of an agreement set in the duplicated system

DefinitionZero-field correlation in an induced subgraph#✓fully proved

The zero-field correlation ⟨σ_P⟩ in the induced subgraph on S.

noncomputable def ghsvp_vertexCorr (E : Finset (Sym2 W)) (J : Sym2 W -> Real)
    (S P : Finset W) : Real :=
  expJ (ghsvp_vertexEdges E S) J (fun _ => 0) (spinProd P)
Uses 3 · Used by 5
Statement usesEdges of the induced subgraph on a vertex set · Spin product over a vertex set · Gibbs expectation with inhomogeneous couplings and site fields
Used byGriffiths–Hurst–Sherman inequality · Griffiths–Hurst–Sherman inequality · Inhomogeneous two-point correlation on the disagreement set · Griffiths–Hurst–Sherman inequality · Two-point correlation on the disagreement subgraph

DefinitionCorrelation with field in an induced subgraph#✓fully proved

The correlation ⟨σ_P⟩ in the induced subgraph on S, with field hf.

noncomputable def ghsvp_vertexCorrField (E : Finset (Sym2 W)) (J : Sym2 W -> Real)
    (hf : W -> Real) (S P : Finset W) : Real :=
  expJ (ghsvp_vertexEdges E S) J hf (spinProd P)
Uses 3 · Used by 5
Statement usesEdges of the induced subgraph on a vertex set · Spin product over a vertex set · Gibbs expectation with inhomogeneous couplings and site fields
Used byGriffiths–Hurst–Sherman inequality · Griffiths–Hurst–Sherman inequality · Inhomogeneous magnetization on the agreement set · Griffiths–Hurst–Sherman inequality · Magnetization on the agreement subgraph

DefinitionConfiguration merged from two configurations along a set#✓fully proved

The configuration equal to a on S and to b off S.

def ghsvp_mergeConfig (S : Finset W) (a : (↑S -> Bool))
    (b : ({v : W // v ∉ S}) -> Bool) : ConfigSpace W :=
  fun v => if hv : v ∈ S then a ⟨v, hv⟩ else b ⟨v, hv⟩
Uses 1 · Used by 2
Statement usesConfiguration space of a statistical-mechanics model
Used byInduced-subgraph partition function over the active sites only · Splitting a configuration into a set and its complement

DefinitionSplitting a configuration into a set and its complement#✓fully proved

Configurations split into their restrictions to S and to its complement.

def ghsvp_splitConfig (S : Finset W) :
    ConfigSpace W ≃ ((↑S -> Bool) × (({v : W // v ∉ S}) -> Bool)) where
  toFun s := (fun v => s v, fun v => s v)
  invFun p := ghsvp_mergeConfig S p.1 p.2
  left_inv s := by
    funext v
    simp only [ghsvp_mergeConfig]
    split <;> rfl
  right_inv p := by
    apply Prod.ext
    · funext v
      simp [ghsvp_mergeConfig, v.property]
    · funext v
      simp [ghsvp_mergeConfig, v.property]
Uses 2
Statement usesConfiguration space of a statistical-mechanics model · Configuration merged from two configurations along a set

DefinitionInduced-subgraph partition function over the active sites only#✓fully proved

The partition function of the induced subgraph on S, summed over configurations on S only.

noncomputable def ghsvp_activeZ (E : Finset (Sym2 W)) (J : Sym2 W -> Real)
    (S : Finset W) : Real :=
  ∑ a : ↑S -> Bool,
    wJ (ghsvp_vertexEdges E S) J (fun _ => 0)
      (ghsvp_mergeConfig S a (fun _ => false))
Uses 3
Statement usesConfiguration merged from two configurations along a set · Edges of the induced subgraph on a vertex set · Boltzmann weight with inhomogeneous couplings and site fields

DefinitionImage of a vertex set among non-ghost vertices#✓fully proved

The image of A among the non-ghost vertices some x of Option V.

def ghsvp_someSet (A : Finset V) : Finset (Option V) := A.map someEmb
Uses 1 · Used by 7
Statement usesEmbedding of vertices into the ghost graph
Used byGriffiths–Hurst–Sherman inequality · FKG lattice condition for the agreement law when \(\beta, h \ge 0\) · Griffiths–Hurst–Sherman inequality · Inhomogeneous weight of an agreement set · Griffiths–Hurst–Sherman inequality · Image of a vertex set together with the ghost vertex · Weight of an agreement set in the duplicated system

DefinitionImage of a vertex set together with the ghost vertex#✓fully proved

The image of A together with the ghost vertex none.

def ghsvp_fieldSet (A : Finset V) : Finset (Option V) := insert none (ghsvp_someSet A)
Uses 1 · Used by 6
Statement usesImage of a vertex set among non-ghost vertices
Used byGriffiths–Hurst–Sherman inequality · FKG lattice condition for the agreement law when \(\beta, h \ge 0\) · Griffiths–Hurst–Sherman inequality · Inhomogeneous weight of an agreement set · Griffiths–Hurst–Sherman inequality · Weight of an agreement set in the duplicated system

DefinitionWeight of an agreement set in the duplicated system#✓fully proved

The weight of the agreement set A in the duplicated system: the product of the ghost-vertex partition functions of A ∪ {ghost} and of Aᶜ, with doubled couplings 2β and field 2βh.

noncomputable def ghsvp_subsetMass (G : SimpleGraph V) [DecidableRel G.Adj]
    (β h : Real) (A : Finset V) : Real :=
  let J2 := ghostCoupling (2 * β * h) 1 (fun _ => 2 * β)
  ghsvp_vertexZ (withGhost G).edgeFinset J2 (ghsvp_fieldSet A) *
    ghsvp_vertexZ (withGhost G).edgeFinset J2 (ghsvp_someSet Aᶜ)
Uses 5 · Used by 3
Statement usesImage of a vertex set together with the ghost vertex · Image of a vertex set among non-ghost vertices · Zero-field partition function of an induced subgraph · Coupling on the ghost graph with uniform field · Graph with a ghost vertex joined to every site
Used byGriffiths–Hurst–Sherman inequality · FKG lattice condition for the agreement law when \(\beta, h \ge 0\) · Griffiths–Hurst–Sherman inequality

DefinitionInduced-subgraph partition function with doubled coupling and field#✓fully proved

The partition function on the induced subgraph on A with couplings 2β and field 2βh.

noncomputable def ghsvp_tZ (G : SimpleGraph V) [DecidableRel G.Adj]
    (β h : Real) (A : Finset V) : Real :=
  ZJ (ghsvp_vertexEdges G.edgeFinset A) (fun _ => 2 * β)
    (fun x => if x ∈ A then 2 * β * h else 0)
Uses 2 · Used by 3
Statement usesEdges of the induced subgraph on a vertex set · Partition function with inhomogeneous couplings and site fields
Used byGriffiths–Hurst–Sherman inequality · FKG lattice condition for the agreement law when \(\beta, h \ge 0\) · Griffiths–Hurst–Sherman inequality

DefinitionZero-field induced-subgraph partition function with doubled coupling#✓fully proved

The zero-field partition function on the induced subgraph on A with couplings 2β.

noncomputable def ghsvp_uZ (G : SimpleGraph V) [DecidableRel G.Adj]
    (β : Real) (A : Finset V) : Real :=
  ZJ (ghsvp_vertexEdges G.edgeFinset A) (fun _ => 2 * β) (fun _ => 0)
Uses 2 · Used by 3
Statement usesEdges of the induced subgraph on a vertex set · Partition function with inhomogeneous couplings and site fields
Used byGriffiths–Hurst–Sherman inequality · FKG lattice condition for the agreement law when \(\beta, h \ge 0\) · Griffiths–Hurst–Sherman inequality

DefinitionTwo-point correlation on the disagreement subgraph#✓fully proved

The zero-field correlation ⟨σ_o σ_x⟩ in the subgraph induced by Aᶜ (couplings 2β), or 0 if o or x lies in A.

noncomputable def ghsvp_disagreementCorr (G : SimpleGraph V) [DecidableRel G.Adj]
    (β : Real) (o x : V) (A : Finset V) : Real :=
  if o ∈ A ∨ x ∈ A then 0
  else ghsvp_vertexCorr G.edgeFinset (fun _ => 2 * β) Aᶜ {o, x}
Uses 1 · Used by 2
Statement usesZero-field correlation in an induced subgraph
Used byGriffiths–Hurst–Sherman inequality · Griffiths–Hurst–Sherman inequality

DefinitionMagnetization on the agreement subgraph#✓fully proved

The magnetization ⟨σ_y⟩ in the subgraph induced by A (couplings 2β, field 2βh), or 0 if y ∉ A.

noncomputable def ghsvp_agreementMag (G : SimpleGraph V) [DecidableRel G.Adj]
    (β h : Real) (y : V) (A : Finset V) : Real :=
  if y ∈ A then
    ghsvp_vertexCorrField G.edgeFinset (fun _ => 2 * β) (fun _ => 2 * β * h) A {y}
  else 0
Uses 1 · Used by 2
Statement usesCorrelation with field in an induced subgraph
Used byGriffiths–Hurst–Sherman inequality · Griffiths–Hurst–Sherman inequality

DefinitionInhomogeneous ghost-vertex couplings#✓fully proved

The ghost-vertex couplings: 2K_{xy} on an edge {x, y}, 2h_x between x and the ghost.

noncomputable def ghsiGhostCoupling (K : Sym2 V → ℝ) (hf : V → ℝ)
    (e : Sym2 (Option V)) : ℝ :=
  Sym2.lift ⟨fun a b =>
    match a, b with
    | some x, some y => 2 * K s(x, y)
    | some x, none => 2 * hf x
    | none, some y => 2 * hf y
    | none, none => 0,
    by rintro (_ | x) (_ | y) <;> simp only [] <;> rw [Sym2.eq_swap]⟩ e
Used by 2
Used byInhomogeneous weight of an agreement set · Griffiths–Hurst–Sherman inequality

DefinitionInhomogeneous induced-subgraph partition function with field#✓fully proved

The partition function of the subgraph induced by A with couplings 2K and fields 2h on A.

noncomputable def ghsiTZ (G : SimpleGraph V) [DecidableRel G.Adj]
    (K : Sym2 V → ℝ) (hf : V → ℝ) (A : Finset V) : ℝ :=
  ZJ (ghsvp_vertexEdges G.edgeFinset A) (fun e => 2 * K e)
    (fun x => if x ∈ A then 2 * hf x else 0)
Uses 2 · Used by 1
Statement usesEdges of the induced subgraph on a vertex set · Partition function with inhomogeneous couplings and site fields
Used byGriffiths–Hurst–Sherman inequality

DefinitionInhomogeneous zero-field induced-subgraph partition function#✓fully proved

The zero-field partition function of the subgraph induced by A with couplings 2K.

noncomputable def ghsiUZ (G : SimpleGraph V) [DecidableRel G.Adj]
    (K : Sym2 V → ℝ) (A : Finset V) : ℝ :=
  ZJ (ghsvp_vertexEdges G.edgeFinset A) (fun e => 2 * K e) (fun _ => 0)
Uses 2 · Used by 1
Statement usesEdges of the induced subgraph on a vertex set · Partition function with inhomogeneous couplings and site fields
Used byGriffiths–Hurst–Sherman inequality

DefinitionInhomogeneous weight of an agreement set#✓fully proved

The weight of the agreement set A in the duplicated inhomogeneous system.

noncomputable def ghsiSubsetMass (G : SimpleGraph V) [DecidableRel G.Adj]
    (K : Sym2 V → ℝ) (hf : V → ℝ) (A : Finset V) : ℝ :=
  ghsvp_vertexZ (withGhost G).edgeFinset (ghsiGhostCoupling K hf)
      (ghsvp_fieldSet A) *
    ghsvp_vertexZ (withGhost G).edgeFinset (ghsiGhostCoupling K hf)
      (ghsvp_someSet Aᶜ)
Uses 5 · Used by 1
Statement usesInhomogeneous ghost-vertex couplings · Image of a vertex set together with the ghost vertex · Image of a vertex set among non-ghost vertices · Zero-field partition function of an induced subgraph · Graph with a ghost vertex joined to every site
Used byGriffiths–Hurst–Sherman inequality

DefinitionTotal spin of a configuration#✓fully proved

The total spin ∑_x σ_x of a configuration.

noncomputable def totalSpin (s : ConfigSpace V) : ℝ := ∑ x, spin s x
Uses 2 · Used by 8
Statement usesConfiguration space of a statistical-mechanics model · Spin of a configuration at a site
Used byField derivative of the magnetization as a sum of covariances · Field derivative of the two-point covariance · GHS concavity of the magnetization in the field · Susceptibility bound \(\chi(h) \le m(h)/h \le 1/h\) from concavity · Susceptibility bound \(\chi(h) \le m(h)/h\) from concavity · Random-current form of the \(\beta\)-derivative of the magnetization · Finite-volume mean-field inequality for the Ising model · Mean-field lower bound for the spontaneous magnetization

LemmaGriffiths' second inequality for two distinct spins#✓fully proved

Griffiths' second inequality for two distinct spins: ⟨σ_x⟩⟨σ_y⟩ ≤ ⟨σ_x σ_y⟩ for β, h ≥ 0.

lemma cov_nonneg (β h : ℝ) (hβ : 0 ≤ β) (hh : 0 ≤ h) (x y : V) (hxy : x ≠ y) :
    isingExpectation G β h (fun s => spin s x) * isingExpectation G β h (fun s => spin s y)
      ≤ isingExpectation G β h (fun s => spin s x * spin s y)
Uses 5 · Used by 4
Statement usesConfiguration space of a statistical-mechanics model · Finite-volume Ising expectation · Spin of a configuration at a site
Proof usesSecond Griffiths inequality (GKS II) · Spin product over a vertex set
Used byGriffiths–Hurst–Sherman inequality · GHS concavity of the magnetization in the field · Finite-volume mean-field inequality for the Ising model · Mean-field lower bound for the spontaneous magnetization

LemmaField derivative of the magnetization as a sum of covariances#✓fully proved

The field derivative of the magnetization is β times the sum of the two-point covariances ⟨σ_o σ_x⟩ - ⟨σ_o⟩⟨σ_x⟩ (the finite-volume susceptibility).

lemma deriv_magnetization_eq_sum_cov (β h : ℝ) (o : V) :
    deriv (fun h => isingExpectation G β h (fun s => spin s o)) h
      = β * ∑ x, (isingExpectation G β h (fun s => spin s o * spin s x)
            - isingExpectation G β h (fun s => spin s o) * isingExpectation G β h (fun s => spin s
                x))
Uses 10 · Used by 4
Statement usesConfiguration space of a statistical-mechanics model · Finite-volume Ising expectation · Spin of a configuration at a site
Proof usesBond variable of an unordered pair · Ising Hamiltonian on a finite graph · Gibbs probability of an Ising configuration · Boltzmann weight of an Ising configuration · Ising partition function · Positivity of the Ising partition function · Total spin of a configuration
Used byGHS concavity of the magnetization in the field · GHS susceptibility bound \(\chi \le 1/h\) · Finite-volume mean-field inequality for the Ising model · Mean-field lower bound for the spontaneous magnetization

DefinitionGlobal spin flip#✓fully proved

The global spin flip σ ↦ -σ.

def flipCfg (s : ConfigSpace V) : ConfigSpace V := fun x => ! s x
Uses 1 · Used by 2
Statement usesConfiguration space of a statistical-mechanics model
Used byGlobal spin flip as an involutive equivalence · Magnetization vanishes at zero field

DefinitionGlobal spin flip as an involutive equivalence#✓fully proved

The global spin flip as an involutive equivalence of configuration space.

def flipEquiv : ConfigSpace V ≃ ConfigSpace V where
  toFun := flipCfg
  invFun := flipCfg
  left_inv := by intro s; funext x; unfold flipCfg; cases s x <;> rfl
  right_inv := by intro s; funext x; unfold flipCfg; cases s x <;> rfl
Uses 2 · Used by 1
Statement usesConfiguration space of a statistical-mechanics model · Global spin flip
Used byMagnetization vanishes at zero field

LemmaMagnetization vanishes at zero field#✓fully proved

At zero field the global spin-flip symmetry forces the magnetization ⟨σ_o⟩_{β,0} to vanish.

lemma magnetization_zero_field (β : ℝ) (o : V) :
    isingExpectation G β 0 (fun s => spin s o) = 0
Uses 10 · Used by 4
Statement usesConfiguration space of a statistical-mechanics model · Finite-volume Ising expectation · Spin of a configuration at a site
Proof usesBond variable of an unordered pair · Ising Hamiltonian on a finite graph · Gibbs probability of an Ising configuration · Boltzmann weight of an Ising configuration · Ising partition function · Global spin flip · Global spin flip as an involutive equivalence
Used bySusceptibility bound \(\chi(h) \le m(h)/h \le 1/h\) from concavity · Susceptibility bound \(\chi(h) \le m(h)/h\) from concavity · Finite-volume mean-field inequality for the Ising model · Mean-field lower bound for the spontaneous magnetization

TheoremSusceptibility bound \(\chi(h) \le m(h)/h \le 1/h\) from concavity#✓fully proved

If the magnetization is concave in the field on [0, ∞) (the GHS inequality), then for h > 0 the susceptibility satisfies χ(h) ≤ m(h)/h ≤ 1/h. Reference: R. B. Griffiths, C. A. Hurst, S. Sherman, "Concavity of magnetization of an Ising ferromagnet in a positive external field", J. Math. Phys. 11 (1970) 790–795.

theorem ghs_susceptibility_bound (β h : ℝ) (hh : 0 < h) (o : V)
    (hconc : ConcaveOn ℝ (Ici 0) (fun h => isingExpectation G β h (fun s => spin s o))) :
    deriv (fun h => isingExpectation G β h (fun s => spin s o)) h
        ≤ isingExpectation G β h (fun s => spin s o) / h
      ∧ deriv (fun h => isingExpectation G β h (fun s => spin s o)) h ≤ 1 / h
Uses 12 · Used by 1
Statement usesConfiguration space of a statistical-mechanics model · Finite-volume Ising expectation · Spin of a configuration at a site
Proof usesBond variable of an unordered pair · Ising Hamiltonian on a finite graph · Gibbs probability of an Ising configuration · Ising Gibbs probabilities sum to one · Boltzmann weight of an Ising configuration · Ising partition function · Positivity of the Ising partition function · Magnetization vanishes at zero field · Total spin of a configuration
Used byGHS susceptibility bound \(\chi \le 1/h\)

DefinitionAgreement configuration of two spin configurations#✓fully proved

The agreement configuration of a and b: true exactly at the sites where they agree.

def ghsLAgreement (a b : ConfigSpace V) : ConfigSpace V := fun v => decide (a v = b v)
Uses 1 · Used by 4
Statement usesConfiguration space of a statistical-mechanics model
Used byGriffiths–Hurst–Sherman inequality · Change of variables from replica pairs to agreement and first copy · Griffiths–Hurst–Sherman inequality · Griffiths–Hurst–Sherman inequality

DefinitionMate of a configuration over an agreement pattern#✓fully proved

The configuration that agrees with a where q is true and disagrees where q is false.

def ghsLMate (q a : ConfigSpace V) : ConfigSpace V := fun v => if q v then a v else !a v
Uses 1 · Used by 9
Statement usesConfiguration space of a statistical-mechanics model
Used byGriffiths–Hurst–Sherman inequality · FKG lattice condition for the agreement law when \(\beta, h \ge 0\) · Fibre weight integrated against an observable · Two-replica weight in an agreement fibre · Change of variables from replica pairs to agreement and first copy · Griffiths–Hurst–Sherman inequality · Inhomogeneous fibre weight integrated against an observable · Inhomogeneous two-replica weight in an agreement fibre · Griffiths–Hurst–Sherman inequality

DefinitionSet of sites where an agreement configuration is true#✓fully proved

The set of sites where q is true.

def ghsLAgreeFinset (q : ConfigSpace V) : Finset V :=
  Finset.univ.filter (fun v => q v = true)
Uses 1 · Used by 10
Statement usesConfiguration space of a statistical-mechanics model
Used byGriffiths–Hurst–Sherman inequality · FKG lattice condition for the agreement law when \(\beta, h \ge 0\) · Field weight of the disagreement set · Agreement-set Boltzmann weight with doubled couplings and field · Zero-field disagreement-set Boltzmann weight · Griffiths–Hurst–Sherman inequality · Inhomogeneous field weight of the disagreement set · Inhomogeneous agreement-set Boltzmann weight · Griffiths–Hurst–Sherman inequality · Inhomogeneous zero-field disagreement-set weight

DefinitionAgreement-set Boltzmann weight with doubled couplings and field#✓fully proved

The Boltzmann weight, with couplings 2β and field 2βh, of a on the subgraph induced by the agreement set of q.

noncomputable def ghsLTWeight (β h : ℝ) (q a : ConfigSpace V) : ℝ :=
  Real.exp (2 * β *
    ((∑ e ∈ ghsvp_vertexEdges G.edgeFinset (ghsLAgreeFinset q), bond a e)
      + h * ∑ v ∈ ghsLAgreeFinset q, spin a v))
Uses 5 · Used by 4
Statement usesConfiguration space of a statistical-mechanics model · Bond variable of an unordered pair · Set of sites where an agreement configuration is true · Edges of the induced subgraph on a vertex set · Spin of a configuration at a site
Used byGriffiths–Hurst–Sherman inequality · FKG lattice condition for the agreement law when \(\beta, h \ge 0\) · Expectation with field on the agreement set · Griffiths–Hurst–Sherman inequality

DefinitionZero-field disagreement-set Boltzmann weight#✓fully proved

The zero-field Boltzmann weight, with couplings 2β, of a on the subgraph induced by the disagreement set of q.

noncomputable def ghsLUWeight (β : ℝ) (q a : ConfigSpace V) : ℝ :=
  Real.exp (2 * β *
    ∑ e ∈ ghsvp_vertexEdges G.edgeFinset (ghsLAgreeFinset q)ᶜ, bond a e)
Uses 4 · Used by 4
Statement usesConfiguration space of a statistical-mechanics model · Bond variable of an unordered pair · Set of sites where an agreement configuration is true · Edges of the induced subgraph on a vertex set
Used byGriffiths–Hurst–Sherman inequality · FKG lattice condition for the agreement law when \(\beta, h \ge 0\) · Zero-field expectation on the disagreement set · Griffiths–Hurst–Sherman inequality

DefinitionSplitting a configuration along the agreement set#✓fully proved

Configurations split into their restrictions to the agreement and disagreement sets of q.

def ghsLSplitEquiv (q : ConfigSpace V) :
    ConfigSpace V ≃
      ((v : {v : V // q v = true}) → Bool) ×
        ((v : {v : V // ¬ q v = true}) → Bool) :=
  Equiv.piEquivPiSubtypeProd (fun v => q v = true) (fun _ => Bool)
Uses 1 · Used by 6
Statement usesConfiguration space of a statistical-mechanics model
Used byGriffiths–Hurst–Sherman inequality · FKG lattice condition for the agreement law when \(\beta, h \ge 0\) · Completion of agreement-set spins to a full configuration · Completion of disagreement-set spins to a full configuration · Griffiths–Hurst–Sherman inequality · Griffiths–Hurst–Sherman inequality

DefinitionCompletion of agreement-set spins to a full configuration#✓fully proved

The configuration with given spins on the agreement set of q and false elsewhere.

def ghsLTComplete (q : ConfigSpace V)
    (st : (v : {v : V // q v = true}) → Bool) : ConfigSpace V :=
  (ghsLSplitEquiv q).symm (st, fun _ => false)
Uses 2 · Used by 4
Statement usesConfiguration space of a statistical-mechanics model · Splitting a configuration along the agreement set
Used byGriffiths–Hurst–Sherman inequality · FKG lattice condition for the agreement law when \(\beta, h \ge 0\) · Griffiths–Hurst–Sherman inequality · Griffiths–Hurst–Sherman inequality

DefinitionCompletion of disagreement-set spins to a full configuration#✓fully proved

The configuration with given spins on the disagreement set of q and false elsewhere.

def ghsLUComplete (q : ConfigSpace V)
    (su : (v : {v : V // ¬ q v = true}) → Bool) : ConfigSpace V :=
  (ghsLSplitEquiv q).symm (fun _ => false, su)
Uses 2 · Used by 4
Statement usesConfiguration space of a statistical-mechanics model · Splitting a configuration along the agreement set
Used byGriffiths–Hurst–Sherman inequality · FKG lattice condition for the agreement law when \(\beta, h \ge 0\) · Griffiths–Hurst–Sherman inequality · Griffiths–Hurst–Sherman inequality

DefinitionChange of variables from replica pairs to agreement and first copy#✓fully proved

The change of variables (a, b) ↦ (agreement of a and b, a) on pairs of configurations.

def ghsLXnorEquiv :
    (ConfigSpace V × ConfigSpace V) ≃ (ConfigSpace V × ConfigSpace V) where
  toFun p := (ghsLAgreement p.1 p.2, p.1)
  invFun p := (p.2, ghsLMate p.1 p.2)
  left_inv p := by ext <;> simp
  right_inv p := by ext <;> simp
Uses 3 · Used by 3
Statement usesConfiguration space of a statistical-mechanics model · Agreement configuration of two spin configurations · Mate of a configuration over an agreement pattern
Used byGriffiths–Hurst–Sherman inequality · Griffiths–Hurst–Sherman inequality · Griffiths–Hurst–Sherman inequality

DefinitionTwo-replica weight in an agreement fibre#✓fully proved

The two-replica weight of a and its mate in the fibre over the agreement configuration q.

noncomputable def ghsLFibreWeight (β h : ℝ) (q a : ConfigSpace V) : ℝ :=
  isingWeight G β h a * isingWeight G β h (ghsLMate q a)
Uses 3 · Used by 5
Statement usesConfiguration space of a statistical-mechanics model · Mate of a configuration over an agreement pattern · Boltzmann weight of an Ising configuration
Used byGriffiths–Hurst–Sherman inequality · FKG lattice condition for the agreement law when \(\beta, h \ge 0\) · Total two-replica weight of an agreement fibre · Fibre weight integrated against an observable · Griffiths–Hurst–Sherman inequality

DefinitionTotal two-replica weight of an agreement fibre#✓fully proved

The total two-replica weight of the fibre over q.

noncomputable def ghsLFibreMass (β h : ℝ) (q : ConfigSpace V) : ℝ :=
  ∑ a : ConfigSpace V, ghsLFibreWeight G β h q a
Uses 2 · Used by 5
Statement usesConfiguration space of a statistical-mechanics model · Two-replica weight in an agreement fibre
Used byGriffiths–Hurst–Sherman inequality · Law of the agreement configuration of two replicas · FKG lattice condition for the agreement law when \(\beta, h \ge 0\) · Conditional two-replica expectation given the agreement · Griffiths–Hurst–Sherman inequality

DefinitionFibre weight integrated against an observable#✓fully proved

The two-replica weight of the fibre over q, integrated against F.

noncomputable def ghsLFibreNumerator (β h : ℝ)
    (F : ConfigSpace V → ConfigSpace V → ℝ) (q : ConfigSpace V) : ℝ :=
  ∑ a : ConfigSpace V,
    ghsLFibreWeight G β h q a * F a (ghsLMate q a)
Uses 3 · Used by 3
Statement usesConfiguration space of a statistical-mechanics model · Two-replica weight in an agreement fibre · Mate of a configuration over an agreement pattern
Used byGriffiths–Hurst–Sherman inequality · Conditional two-replica expectation given the agreement · Griffiths–Hurst–Sherman inequality

DefinitionConditional two-replica expectation given the agreement#✓fully proved

The conditional two-replica expectation of F given the agreement configuration q.

noncomputable def ghsLFibreExpectation (β h : ℝ)
    (F : ConfigSpace V → ConfigSpace V → ℝ) (q : ConfigSpace V) : ℝ :=
  ghsLFibreNumerator G β h F q / ghsLFibreMass G β h q
Uses 3 · Used by 5
Statement usesConfiguration space of a statistical-mechanics model · Total two-replica weight of an agreement fibre · Fibre weight integrated against an observable
Used byGriffiths–Hurst–Sherman inequality · Conditional expectation of \(t_y\) given the agreement · Conditional expectation of \(u_o u_x\) given the agreement · Griffiths–Hurst–Sherman inequality · Fibre factorization property for \(u_o u_x\) and \(t_y\)

DefinitionLaw of the agreement configuration of two replicas#✓fully proved

The probability that two independent replicas have agreement configuration q.

noncomputable def ghsLAgreementProb (β h : ℝ) (q : ConfigSpace V) : ℝ :=
  ghsLFibreMass G β h q / (isingZ G β h) ^ 2
Uses 3 · Used by 3
Statement usesConfiguration space of a statistical-mechanics model · Total two-replica weight of an agreement fibre · Ising partition function
Used byGriffiths–Hurst–Sherman inequality · FKG lattice condition for the agreement law when \(\beta, h \ge 0\) · Griffiths–Hurst–Sherman inequality

DefinitionConditional expectation of \(u_o u_x\) given the agreement#✓fully proved

The conditional expectation E[u_o u_x | q] of the rotated variables.

noncomputable def ghsLFibreUU (β h : ℝ) (o x : V) (q : ConfigSpace V) : ℝ :=
  ghsLFibreExpectation G β h (fun a b => uvar a b o * uvar a b x) q
Uses 3 · Used by 3
Statement usesConfiguration space of a statistical-mechanics model · Conditional two-replica expectation given the agreement · Rotated two-replica difference variable \(u_w\)
Used byGriffiths–Hurst–Sherman inequality · Griffiths–Hurst–Sherman inequality · Fibre factorization property for \(u_o u_x\) and \(t_y\)

DefinitionConditional expectation of \(t_y\) given the agreement#✓fully proved

The conditional expectation E[t_y | q] of the rotated variable.

noncomputable def ghsLFibreT (β h : ℝ) (y : V) (q : ConfigSpace V) : ℝ :=
  ghsLFibreExpectation G β h (fun a b => tvar a b y) q
Uses 3 · Used by 3
Statement usesConfiguration space of a statistical-mechanics model · Conditional two-replica expectation given the agreement · Rotated two-replica sum variable \(t_w\)
Used byGriffiths–Hurst–Sherman inequality · Griffiths–Hurst–Sherman inequality · Fibre factorization property for \(u_o u_x\) and \(t_y\)

DefinitionZero-field expectation on the disagreement set#✓fully proved

The zero-field expectation on the subgraph induced by the disagreement set of q.

noncomputable def ghsLUExpectation (β : ℝ) (q : ConfigSpace V)
    (F : ConfigSpace V → ℝ) : ℝ :=
  (∑ a : ConfigSpace V, ghsLUWeight G β q a * F a) /
    ∑ a : ConfigSpace V, ghsLUWeight G β q a
Uses 2 · Used by 2
Statement usesConfiguration space of a statistical-mechanics model · Zero-field disagreement-set Boltzmann weight
Used byGriffiths–Hurst–Sherman inequality · Griffiths–Hurst–Sherman inequality

DefinitionExpectation with field on the agreement set#✓fully proved

The expectation with field on the subgraph induced by the agreement set of q.

noncomputable def ghsLTExpectation (β h : ℝ) (q : ConfigSpace V)
    (F : ConfigSpace V → ℝ) : ℝ :=
  (∑ a : ConfigSpace V, ghsLTWeight G β h q a * F a) /
    ∑ a : ConfigSpace V, ghsLTWeight G β h q a
Uses 2 · Used by 2
Statement usesConfiguration space of a statistical-mechanics model · Agreement-set Boltzmann weight with doubled couplings and field
Used byGriffiths–Hurst–Sherman inequality · Griffiths–Hurst–Sherman inequality

DefinitionField weight of the disagreement set#✓fully proved

The field weight exp (2βh ∑_{v ∉ q} σ_v(a)) of the disagreement set.

noncomputable def ghsLOutFieldWeight (β h : ℝ) (q a : ConfigSpace V) : ℝ :=
  Real.exp (2 * β * h * ∑ v ∈ (ghsLAgreeFinset q)ᶜ, spin a v)
Uses 3 · Used by 2
Statement usesConfiguration space of a statistical-mechanics model · Set of sites where an agreement configuration is true · Spin of a configuration at a site
Used byGriffiths–Hurst–Sherman inequality · Griffiths–Hurst–Sherman inequality

DefinitionFibre factorization property for \(u_o u_x\) and \(t_y\)#✓fully proved

Conditioned on the agreement configuration, u_o u_x and t_y are uncorrelated.

def GHSLebowitzFibreFactorization (β h : ℝ) (o x y : V) : Prop :=
  ∀ q : ConfigSpace V,
    ghsLFibreExpectation G β h
        (fun a b => uvar a b o * uvar a b x * tvar a b y) q
      = ghsLFibreUU G β h o x q * ghsLFibreT G β h y q
Uses 6 · Used by 2
Statement usesConfiguration space of a statistical-mechanics model · Conditional two-replica expectation given the agreement · Conditional expectation of \(t_y\) given the agreement · Conditional expectation of \(u_o u_x\) given the agreement · Rotated two-replica sum variable \(t_w\) · Rotated two-replica difference variable \(u_w\)
Used byGriffiths–Hurst–Sherman inequality · Griffiths–Hurst–Sherman inequality

LemmaFKG lattice condition for the agreement law when \(\beta, h \ge 0\)#✓fully proved

The law of the agreement configuration satisfies the FKG lattice condition.

lemma ghsLAgreementProb_fkg (β h : ℝ) (hβ : 0 ≤ β) (hh : 0 ≤ h) :
    FKGLatticeCondition (ghsLAgreementProb G β h)
Uses 40
Statement usesFKG lattice condition · Law of the agreement configuration of two replicas
Proof usesConfiguration space of a statistical-mechanics model · Being a spin monomial · Bond variable of an unordered pair · Bond variable takes values \(\pm 1\) · Set of sites where an agreement configuration is true · Total two-replica weight of an agreement fibre · Two-replica weight in an agreement fibre · Mate of a configuration over an agreement pattern · Splitting a configuration along the agreement set · Completion of agreement-set spins to a full configuration · Agreement-set Boltzmann weight with doubled couplings and field · Completion of disagreement-set spins to a full configuration · Zero-field disagreement-set Boltzmann weight · Image of a vertex set together with the ghost vertex · Image of a vertex set among non-ghost vertices · Weight of an agreement set in the duplicated system · Induced-subgraph partition function with doubled coupling and field · Zero-field induced-subgraph partition function with doubled coupling · Edges of the induced subgraph on a vertex set · Zero-field partition function of an induced subgraph · Nonnegativity of the GKS positivity kernel · Ising Hamiltonian on a finite graph · Boltzmann weight of an Ising configuration · Ising partition function · Spin monomial with given exponents · Spin of a configuration at a site · Spin product over a vertex set · Global spin flip · Coupling on the ghost graph with uniform field · Ghost edges · Graph edges as ghost-graph edges · Embedding of vertices into the ghost graph · Partition function with inhomogeneous couplings and site fields · Unordered pair inside a set · Gibbs expectation with inhomogeneous couplings and site fields · Griffiths monotonicity of correlations in the edge set · Boltzmann weight with inhomogeneous couplings and site fields · Graph with a ghost vertex joined to every site

TheoremGriffiths–Hurst–Sherman inequality#✓fully proved

For the ferromagnetic Ising model on a finite graph with β ≥ 0 and h ≥ 0, the third Ursell function u₃(o, x, y) is nonpositive for every site o and every edge {x, y}.

R. B. Griffiths, C. A. Hurst and S. Sherman, Concavity of magnetization of an Ising ferromagnet in a positive external field, J. Math. Phys. 11 (1970); proof of J. L. Lebowitz, GHS and other inequalities, Comm. Math. Phys. 35 (1974).

theorem ghsL_threePoint (β h : ℝ) (hβ : 0 ≤ β) (hh : 0 ≤ h) (o : V) :
    GHSThreePointSym G β h o
Uses 69
Statement usesGHS three-point inequality at a site for every edge
Proof usesConfiguration space of a statistical-mechanics model · FKG lattice condition · Fibre factorization property for \(u_o u_x\) and \(t_y\) · Being a spin monomial · Bond variable of an unordered pair · Bond variable takes values \(\pm 1\) · Two-point spin covariance · Covariance of a spin with a bond variable · GHS bound for a bond · Set of sites where an agreement configuration is true · Agreement configuration of two spin configurations · Law of the agreement configuration of two replicas · Conditional two-replica expectation given the agreement · Total two-replica weight of an agreement fibre · Fibre weight integrated against an observable · Conditional expectation of \(t_y\) given the agreement · Conditional expectation of \(u_o u_x\) given the agreement · Two-replica weight in an agreement fibre · Mate of a configuration over an agreement pattern · Field weight of the disagreement set · Splitting a configuration along the agreement set · Completion of agreement-set spins to a full configuration · Expectation with field on the agreement set · Agreement-set Boltzmann weight with doubled couplings and field · Completion of disagreement-set spins to a full configuration · Zero-field expectation on the disagreement set · Zero-field disagreement-set Boltzmann weight · Change of variables from replica pairs to agreement and first copy · Magnetization on the agreement subgraph · Two-point correlation on the disagreement subgraph · Image of a vertex set together with the ghost vertex · Image of a vertex set among non-ghost vertices · Weight of an agreement set in the duplicated system · Induced-subgraph partition function with doubled coupling and field · Zero-field induced-subgraph partition function with doubled coupling · Zero-field correlation in an induced subgraph · Correlation with field in an induced subgraph · Edges of the induced subgraph on a vertex set · Zero-field partition function of an induced subgraph · First Griffiths inequality (GKS I) · Nonnegativity of the GKS positivity kernel · Ising Hamiltonian on a finite graph · Two-replica Ising expectation · Finite-volume Ising expectation · Gibbs probability of an Ising configuration · Ising Gibbs probabilities sum to one · Boltzmann weight of an Ising configuration · Ising partition function · Positivity of the Ising partition function · Spin monomial with given exponents · Ising one-point function · Spin of a configuration at a site · Spin product over a vertex set · Rotated two-replica sum variable \(t_w\) · Rotated two-replica difference variable \(u_w\) · Global spin flip · Coupling on the ghost graph with uniform field · Ghost edges · Graph edges as ghost-graph edges · Embedding of vertices into the ghost graph · Partition function with inhomogeneous couplings and site fields · Griffiths' second inequality for two distinct spins · Unordered pair inside a set · Gibbs expectation with inhomogeneous couplings and site fields · Griffiths monotonicity of correlations in the edge set · Boltzmann weight with inhomogeneous couplings and site fields · Graph with a ghost vertex joined to every site · FKG inequality

LemmaDerivative of a concave function is at most a secant slope#✓fully proved

The derivative of a concave function on [0, ∞) at b is at most the secant slope over [a, b]. This is Mathlib's ConcaveOn.deriv_le_slope with the slope unfolded.

lemma shg_concaveOn_deriv_le_slope (φ : ℝ → ℝ) (hconc : ConcaveOn ℝ (Ici 0) φ)
    {a b : ℝ} (ha : a ∈ Ici (0 : ℝ)) (hb : b ∈ Ici (0 : ℝ)) (hab : a < b)
    (hd : DifferentiableAt ℝ φ b) :
    deriv φ b ≤ (φ b - φ a) / (b - a)
Used by 2
Used bySusceptibility bound \(\chi(h) \le m(h)/h\) from concavity · Mean-field lower bound for the spontaneous magnetization

LemmaConcavity from a nonpositive second derivative on \((0, \infty)\)#✓fully proved

A continuous function on [0, ∞), twice differentiable on the interior with nonpositive second derivative, is concave. This is Mathlib's concaveOn_of_deriv2_nonpos specialized to Ici 0.

lemma shg_concaveOn_of_deriv2_nonpos (φ : ℝ → ℝ)
    (hcont : ContinuousOn φ (Ici 0))
    (hf' : DifferentiableOn ℝ φ (interior (Ici 0)))
    (hf'' : DifferentiableOn ℝ (deriv φ) (interior (Ici 0)))
    (hu3 : ∀ h ∈ interior (Ici (0 : ℝ)), deriv^[2] φ h ≤ 0) :
    ConcaveOn ℝ (Ici 0) φ
Used by 2
Used byGHS concavity of the magnetization in the field · GHS concavity

LemmaSusceptibility bound \(\chi(h) \le m(h)/h\) from concavity#✓fully proved

If the magnetization is concave in the field on [0, ∞), then for h > 0 the susceptibility satisfies χ(h) ≤ m(h)/h, using m(0) = 0.

lemma shg_magnetization_susceptibility_bound (β h : ℝ) (hh : 0 < h) (o : V)
    (hconc : ConcaveOn ℝ (Ici 0) (fun h => isingExpectation G β h (fun s => spin s o))) :
    deriv (fun h => isingExpectation G β h (fun s => spin s o)) h
      ≤ isingExpectation G β h (fun s => spin s o) / h
Uses 12
Statement usesConfiguration space of a statistical-mechanics model · Finite-volume Ising expectation · Spin of a configuration at a site
Proof usesBond variable of an unordered pair · Ising Hamiltonian on a finite graph · Gibbs probability of an Ising configuration · Boltzmann weight of an Ising configuration · Ising partition function · Positivity of the Ising partition function · Magnetization vanishes at zero field · Derivative of a concave function is at most a secant slope · Total spin of a configuration

DefinitionTwo-replica expectation with inhomogeneous couplings#✓fully proved

The expectation of F a b over two independent copies of the Ising model with couplings K and fields hf.

noncomputable def ghsiExp2 (K : Sym2 V → ℝ) (hf : V → ℝ)
    (F : ConfigSpace V → ConfigSpace V → ℝ) : ℝ :=
  (∑ a : ConfigSpace V, ∑ b : ConfigSpace V,
      wJ G.edgeFinset K hf a * wJ G.edgeFinset K hf b * F a b) /
    (ZJ G.edgeFinset K hf) ^ 2
Uses 3 · Used by 1
Statement usesConfiguration space of a statistical-mechanics model · Partition function with inhomogeneous couplings and site fields · Boltzmann weight with inhomogeneous couplings and site fields
Used byGriffiths–Hurst–Sherman inequality

DefinitionInhomogeneous agreement-set Boltzmann weight#✓fully proved

The Boltzmann weight, with couplings 2K and fields 2hf, of a on the subgraph induced by the agreement set of q.

noncomputable def ghsiTWeight (K : Sym2 V → ℝ) (hf : V → ℝ)
    (q a : ConfigSpace V) : ℝ :=
  Real.exp
    ((∑ e ∈ ghsvp_vertexEdges G.edgeFinset (ghsLAgreeFinset q),
        (2 * K e) * bond a e) +
      ∑ v ∈ ghsLAgreeFinset q, (2 * hf v) * spin a v)
Uses 5 · Used by 2
Statement usesConfiguration space of a statistical-mechanics model · Bond variable of an unordered pair · Set of sites where an agreement configuration is true · Edges of the induced subgraph on a vertex set · Spin of a configuration at a site
Used byInhomogeneous expectation with field on the agreement set · Griffiths–Hurst–Sherman inequality

DefinitionInhomogeneous zero-field disagreement-set weight#✓fully proved

The zero-field Boltzmann weight, with couplings 2K, of a on the subgraph induced by the disagreement set of q.

noncomputable def ghsiUWeight (K : Sym2 V → ℝ) (q a : ConfigSpace V) : ℝ :=
  Real.exp
    (∑ e ∈ ghsvp_vertexEdges G.edgeFinset (ghsLAgreeFinset q)ᶜ,
      (2 * K e) * bond a e)
Uses 4 · Used by 2
Statement usesConfiguration space of a statistical-mechanics model · Bond variable of an unordered pair · Set of sites where an agreement configuration is true · Edges of the induced subgraph on a vertex set
Used byInhomogeneous zero-field expectation on the disagreement set · Griffiths–Hurst–Sherman inequality

DefinitionInhomogeneous two-replica weight in an agreement fibre#✓fully proved

The two-replica weight of a and its mate in the fibre over the agreement configuration q.

noncomputable def ghsiFibreWeight (K : Sym2 V → ℝ) (hf : V → ℝ)
    (q a : ConfigSpace V) : ℝ :=
  wJ G.edgeFinset K hf a * wJ G.edgeFinset K hf (ghsLMate q a)
Uses 3 · Used by 3
Statement usesConfiguration space of a statistical-mechanics model · Mate of a configuration over an agreement pattern · Boltzmann weight with inhomogeneous couplings and site fields
Used byInhomogeneous total weight of an agreement fibre · Inhomogeneous fibre weight integrated against an observable · Griffiths–Hurst–Sherman inequality

DefinitionInhomogeneous total weight of an agreement fibre#✓fully proved

The total two-replica weight of the fibre over q.

noncomputable def ghsiFibreMass (K : Sym2 V → ℝ) (hf : V → ℝ)
    (q : ConfigSpace V) : ℝ :=
  ∑ a : ConfigSpace V, ghsiFibreWeight G K hf q a
Uses 2 · Used by 3
Statement usesConfiguration space of a statistical-mechanics model · Inhomogeneous two-replica weight in an agreement fibre
Used byInhomogeneous law of the agreement configuration · Inhomogeneous conditional expectation given the agreement · Griffiths–Hurst–Sherman inequality

DefinitionInhomogeneous fibre weight integrated against an observable#✓fully proved

The two-replica weight of the fibre over q, integrated against F.

noncomputable def ghsiFibreNumerator (K : Sym2 V → ℝ) (hf : V → ℝ)
    (F : ConfigSpace V → ConfigSpace V → ℝ) (q : ConfigSpace V) : ℝ :=
  ∑ a : ConfigSpace V, ghsiFibreWeight G K hf q a * F a (ghsLMate q a)
Uses 3 · Used by 2
Statement usesConfiguration space of a statistical-mechanics model · Mate of a configuration over an agreement pattern · Inhomogeneous two-replica weight in an agreement fibre
Used byInhomogeneous conditional expectation given the agreement · Griffiths–Hurst–Sherman inequality

DefinitionInhomogeneous conditional expectation given the agreement#✓fully proved

The conditional two-replica expectation of F given the agreement configuration q.

noncomputable def ghsiFibreExpectation (K : Sym2 V → ℝ) (hf : V → ℝ)
    (F : ConfigSpace V → ConfigSpace V → ℝ) (q : ConfigSpace V) : ℝ :=
  ghsiFibreNumerator G K hf F q / ghsiFibreMass G K hf q
Uses 3 · Used by 3
Statement usesConfiguration space of a statistical-mechanics model · Inhomogeneous total weight of an agreement fibre · Inhomogeneous fibre weight integrated against an observable
Used byInhomogeneous conditional expectation of \(t_y\) · Inhomogeneous conditional expectation of \(u_o u_x\) · Griffiths–Hurst–Sherman inequality

DefinitionInhomogeneous law of the agreement configuration#✓fully proved

The probability that two independent replicas have agreement configuration q.

noncomputable def ghsiAgreementProb (K : Sym2 V → ℝ) (hf : V → ℝ)
    (q : ConfigSpace V) : ℝ :=
  ghsiFibreMass G K hf q / (ZJ G.edgeFinset K hf) ^ 2
Uses 3 · Used by 1
Statement usesConfiguration space of a statistical-mechanics model · Inhomogeneous total weight of an agreement fibre · Partition function with inhomogeneous couplings and site fields
Used byGriffiths–Hurst–Sherman inequality

DefinitionInhomogeneous conditional expectation of \(u_o u_x\)#✓fully proved

The conditional expectation E[u_o u_x | q] of the rotated variables.

noncomputable def ghsiFibreUU (K : Sym2 V → ℝ) (hf : V → ℝ)
    (o x : V) (q : ConfigSpace V) : ℝ :=
  ghsiFibreExpectation G K hf (fun a b => uvar a b o * uvar a b x) q
Uses 3 · Used by 1
Statement usesConfiguration space of a statistical-mechanics model · Inhomogeneous conditional expectation given the agreement · Rotated two-replica difference variable \(u_w\)
Used byGriffiths–Hurst–Sherman inequality

DefinitionInhomogeneous conditional expectation of \(t_y\)#✓fully proved

The conditional expectation E[t_y | q] of the rotated variable.

noncomputable def ghsiFibreT (K : Sym2 V → ℝ) (hf : V → ℝ)
    (y : V) (q : ConfigSpace V) : ℝ :=
  ghsiFibreExpectation G K hf (fun a b => tvar a b y) q
Uses 3 · Used by 1
Statement usesConfiguration space of a statistical-mechanics model · Inhomogeneous conditional expectation given the agreement · Rotated two-replica sum variable \(t_w\)
Used byGriffiths–Hurst–Sherman inequality

DefinitionInhomogeneous zero-field expectation on the disagreement set#✓fully proved

The zero-field expectation on the subgraph induced by the disagreement set of q.

noncomputable def ghsiUExpectation (K : Sym2 V → ℝ) (q : ConfigSpace V)
    (F : ConfigSpace V → ℝ) : ℝ :=
  (∑ a : ConfigSpace V, ghsiUWeight G K q a * F a) /
    ∑ a : ConfigSpace V, ghsiUWeight G K q a
Uses 2 · Used by 1
Statement usesConfiguration space of a statistical-mechanics model · Inhomogeneous zero-field disagreement-set weight
Used byGriffiths–Hurst–Sherman inequality

DefinitionInhomogeneous expectation with field on the agreement set#✓fully proved

The expectation with field on the subgraph induced by the agreement set of q.

noncomputable def ghsiTExpectation (K : Sym2 V → ℝ) (hf : V → ℝ)
    (q : ConfigSpace V) (F : ConfigSpace V → ℝ) : ℝ :=
  (∑ a : ConfigSpace V, ghsiTWeight G K hf q a * F a) /
    ∑ a : ConfigSpace V, ghsiTWeight G K hf q a
Uses 2 · Used by 1
Statement usesConfiguration space of a statistical-mechanics model · Inhomogeneous agreement-set Boltzmann weight
Used byGriffiths–Hurst–Sherman inequality

DefinitionInhomogeneous two-point correlation on the disagreement set#✓fully proved

The zero-field correlation ⟨σ_o σ_x⟩ on the subgraph induced by Aᶜ (couplings 2K), or 0 if o or x lies in A.

noncomputable def ghsiDisagreementCorr (K : Sym2 V → ℝ)
    (o x : V) (A : Finset V) : ℝ :=
  if o ∈ A ∨ x ∈ A then 0
  else ghsvp_vertexCorr G.edgeFinset (fun e => 2 * K e) Aᶜ {o, x}
Uses 1 · Used by 1
Statement usesZero-field correlation in an induced subgraph
Used byGriffiths–Hurst–Sherman inequality

DefinitionInhomogeneous magnetization on the agreement set#✓fully proved

The magnetization ⟨σ_y⟩ on the subgraph induced by A (couplings 2K, fields 2hf), or 0 if y ∉ A.

noncomputable def ghsiAgreementMag (K : Sym2 V → ℝ) (hf : V → ℝ)
    (y : V) (A : Finset V) : ℝ :=
  if y ∈ A then
    ghsvp_vertexCorrField G.edgeFinset (fun e => 2 * K e) (fun x => 2 * hf x) A {y}
  else 0
Uses 1 · Used by 1
Statement usesCorrelation with field in an induced subgraph
Used byGriffiths–Hurst–Sherman inequality

DefinitionInhomogeneous field weight of the disagreement set#✓fully proved

The field weight exp (∑_{v ∉ q} 2h_v σ_v(a)) of the disagreement set.

noncomputable def ghsiOutFieldWeight (hf : V → ℝ)
    (q a : ConfigSpace V) : ℝ :=
  Real.exp (∑ v ∈ (ghsLAgreeFinset q)ᶜ, (2 * hf v) * spin a v)
Uses 3 · Used by 1
Statement usesConfiguration space of a statistical-mechanics model · Set of sites where an agreement configuration is true · Spin of a configuration at a site
Used byGriffiths–Hurst–Sherman inequality

TheoremGriffiths–Hurst–Sherman inequality#✓fully proved

Griffiths–Hurst–Sherman inequality for inhomogeneous ferromagnets. With couplings K_e ≥ 0 and fields h_x ≥ 0, the third Ursell function satisfies u₃(o, x, y) ≤ 0 whenever o ≠ x.

R. B. Griffiths, C. A. Hurst and S. Sherman, Concavity of magnetization of an Ising ferromagnet in a positive external field, J. Math. Phys. 11 (1970); J. L. Lebowitz, GHS and other inequalities, Comm. Math. Phys. 35 (1974).

theorem ghsi_ursell_nonpos (K : Sym2 V → ℝ) (hf : V → ℝ)
    (hK : ∀ e, 0 ≤ K e) (hhf : ∀ x, 0 ≤ hf x)
    (o x y : V) (hox : o ≠ x) :
    expJ G.edgeFinset K hf (fun s => spin s o * (spin s x * spin s y)) -
          expJ G.edgeFinset K hf (fun s => spin s o) *
            expJ G.edgeFinset K hf (fun s => spin s x * spin s y) -
          expJ G.edgeFinset K hf (fun s => spin s o * spin s x) *
            expJ G.edgeFinset K hf (fun s => spin s y) -
          expJ G.edgeFinset K hf (fun s => spin s o * spin s y) *
            expJ G.edgeFinset K hf (fun s => spin s x) +
          2 * expJ G.edgeFinset K hf (fun s => spin s o) *
            expJ G.edgeFinset K hf (fun s => spin s x) *
            expJ G.edgeFinset K hf (fun s => spin s y) ≤ 0
Uses 54 · Used by 1
Statement usesConfiguration space of a statistical-mechanics model · Spin of a configuration at a site · Gibbs expectation with inhomogeneous couplings and site fields
Proof usesFKG lattice condition · Being a spin monomial · Bond variable of an unordered pair · Bond variable takes values \(\pm 1\) · Set of sites where an agreement configuration is true · Agreement configuration of two spin configurations · Mate of a configuration over an agreement pattern · Splitting a configuration along the agreement set · Completion of agreement-set spins to a full configuration · Completion of disagreement-set spins to a full configuration · Change of variables from replica pairs to agreement and first copy · Inhomogeneous magnetization on the agreement set · Inhomogeneous law of the agreement configuration · Inhomogeneous two-point correlation on the disagreement set · Two-replica expectation with inhomogeneous couplings · Inhomogeneous conditional expectation given the agreement · Inhomogeneous total weight of an agreement fibre · Inhomogeneous fibre weight integrated against an observable · Inhomogeneous conditional expectation of \(t_y\) · Inhomogeneous conditional expectation of \(u_o u_x\) · Inhomogeneous two-replica weight in an agreement fibre · Inhomogeneous ghost-vertex couplings · Inhomogeneous field weight of the disagreement set · Inhomogeneous weight of an agreement set · Inhomogeneous expectation with field on the agreement set · Inhomogeneous agreement-set Boltzmann weight · Inhomogeneous induced-subgraph partition function with field · Inhomogeneous zero-field expectation on the disagreement set · Inhomogeneous zero-field disagreement-set weight · Inhomogeneous zero-field induced-subgraph partition function · Image of a vertex set together with the ghost vertex · Image of a vertex set among non-ghost vertices · Zero-field correlation in an induced subgraph · Correlation with field in an induced subgraph · Edges of the induced subgraph on a vertex set · Zero-field partition function of an induced subgraph · Nonnegativity of the GKS positivity kernel · Spin monomial with given exponents · Spin product over a vertex set · Rotated two-replica sum variable \(t_w\) · Rotated two-replica difference variable \(u_w\) · Global spin flip · Ghost edges · Graph edges as ghost-graph edges · Embedding of vertices into the ghost graph · Partition function with inhomogeneous couplings and site fields · Unordered pair inside a set · Griffiths monotonicity of correlations in the edge set · Boltzmann weight with inhomogeneous couplings and site fields · Graph with a ghost vertex joined to every site · FKG inequality
Used byThird Ursell function nonpositive for \(o \ne x\), \(K, h \ge 0\)

DefinitionDirectional spin sum#✓fully proved

The directional spin ∑_x d_x σ_x.

noncomputable def ghsiDirSpin (dir : V → ℝ) (s : ConfigSpace V) : ℝ :=
  ∑ x, dir x * spin s x
Uses 2 · Used by 3
Statement usesConfiguration space of a statistical-mechanics model · Spin of a configuration at a site
Used byCovariance with the directional spin · GHS concavity · Mean-field lower bound for the spontaneous magnetization

DefinitionField line in a given direction#✓fully proved

The field line t ↦ h + t·d.

def ghsiFieldLine (hf dir : V → ℝ) (t : ℝ) : V → ℝ :=
  fun x => hf x + t * dir x
Used by 2
Used byGHS concavity · Mean-field lower bound for the spontaneous magnetization

DefinitionCovariance with the directional spin#✓fully proved

The covariance of f with the directional spin ∑_x d_x σ_x.

noncomputable def ghsiDirectionalCovariance (K : Sym2 V → ℝ)
    (hf dir : V → ℝ) (f : ConfigSpace V → ℝ) : ℝ :=
  expJ G.edgeFinset K hf (fun s => f s * ghsiDirSpin dir s) -
    expJ G.edgeFinset K hf f * expJ G.edgeFinset K hf (ghsiDirSpin dir)
Uses 3 · Used by 2
Statement usesConfiguration space of a statistical-mechanics model · Directional spin sum · Gibbs expectation with inhomogeneous couplings and site fields
Used byGHS concavity · Mean-field lower bound for the spontaneous magnetization

DefinitionThird Ursell function of the inhomogeneous Ising model#✓fully proved

The third Ursell function u₃(o, x, y) of the inhomogeneous Ising model.

noncomputable def ghsiUrsell3 (K : Sym2 V → ℝ) (hf : V → ℝ)
    (o x y : V) : ℝ :=
  expJ G.edgeFinset K hf (fun s => spin s o * (spin s x * spin s y)) -
    expJ G.edgeFinset K hf (fun s => spin s o) *
      expJ G.edgeFinset K hf (fun s => spin s x * spin s y) -
    expJ G.edgeFinset K hf (fun s => spin s o * spin s x) *
      expJ G.edgeFinset K hf (fun s => spin s y) -
    expJ G.edgeFinset K hf (fun s => spin s o * spin s y) *
      expJ G.edgeFinset K hf (fun s => spin s x) +
    2 * expJ G.edgeFinset K hf (fun s => spin s o) *
      expJ G.edgeFinset K hf (fun s => spin s x) *
      expJ G.edgeFinset K hf (fun s => spin s y)
Uses 3 · Used by 2
Statement usesConfiguration space of a statistical-mechanics model · Spin of a configuration at a site · Gibbs expectation with inhomogeneous couplings and site fields
Used byGHS concavity · Third Ursell function nonpositive for \(o \ne x\), \(K, h \ge 0\)

LemmaThird Ursell function nonpositive for \(o \ne x\), \(K, h \ge 0\)#✓fully proved

The GHS inequality u₃(o, x, y) ≤ 0 for the named Ursell function, when o ≠ x.

lemma ghsiUrsell3_nonpos (K : Sym2 V → ℝ) (hf : V → ℝ)
    (hK : ∀ e, 0 ≤ K e) (hhf : ∀ x, 0 ≤ hf x)
    (o x y : V) (hox : o ≠ x) :
    ghsiUrsell3 G K hf o x y ≤ 0
Uses 2 · Used by 1
Statement usesThird Ursell function of the inhomogeneous Ising model
Proof usesGriffiths–Hurst–Sherman inequality
Used byGHS concavity

DefinitionSpin covariance in the inhomogeneous model#✓fully proved

The spin covariance ⟨σ_o σ_x⟩ - ⟨σ_o⟩⟨σ_x⟩.

noncomputable def ghsiCovariance (K : Sym2 V → ℝ) (hf : V → ℝ)
    (o x : V) : ℝ :=
  expJ G.edgeFinset K hf (fun s => spin s o * spin s x) -
    expJ G.edgeFinset K hf (fun s => spin s o) *
      expJ G.edgeFinset K hf (fun s => spin s x)
Uses 3 · Used by 2
Statement usesConfiguration space of a statistical-mechanics model · Spin of a configuration at a site · Gibbs expectation with inhomogeneous couplings and site fields
Used byGHS concavity · Mean-field lower bound for the spontaneous magnetization

TheoremGHS concavity#✓fully proved

With couplings K_e ≥ 0, fields h_x ≥ 0, and a direction d ≥ 0 with d_o = 0, the magnetization ⟨σ_o⟩ is concave in t ≥ 0 along the field line h + t·d.

R. B. Griffiths, C. A. Hurst and S. Sherman, J. Math. Phys. 11 (1970).

theorem ghsi_magnetization_fieldLine_concaveOn
    (K : Sym2 V → ℝ) (hf dir : V → ℝ)
    (hK : ∀ e, 0 ≤ K e) (hhf : ∀ x, 0 ≤ hf x)
    (hdir : ∀ x, 0 ≤ dir x) (o : V) (hdiro : dir o = 0) :
    ConcaveOn ℝ (Ici 0)
      (fun t => expJ G.edgeFinset K (ghsiFieldLine hf dir t)
        (fun s => spin s o))
Uses 13 · Used by 1
Statement usesConfiguration space of a statistical-mechanics model · Field line in a given direction · Spin of a configuration at a site · Gibbs expectation with inhomogeneous couplings and site fields
Proof usesBond variable of an unordered pair · Spin covariance in the inhomogeneous model · Directional spin sum · Covariance with the directional spin · Third Ursell function of the inhomogeneous Ising model · Third Ursell function nonpositive for \(o \ne x\), \(K, h \ge 0\) · Partition function with inhomogeneous couplings and site fields · Concavity from a nonpositive second derivative on \((0, \infty)\) · Boltzmann weight with inhomogeneous couplings and site fields
Used byMean-field lower bound for the spontaneous magnetization

DefinitionField derivative of the two-point covariance#✓fully proved

The field derivative of the two-point covariance Cov(σ_o, σ_x), written as a combination of Gibbs expectations involving the total spin.

noncomputable def gc4_D1cov2 (β h : ℝ) (o x : V) : ℝ :=
    (β * (isingExpectation G β h (fun s => (spin s o * spin s x) * totalSpin s)
        - isingExpectation G β h (fun s => spin s o * spin s x) * isingExpectation G β h totalSpin))
    - ((β * (isingExpectation G β h (fun s => spin s o * totalSpin s)
            - isingExpectation G β h (fun s => spin s o) * isingExpectation G β h totalSpin))
          * isingExpectation G β h (fun s => spin s x)
        + isingExpectation G β h (fun s => spin s o)
          * (β * (isingExpectation G β h (fun s => spin s x * totalSpin s)
              - isingExpectation G β h (fun s => spin s x) * isingExpectation G β h totalSpin)))
Uses 4 · Used by 1
Statement usesConfiguration space of a statistical-mechanics model · Finite-volume Ising expectation · Spin of a configuration at a site · Total spin of a configuration
Used byGHS concavity of the magnetization in the field

DefinitionThird Ursell function of the finite Ising model#✓fully proved

The third Ursell function (joint cumulant) u₃(o, x, y) = ⟨σ_oσ_xσ_y⟩ - ⟨σ_o⟩⟨σ_xσ_y⟩ - ⟨σ_oσ_x⟩⟨σ_y⟩ - ⟨σ_oσ_y⟩⟨σ_x⟩ + 2⟨σ_o⟩⟨σ_x⟩⟨σ_y⟩ of the finite Ising model at (β, h).

noncomputable def eg_ursell3 (β h : ℝ) (o x y : V) : ℝ :=
  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)
    - isingExpectation G β h (fun s => spin s o * spin s x)
        * isingExpectation G β h (fun s => spin s y)
    - isingExpectation G β h (fun s => spin s o * spin s y)
        * isingExpectation G β h (fun s => spin s x)
    + 2 * isingExpectation G β h (fun s => spin s o)
        * isingExpectation G β h (fun s => spin s x)
        * isingExpectation G β h (fun s => spin s y)
Uses 3 · Used by 4
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 · GHS concavity of the magnetization in the field · Griffiths–Hurst–Sherman inequality · GHS sign condition

LemmaGHS gap on an edge equals the third Ursell function#✓fully proved

On an edge {x, y}, the gap cov3sym - ghsBoundSym between the three-point covariance and the GHS bound equals u₃(o, x, y).

lemma ghc_ursellEqGap (β h : ℝ) (o x y : V) :
    cov3sym G β h o s(x, y) - ghsBoundSym G β h o s(x, y) = eg_ursell3 G β h o x y
Uses 8 · Used by 1
Statement usesCovariance of a spin with a bond variable · GHS bound for a bond · Third Ursell function of the finite Ising model
Proof usesConfiguration space of a statistical-mechanics model · Two-point spin covariance · Finite-volume Ising expectation · Ising one-point function · Spin of a configuration at a site
Used byGHS concavity of the magnetization in the field

DefinitionLebowitz four-point combination#✓fully proved

Lebowitz's four-point combination ⟨σ_oσ_xσ_y⟩ - ⟨σ_oσ_x⟩⟨σ_y⟩ - ⟨σ_oσ_y⟩⟨σ_x⟩ - ⟨σ_o⟩⟨σ_xσ_y⟩, which differs from the Ursell function u₃ by 2⟨σ_o⟩⟨σ_x⟩⟨σ_y⟩.

noncomputable def gc_lebowitzU4 (β h : ℝ) (o x y : V) : ℝ :=
  isingExpectation G β h (fun s => spin s o * (spin s x * spin s y))
    - isingExpectation G β h (fun s => spin s o * spin s x)
        * isingExpectation G β h (fun s => spin s y)
    - isingExpectation G β h (fun s => spin s o * spin s y)
        * isingExpectation G β h (fun s => spin s x)
    - isingExpectation G β h (fun s => spin s o)
        * isingExpectation G β h (fun s => spin s x * spin s y)
Uses 3
Statement usesConfiguration space of a statistical-mechanics model · Finite-volume Ising expectation · Spin of a configuration at a site

DefinitionGHS sign condition#✓fully proved

The GHS sign condition at (β, h) and root o: the third Ursell function u₃(o, x, y) is nonpositive for all pairwise distinct o, x, y. It holds for β, h ≥ 0 by ghs_signDominance.

def GHSSignDominance (β h : ℝ) (o : V) : Prop :=
  ∀ x y : V, o ≠ x → o ≠ y → x ≠ y → eg_ursell3 G β h o x y ≤ 0
Uses 1 · Used by 2
Statement usesThird Ursell function of the finite Ising model
Used byGHS concavity of the magnetization in the field · Griffiths–Hurst–Sherman inequality

TheoremGriffiths–Hurst–Sherman inequality#✓fully proved

The Griffiths–Hurst–Sherman inequality: for β ≥ 0 and h ≥ 0, the third Ursell function u₃(o, x, y) is nonpositive for distinct sites. Reference: R. B. Griffiths, C. A. Hurst, S. Sherman, "Concavity of magnetization of an Ising ferromagnet in a positive external field", J. Math. Phys. 11 (1970) 790–795; proof via J. L. Lebowitz, "GHS and other inequalities", Comm. Math. Phys. 35 (1974) 87–92.

theorem ghs_signDominance (β h : ℝ) (hβ : 0 ≤ β) (hh : 0 ≤ h) (o : V) :
    GHSSignDominance G β h o
Uses 68 · Used by 1
Statement usesGHS sign condition
Proof usesConfiguration space of a statistical-mechanics model · FKG lattice condition · Fibre factorization property for \(u_o u_x\) and \(t_y\) · Being a spin monomial · Bond variable of an unordered pair · Bond variable takes values \(\pm 1\) · Two-point spin covariance · Covariance of a spin with a bond variable · GHS bound for a bond · Set of sites where an agreement configuration is true · Agreement configuration of two spin configurations · Law of the agreement configuration of two replicas · Conditional two-replica expectation given the agreement · Total two-replica weight of an agreement fibre · Fibre weight integrated against an observable · Conditional expectation of \(t_y\) given the agreement · Conditional expectation of \(u_o u_x\) given the agreement · Two-replica weight in an agreement fibre · Mate of a configuration over an agreement pattern · Field weight of the disagreement set · Splitting a configuration along the agreement set · Completion of agreement-set spins to a full configuration · Expectation with field on the agreement set · Agreement-set Boltzmann weight with doubled couplings and field · Completion of disagreement-set spins to a full configuration · Zero-field expectation on the disagreement set · Zero-field disagreement-set Boltzmann weight · Change of variables from replica pairs to agreement and first copy · Magnetization on the agreement subgraph · Two-point correlation on the disagreement subgraph · Image of a vertex set together with the ghost vertex · Image of a vertex set among non-ghost vertices · Weight of an agreement set in the duplicated system · Induced-subgraph partition function with doubled coupling and field · Zero-field induced-subgraph partition function with doubled coupling · Zero-field correlation in an induced subgraph · Correlation with field in an induced subgraph · Edges of the induced subgraph on a vertex set · Zero-field partition function of an induced subgraph · Nonnegativity of the GKS positivity kernel · Ising Hamiltonian on a finite graph · Two-replica Ising expectation · Finite-volume Ising expectation · Gibbs probability of an Ising configuration · Ising Gibbs probabilities sum to one · Boltzmann weight of an Ising configuration · Ising partition function · Positivity of the Ising partition function · Spin monomial with given exponents · Ising one-point function · Spin of a configuration at a site · Spin product over a vertex set · Rotated two-replica sum variable \(t_w\) · Rotated two-replica difference variable \(u_w\) · Global spin flip · Coupling on the ghost graph with uniform field · Ghost edges · Graph edges as ghost-graph edges · Embedding of vertices into the ghost graph · Partition function with inhomogeneous couplings and site fields · Unordered pair inside a set · Gibbs expectation with inhomogeneous couplings and site fields · Griffiths monotonicity of correlations in the edge set · Boltzmann weight with inhomogeneous couplings and site fields · Graph with a ghost vertex joined to every site · Third Ursell function of the finite Ising model · FKG inequality
Used byGHS concavity of the magnetization in the field

TheoremGHS concavity of the magnetization in the field#✓fully proved

GHS concavity: for β ≥ 0 the magnetization h ↦ ⟨σ_o⟩_{β,h} is concave on [0, ∞). Reference: R. B. Griffiths, C. A. Hurst, S. Sherman, "Concavity of magnetization of an Ising ferromagnet in a positive external field", J. Math. Phys. 11 (1970) 790–795.

theorem ghs_magnetization_concaveOn (β : ℝ) (hβ : 0 ≤ β) (o : V) :
    ConcaveOn ℝ (Ici 0) (fun h => isingExpectation G β h (fun s => spin s o))
Uses 25 · Used by 1
Statement usesConfiguration space of a statistical-mechanics model · Finite-volume Ising expectation · Spin of a configuration at a site
Proof usesBond variable of an unordered pair · Two-point spin covariance · Covariance of a spin with a bond variable · GHS bound for a bond · First Griffiths inequality (GKS I) · Ising Hamiltonian on a finite graph · Gibbs probability of an Ising configuration · Ising Gibbs probabilities sum to one · Boltzmann weight of an Ising configuration · Ising partition function · Positivity of the Ising partition function · Ising one-point function · Spin product over a vertex set · Griffiths' second inequality for two distinct spins · Field derivative of the magnetization as a sum of covariances · Griffiths–Hurst–Sherman inequality · Concavity from a nonpositive second derivative on \((0, \infty)\) · Total spin of a configuration · GHS sign condition · Third Ursell function of the finite Ising model · GHS gap on an edge equals the third Ursell function · Field derivative of the two-point covariance
Used byGHS susceptibility bound \(\chi \le 1/h\)

TheoremGHS susceptibility bound \(\chi \le 1/h\)#✓fully proved

The GHS susceptibility bound: for β ≥ 0 and h > 0, the field derivative of the magnetization equals β ∑_x (⟨σ_oσ_x⟩ - ⟨σ_o⟩⟨σ_x⟩) and is at most 1/h. Reference: R. B. Griffiths, C. A. Hurst, S. Sherman, "Concavity of magnetization of an Ising ferromagnet in a positive external field", J. Math. Phys. 11 (1970) 790–795. Scope: a finite graph with uniform coupling and uniform field, the field entering the Hamiltonian as -h ∑ σ_x and the derivative taken in h; χ ≤ 1/h is the weak form of the GHS consequence χ ≤ m/h, the full concavity statement being ghs_magnetization_concaveOn. The hypotheses β ≥ 0, h > 0 are satisfiable.

theorem ghs_susceptibility_le_inv_field (β h : ℝ) (hβ : 0 ≤ β) (hh : 0 < h)
    (o : V) :
    deriv (fun t => isingExpectation G β t (fun s => spin s o)) h =
        β * ∑ x, (isingExpectation G β h (fun s => spin s o * spin s x) -
          isingExpectation G β h (fun s => spin s o) *
            isingExpectation G β h (fun s => spin s x))
      ∧ deriv (fun t => isingExpectation G β t (fun s => spin s o)) h ≤ 1 / h
Uses 6
Statement usesConfiguration space of a statistical-mechanics model · Finite-volume Ising expectation · Spin of a configuration at a site
Proof usesField derivative of the magnetization as a sum of covariances · GHS concavity of the magnetization in the field · Susceptibility bound \(\chi(h) \le m(h)/h \le 1/h\) from concavity
96 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.