Mean-field lower bound for the Ising magnetization

DefinitionMinimal magnetization ratio for sites indexed by \(\mathbb{N}\)#✓fully proved

The minimal ratio min_{y ∈ sites n} M(n)/m(n, y) for sites indexed by ℕ.

noncomputable def sct_cInf (M : ℕ → ℝ) (sites : ℕ → Finset ℕ)
    (m : ℕ → ℕ → ℝ) (hne : ∀ n, (sites n).Nonempty) (n : ℕ) : ℝ :=
  (sites n).inf' (hne n) (fun y => M n / m n y)

DefinitionMinimal magnetization ratio for \(n\)-dependent site types#✓fully proved

The minimal ratio min_{y ∈ sites n} M(n)/m(n, y) for site types depending on n.

noncomputable def sct_cInfDep (ι : ℕ → Type*) [∀ n, DecidableEq (ι n)]
    (M : ℕ → ℝ) (sites : (n : ℕ) → Finset (ι n))
    (m : (n : ℕ) → ι n → ℝ) (hne : ∀ n, (sites n).Nonempty) (n : ℕ) : ℝ :=
  (sites n).inf' (hne n) (fun y => M n / m n y)

Used by 3

Used byFinite-volume mean-field inequality for the Ising model · Minimal origin-to-site magnetization ratio in a box · Mean-field lower bound for the spontaneous magnetization

AbbreviationBox \(\Lambda_n\) as a type#✓fully proved

The box Λ_n = [-n, n]^d ⊆ ℤ^d as a type.

abbrev sctBox (d n : ℕ) := {x : Site d // x ∈ box d n}

Uses 2 · Used by 31

Statement usesSite of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice

Used byBoundary covariance error · Origin–site covariance in a box · Nearest-neighbour graph on a box · Membership of a larger-box site in a smaller box · Smaller box as a subtype of a larger box · Free-boundary site magnetization in a box · Origin as a site of a box · All sites of a box · Lattice site as a box site, defaulting to the origin · Edge with exactly one endpoint in a cut set · Boundary error of the finite-volume mean-field inequality · Cut mass of a box set rooted at the field ghost · Lattice sites underlying a set of box sites · Identification of a box cut set with its lattice sites · Boundary correlation of an edge crossing a cut · Symmetrized cut mass of an edge · External boundary correlation of a cut, over edges leaving the box · Pairs of a box site and an outside lattice neighbour · Finite-volume mean-field inequality for the Ising model · Field switched off on the outer layer · Origin magnetization with the outer-layer field switched off · Internal boundary correlation of a cut in the box · Minimal origin-to-site magnetization ratio in a box · Mean-field lower bound for the spontaneous magnetization · Oriented cut mass over cuts \(T \ni 0, x\) with \(y \notin T\) · \(\beta\)-derivative of the origin magnetization in a box · Covariance sum over the outer layer · Outer-layer indicator as a field direction · Translation onto a translated box · Membership of a doubled-box site in a translated box · Translated box as a subtype of the doubled box

DefinitionNearest-neighbour graph on a box#✓fully proved

The nearest-neighbour graph induced on Λ_n.

def sctBoxGraph (d n : ℕ) : SimpleGraph (sctBox d n) :=
  (hypercubicLattice d).induce (box d n)

Uses 4 · Used by 8

Statement usesSite of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice · Hypercubic lattice \(\mathbb{Z}^d\) · Box \(\Lambda_n\) as a type

Used byOrigin–site covariance in a box · Free-boundary site magnetization in a box · Cut mass of a box set rooted at the field ghost · Finite-volume mean-field inequality for the Ising model · Origin magnetization with the outer-layer field switched off · Internal boundary correlation of a cut in the box · Mean-field lower bound for the spontaneous magnetization · \(\beta\)-derivative of the origin magnetization in a box

DefinitionMembership of a larger-box site in a smaller box#✓fully proved

A site of Λ_m lies in Λ_n.

def sctBoxInLarger (d n m : ℕ) (z : sctBox d m) : Prop := z.1 ∈ box d n

Uses 3 · Used by 2

Statement usesSite of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice · Box \(\Lambda_n\) as a type

Used bySmaller box as a subtype of a larger box · Mean-field lower bound for the spontaneous magnetization

DefinitionSmaller box as a subtype of a larger box#✓fully proved

For n ≤ m, Λ_n is equivalent to the subtype of Λ_m of sites lying in Λ_n.

noncomputable def sctBoxInclusionEquiv (d : ℕ) {n m : ℕ} (hnm : n ≤ m) :
    sctBox d n ≃ {z : sctBox d m // sctBoxInLarger d n m z} where
  toFun z := ⟨⟨z.1, fun i => le_trans (z.2 i) hnm⟩, z.2⟩
  invFun z := ⟨z.1.1, z.2⟩
  left_inv z := by ext i; rfl
  right_inv z := by ext i; rfl

Uses 4 · Used by 1

Statement usesSite of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice · Box \(\Lambda_n\) as a type · Membership of a larger-box site in a smaller box

Used byMean-field lower bound for the spontaneous magnetization

DefinitionOrigin as a site of a box#✓fully proved

The origin as a site of Λ_n.

def sctBoxOrigin (d n : ℕ) : sctBox d n :=
  ⟨fun _ => 0, by intro i; simp⟩

Uses 3 · Used by 10

Statement usesSite of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice · Box \(\Lambda_n\) as a type

Used byOrigin–site covariance in a box · Lattice site as a box site, defaulting to the origin · Boundary error of the finite-volume mean-field inequality · Finite-volume mean-field inequality for the Ising model · Origin magnetization with the outer-layer field switched off · Minimal origin-to-site magnetization ratio in a box · Mean-field lower bound for the spontaneous magnetization · Oriented cut mass over cuts \(T \ni 0, x\) with \(y \notin T\) · Origin magnetization in a box · \(\beta\)-derivative of the origin magnetization in a box

DefinitionTranslated box \(\Lambda_n - y\)#✓fully proved

The translate Λ_n - y.

def sctTranslatedBox (d n : ℕ) (y : Site d) : Set (Site d) :=
  (fun z : Site d => z - y) '' box d n

Uses 2 · Used by 5

Statement usesSite of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice

Used byMean-field lower bound for the spontaneous magnetization · Translation onto a translated box · Nearest-neighbour graph on a translated box · Membership of a doubled-box site in a translated box · Translated box as a subtype of the doubled box

DefinitionTranslation onto a translated box#✓fully proved

Translation by -y as an equivalence Λ_n ≃ Λ_n - y.

noncomputable def sctTranslateEquiv (d n : ℕ) (y : Site d) :
    sctBox d n ≃ {z : Site d // z ∈ sctTranslatedBox d n y} where
  toFun z := ⟨z.1 - y, ⟨z.1, z.2, rfl⟩⟩
  invFun w := ⟨w.1 + y, by
    rcases w.2 with ⟨z, hz, hzy⟩
    have hw : w.1 + y = z := by
      rw [← hzy]
      funext i
      dsimp
      ring
    rwa [hw]⟩
  left_inv z := by ext i; simp
  right_inv w := by ext i; simp

Uses 4 · Used by 1

Statement usesSite of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice · Box \(\Lambda_n\) as a type · Translated box \(\Lambda_n - y\)

Used byMean-field lower bound for the spontaneous magnetization

DefinitionNearest-neighbour graph on a translated box#✓fully proved

The nearest-neighbour graph induced on Λ_n - y.

def sctTranslatedBoxGraph (d n : ℕ) (y : Site d) :
    SimpleGraph {z : Site d // z ∈ sctTranslatedBox d n y} :=
  (hypercubicLattice d).induce (sctTranslatedBox d n y)

Uses 3 · Used by 1

Statement usesSite of the hypercubic lattice · Hypercubic lattice \(\mathbb{Z}^d\) · Translated box \(\Lambda_n - y\)

Used byMean-field lower bound for the spontaneous magnetization

DefinitionMembership of a doubled-box site in a translated box#✓fully proved

A site of Λ_{2n} lies in Λ_n - y.

def sctTranslatedInDouble (d n : ℕ) (y : sctBox d n) (z : sctBox d (2 * n)) : Prop :=
  z.1 ∈ sctTranslatedBox d n y.1

Uses 4 · Used by 2

Statement usesSite of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice · Box \(\Lambda_n\) as a type · Translated box \(\Lambda_n - y\)

Used byMean-field lower bound for the spontaneous magnetization · Translated box as a subtype of the doubled box

DefinitionTranslated box as a subtype of the doubled box#✓fully proved

For y ∈ Λ_n, Λ_n - y is equivalent to the subtype of Λ_{2n} of sites lying in it.

noncomputable def sctTranslatedInDoubleEquiv (d n : ℕ) (y : sctBox d n) :
    {z : Site d // z ∈ sctTranslatedBox d n y.1} ≃
      {z : sctBox d (2 * n) // sctTranslatedInDouble d n y z} where
  toFun z := ⟨⟨z.1, sct_translate_box_subset_double y.2 z.2⟩, z.2⟩
  invFun z := ⟨z.1.1, z.2⟩
  left_inv z := by ext i; rfl
  right_inv z := by ext i; rfl

Uses 5 · Used by 1

Statement usesSite of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice · Box \(\Lambda_n\) as a type · Translated box \(\Lambda_n - y\) · Membership of a doubled-box site in a translated box

Used byMean-field lower bound for the spontaneous magnetization

DefinitionFree-boundary site magnetization in a box#✓fully proved

The free-boundary magnetization ⟨σ_x⟩_{Λ_n, β, h} at a site x ∈ Λ_n.

noncomputable def sctBoxMag (d : ℕ) (β h : ℝ) (n : ℕ) (x : sctBox d n) : ℝ :=
  isingExpectation (sctBoxGraph d n) β h (fun s => spin s x)

Uses 8 · Used by 5

Statement usesConfiguration space of a statistical-mechanics model · Vertices of the box \((-n, n)^d\) · Finite-volume Ising expectation · Spin of a configuration at a site · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice · Box \(\Lambda_n\) as a type · Nearest-neighbour graph on a box

Used byOrigin–site covariance in a box · Finite-volume mean-field inequality for the Ising model · Minimal origin-to-site magnetization ratio in a box · Mean-field lower bound for the spontaneous magnetization · Origin magnetization in a box

DefinitionOrigin magnetization in a box#✓fully proved

The origin magnetization ⟨σ_0⟩_{Λ_n, β, h}.

noncomputable def sctOriginMag (d : ℕ) (β h : ℝ) (n : ℕ) : ℝ :=
  sctBoxMag d β h n (sctBoxOrigin d n)

Uses 2 · Used by 10

Statement usesFree-boundary site magnetization in a box · Origin as a site of a box

Used byOrigin–site covariance in a box · Finite-volume mean-field inequality for the Ising model · Infinite-volume magnetization in a field as a supremum over boxes · Minimal origin-to-site magnetization ratio in a box · Mean-field lower bound for the spontaneous magnetization · Box mean-field function \(\beta^2(1 - \langle\sigma_0\rangle^2)\) · \(\beta\)-derivative of the box mean-field function · Error term bounding the derivative of the box mean-field function · \(\beta\)-derivative of the origin magnetization in a box · \(\beta\)-derivative of the squared origin magnetization in a box

DefinitionAll sites of a box#✓fully proved

All sites of Λ_n.

noncomputable def sctBoxSites (d n : ℕ) : Finset (sctBox d n) := Finset.univ

Uses 3 · Used by 3

Statement usesSite of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice · Box \(\Lambda_n\) as a type

Used byFinite-volume mean-field inequality for the Ising model · Minimal origin-to-site magnetization ratio in a box · Mean-field lower bound for the spontaneous magnetization

DefinitionMinimal origin-to-site magnetization ratio in a box#✓fully proved

The minimal ratio min_{x ∈ Λ_n} ⟨σ_0⟩_{Λ_n}/⟨σ_x⟩_{Λ_n}.

noncomputable def sctLatticeC (d : ℕ) (β h : ℝ) (n : ℕ) : ℝ :=
  sct_cInfDep (sctBox d) (sctOriginMag d β h) (sctBoxSites d)
    (sctBoxMag d β h) (sctBoxSites_nonempty d) n

Uses 9 · Used by 3

Statement usesVertices of the box \((-n, n)^d\) · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice · Box \(\Lambda_n\) as a type · Free-boundary site magnetization in a box · Origin as a site of a box · All sites of a box · Origin magnetization in a box · Minimal magnetization ratio for \(n\)-dependent site types

Used byFinite-volume mean-field inequality for the Ising model · Mean-field lower bound for the spontaneous magnetization · Error term bounding the derivative of the box mean-field function

DefinitionOrigin–site covariance in a box#✓fully proved

The covariance ⟨σ_0σ_x⟩_{Λ_n} - ⟨σ_0⟩_{Λ_n}⟨σ_x⟩_{Λ_n} in the box at (β, h).

noncomputable def sctBoxCovariance (d : ℕ) (beta h : ℝ) (n : ℕ)
    (x : sctBox d n) : ℝ :=
  isingExpectation (sctBoxGraph d n) beta h
      (fun s => spin s (sctBoxOrigin d n) * spin s x) -
    sctOriginMag d beta h n * sctBoxMag d beta h n x

Uses 11 · Used by 3

Statement usesConfiguration space of a statistical-mechanics model · Vertices of the box \((-n, n)^d\) · Finite-volume Ising expectation · Spin of a configuration at a site · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice · Box \(\Lambda_n\) as a type · Nearest-neighbour graph on a box · Free-boundary site magnetization in a box · Origin as a site of a box · Origin magnetization in a box

Used byBoundary covariance error · Mean-field lower bound for the spontaneous magnetization · Covariance sum over the outer layer

DefinitionExterior neighbours of a site#✓fully proved

The lattice neighbours of x outside Λ_n.

noncomputable def sctExteriorNeighbours (d n : ℕ) (x : Site d) : Finset (Site d) :=
  ((hypercubicLattice d).neighborFinset x).filter (fun y => y ∉ box d n)

Uses 7 · Used by 3

Statement usesNearest neighbours in \(\mathbb{Z}^d\) · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice · Nearest neighbours of a lattice site · Neighbour of a site in a coordinate direction · Hypercubic lattice \(\mathbb{Z}^d\) · Shift of a site along a coordinate

Used byBoundary covariance error · Pairs of a box site and an outside lattice neighbour · Mean-field lower bound for the spontaneous magnetization

DefinitionBoundary covariance error#✓fully proved

The boundary error ∑_{x ∈ Λ_n} #(exterior neighbours of x) · Cov(σ_0, σ_x).

noncomputable def sctBoundaryCovarianceError (d : ℕ) (beta h : ℝ) (n : ℕ) : ℝ :=
  ∑ x : sctBox d n,
    ((sctExteriorNeighbours d n x.1).card : ℝ) * sctBoxCovariance d beta h n x

Uses 5 · Used by 2

Statement usesSite of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice · Box \(\Lambda_n\) as a type · Origin–site covariance in a box · Exterior neighbours of a site

Used byMean-field lower bound for the spontaneous magnetization · Error term bounding the derivative of the box mean-field function

DefinitionCovariance sum over the outer layer#✓fully proved

The sum of Cov(σ_0, σ_x) over the outer layer Λ_n \ Λ_{n-1}.

noncomputable def sctOuterCovarianceSum (d : ℕ) (beta h : ℝ) (n : ℕ) : ℝ :=
  ∑ x : sctBox d n,
    if x.1 ∈ box d (n - 1) then 0 else sctBoxCovariance d beta h n x

Uses 4 · Used by 1

Statement usesSite of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice · Box \(\Lambda_n\) as a type · Origin–site covariance in a box

Used byMean-field lower bound for the spontaneous magnetization

DefinitionField switched off on the outer layer#✓fully proved

The site field equal to βh on Λ_{n-1} and 0 on the outer layer.

def sctInnerField (d : ℕ) (beta h : ℝ) (n : ℕ) (x : sctBox d n) : ℝ :=
  if x.1 ∈ box d (n - 1) then beta * h else 0

Uses 3 · Used by 2

Statement usesSite of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice · Box \(\Lambda_n\) as a type

Used byOrigin magnetization with the outer-layer field switched off · Mean-field lower bound for the spontaneous magnetization

DefinitionOuter-layer indicator as a field direction#✓fully proved

The indicator of the outer layer Λ_n \ Λ_{n-1}, used as a field direction.

def sctOuterDirection (d n : ℕ) (x : sctBox d n) : ℝ :=
  if x.1 ∈ box d (n - 1) then 0 else 1

Uses 3 · Used by 1

Statement usesSite of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice · Box \(\Lambda_n\) as a type

Used byMean-field lower bound for the spontaneous magnetization

DefinitionOrigin magnetization with the outer-layer field switched off#✓fully proved

The origin magnetization in Λ_n with the field switched off on the outer layer.

noncomputable def sctInnerFieldMag (d : ℕ) (beta h : ℝ) (n : ℕ) : ℝ :=
  expJ (sctBoxGraph d n).edgeFinset (fun _ => beta)
    (sctInnerField d beta h n) (fun s => spin s (sctBoxOrigin d n))

Uses 10 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Vertices of the box \((-n, n)^d\) · Spin of a configuration at a site · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice · Gibbs expectation with inhomogeneous couplings and site fields · Box \(\Lambda_n\) as a type · Nearest-neighbour graph on a box · Origin as a site of a box · Field switched off on the outer layer

Used byMean-field lower bound for the spontaneous magnetization

DefinitionCoupling restricted to the edges inside a set#✓fully proved

The coupling J restricted to the edges inside S (zero on all other edges).

noncomputable def couplingIn (J : Sym2 V → ℝ) (S : Finset V) : Sym2 V → ℝ :=
  fun e => if edgeInside S e then J e else 0

Uses 1 · Used by 9

Statement usesUnordered pair inside a set

Used byCluster lower bound for double-current sums · Four-source lower bound for the pattern sum · Lower mass of the four-source bound · Finite-volume mean-field inequality for the Ising model · Mean-field lower bound for the spontaneous magnetization · Simon–Lieb inequality in the infinite-volume plus state · Simon weight of a boundary pair · Simon–Lieb weight · Simon–Lieb inequality on a finite graph

DefinitionEdge lying inside a set#✓fully proved

An edge of G lies inside S.

def isIn (S : Finset V) : (↥G.edgeFinset) → Prop := fun i => edgeInside S (i : Sym2 V)

Uses 1 · Used by 11

Statement usesUnordered pair inside a set

Used byExtension by zero of a current inside a set · Extension by zero of a current outside a set · Outside part of a gated double-current summand · Cluster lower bound for double-current sums · Outside summand of a gated double-current sum · Inside weight with prescribed sources · Four-source lower bound for the pattern sum · Regrouping a split pair of currents · Reassembly of a current from its inside and outside parts · Finite-volume mean-field inequality for the Ising model · Mean-field lower bound for the spontaneous magnetization

DefinitionExtension by zero of a current inside a set#✓fully proved

Extension by zero of a current on the edges inside S to all edges of G.

noncomputable def aFull (S : Finset V) (a : {i : ↥G.edgeFinset // isIn G S i} → ℕ) :
    ↥G.edgeFinset → ℕ := fun i => if h : isIn G S i then a ⟨i, h⟩ else 0

Uses 2 · Used by 5

Statement usesUnordered pair inside a set · Edge lying inside a set

Used byCluster lower bound for double-current sums · Inside weight with prescribed sources · Four-source lower bound for the pattern sum · Finite-volume mean-field inequality for the Ising model · Mean-field lower bound for the spontaneous magnetization

DefinitionExtension by zero of a current outside a set#✓fully proved

Extension by zero of a current on the edges not inside S to all edges of G.

noncomputable def bFull (S : Finset V) (b : {i : ↥G.edgeFinset // ¬ isIn G S i} → ℕ) :
    ↥G.edgeFinset → ℕ := fun i => if h : isIn G S i then 0 else b ⟨i, h⟩

Uses 2 · Used by 6

Statement usesUnordered pair inside a set · Edge lying inside a set

Used byOutside part of a gated double-current summand · Cluster lower bound for double-current sums · Outside summand of a gated double-current sum · Four-source lower bound for the pattern sum · Finite-volume mean-field inequality for the Ising model · Mean-field lower bound for the spontaneous magnetization

DefinitionReassembly of a current from its inside and outside parts#✓fully proved

Reassembly of a current from its parts inside and outside S.

noncomputable def reEdge (S : Finset V)
    (ab : ({i : ↥G.edgeFinset // isIn G S i} → ℕ) × ({i : ↥G.edgeFinset // ¬ isIn G S i} → ℕ)) :
    ↥G.edgeFinset → ℕ := (Equiv.piEquivPiSubtypeProd (isIn G S) (fun _ => ℕ)).symm ab

Uses 2 · Used by 4

Statement usesUnordered pair inside a set · Edge lying inside a set

Used byCluster lower bound for double-current sums · Four-source lower bound for the pattern sum · Finite-volume mean-field inequality for the Ising model · Mean-field lower bound for the spontaneous magnetization

DefinitionOutside summand of a gated double-current sum#✓fully proved

The summand of the outside double-current sum: weights of the outside part and of the second current, gated by P on their sum.

noncomputable def contextSummand (β : ℝ) (J : Sym2 V → ℝ) (S : Finset V) (P : Current V → Prop)
    [DecidablePred P]
    (bn : ({i : ↥G.edgeFinset // ¬ isIn G S i} → ℕ) × (↥G.edgeFinset → ℕ)) : ℝ :=
  (if sources G (ofEdgeFun G (bFull G S bn.1)) = ∅ then weight G β J (ofEdgeFun G (bFull G S bn.1))
      else 0)
    * (if sources G (ofEdgeFun G bn.2) = ∅ then weight G β J (ofEdgeFun G bn.2) else 0)
    * (if P (fun e => ofEdgeFun G (bFull G S bn.1) e + ofEdgeFun G bn.2 e) then 1 else 0)

Uses 6 · Used by 3

Statement usesCurrent: a multiplicity in \(\mathbb{N}\) for each unordered pair · Extension by zero of a current outside a set · Edge lying inside a set · Extension of an edge function to a current · Sources of a current · Weight of a random current

Used byFour-source lower bound for the pattern sum · Finite-volume mean-field inequality for the Ising model · Mean-field lower bound for the spontaneous magnetization

DefinitionInside weight with prescribed sources#✓fully proved

The weight of the inside part of a current, restricted to source set A.

noncomputable def factorSummand (β : ℝ) (J : Sym2 V → ℝ) (S : Finset V) (A : Finset V)
    (a : {i : ↥G.edgeFinset // isIn G S i} → ℕ) : ℝ :=
  if sources G (ofEdgeFun G (aFull G S a)) = A then weight G β J (ofEdgeFun G (aFull G S a)) else 0

Uses 5 · Used by 4

Statement usesExtension by zero of a current inside a set · Edge lying inside a set · Extension of an edge function to a current · Sources of a current · Weight of a random current

Used byCluster lower bound for double-current sums · Four-source lower bound for the pattern sum · Finite-volume mean-field inequality for the Ising model · Mean-field lower bound for the spontaneous magnetization

DefinitionVertices not connected to a vertex by positive current#✓fully proved

The set of vertices not connected to g by edges carrying positive current.

noncomputable def notConnComp (m : Current V) (g : V) : Finset V :=
  Finset.univ.filter (fun v => ¬ CurrentConnected G m g v)

Uses 2 · Used by 7

Statement usesCurrent: a multiplicity in \(\mathbb{N}\) for each unordered pair · Connectivity through edges carrying positive current

Used byCluster lower bound for double-current sums · Random-current cut mass of a vertex set · Four-source lower bound for the pattern sum · Lower mass of the four-source bound · Lower mass in the degenerate case \(x = o\) · Finite-volume mean-field inequality for the Ising model · Mean-field lower bound for the spontaneous magnetization

DefinitionOutside part of a gated double-current summand#✓fully proved

The outside part of a double-current summand: weights of the two outside currents with sources B and D, gated by P.

noncomputable def claim1Context (β : ℝ) (J : Sym2 V → ℝ) (S : Finset V)
    (P : Current V → Prop) [DecidablePred P] (B D : Finset V)
    (bd : ({i : ↥G.edgeFinset // ¬ isIn G S i} → ℕ) ×
      ({i : ↥G.edgeFinset // ¬ isIn G S i} → ℕ)) : ℝ :=
  (if sources G (ofEdgeFun G (bFull G S bd.1)) = B
      then weight G β J (ofEdgeFun G (bFull G S bd.1)) else 0) *
    (if sources G (ofEdgeFun G (bFull G S bd.2)) = D
      then weight G β J (ofEdgeFun G (bFull G S bd.2)) else 0) *
    (if P (fun e => ofEdgeFun G (bFull G S bd.1) e +
        ofEdgeFun G (bFull G S bd.2) e) then 1 else 0)

Uses 6 · Used by 3

Statement usesCurrent: a multiplicity in \(\mathbb{N}\) for each unordered pair · Extension by zero of a current outside a set · Edge lying inside a set · Extension of an edge function to a current · Sources of a current · Weight of a random current

Used byCluster lower bound for double-current sums · Four-source lower bound for the pattern sum · Finite-volume mean-field inequality for the Ising model

DefinitionRegrouping a split pair of currents#✓fully proved

Regrouping a pair of currents split along S into the pair of inside parts and the pair of outside parts.

noncomputable def pairCutEquiv (S : Finset V) :
    ((({i : ↥G.edgeFinset // isIn G S i} → ℕ) ×
        ({i : ↥G.edgeFinset // ¬ isIn G S i} → ℕ)) ×
      (({i : ↥G.edgeFinset // isIn G S i} → ℕ) ×
        ({i : ↥G.edgeFinset // ¬ isIn G S i} → ℕ))) ≃
    ((({i : ↥G.edgeFinset // isIn G S i} → ℕ) ×
        ({i : ↥G.edgeFinset // isIn G S i} → ℕ)) ×
      (({i : ↥G.edgeFinset // ¬ isIn G S i} → ℕ) ×
        ({i : ↥G.edgeFinset // ¬ isIn G S i} → ℕ))) where
  toFun p := ((p.1.1, p.2.1), (p.1.2, p.2.2))
  invFun p := ((p.1.1, p.2.1), (p.1.2, p.2.2))
  left_inv := by rintro ⟨⟨a, b⟩, ⟨c, d⟩⟩; rfl
  right_inv := by rintro ⟨⟨a, c⟩, ⟨b, d⟩⟩; rfl

Uses 1 · Used by 3

Statement usesEdge lying inside a set

Used byCluster lower bound for double-current sums · Four-source lower bound for the pattern sum · Finite-volume mean-field inequality for the Ising model

DefinitionGated double-current sum over edge-indexed currents#✓fully proved

The gated double-current sum ∑_{∂n₁ = A, ∂n₂ = B} w(n₁) w(n₂) 1_{P(n₁ + n₂)} over edge-indexed currents.

noncomputable def gatedSourcePairSum (β : ℝ) (J : Sym2 V → ℝ)
    (A B : Finset V) (P : Current V → Prop) [DecidablePred P] : ℝ :=
  ∑' pq : (↥G.edgeFinset → ℕ) × (↥G.edgeFinset → ℕ),
    (if sources G (ofEdgeFun G pq.1) = A then weight G β J (ofEdgeFun G pq.1) else 0) *
      (if sources G (ofEdgeFun G pq.2) = B then weight G β J (ofEdgeFun G pq.2) else 0) *
      (if P (ofEdgeFun G (fun e => pq.1 e + pq.2 e)) then 1 else 0)

Uses 4 · Used by 8

Statement usesCurrent: a multiplicity in \(\mathbb{N}\) for each unordered pair · Extension of an edge function to a current · Sources of a current · Weight of a random current

Used byCluster lower bound for double-current sums · Random-current cut mass of a vertex set · Four-source lower bound for the pattern sum · Lower mass of the four-source bound · Four-source double-current sum with a connection pattern · Lower mass in the degenerate case \(x = o\) · Finite-volume mean-field inequality for the Ising model · Mean-field lower bound for the spontaneous magnetization

DefinitionEdges of a graph inside a set#✓fully proved

The edges of G inside S.

def edgesIn (S : Finset V) : Finset (Sym2 V) :=
  G.edgeFinset.filter (edgeInside S)

Uses 1 · Used by 6

Statement usesUnordered pair inside a set

Used byCluster lower bound for double-current sums · Four-source lower bound for the pattern sum · Subgraph of edges inside a vertex set · Finite-volume mean-field inequality for the Ising model · Mean-field lower bound for the spontaneous magnetization · Simon–Lieb inequality in the infinite-volume plus state

LemmaCluster lower bound for double-current sums#✓fully proved

The cluster lower bound: for β, J ≥ 0, o, x ∉ S, y, g ∈ S, y ≠ g and ⟨σ_yσ_g⟩ > 0, the double-current sum with sources {y, g} ∆ {o, x} and ∅ on the event that the vertices not connected to o form S is at least ⟨σ_yσ_g⟩⁻¹ times the sum with sources {o, x} and ∅ on the same event and y ↔ g. Reference: M. Aizenman, D. J. Barsky, R. Fernández, "The phase transition in a general class of Ising-type models is sharp", J. Stat. Phys. 47 (1987) 343–374.

lemma claim1_ising_of_expectation_pos (β : ℝ) (J : Sym2 V → ℝ)
    (hβ : 0 ≤ β) (hJ : ∀ e, 0 ≤ J e)
    (S : Finset V) (o x y g : V)
    (ho : o ∉ S) (hx : x ∉ S) (hy : y ∈ S) (hg : g ∈ S)
    (hyg : y ≠ g) (hm : 0 < expectationJ G β J {y, g}) :
    gatedSourcePairSum G β J (({y, g} : Finset V) ∆ {o, x}) ∅
        (fun m => notConnComp G m o = S) ≥
      (expectationJ G β J {y, g})⁻¹ * gatedSourcePairSum G β J {o, x} ∅
        (fun m => notConnComp G m o = S ∧ CurrentConnected G m y g)

Uses 49

Statement usesCurrent: a multiplicity in \(\mathbb{N}\) for each unordered pair · Connectivity through edges carrying positive current · Correlation function with couplings · Gated double-current sum over edge-indexed currents · Vertices not connected to a vertex by positive current

Proof usesConfiguration space of a statistical-mechanics model · Sourced current sum as correlation times sourceless sum · Bond variable of an unordered pair · Spin of a configuration at a site · Spin value of a Boolean · Spin product over a vertex set · Edge copies of a current · Endpoints of an edge copy · Profile of a set of edge copies · Subsets of a sigma type as families of fibre subsets · Current with no edge crossing a set's boundary · Adjacency through an edge of a multigraph edge set · Connectivity in a multigraph edge set · Degree of a vertex in a multigraph edge set · Sources of a multigraph edge set · Switching lemma for multigraph currents · Partition function with inhomogeneous couplings and site fields · Extension by zero of a current inside a set · Extension by zero of a current outside a set · Boltzmann weight with couplings · Outside part of a gated double-current summand · Coupling restricted to the edges inside a set · Subgraph of edges carrying positive current · Current sum with prescribed sources · Random-current representation · Unordered pair inside a set · Edges of a graph inside a set · Gibbs expectation with inhomogeneous couplings and site fields · Inside weight with prescribed sources · Term of the exponential expansion of an edge weight · Griffiths monotonicity of correlations in the edge set · Incident flux of a current at a vertex · Edge lying inside a set · Extension of an edge function to a current · Regrouping a split pair of currents · Reparametrizing pairs of functions by their sum and one summand · Partition function with couplings · Reassembly of a current from its inside and outside parts · Restriction of a current to a set · Sources of a current · Single-edge current weight \((\beta J_e)^k/k!\) · Boltzmann weight with inhomogeneous couplings and site fields · Weight of a random current · Current weights are nonnegative for nonnegative \(\beta\) and couplings

DefinitionFour-source double-current sum with a connection pattern#✓fully proved

The double-current sum with sources {o, g} ∆ {x, y} and ∅ restricted to o ↔ x, y ↔ g and o ↮ g in the summed current.

noncomputable def isingDeltaPairSum (β : ℝ) (J : Sym2 V → ℝ)
    (o x y g : V) : ℝ :=
  gatedSourcePairSum G β J (({o, g} : Finset V) ∆ {x, y}) ∅
    (fun m => CurrentConnected G m o x ∧ CurrentConnected G m y g ∧
      ¬ CurrentConnected G m o g)

Uses 3 · Used by 2

Statement usesCurrent: a multiplicity in \(\mathbb{N}\) for each unordered pair · Connectivity through edges carrying positive current · Gated double-current sum over edge-indexed currents

Used byFour-source lower bound for the pattern sum · Finite-volume mean-field inequality for the Ising model

DefinitionLower mass of the four-source bound#✓fully proved

The lower mass ∑_S ⟨σ_oσ_x⟩_{J|S} · Z(∂ = ∅, C(g)ᶜ = S) over sets S containing o, x and not y, g, where C(g)ᶜ is the set of vertices not connected to g.

noncomputable def isingDeltaLowerMass (β : ℝ) (J : Sym2 V → ℝ)
    (o x y g : V) : ℝ :=
  ∑ S : Finset V,
    if o ∈ S ∧ x ∈ S ∧ y ∉ S ∧ g ∉ S then
      expectationJ G β (couplingIn J S) {o, x} *
        gatedSourcePairSum G β J ∅ ∅ (fun m => notConnComp G m g = S)
    else 0

Uses 5 · Used by 2

Statement usesCurrent: a multiplicity in \(\mathbb{N}\) for each unordered pair · Coupling restricted to the edges inside a set · Correlation function with couplings · Gated double-current sum over edge-indexed currents · Vertices not connected to a vertex by positive current

Used byFour-source lower bound for the pattern sum · Finite-volume mean-field inequality for the Ising model

DefinitionLower mass in the degenerate case \(x = o\)#✓fully proved

The lower mass in the degenerate case x = o: ∑_S Z(∂ = ∅, C(g)ᶜ = S) over S ∋ o with y, g ∉ S.

noncomputable def isingDeltaSelfLowerMass (β : ℝ) (J : Sym2 V → ℝ)
    (o y g : V) : ℝ :=
  ∑ S : Finset V,
    if o ∈ S ∧ y ∉ S ∧ g ∉ S then
      gatedSourcePairSum G β J ∅ ∅ (fun m => notConnComp G m g = S)
    else 0

Uses 3 · Used by 1

Statement usesCurrent: a multiplicity in \(\mathbb{N}\) for each unordered pair · Gated double-current sum over edge-indexed currents · Vertices not connected to a vertex by positive current

Used byFinite-volume mean-field inequality for the Ising model

LemmaFour-source lower bound for the pattern sum#✓fully proved

The four-source lower bound: for β ≥ 0, J ≥ 0, distinct o, x, y, g and ⟨σ_yσ_g⟩ > 0, the pattern sum Δ(o, x, y, g) is at least ⟨σ_yσ_g⟩⁻¹ times the lower mass. Reference: M. Aizenman, D. J. Barsky, R. Fernández, "The phase transition in a general class of Ising-type models is sharp", J. Stat. Phys. 47 (1987) 343–374.

lemma ising_delta_bound (β : ℝ) (J : Sym2 V → ℝ)
    (hβ : 0 ≤ β) (hJ : ∀ e, 0 ≤ J e)
    {o x y g : V}
    (hox : o ≠ x) (hoy : o ≠ y) (hog : o ≠ g)
    (hxy : x ≠ y) (hxg : x ≠ g) (hyg : y ≠ g)
    (hmy : 0 < expectationJ G β J {y, g}) :
    isingDeltaPairSum G β J o x y g ≥
      (expectationJ G β J {y, g})⁻¹ * isingDeltaLowerMass G β J o x y g

Uses 64

Statement usesCorrelation function with couplings · Lower mass of the four-source bound · Four-source double-current sum with a connection pattern

Proof usesConfiguration space of a statistical-mechanics model · Current as a multiplicity on unordered pairs · Sourced current sum as correlation times sourceless sum · Adjacency through an edge of an edge set · Bond variable of an unordered pair · Cluster of a site in an edge set · Connectivity through the edges of an edge set · Degree of a site in an edge set · Incident flux of a current on an edge set · Edges of an edge set with odd multiplicity · Edges of an edge set with positive multiplicity · Source set of a current on an edge set · Spin of a configuration at a site · Spin value of a Boolean · Spin product over a vertex set · Odd-degree sites of an edge set · Current: a multiplicity in \(\mathbb{N}\) for each unordered pair · Connectivity through edges carrying positive current · Edge copies of a current · Endpoints of an edge copy · Profile of a set of edge copies · Subsets of a sigma type as families of fibre subsets · Current with no edge crossing a set's boundary · Adjacency through an edge of a multigraph edge set · Odd-degree vertices in a cluster · Cluster of a vertex in a multigraph edge set · Connectivity in a multigraph edge set · Degree of a vertex in a multigraph edge set · Sources of a multigraph edge set · Switching lemma for multigraph currents · Partition function with inhomogeneous couplings and site fields · Extension by zero of a current inside a set · Extension by zero of a current outside a set · Boltzmann weight with couplings · Outside part of a gated double-current summand · Outside summand of a gated double-current sum · Coupling restricted to the edges inside a set · Subgraph of edges carrying positive current · Current sum with prescribed sources · Random-current representation · Unordered pair inside a set · Edges of a graph inside a set · Gibbs expectation with inhomogeneous couplings and site fields · Inside weight with prescribed sources · Term of the exponential expansion of an edge weight · Gated double-current sum over edge-indexed currents · Griffiths monotonicity of correlations in the edge set · Incident flux of a current at a vertex · Edge lying inside a set · Vertices not connected to a vertex by positive current · Extension of an edge function to a current · Regrouping a split pair of currents · Reparametrizing pairs of functions by their sum and one summand · Partition function with couplings · Reassembly of a current from its inside and outside parts · Restriction of a current to a set · Sources of a current · Single-edge current weight \((\beta J_e)^k/k!\) · Boltzmann weight with inhomogeneous couplings and site fields · Weight of a random current · Current weights are nonnegative for nonnegative \(\beta\) and couplings

DefinitionBond energy of a configuration#✓fully proved

The bond energy ∑_{e ∈ E(G)} σ_e of a configuration, where σ_{xy} = σ_x σ_y.

noncomputable def sdrBondEnergy (s : ConfigSpace V) : ℝ := ∑ e ∈ G.edgeFinset, bond s e

Uses 2 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Bond variable of an unordered pair

Used byRandom-current form of the \(\beta\)-derivative of the magnetization

DefinitionSwitching gap of a current#✓fully proved

The switching gap of a current m with sources A: the number of sub-currents (subsets of edge copies) with sources A minus the number with sources A ∆ {u, v}; zero if the sources of m are not A.

noncomputable def hca_gap (m : ↥H.edgeFinset → ℕ) (A : Finset V) (u v : V) : ℝ :=
  if RandomCurrent.sources (endsM H m) univ = A then
    ((#((univ : Finset (Copy H m)).powerset.filter
        (fun K => RandomCurrent.sources (endsM H m) K = A)) : ℝ)
      - #((univ : Finset (Copy H m)).powerset.filter
        (fun K => RandomCurrent.sources (endsM H m) K = A ∆ {u, v})))
   else 0

Uses 3 · Used by 2

Statement usesEdge copies of a current · Endpoints of an edge copy · Sources of a multigraph edge set

Used byGap-weighted current sum restricted to a predicate · Finite-volume mean-field inequality for the Ising model

DefinitionGap-weighted current sum restricted to a predicate#✓fully proved

The current sum ∑_m 1_{P m} · gap(m) · w(m) of the switching gap weighted by the current weight, restricted to currents satisfying P.

noncomputable def hca_pairSum (β : ℝ) (J : Sym2 V → ℝ) (A : Finset V) (u v : V)
    (P : (↥H.edgeFinset → ℕ) → Prop) : ℝ :=
  ∑' m : ↥H.edgeFinset → ℕ,
    (if P m then (1 : ℝ) else 0) * hca_gap H m A u v * weight H β J (ofEdgeFun H m)

Uses 3 · Used by 1

Statement usesSwitching gap of a current · Extension of an edge function to a current · Weight of a random current

Used byFinite-volume mean-field inequality for the Ising model

DefinitionGhost source set of a bond covariance#✓fully proved

The ghost-graph source set {ghost} ∪ ({o} ∆ {x, y}) attached to the bond covariance Cov(σ_o, σ_xσ_y).

noncomputable def hcaBondSource (o : V) : Sym2 V -> Finset (Option V) :=
  Sym2.lift <| by
    refine ⟨fun x y => insert none ((({o} : Finset V) ∆ {x, y}).map someEmb), ?_⟩
    intro x y
    simp [Finset.pair_comm]

Uses 1 · Used by 3

Statement usesEmbedding of vertices into the ghost graph

Used byBond term \(\Delta_e\) of the magnetization derivative · Finite-volume mean-field inequality for the Ising model · Bond term: ghost-graph disconnection sum for a bond covariance

DefinitionBond term \(\Delta_e\) of the magnetization derivative#✓fully proved

The bond term Δ_e: the ghost-graph double-current sum with sources hcaBondSource o e and ∅ in which o is not connected to the ghost.

noncomputable def hcaBondDelta (β h : ℝ) (o : V) (e : Sym2 V) : ℝ :=
  sourcePairDisconnSum (withGhost G) β (ghostCoupling h β (fun _ => 1))
    (hcaBondSource o e) ∅ (some o) none

Uses 4 · Used by 2

Statement usesCoupling on the ghost graph with uniform field · Double-current sum restricted to disconnection · Ghost source set of a bond covariance · Graph with a ghost vertex joined to every site

Used byRandom-current form of the \(\beta\)-derivative of the magnetization · Finite-volume mean-field inequality for the Ising model

DefinitionGhost source set of a field covariance#✓fully proved

The ghost-graph source set {o} ∆ {z} attached to the field covariance Cov(σ_o, σ_z).

noncomputable def hcaFieldSource (o z : V) : Finset (Option V) :=
  ((({o} : Finset V) ∆ {z}).map someEmb)

Uses 1 · Used by 3

Statement usesEmbedding of vertices into the ghost graph

Used byField term \(\Delta_z\) of the magnetization derivative · Finite-volume mean-field inequality for the Ising model · Field term: ghost-graph disconnection sum for a site covariance

DefinitionField term \(\Delta_z\) of the magnetization derivative#✓fully proved

The field term Δ_z: the ghost-graph double-current sum with sources hcaFieldSource o z and ∅ in which o is not connected to the ghost.

noncomputable def hcaFieldDelta (β h : ℝ) (o z : V) : ℝ :=
  sourcePairDisconnSum (withGhost G) β (ghostCoupling h β (fun _ => 1))
    (hcaFieldSource o z) ∅ (some o) none

Uses 4 · Used by 2

Statement usesCoupling on the ghost graph with uniform field · Double-current sum restricted to disconnection · Ghost source set of a field covariance · Graph with a ghost vertex joined to every site

Used byRandom-current form of the \(\beta\)-derivative of the magnetization · Finite-volume mean-field inequality for the Ising model

LemmaRandom-current form of the \(\beta\)-derivative of the magnetization#✓fully proved

The β-derivative of the magnetization in random-current form: ∂_β ⟨σ_o⟩_{β,h} = Z⁻² (∑_{e ∈ E(G)} Δ_e + h ∑_z Δ_z), with Z the sourceless ghost-graph current sum. Reference: M. Aizenman, D. J. Barsky, R. Fernández, "The phase transition in a general class of Ising-type models is sharp", J. Stat. Phys. 47 (1987) 343–374.

lemma hca_deriv_magnetization_eq_currentDelta (β h : ℝ) (o : V) :
    HasDerivAt (fun β => isingExpectation G β h (fun s => Ising.spin s o))
      ((1 / (currentSum (withGhost G) β (ghostCoupling h β (fun _ => 1)) ∅) ^ 2) *
        ((∑ e ∈ G.edgeFinset, hcaBondDelta G β h o e)
          + h * ∑ z, hcaFieldDelta G β h o z)) β

Uses 48 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Finite-volume Ising expectation · Spin of a configuration at a site · Coupling on the ghost graph with uniform field · Bond term \(\Delta_e\) of the magnetization derivative · Field term \(\Delta_z\) of the magnetization derivative · Current sum with prescribed sources · Graph with a ghost vertex joined to every 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 · Spin value of a Boolean · Spin product over a vertex set · Current: a multiplicity in \(\mathbb{N}\) for each unordered pair · Connectivity through edges carrying positive current · Random-current representation with a field for even source sets · Global spin flip · Ghost edges · Graph edges as ghost-graph edges · Embedding of vertices into the ghost graph · Edge copies of a current · Endpoints of an edge copy · Profile of a set of edge copies · Subsets of a sigma type as families of fibre subsets · Double-current sum restricted to disconnection · Adjacency through an edge of a multigraph edge set · Cluster of a vertex in a multigraph edge set · Connectivity in a multigraph edge set · Degree of a vertex in a multigraph edge set · Sources of a multigraph edge set · Boltzmann weight with couplings · Subgraph of edges carrying positive current · Random-current representation · Correlation function with couplings · Term of the exponential expansion of an edge weight · Incident flux of a current at a vertex · Extension of an edge function to a current · Reparametrizing pairs of functions by their sum and one summand · Partition function with couplings · Bond energy of a configuration · Double-current sum with prescribed sources · Sources of a current · Total spin of a configuration · Single-edge current weight \((\beta J_e)^k/k!\) · Weight of a random current

Used byFinite-volume mean-field inequality for the Ising model

LemmaIntegrated mean-field lower bound from \(m(\beta_0) = 0\)#✓fully proved

If (m²)' ≥ (2/β)(1 - m²) above β₀ > 0, m(β₀) = 0 and m ≥ 0, then m(β) ≥ √(1 - (β₀/β)²) for β ≥ β₀. See also meanfield_lower_bound_of_initial_nonneg, which drops the hypothesis m(β₀) = 0.

lemma meanfield_lower_bound (β₀ : ℝ) (hβ₀ : 0 < β₀) (m : ℝ → ℝ)
    (hdiff : ∀ β ∈ Ici β₀, DifferentiableAt ℝ (fun β => (m β) ^ 2) β)
    (hineq : ∀ β ∈ Ioi β₀, (2 / β) * (1 - (m β) ^ 2) ≤ deriv (fun β => (m β) ^ 2) β)
    (hzero : m β₀ = 0) (hnonneg : ∀ β ∈ Ici β₀, 0 ≤ m β)
    {β : ℝ} (hβ : β₀ ≤ β) :
    Real.sqrt (1 - (β₀ / β) ^ 2) ≤ m β

Used by 1

Used byAbstract form of the sharpness theorem

DefinitionRandom-current cut mass of a vertex set#✓fully proved

The cut mass Z⁻² Z(∂n₁ = ∂n₂ = ∅; {v : v ↮ g in n₁ + n₂} = S), with Z the sourceless current sum.

noncomputable def isingCutMass (beta : ℝ) (J : Sym2 V → ℝ)
    (g : V) (S : Finset V) : ℝ :=
  (currentSum G beta J ∅)⁻¹ ^ 2 *
    gatedSourcePairSum G beta J ∅ ∅
      (fun m => notConnComp G m g = S)

Uses 4 · Used by 3

Statement usesCurrent: a multiplicity in \(\mathbb{N}\) for each unordered pair · Current sum with prescribed sources · Gated double-current sum over edge-indexed currents · Vertices not connected to a vertex by positive current

Used byCut mass of a box set rooted at the field ghost · Finite-volume mean-field inequality for the Ising model · Mean-field lower bound for the spontaneous magnetization

DefinitionVertex subsets as ghost-free subsets of the extended vertex set#✓fully proved

Subsets of V correspond to subsets of V ⊔ {ghost} not containing the ghost.

StatMech.Sharpness.ghostFreeFinsetEquiv · 17 lines

noncomputable def ghostFreeFinsetEquiv :
    Finset V ≃ {S : Finset (Option V) // none ∉ S} :=
  Equiv.ofBijective
    (fun T => (⟨T.map someEmb, by simp⟩ :
      {S : Finset (Option V) // none ∉ S}))
    ⟨by
      intro T U h
      apply Finset.map_injective someEmb
      exact Subtype.ext_iff.mp h,
    by
      intro S
      let T := S.1.preimage some (Set.injOn_of_injective someEmb.injective)
      refine ⟨T, Subtype.ext ?_⟩
      ext z
      cases z with
      | none => simp [S.2]
      | some z => simp [T]; exact Finset.mem_preimage⟩

Uses 1 · Used by 2

Statement usesEmbedding of vertices into the ghost graph

Used byFinite-volume mean-field inequality for the Ising model · Mean-field lower bound for the spontaneous magnetization

DefinitionSubgraph of edges inside a vertex set#✓fully proved

The subgraph of G with the edges inside T.

def localizedGraph (T : Finset V) : SimpleGraph V :=
  SimpleGraph.fromEdgeSet (↑(edgesIn G T) : Set (Sym2 V))

Uses 1 · Used by 3

Statement usesEdges of a graph inside a set

Used byFinite-volume mean-field inequality for the Ising model · Mean-field lower bound for the spontaneous magnetization · Simon–Lieb inequality in the infinite-volume plus state

LemmaIntegrated mean-field lower bound without an initial condition#✓fully proved

If (m²)' ≥ (2/β)(1 - m²) above β₀ > 0 and m ≥ 0, then m(β) ≥ √(1 - (β₀/β)²) for β ≥ β₀. This strengthens meanfield_lower_bound by dropping m(β₀) = 0.

lemma meanfield_lower_bound_of_initial_nonneg
    (β₀ : ℝ) (hβ₀ : 0 < β₀) (m : ℝ → ℝ)
    (hdiff : ∀ β ∈ Ici β₀, DifferentiableAt ℝ (fun β => (m β) ^ 2) β)
    (hineq : ∀ β ∈ Ioi β₀,
      (2 / β) * (1 - (m β) ^ 2) ≤ deriv (fun β => (m β) ^ 2) β)
    (hnonneg : ∀ β ∈ Ici β₀, 0 ≤ m β)
    {β : ℝ} (hβ : β₀ ≤ β) :
    Real.sqrt (1 - (β₀ / β) ^ 2) ≤ m β

DefinitionInfinite-volume magnetization in a field as a supremum over boxes#✓fully proved

The infinite-volume magnetization in field h, the supremum over n of the origin magnetizations in the boxes Λ_n.

noncomputable def sctInfiniteFieldMag (d : ℕ) (beta h : ℝ) : ℝ :=
  ⨆ n : ℕ, sctOriginMag d beta h n

Uses 1 · Used by 3

Statement usesOrigin magnetization in a box

Used byInfinite-volume mean-field function \(\beta^2(1 - m(\beta,h)^2)\) · Mean-field lower bound for the spontaneous magnetization · Zero-field limit of the positive-field magnetization

Definition\(\beta\)-derivative of the origin magnetization in a box#✓fully proved

The β-derivative of the origin magnetization in Λ_n, as the covariance of σ_0 with -H.

noncomputable def sctOriginMagBetaDeriv (d n : ℕ) (h beta : ℝ) : ℝ :=
  isingExpectation (sctBoxGraph d n) beta h
      (fun s => spin s (sctBoxOrigin d n) * negHam (sctBoxGraph d n) h s) -
    sctOriginMag d beta h n *
      isingExpectation (sctBoxGraph d n) beta h (negHam (sctBoxGraph d n) h)

Uses 11 · Used by 2

Statement usesConfiguration space of a statistical-mechanics model · Vertices of the box \((-n, n)^d\) · Finite-volume Ising expectation · Negative Hamiltonian of the Ising model · Spin of a configuration at a site · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice · Box \(\Lambda_n\) as a type · Nearest-neighbour graph on a box · Origin as a site of a box · Origin magnetization in a box

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

Definition\(\beta\)-derivative of the squared origin magnetization in a box#✓fully proved

The β-derivative of the squared origin magnetization.

noncomputable def sctOriginMagSqBetaDeriv (d n : ℕ) (h beta : ℝ) : ℝ :=
  2 * sctOriginMag d beta h n * sctOriginMagBetaDeriv d n h beta

Uses 2 · Used by 2

Statement usesOrigin magnetization in a box · \(\beta\)-derivative of the origin magnetization in a box

Used byMean-field lower bound for the spontaneous magnetization · \(\beta\)-derivative of the box mean-field function

DefinitionBox mean-field function \(\beta^2(1 - \langle\sigma_0\rangle^2)\)#✓fully proved

g_n(β) = β²(1 - ⟨σ_0⟩²_{Λ_n,β,h}).

noncomputable def sctMeanfieldG (d n : ℕ) (h beta : ℝ) : ℝ :=
  beta ^ 2 * (1 - (sctOriginMag d beta h n) ^ 2)

Uses 1 · Used by 1

Statement usesOrigin magnetization in a box

Used byMean-field lower bound for the spontaneous magnetization

Definition\(\beta\)-derivative of the box mean-field function#✓fully proved

The β-derivative of g_n.

noncomputable def sctMeanfieldGDeriv (d n : ℕ) (h beta : ℝ) : ℝ :=
  2 * beta * (1 - (sctOriginMag d beta h n) ^ 2) -
    beta ^ 2 * sctOriginMagSqBetaDeriv d n h beta

Uses 2 · Used by 1

Statement usesOrigin magnetization in a box · \(\beta\)-derivative of the squared origin magnetization in a box

Used byMean-field lower bound for the spontaneous magnetization

DefinitionError term bounding the derivative of the box mean-field function#✓fully proved

The error 2β(1 - c_n)(1 - ⟨σ_0⟩²) + 2β² c_n ε_n bounding g_n' from above.

noncomputable def sctMeanfieldIntegratedError
    (d n : ℕ) (h beta : ℝ) : ℝ :=
  2 * beta * (1 - sctLatticeC d beta h n) *
      (1 - (sctOriginMag d beta h n) ^ 2) +
    2 * beta ^ 2 * sctLatticeC d beta h n *
      sctBoundaryCovarianceError d beta h n

Uses 3 · Used by 1

Statement usesBoundary covariance error · Minimal origin-to-site magnetization ratio in a box · Origin magnetization in a box

Used byMean-field lower bound for the spontaneous magnetization

DefinitionInfinite-volume mean-field function \(\beta^2(1 - m(\beta,h)^2)\)#✓fully proved

β²(1 - m(β, h)²) for the infinite-volume magnetization in field h.

noncomputable def sctInfiniteMeanfieldG (d : ℕ) (h beta : ℝ) : ℝ :=
  beta ^ 2 * (1 - (sctInfiniteFieldMag d beta h) ^ 2)

Uses 1 · Used by 1

Statement usesInfinite-volume magnetization in a field as a supremum over boxes

Used byMean-field lower bound for the spontaneous magnetization

DefinitionField sequence \(h_k = 1/(k + 1)\)#✓fully proved

The field sequence h_k = 1/(k + 1).

noncomputable def sctFieldToZero (n : ℕ) : ℝ :=
  1 / ((n : ℝ) + 1)

Used by 2

Used byMean-field lower bound for the spontaneous magnetization · Zero-field limit of the positive-field magnetization

DefinitionZero-field limit of the positive-field magnetization#✓fully proved

The zero-field limit m⁺(β) = inf_k m(β, h_k) of the infinite-volume magnetization in positive field.

noncomputable def sctZeroPlusMag (d : ℕ) (beta : ℝ) : ℝ :=
  ⨅ n : ℕ, sctInfiniteFieldMag d beta (sctFieldToZero n)

Uses 2 · Used by 1

Statement usesField sequence \(h_k = 1/(k + 1)\) · Infinite-volume magnetization in a field as a supremum over boxes

Used byMean-field lower bound for the spontaneous magnetization

DefinitionEnergy with general couplings and a uniform field#✓fully proved

The energy ∑_e J_e σ_e + h ∑_x σ_x.

noncomputable def weightedEnergy (J : Sym2 V -> ℝ) (h : ℝ) (s : ConfigSpace V) : ℝ :=
  (∑ e ∈ G.edgeFinset, J e * bond s e) + h * ∑ x, spin s x

Uses 3 · Used by 3

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

Used byFinite-volume mean-field inequality for the Ising model · Mean-field lower bound for the spontaneous magnetization · Boltzmann weight with general couplings and a uniform field

DefinitionBoltzmann weight with general couplings and a uniform field#✓fully proved

The Boltzmann weight exp(β (∑_e J_e σ_e + h ∑_x σ_x)).

noncomputable def weightedWeight (β : ℝ) (J : Sym2 V -> ℝ) (h : ℝ)
    (s : ConfigSpace V) : ℝ :=
  Real.exp (β * weightedEnergy G J h s)

Uses 2 · Used by 4

Statement usesConfiguration space of a statistical-mechanics model · Energy with general couplings and a uniform field

Used byFinite-volume mean-field inequality for the Ising model · Mean-field lower bound for the spontaneous magnetization · Gibbs expectation with general couplings and a uniform field · Partition function with general couplings and a uniform field

DefinitionPartition function with general couplings and a uniform field#✓fully proved

The partition function with couplings J and field h.

noncomputable def weightedZ (β : ℝ) (J : Sym2 V -> ℝ) (h : ℝ) : ℝ :=
  ∑ s : ConfigSpace V, weightedWeight G β J h s

Uses 2 · Used by 3

Statement usesConfiguration space of a statistical-mechanics model · Boltzmann weight with general couplings and a uniform field

Used byFinite-volume mean-field inequality for the Ising model · Mean-field lower bound for the spontaneous magnetization · Gibbs expectation with general couplings and a uniform field

DefinitionGibbs expectation with general couplings and a uniform field#✓fully proved

The Gibbs expectation with couplings J and field h.

noncomputable def weightedExpectation (β : ℝ) (J : Sym2 V -> ℝ) (h : ℝ)
    (f : ConfigSpace V -> ℝ) : ℝ :=
  (∑ s : ConfigSpace V, f s * weightedWeight G β J h s) / weightedZ G β J h

Uses 3 · Used by 2

Statement usesConfiguration space of a statistical-mechanics model · Boltzmann weight with general couplings and a uniform field · Partition function with general couplings and a uniform field

Used byFinite-volume mean-field inequality for the Ising model · Mean-field lower bound for the spontaneous magnetization

DefinitionBond term: ghost-graph disconnection sum for a bond covariance#✓fully proved

The bond term: the ghost-graph disconnection sum for Cov(σ_o, σ_e) with couplings J.

noncomputable def weightedBondDelta (β h : ℝ) (J : Sym2 V -> ℝ)
    (o : V) (e : Sym2 V) : ℝ :=
  sourcePairDisconnSum (withGhost G) β (ghostCoupling h β J)
    (hcaBondSource o e) ∅ (some o) none

Uses 4

Statement usesCoupling on the ghost graph with uniform field · Double-current sum restricted to disconnection · Ghost source set of a bond covariance · Graph with a ghost vertex joined to every site

DefinitionField term: ghost-graph disconnection sum for a site covariance#✓fully proved

The field term: the ghost-graph disconnection sum for Cov(σ_o, σ_z) with couplings J.

noncomputable def weightedFieldDelta (β h : ℝ) (J : Sym2 V -> ℝ)
    (o z : V) : ℝ :=
  sourcePairDisconnSum (withGhost G) β (ghostCoupling h β J)
    (hcaFieldSource o z) ∅ (some o) none

Uses 4

Statement usesCoupling on the ghost graph with uniform field · Double-current sum restricted to disconnection · Ghost source set of a field covariance · Graph with a ghost vertex joined to every site

DefinitionLattice sites underlying a set of box sites#✓fully proved

The sites of ℤ^d underlying a set T of sites of Λ_n.

noncomputable def sctCutSites {d n : ℕ} (T : Finset (sctBox d n)) :
    Finset (Site d) :=
  T.image Subtype.val

Uses 3 · Used by 6

Statement usesSite of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice · Box \(\Lambda_n\) as a type

Used byIdentification of a box cut set with its lattice sites · Boundary correlation of an edge crossing a cut · External boundary correlation of a cut, over edges leaving the box · Finite-volume mean-field inequality for the Ising model · Mean-field lower bound for the spontaneous magnetization · Oriented cut mass over cuts \(T \ni 0, x\) with \(y \notin T\)

DefinitionIdentification of a box cut set with its lattice sites#✓fully proved

The identification of T with sctCutSites T.

StatMech.Sharpness.sctCutVertexEquiv · 17 lines

noncomputable def sctCutVertexEquiv {d n : ℕ} (T : Finset (sctBox d n)) :
    {x : sctBox d n // x ∈ T} ≃ {z : Site d // z ∈ sctCutSites T} :=
  Equiv.ofBijective
    (fun x => (⟨x.1.1, mem_sctCutSites.mpr x.2⟩ :
      {z : Site d // z ∈ sctCutSites T}))
    ⟨by
      intro x y h
      apply Subtype.ext
      apply Subtype.ext
      exact congrArg (fun z : {z : Site d // z ∈ sctCutSites T} => z.1) h,
    by
      intro z
      have hz : z.1 ∈ T.image Subtype.val := z.2
      rw [Finset.mem_image] at hz
      obtain ⟨x, hx, hv⟩ := hz
      refine ⟨⟨x, hx⟩, Subtype.ext ?_⟩
      exact hv⟩

Uses 4 · Used by 2

Statement usesSite of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice · Box \(\Lambda_n\) as a type · Lattice sites underlying a set of box sites

Used byFinite-volume mean-field inequality for the Ising model · Mean-field lower bound for the spontaneous magnetization

DefinitionCut mass of a box set rooted at the field ghost#✓fully proved

The cut mass of T in Λ_n with the field ghost as root.

noncomputable def sctCurrentCutMass (d : ℕ) (beta h : ℝ) (n : ℕ)
    (T : Finset (sctBox d n)) : ℝ :=
  isingCutMass (withGhost (sctBoxGraph d n)) beta
    (ghostCoupling h beta (fun _ => 1)) none (T.map someEmb)

Uses 9 · Used by 4

Statement usesVertices of the box \((-n, n)^d\) · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice · Coupling on the ghost graph with uniform field · Embedding of vertices into the ghost graph · Random-current cut mass of a vertex set · Box \(\Lambda_n\) as a type · Nearest-neighbour graph on a box · Graph with a ghost vertex joined to every site

Used byBoundary error of the finite-volume mean-field inequality · Finite-volume mean-field inequality for the Ising model · Mean-field lower bound for the spontaneous magnetization · Oriented cut mass over cuts \(T \ni 0, x\) with \(y \notin T\)

DefinitionOriented cut mass over cuts \(T \ni 0, x\) with \(y \notin T\)#✓fully proved

The sum over cut sets T ∋ 0, x with y ∉ T of ⟨σ_0σ_x⟩_T times the cut mass of T.

noncomputable def sctOrientedCutMass (d : ℕ) (beta h : ℝ) (n : ℕ)
    (x y : sctBox d n) : ℝ :=
  ∑ T : Finset (sctBox d n),
    if sctBoxOrigin d n ∈ T ∧ x ∈ T ∧ y ∉ T then
      corrOriginInner d beta (sctCutSites T) x.1 *
        sctCurrentCutMass d beta h n T
    else 0

Uses 8 · Used by 2

Statement usesVertices of the box \((-n, n)^d\) · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice · Free origin correlation in a set, extended by zero · Box \(\Lambda_n\) as a type · Origin as a site of a box · Cut mass of a box set rooted at the field ghost · Lattice sites underlying a set of box sites

Used bySymmetrized cut mass of an edge · Finite-volume mean-field inequality for the Ising model

DefinitionSymmetrized cut mass of an edge#✓fully proved

The symmetrized cut mass sctOrientedCutMass x y + sctOrientedCutMass y x of an edge.

noncomputable def sctEdgeCutMass (d : ℕ) (beta h : ℝ) (n : ℕ) :
    Sym2 (sctBox d n) → ℝ :=
  Sym2.lift ⟨fun x y =>
    sctOrientedCutMass d beta h n x y +
      sctOrientedCutMass d beta h n y x, by
    intro x y
    ring⟩

Uses 2 · Used by 1

Statement usesBox \(\Lambda_n\) as a type · Oriented cut mass over cuts \(T \ni 0, x\) with \(y \notin T\)

Used byFinite-volume mean-field inequality for the Ising model

DefinitionBoundary correlation of an edge crossing a cut#✓fully proved

For an edge crossing the cut T, the correlation ⟨σ_0σ_x⟩_T at its endpoint x ∈ T; zero otherwise.

noncomputable def sctEdgeBoundaryCorr {d n : ℕ} (beta : ℝ)
    (T : Finset (sctBox d n)) : Sym2 (sctBox d n) → ℝ :=
  Sym2.lift ⟨fun x y =>
    if x ∈ T ∧ y ∉ T then corrOriginInner d beta (sctCutSites T) x.1
    else if y ∈ T ∧ x ∉ T then corrOriginInner d beta (sctCutSites T) y.1
    else 0, by
      intro x y
      by_cases hx : x ∈ T <;> by_cases hy : y ∈ T <;> simp [hx, hy]⟩

Uses 6 · Used by 2

Statement usesVertices of the box \((-n, n)^d\) · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice · Free origin correlation in a set, extended by zero · Box \(\Lambda_n\) as a type · Lattice sites underlying a set of box sites

Used byFinite-volume mean-field inequality for the Ising model · Internal boundary correlation of a cut in the box

DefinitionInternal boundary correlation of a cut in the box#✓fully proved

The sum of sctEdgeBoundaryCorr over the edges of Λ_n.

noncomputable def sctInternalBoundaryCorr (d : ℕ) (beta : ℝ) (n : ℕ)
    (T : Finset (sctBox d n)) : ℝ :=
  ∑ e ∈ (sctBoxGraph d n).edgeFinset, sctEdgeBoundaryCorr beta T e

Uses 5 · Used by 1

Statement usesSite of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice · Box \(\Lambda_n\) as a type · Nearest-neighbour graph on a box · Boundary correlation of an edge crossing a cut

Used byFinite-volume mean-field inequality for the Ising model

DefinitionLattice site as a box site, defaulting to the origin#✓fully proved

A site of ℤ^d as a site of Λ_n (the origin if it lies outside).

noncomputable def sctBoxize (d n : ℕ) (z : Site d) : sctBox d n :=
  if hz : z ∈ box d n then ⟨z, hz⟩ else sctBoxOrigin d n

Uses 4 · Used by 2

Statement usesSite of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice · Box \(\Lambda_n\) as a type · Origin as a site of a box

Used byFinite-volume mean-field inequality for the Ising model · Mean-field lower bound for the spontaneous magnetization

DefinitionEdge with exactly one endpoint in a cut set#✓fully proved

An edge has exactly one endpoint in T.

def sctCrossesCut {d n : ℕ} (T : Finset (sctBox d n)) :
    Sym2 (sctBox d n) → Prop :=
  Sym2.lift ⟨fun x y => (x ∈ T ∧ y ∉ T) ∨ (y ∈ T ∧ x ∉ T), by
    intro x y
    apply propext
    tauto⟩

Uses 4 · Used by 1

Statement usesVertices of the box \((-n, n)^d\) · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice · Box \(\Lambda_n\) as a type

Used byFinite-volume mean-field inequality for the Ising model

DefinitionExternal boundary correlation of a cut, over edges leaving the box#✓fully proved

The sum of ⟨σ_0σ_x⟩_T over boundary edges (x, y) of T with y ∉ Λ_n.

noncomputable def sctExternalBoundaryCorr (d : ℕ) (beta : ℝ) (n : ℕ)
    (T : Finset (sctBox d n)) : ℝ :=
  ∑ e ∈ (boundaryEdges d (sctCutSites T)).filter
      (fun e => e.2 ∉ box d n),
    corrOriginInner d beta (sctCutSites T) e.1

Uses 6 · Used by 3

Statement usesSite of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice · Oriented edge boundary of a finite lattice set · Free origin correlation in a set, extended by zero · Box \(\Lambda_n\) as a type · Lattice sites underlying a set of box sites

Used byBoundary error of the finite-volume mean-field inequality · Finite-volume mean-field inequality for the Ising model · Mean-field lower bound for the spontaneous magnetization

DefinitionBoundary error of the finite-volume mean-field inequality#✓fully proved

The boundary error ∑_{T ∋ 0} (external boundary correlation of T) × (cut mass of T).

noncomputable def sctCurrentBoundaryError (d : ℕ) (beta h : ℝ) (n : ℕ) : ℝ :=
  ∑ T : Finset (sctBox d n),
    if sctBoxOrigin d n ∈ T then
      sctExternalBoundaryCorr d beta n T * sctCurrentCutMass d beta h n T
    else 0

Uses 7 · Used by 2

Statement usesVertices of the box \((-n, n)^d\) · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice · Box \(\Lambda_n\) as a type · Origin as a site of a box · Cut mass of a box set rooted at the field ghost · External boundary correlation of a cut, over edges leaving the box

Used byFinite-volume mean-field inequality for the Ising model · Mean-field lower bound for the spontaneous magnetization

LemmaFinite-volume mean-field inequality for the Ising model#✓fully proved

The finite-volume mean-field inequality: for β, h > 0 and inf_S φ_β(S) ≥ φ₀, ∂_β ⟨σ_0⟩²_{Λ_n} ≥ 2 c_n ((φ₀/β)(1 - ⟨σ_0⟩²) - ε_n). Reference: H. Duminil-Copin, V. Tassion, "A new proof of the sharpness of the phase transition for Bernoulli percolation and the Ising model", Comm. Math. Phys. 343 (2016) 725–745.

lemma sct_finite_meanfield_inequality {d n : ℕ} (beta h infphi : ℝ)
    (hbeta : 0 < beta) (hh : 0 < h)
    (hinf : ∀ S : Finset (Site d), origin d ∈ S → infphi ≤ phiIsing d beta S) :
    deriv (fun b => (sctOriginMag d b h n) ^ 2) beta ≥
      2 * sctLatticeC d beta h n *
        ((1 / beta) * (infphi * (1 - (sctOriginMag d beta h n) ^ 2)) -
          sctCurrentBoundaryError d beta h n)

Uses 134 · Used by 1

Statement usesSite of the hypercubic lattice · Origin of the hypercubic lattice · Duminil-Copin–Tassion quantity \(\varphi_\beta(S)\) for the Ising model · Boundary error of the finite-volume mean-field inequality · Minimal origin-to-site magnetization ratio in a box · Origin magnetization in a box

Proof usesConfiguration space of a statistical-mechanics model · Graph induced on the vertices satisfying a predicate · Vertex set as a disjoint sum of a subset and its complement · Vertices of the box \((-n, n)^d\) · Current as a multiplicity on unordered pairs · Sourced current sum as correlation times sourceless sum · Adjacency through an edge of an edge set · Bond variable of an unordered pair · Cluster of a site in an edge set · Connectivity through the edges of an edge set · Degree of a site in an edge set · First Griffiths inequality (GKS I) · Ising Hamiltonian on a finite graph · Incident flux of a current on an edge set · Configuration equivalence induced by a vertex relabeling · Finite-volume Ising expectation · Gibbs probability of an Ising configuration · Ising Gibbs probabilities sum to one · Configurations on a disjoint union as pairs of configurations · Boltzmann weight of an Ising configuration · Ising partition function · Positivity of the Ising partition function · Edges of an edge set with odd multiplicity · Edges of an edge set with positive multiplicity · Source set of a current on an edge set · Spin of a configuration at a site · Spin value of a Boolean · Spin product over a vertex set · Odd-degree sites of an edge set · Box \((-n, n)^d\) in the hypercubic lattice · Hypercubic lattice \(\mathbb{Z}^d\) · Oriented edge boundary of a finite lattice set · Shift of a lattice site in one coordinate · Sign of a unit lattice step · Current: a multiplicity in \(\mathbb{N}\) for each unordered pair · Connectivity through edges carrying positive current · 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 · Edge copies of a current · Endpoints of an edge copy · Profile of a set of edge copies · Subsets of a sigma type as families of fibre subsets · Double-current sum restricted to disconnection · Bond term \(\Delta_e\) of the magnetization derivative · Ghost source set of a bond covariance · Field term \(\Delta_z\) of the magnetization derivative · Ghost source set of a field covariance · Random-current form of the \(\beta\)-derivative of the magnetization · Switching gap of a current · Gap-weighted current sum restricted to a predicate · Current with no edge crossing a set's boundary · Adjacency through an edge of a multigraph edge set · Odd-degree vertices in a cluster · Cluster of a vertex in a multigraph edge set · Connectivity in a multigraph edge set · Degree of a vertex in a multigraph edge set · Sources of a multigraph edge set · Switching lemma for multigraph currents · Energy with general couplings and a uniform field · Gibbs expectation with general couplings and a uniform field · Boltzmann weight with general couplings and a uniform field · Partition function with general couplings and a uniform field · Partition function with inhomogeneous couplings and site fields · Extension by zero of a current inside a set · Extension by zero of a current outside a set · Boltzmann weight with couplings · Outside part of a gated double-current summand · Outside summand of a gated double-current sum · Free origin correlation in a set, extended by zero · Coupling restricted to the edges inside a set · Griffiths' second inequality for two distinct spins · Subgraph of edges carrying positive current · Current sum with prescribed sources · Random-current representation · Field derivative of the magnetization as a sum of covariances · Unordered pair inside a set · Edges of a graph inside a set · Gibbs expectation with inhomogeneous couplings and site fields · Correlation function with couplings · Inside weight with prescribed sources · Free-boundary zero-field two-point function in a finite set · Term of the exponential expansion of an edge weight · Gated double-current sum over edge-indexed currents · Vertex subsets as ghost-free subsets of the extended vertex set · Induced subgraph of \(\mathbb{Z}^d\) on a finite set · Griffiths monotonicity of correlations in the edge set · Incident flux of a current at a vertex · Edge lying inside a set · Random-current cut mass of a vertex set · Lower mass of the four-source bound · Four-source double-current sum with a connection pattern · Lower mass in the degenerate case \(x = o\) · Subgraph of edges inside a vertex set · Magnetization vanishes at zero field · Vertices not connected to a vertex by positive current · Extension of an edge function to a current · Regrouping a split pair of currents · Reparametrizing pairs of functions by their sum and one summand · Partition function with couplings · Reassembly of a current from its inside and outside parts · Restriction of a current to a set · Box \(\Lambda_n\) as a type · Nearest-neighbour graph on a box · Free-boundary site magnetization in a box · Origin as a site of a box · All sites of a box · Lattice site as a box site, defaulting to the origin · Edge with exactly one endpoint in a cut set · Cut mass of a box set rooted at the field ghost · Lattice sites underlying a set of box sites · Identification of a box cut set with its lattice sites · Boundary correlation of an edge crossing a cut · Symmetrized cut mass of an edge · External boundary correlation of a cut, over edges leaving the box · Internal boundary correlation of a cut in the box · Oriented cut mass over cuts \(T \ni 0, x\) with \(y \notin T\) · Minimal magnetization ratio for \(n\)-dependent site types · Double-current sum with prescribed sources · Sources of a current · Total spin of a configuration · Single-edge current weight \((\beta J_e)^k/k!\) · Boltzmann weight with inhomogeneous couplings and site fields · Weight of a random current · Current weights are nonnegative for nonnegative \(\beta\) and couplings · Graph with a ghost vertex joined to every site

Used byMean-field lower bound for the spontaneous magnetization

DefinitionPairs of a box site and an outside lattice neighbour#✓fully proved

Pairs (x, y) with x ∈ Λ_n and y a lattice neighbour of x outside Λ_n.

noncomputable def sctExternalBoxPairs (d n : ℕ) :
    Finset (sctBox d n × Site d) :=
  (Finset.univ : Finset (sctBox d n)).biUnion fun x =>
    (sctExteriorNeighbours d n x.1).image fun y => (x, y)

Uses 5 · Used by 1

Statement usesVertices of the box \((-n, n)^d\) · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice · Box \(\Lambda_n\) as a type · Exterior neighbours of a site

Used byMean-field lower bound for the spontaneous magnetization

LemmaMean-field lower bound for the spontaneous magnetization#✓fully proved

The mean-field lower bound for the spontaneous magnetization: if β̃_c > 0 and its defining set is bounded, then m*(β) ≥ √(1 - (β̃_c/β)²) for β ≥ β̃_c. Reference: H. Duminil-Copin, V. Tassion, "A new proof of the sharpness of the phase transition for Bernoulli percolation and the Ising model", Comm. Math. Phys. 343 (2016) 725–745.

lemma sct_magnetization_meanfield_lower_bound_integrated
    (d : ℕ) (hbdd : BddAbove (tildeBetaCIsingSet d))
    (hcrit : 0 < tildeBetaCIsing d) {beta : ℝ}
    (hbeta : tildeBetaCIsing d ≤ beta) :
    Real.sqrt (1 - (tildeBetaCIsing d / beta) ^ 2) ≤
      magnetization d beta

Uses 186 · Used by 1

Statement usesSpontaneous magnetization of the Ising model · Auxiliary critical point \(\tilde\beta_c\) of the Ising model · Inverse temperatures with an Ising witness \(\varphi_\beta(S) < 1\)

Proof usesConfiguration space of a statistical-mechanics model · Graph transported to the sum of a subset and its complement · Graph induced on the vertices satisfying a predicate · Graph induced on the vertices failing a predicate · Vertex set as a disjoint sum of a subset and its complement · Vertices of the box \((-n, n)^d\) · Graph glued from two graphs along an interface · Increasing event · Current as a multiplicity on unordered pairs · Infinite-volume state of a sequence of measures · Adjacency through an edge of an edge set · Bond variable of an unordered pair · Bonds inside the box · Bonds touching the box · Ordered nearest-neighbour pairs inside the box · Ordered nearest-neighbour pairs touching the box · Box \((-n, n)^d\) as a finite set of sites · Cluster of a site in an edge set · Connectivity through the edges of an edge set · Two-point spin covariance · Degree of a site in an edge set · Existence of infinite-volume states · Free-boundary Ising measure in a box · Box energy with a boundary condition · Finite-volume Gibbs measure on configurations of \(\mathbb{Z}^d\) · Finite-volume Gibbs probability with a boundary condition · Finite-volume Boltzmann weight with a boundary condition · Finite-volume partition function with a boundary condition · Spin covariance in the inhomogeneous model · Directional spin sum · Covariance with the directional spin · Field line in a given direction · GHS concavity · First Griffiths inequality (GKS I) · Configuration glued from inside spins and a boundary condition · Ising Hamiltonian on a finite graph · Incident flux of a current on an edge set · Configuration equivalence induced by a vertex relabeling · Finite-volume Ising expectation · Gibbs probability of an Ising configuration · Ising Gibbs probabilities sum to one · Configurations on a disjoint union as pairs of configurations · Boltzmann weight of an Ising configuration · Ising partition function · Positivity of the Ising partition function · Chosen subsequential weak limit of a sequence of measures · All-minus configuration · Negative Hamiltonian of the Ising model · Edges of an edge set with odd multiplicity · Overwriting a configuration on an inner box · All-plus configuration · Plus-boundary Ising measure in a box · Infinite-volume plus state as a subsequential weak limit · Edges of an edge set with positive multiplicity · Plus-spin indicator at a site as a bounded continuous function · Restriction of a configuration to an inner box · Source set of a current on an edge set · Spin of a configuration at a site · Spin value of a Boolean · Spin at a site as a bounded continuous function · Spin product over a vertex set · Odd-degree sites of an edge set · Involution swapping inner-box parts of configuration pairs · Nearest neighbours in \(\mathbb{Z}^d\) · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice · Nearest neighbours of a lattice site · Neighbour of a site in a coordinate direction · Hypercubic lattice \(\mathbb{Z}^d\) · Shift of a site along a coordinate · Oriented edge boundary of a finite lattice set · Shift of a lattice site in one coordinate · Origin of the hypercubic lattice · Sign of a unit lattice step · Current: a multiplicity in \(\mathbb{N}\) for each unordered pair · Connectivity through edges carrying positive current · 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 · Edge copies of a current · Endpoints of an edge copy · Profile of a set of edge copies · Subsets of a sigma type as families of fibre subsets · Double-current sum restricted to disconnection · Current with no edge crossing a set's boundary · Adjacency through an edge of a multigraph edge set · Cluster of a vertex in a multigraph edge set · Connectivity in a multigraph edge set · Degree of a vertex in a multigraph edge set · Sources of a multigraph edge set · Energy with general couplings and a uniform field · Gibbs expectation with general couplings and a uniform field · Boltzmann weight with general couplings and a uniform field · Partition function with general couplings and a uniform field · Partition function with inhomogeneous couplings and site fields · Extension by zero of a current inside a set · Extension by zero of a current outside a set · Boltzmann weight with couplings · Outside summand of a gated double-current sum · Free origin correlation in a set, extended by zero · Coupling restricted to the edges inside a set · Griffiths' second inequality for two distinct spins · Subgraph of edges carrying positive current · Current sum with prescribed sources · Random-current representation · Field derivative of the magnetization as a sum of covariances · Unordered pair inside a set · Edges of a graph inside a set · Gibbs expectation with inhomogeneous couplings and site fields · Correlation function with couplings · Inside weight with prescribed sources · Free-boundary zero-field two-point function in a finite set · Term of the exponential expansion of an edge weight · Gated double-current sum over edge-indexed currents · Vertex subsets as ghost-free subsets of the extended vertex set · Induced subgraph of \(\mathbb{Z}^d\) on a finite set · Griffiths monotonicity of correlations in the edge set · Incident flux of a current at a vertex · Edge lying inside a set · Random-current cut mass of a vertex set · Subgraph of edges inside a vertex set · Magnetization vanishes at zero field · Vertices not connected to a vertex by positive current · Extension of an edge function to a current · Reparametrizing pairs of functions by their sum and one summand · Partition function with couplings · Duminil-Copin–Tassion quantity \(\varphi_\beta(S)\) for the Ising model · Reassembly of a current from its inside and outside parts · Restriction of a current to a set · Boundary covariance error · Box \(\Lambda_n\) as a type · Origin–site covariance in a box · Nearest-neighbour graph on a box · Membership of a larger-box site in a smaller box · Smaller box as a subtype of a larger box · Free-boundary site magnetization in a box · Origin as a site of a box · All sites of a box · Lattice site as a box site, defaulting to the origin · Boundary error of the finite-volume mean-field inequality · Cut mass of a box set rooted at the field ghost · Lattice sites underlying a set of box sites · Identification of a box cut set with its lattice sites · Exterior neighbours of a site · External boundary correlation of a cut, over edges leaving the box · Pairs of a box site and an outside lattice neighbour · Field sequence \(h_k = 1/(k + 1)\) · Infinite-volume magnetization in a field as a supremum over boxes · Infinite-volume mean-field function \(\beta^2(1 - m(\beta,h)^2)\) · Field switched off on the outer layer · Origin magnetization with the outer-layer field switched off · Minimal origin-to-site magnetization ratio in a box · Box mean-field function \(\beta^2(1 - \langle\sigma_0\rangle^2)\) · \(\beta\)-derivative of the box mean-field function · Error term bounding the derivative of the box mean-field function · Origin magnetization in a box · \(\beta\)-derivative of the origin magnetization in a box · \(\beta\)-derivative of the squared origin magnetization in a box · Covariance sum over the outer layer · Outer-layer indicator as a field direction · Translation onto a translated box · Translated box \(\Lambda_n - y\) · Nearest-neighbour graph on a translated box · Membership of a doubled-box site in a translated box · Translated box as a subtype of the doubled box · Zero-field limit of the positive-field magnetization · Minimal magnetization ratio for \(n\)-dependent site types · Finite-volume mean-field inequality for the Ising model · Derivative of a concave function is at most a secant slope · Double-current sum with prescribed sources · Sources of a current · Total spin of a configuration · Single-edge current weight \((\beta J_e)^k/k!\) · Boltzmann weight with inhomogeneous couplings and site fields · Weight of a random current · Graph with a ghost vertex joined to every site · Stochastic domination of measures on configurations · Stochastic domination compares real-valued masses · Weak convergence of probability measures on configuration space · Weak convergence implies convergence of integrals · Holley inequality for increasing events

Used bySharpness of the Ising phase transition on \(\mathbb{Z}^d\), \(d \ge 2\)

82 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.