Simon–Lieb inequality

DefinitionEdge set with prescribed odd-degree vertices#✓fully proved

The set of vertices of odd degree in the edge set F is exactly A.

def HasOddBoundary (F : Finset (Sym2 V)) (A : Finset V) : Prop :=
  ∀ v : V, Odd (incCount F v) ↔ v ∈ A

Uses 1 · Used by 11

Statement usesNumber of edges of an edge set incident to a vertex

Used byInf-based and sup-based Ising critical points agree for \(d \ge 2\) · Sharpness of the Ising phase transition on \(\mathbb{Z}^d\), \(d \ge 2\) · Auxiliary critical point \(\tilde\beta_c(d)\) is positive for \(d \ge 2\) · First-exit data for a high-temperature edge set · Chosen first-exit data · Edge sets with a given boundary · High-temperature switching map · Switching map between valid inputs and outputs · Simon–Lieb inequality on a finite graph · Valid switching inputs · Valid switching outputs

DefinitionHigh-temperature weight of an edge set#✓fully proved

The high-temperature weight ∏_{e ∈ F} tanh(βJ_e) of an edge set.

noncomputable def highTempSubgraphWeight (beta : ℝ) (J : Sym2 V → ℝ)
    (F : Finset (Sym2 V)) : ℝ :=
  ∏ e ∈ F, Real.tanh (beta * J e)

Used by 4

Used byInf-based and sup-based Ising critical points agree for \(d \ge 2\) · Sharpness of the Ising phase transition on \(\mathbb{Z}^d\), \(d \ge 2\) · Auxiliary critical point \(\tilde\beta_c(d)\) is positive for \(d \ge 2\) · Simon–Lieb inequality on a finite graph

DefinitionIndicator current of an edge set#✓fully proved

The current equal to 1 on the edges of F and 0 elsewhere.

noncomputable def edgeIndicatorCurrent (F : Finset (Sym2 V)) : Current V :=
  fun e => if e ∈ F then 1 else 0

Uses 1 · Used by 1

Statement usesCurrent: a multiplicity in \(\mathbb{N}\) for each unordered pair

Used byChosen first-exit data

DefinitionSource pair \(\{a\} \triangle \{b\}\)#✓fully proved

The source set {a} ∆ {b} (empty when a = b).

def sourcePair (a b : V) : Finset V := ({a} : Finset V) ∆ {b}

Used by 13

Used byInf-based and sup-based Ising critical points agree for \(d \ge 2\) · Sharpness of the Ising phase transition on \(\mathbb{Z}^d\), \(d \ge 2\) · Auxiliary critical point \(\tilde\beta_c(d)\) is positive for \(d \ge 2\) · First-exit data for a high-temperature edge set · Chosen first-exit data · High-temperature switching map · Switching map between valid inputs and outputs · Simon–Lieb inequality in the infinite-volume plus state · Two-point function with couplings · Simon–Lieb inequality on a finite graph · Valid switching inputs · Valid switching outputs · Two-point function with a site field

StructureFirst-exit data for a high-temperature edge set#✓fully proved

First-exit data for an edge set K with boundary {o} ∆ {z} and a set S ∋ o, z ∉ S: an exit edge xy of K with x ∈ S, y ∉ S, and a subset Q ⊆ K of edges inside S with boundary {o} ∆ {x} not containing xy.

StatMech.Sharpness.HighTempFirstExit · 24 lines

structure HighTempFirstExit (K : Finset (Sym2 V)) (o z : V)
    (S : Finset V) where
  /-- The last vertex in `S`. -/
  x : V
  /-- The first vertex outside `S`. -/
  y : V
  /-- The part of `K` inside `S` joining `o` to `x`. -/
  Q : Finset (Sym2 V)
  /-- `x ∈ S`. -/
  x_mem : x ∈ S
  /-- `y ∉ S`. -/
  y_notMem : y ∉ S
  /-- `Q ⊆ K`. -/
  Q_subset : Q ⊆ K
  /-- Every edge of `Q` lies inside `S`. -/
  Q_inside : ∀ e ∈ Q, edgeInside S e
  /-- `Q` has boundary `{o} ∆ {x}`. -/
  Q_sources : HasOddBoundary Q (sourcePair o x)
  /-- The exit edge belongs to `K`. -/
  exit_mem : s(x, y) ∈ K
  /-- The exit edge is not in `Q`. -/
  exit_notMem : s(x, y) ∉ Q
  /-- `x ≠ y`. -/
  ne : x ≠ y

Uses 3 · Used by 4

Statement usesEdge set with prescribed odd-degree vertices · Unordered pair inside a set · Source pair \(\{a\} \triangle \{b\}\)

Used byChosen first-exit data · High-temperature switching map · Switching map between valid inputs and outputs · Simon–Lieb inequality on a finite graph

DefinitionChosen first-exit data#✓fully proved

A choice of first-exit data, from exists_highTempFirstExit.

noncomputable def highTempFirstExit (G : SimpleGraph V) [DecidableRel G.Adj]
    (K : Finset (Sym2 V)) (hK : K ⊆ G.edgeFinset) {o z : V}
    (hbd : HasOddBoundary K (sourcePair o z)) (S : Finset V)
    (ho : o ∈ S) (hz : z ∉ S) : HighTempFirstExit K o z S :=
  (exists_highTempFirstExit G K hK hbd S ho hz).some

Uses 21 · Used by 3

Statement usesCurrent as a multiplicity on unordered pairs · Adjacency through an edge of an edge set · Cluster of a site in an edge set · Connectivity through the edges of an edge set · Degree of a site in an edge set · Number of edges of an edge set incident to a vertex · Incident flux of a current on an edge set · Edges of an edge set with odd multiplicity · Source set of a current on an edge set · Odd-degree sites of an edge set · Current: a multiplicity in \(\mathbb{N}\) for each unordered pair · Edge set with prescribed odd-degree vertices · First-exit data for a high-temperature edge set · Backbone paths along odd-current edges · Indicator current of an edge set · Unordered pair inside a set · Incident flux of a current at a vertex · Subgraph of edges with odd current · Source pair \(\{a\} \triangle \{b\}\) · Sources of a current · Number of walk edges at a vertex

Used byHigh-temperature switching map · Switching map between valid inputs and outputs · Simon–Lieb inequality on a finite graph

DefinitionEdges of a graph inside a set#✓fully proved

The edges of G inside S.

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

Uses 1 · Used by 5

Statement usesUnordered pair inside a set

Used byHigh-temperature switching map · Switching map between valid inputs and outputs · Simon–Lieb inequality on a finite graph · Valid switching inputs · Valid switching outputs

StructureInput pair of the high-temperature switching#✓fully proved

A pair of edge sets (F, H), the input of the switching.

structure HighTempSwitchInput where
  /-- The edge set with boundary `{o} ∆ {z}`. -/
  F : Finset (Sym2 V)
  /-- The sourceless edge set inside `S`. -/
  H : Finset (Sym2 V)
deriving DecidableEq, Fintype

Used by 6

Used byHigh-temperature switching map · Weight of a switching input · Finite set of valid switching inputs · Switching map between valid inputs and outputs · Simon–Lieb inequality on a finite graph · Valid switching inputs

StructureOutput tuple of the high-temperature switching#✓fully proved

A tuple (x, y, A, B) of an exit edge and two edge sets, the output of the switching.

structure HighTempSwitchOutput where
  /-- The inner endpoint of the exit edge. -/
  x : V
  /-- The outer endpoint of the exit edge. -/
  y : V
  /-- The edge set inside `S` with boundary `{o} ∆ {x}`. -/
  A : Finset (Sym2 V)
  /-- The edge set with boundary `{y} ∆ {z}`. -/
  B : Finset (Sym2 V)
deriving DecidableEq, Fintype

Used by 6

Used byHigh-temperature switching map · Switching map between valid inputs and outputs · Weight of a switching output · Finite set of valid switching outputs · Simon–Lieb inequality on a finite graph · Valid switching outputs

DefinitionValid switching inputs#✓fully proved

Valid inputs: F ⊆ E(G) with boundary {o} ∆ {z} and H inside S with empty boundary.

def HighTempSwitchInput.Valid (S : Finset V) (o z : V)
    (p : HighTempSwitchInput (V := V)) : Prop :=
  p.F ⊆ G.edgeFinset ∧
    p.H ⊆ highTempInternalEdges G S ∧
    HasOddBoundary p.F (sourcePair o z) ∧
    HasOddBoundary p.H ∅

Uses 4 · Used by 4

Statement usesEdge set with prescribed odd-degree vertices · Input pair of the high-temperature switching · Edges of a graph inside a set · Source pair \(\{a\} \triangle \{b\}\)

Used byHigh-temperature switching map · Finite set of valid switching inputs · Switching map between valid inputs and outputs · Simon–Lieb inequality on a finite graph

DefinitionValid switching outputs#✓fully proved

Valid outputs: x ∈ S, y ∉ S, A inside S with boundary {o} ∆ {x}, and B ⊆ E(G) with boundary {y} ∆ {z}.

def HighTempSwitchOutput.Valid (S : Finset V) (o z : V)
    (r : HighTempSwitchOutput (V := V)) : Prop :=
  r.x ∈ S ∧ r.y ∉ S ∧
    r.A ⊆ highTempInternalEdges G S ∧
    r.B ⊆ G.edgeFinset ∧
    HasOddBoundary r.A (sourcePair o r.x) ∧
    HasOddBoundary r.B (sourcePair r.y z)

Uses 4 · Used by 3

Statement usesEdge set with prescribed odd-degree vertices · Output tuple of the high-temperature switching · Edges of a graph inside a set · Source pair \(\{a\} \triangle \{b\}\)

Used bySwitching map between valid inputs and outputs · Finite set of valid switching outputs · Simon–Lieb inequality on a finite graph

DefinitionFinite set of valid switching inputs#✓fully proved

The finite set of valid inputs.

noncomputable def highTempSwitchInputs (S : Finset V) (o z : V) :
    Finset (HighTempSwitchInput (V := V)) :=
  Finset.univ.filter (HighTempSwitchInput.Valid G S o z)

Uses 2 · Used by 2

Statement usesInput pair of the high-temperature switching · Valid switching inputs

Used bySwitching map between valid inputs and outputs · Simon–Lieb inequality on a finite graph

DefinitionFinite set of valid switching outputs#✓fully proved

The finite set of valid outputs.

noncomputable def highTempSwitchOutputs (S : Finset V) (o z : V) :
    Finset (HighTempSwitchOutput (V := V)) :=
  Finset.univ.filter (HighTempSwitchOutput.Valid G S o z)

Uses 2 · Used by 2

Statement usesOutput tuple of the high-temperature switching · Valid switching outputs

Used bySwitching map between valid inputs and outputs · Simon–Lieb inequality on a finite graph

DefinitionHigh-temperature switching map#✓fully proved

The switching map: cut F ∆ H at its first exit from S and redistribute the pieces.

noncomputable def highTempSwitch (S : Finset V) (o z : V)
    (ho : o ∈ S) (hz : z ∉ S) (p : HighTempSwitchInput (V := V))
    (hp : p.Valid G S o z) : HighTempSwitchOutput (V := V) := by
  let K := p.F ∆ p.H
  let d := highTempFirstExit G K
    (highTempInput_symmDiff_subset G hp)
    (highTempInput_symmDiff_sources G hp) S ho hz
  exact
    { x := d.x
      y := d.y
      A := p.H ∆ d.Q
      B := (p.F ∆ d.Q).erase s(d.x, d.y) }

Uses 12 · Used by 2

Statement usesDegree of a site in an edge set · Number of edges of an edge set incident to a vertex · Odd-degree sites of an edge set · Edge set with prescribed odd-degree vertices · First-exit data for a high-temperature edge set · Input pair of the high-temperature switching · Valid switching inputs · Output tuple of the high-temperature switching · Unordered pair inside a set · Chosen first-exit data · Edges of a graph inside a set · Source pair \(\{a\} \triangle \{b\}\)

Used bySwitching map between valid inputs and outputs · Simon–Lieb inequality on a finite graph

DefinitionSwitching map between valid inputs and outputs#✓fully proved

The switching as a map between the finite sets of valid inputs and outputs.

noncomputable def highTempSwitchMap (S : Finset V) (o z : V)
    (ho : o ∈ S) (hz : z ∉ S) :
    ↥(highTempSwitchInputs G S o z) → ↥(highTempSwitchOutputs G S o z) :=
  fun p => ⟨highTempSwitch G S o z ho hz p.1 (by
      have h := p.2
      change p.1 ∈ Finset.univ.filter
        (HighTempSwitchInput.Valid G S o z) at h
      exact (Finset.mem_filter.mp h).2),
    highTempSwitch_mem_outputs G S o z ho hz p.1 p.2⟩

Uses 16 · Used by 1

Statement usesDegree of a site in an edge set · Number of edges of an edge set incident to a vertex · Odd-degree sites of an edge set · Edge set with prescribed odd-degree vertices · First-exit data for a high-temperature edge set · Input pair of the high-temperature switching · Valid switching inputs · Output tuple of the high-temperature switching · Valid switching outputs · Unordered pair inside a set · Chosen first-exit data · Edges of a graph inside a set · High-temperature switching map · Finite set of valid switching inputs · Finite set of valid switching outputs · Source pair \(\{a\} \triangle \{b\}\)

Used bySimon–Lieb inequality on a finite graph

DefinitionWeight of a switching input#✓fully proved

The weight ∏_{e ∈ F} t_e ∏_{e ∈ H} t_e of an input.

noncomputable def highTempSwitchInputWeight (t : Sym2 V → ℝ)
    (p : HighTempSwitchInput (V := V)) : ℝ :=
  (∏ e ∈ p.F, t e) * ∏ e ∈ p.H, t e

Uses 1 · Used by 1

Statement usesInput pair of the high-temperature switching

Used bySimon–Lieb inequality on a finite graph

DefinitionWeight of a switching output#✓fully proved

The weight ∏_{e ∈ A} t_e · t_{xy} · ∏_{e ∈ B} t_e of an output.

noncomputable def highTempSwitchOutputWeight (t : Sym2 V → ℝ)
    (r : HighTempSwitchOutput (V := V)) : ℝ :=
  (∏ e ∈ r.A, t e) * t s(r.x, r.y) * ∏ e ∈ r.B, t e

Uses 1 · Used by 1

Statement usesOutput tuple of the high-temperature switching

Used bySimon–Lieb inequality on a finite graph

DefinitionEdge sets with a given boundary#✓fully proved

The edge sets F ⊆ E with boundary A.

noncomputable def highTempSourceSubgraphs (E : Finset (Sym2 V))
    (A : Finset V) : Finset (Finset (Sym2 V)) :=
  E.powerset.filter (fun F => HasOddBoundary F A)

Uses 2 · Used by 5

Statement usesNumber of edges of an edge set incident to a vertex · Edge set with prescribed odd-degree vertices

Used byInf-based and sup-based Ising critical points agree for \(d \ge 2\) · Sharpness of the Ising phase transition on \(\mathbb{Z}^d\), \(d \ge 2\) · Auxiliary critical point \(\tilde\beta_c(d)\) is positive for \(d \ge 2\) · High-temperature source sum · Simon–Lieb inequality on a finite graph

DefinitionHigh-temperature source sum#✓fully proved

The high-temperature source sum ∑_{F ⊆ E, ∂F = A} ∏_{e ∈ F} t_e.

noncomputable def highTempSourceSum (E : Finset (Sym2 V))
    (t : Sym2 V → ℝ) (A : Finset V) : ℝ :=
  ∑ F ∈ highTempSourceSubgraphs E A, ∏ e ∈ F, t e

Uses 1 · Used by 4

Statement usesEdge sets with a given boundary

Used byInf-based and sup-based Ising critical points agree for \(d \ge 2\) · Sharpness of the Ising phase transition on \(\mathbb{Z}^d\), \(d \ge 2\) · Auxiliary critical point \(\tilde\beta_c(d)\) is positive for \(d \ge 2\) · Simon–Lieb inequality on a finite graph

DefinitionTwo-point function with couplings#✓fully proved

The two-point function ⟨σ_aσ_b⟩_{β,J} (equal to 1 when a = b).

noncomputable def twoPointJ (beta : ℝ) (J : Sym2 V → ℝ)
    (a b : V) : ℝ :=
  expectationJ G beta J (sourcePair a b)

Uses 2 · Used by 6

Statement usesCorrelation function with couplings · Source pair \(\{a\} \triangle \{b\}\)

Used byInf-based and sup-based Ising critical points agree for \(d \ge 2\) · Sharpness of the Ising phase transition on \(\mathbb{Z}^d\), \(d \ge 2\) · Auxiliary critical point \(\tilde\beta_c(d)\) is positive for \(d \ge 2\) · Simon–Lieb inequality in the infinite-volume plus state · Simon–Lieb weight · Simon–Lieb inequality on a finite graph

TheoremSimon–Lieb inequality on a finite graph#✓fully proved

The Simon–Lieb inequality: for β, J ≥ 0, o ∈ S and z ∉ S, ⟨σ_oσ_z⟩ ≤ ∑_{x ∈ S} ∑_{y ∉ S} tanh(βJ_{xy}) ⟨σ_oσ_x⟩_{J|S} ⟨σ_yσ_z⟩. Reference: B. Simon, "Correlation inequalities and the decay of correlations in ferromagnets", Comm. Math. Phys. 77 (1980) 111–126; E. H. Lieb, "A refinement of Simon's correlation inequality", Comm. Math. Phys. 77 (1980) 127–135.

theorem twoPointJ_simon_finite (beta : ℝ) (J : Sym2 V → ℝ)
    (hbeta : 0 ≤ beta) (hJ : ∀ e, 0 ≤ J e)
    (S : Finset V) (o z : V) (ho : o ∈ S) (hz : z ∉ S) :
    twoPointJ G beta J o z ≤
      ∑ x ∈ S, ∑ y ∈ (Finset.univ \ S),
        Real.tanh (beta * J s(x, y)) *
          twoPointJ G beta (couplingIn J S) o x *
          twoPointJ G beta J y z

Uses 34 · Used by 1

Statement usesCoupling restricted to the edges inside a set · Two-point function with couplings

Proof usesConfiguration space of a statistical-mechanics model · Even subgraph condition on an edge set · Bond variable of an unordered pair · Bond variable takes values \(\pm 1\) · Degree of a site in an edge set · Number of edges of an edge set incident to a vertex · 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 · Edge set with prescribed odd-degree vertices · First-exit data for a high-temperature edge set · Input pair of the high-temperature switching · Valid switching inputs · Output tuple of the high-temperature switching · Valid switching outputs · Boltzmann weight with couplings · Unordered pair inside a set · Correlation function with couplings · Chosen first-exit data · Edges of a graph inside a set · Edge sets with a given boundary · High-temperature source sum · High-temperature weight of an edge set · High-temperature switching map · Weight of a switching input · Finite set of valid switching inputs · Switching map between valid inputs and outputs · Weight of a switching output · Finite set of valid switching outputs · Partition function with couplings · Source pair \(\{a\} \triangle \{b\}\)

Used bySimon–Lieb inequality in the infinite-volume plus state

DefinitionSimon–Lieb weight#✓fully proved

The Simon–Lieb weight tanh(βJ_{xy}) ⟨σ_oσ_x⟩_{J|S}.

noncomputable def simonWeightPair (beta : ℝ) (J : Sym2 V → ℝ)
    (S : Finset V) (o x y : V) : ℝ :=
  Real.tanh (beta * J s(x, y)) *
    twoPointJ G beta (couplingIn J S) o x

Uses 2

Statement usesCoupling restricted to the edges inside a set · Two-point function with couplings

DefinitionGhost-graph coupling with a site field#✓fully proved

The coupling on G plus a ghost vertex: J on the edges of G and H_x on the edge {x, ghost}.

noncomputable def vertexGhostCoupling (J : Sym2 V → ℝ) (H : V → ℝ)
    (e : Sym2 (Option V)) : ℝ :=
  Sym2.lift ⟨fun a b ↦
    match a, b with
    | some x, some y => J s(x, y)
    | some x, none => H x
    | none, some y => H y
    | none, none => 0,
    by rintro (_ | x) (_ | y) <;> simp only []; rw [Sym2.eq_swap]⟩ e

Used by 4

Used byInf-based and sup-based Ising critical points agree for \(d \ge 2\) · Sharpness of the Ising phase transition on \(\mathbb{Z}^d\), \(d \ge 2\) · Auxiliary critical point \(\tilde\beta_c(d)\) is positive for \(d \ge 2\) · Simon–Lieb inequality in the infinite-volume plus state

DefinitionBoltzmann weight with a site field#✓fully proved

The Boltzmann weight exp(β(∑_e J_e σ_e + ∑_x H_x σ_x)) with a site field H.

noncomputable def vertexFieldWeight (β : ℝ) (J : Sym2 V → ℝ)
    (H : V → ℝ) (s : ConfigSpace V) : ℝ :=
  Real.exp (β * ((∑ e ∈ G.edgeFinset, J e * bond s e) +
    ∑ x : V, H x * spin s x))

Uses 3 · Used by 6

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

Used byInf-based and sup-based Ising critical points agree for \(d \ge 2\) · Sharpness of the Ising phase transition on \(\mathbb{Z}^d\), \(d \ge 2\) · Auxiliary critical point \(\tilde\beta_c(d)\) is positive for \(d \ge 2\) · Simon–Lieb inequality in the infinite-volume plus state · Gibbs expectation with a site field · Partition function with a site field

DefinitionPartition function with a site field#✓fully proved

The partition function with site field H.

noncomputable def vertexFieldZ (β : ℝ) (J : Sym2 V → ℝ)
    (H : V → ℝ) : ℝ :=
  ∑ s : ConfigSpace V, vertexFieldWeight G β J H s

Uses 2 · Used by 5

Statement usesConfiguration space of a statistical-mechanics model · Boltzmann weight with a site field

Used byInf-based and sup-based Ising critical points agree for \(d \ge 2\) · Sharpness of the Ising phase transition on \(\mathbb{Z}^d\), \(d \ge 2\) · Auxiliary critical point \(\tilde\beta_c(d)\) is positive for \(d \ge 2\) · Simon–Lieb inequality in the infinite-volume plus state · Gibbs expectation with a site field

DefinitionGibbs expectation with a site field#✓fully proved

The Gibbs expectation with site field H.

noncomputable def vertexFieldExpectation (β : ℝ) (J : Sym2 V → ℝ)
    (H : V → ℝ) (f : ConfigSpace V → ℝ) : ℝ :=
  (∑ s : ConfigSpace V, f s * vertexFieldWeight G β J H s) /
    vertexFieldZ G β J H

Uses 3 · Used by 5

Statement usesConfiguration space of a statistical-mechanics model · Boltzmann weight with a site field · Partition function with a site field

Used byInf-based and sup-based Ising critical points agree for \(d \ge 2\) · Sharpness of the Ising phase transition on \(\mathbb{Z}^d\), \(d \ge 2\) · Auxiliary critical point \(\tilde\beta_c(d)\) is positive for \(d \ge 2\) · Simon–Lieb inequality in the infinite-volume plus state · Two-point function with a site field

DefinitionTwo-point function with a site field#✓fully proved

The two-point function ⟨σ_aσ_b⟩_{β,J,H} with site field H.

noncomputable def vertexFieldTwoPoint (β : ℝ) (J : Sym2 V → ℝ)
    (H : V → ℝ) (a b : V) : ℝ :=
  vertexFieldExpectation G β J H (spinProd (sourcePair a b))

Uses 3 · Used by 4

Statement usesSpin product over a vertex set · Source pair \(\{a\} \triangle \{b\}\) · Gibbs expectation with a site field

Used byInf-based and sup-based Ising critical points agree for \(d \ge 2\) · Sharpness of the Ising phase transition on \(\mathbb{Z}^d\), \(d \ge 2\) · Auxiliary critical point \(\tilde\beta_c(d)\) is positive for \(d \ge 2\) · Simon–Lieb inequality in the infinite-volume plus state

DefinitionSimon weight of a boundary pair#✓fully proved

The Simon weight w(x, y) = tanh(βJ_{xy}) ⟨σ_oσ_x⟩_{J|S}.

noncomputable def simonWeight (β : ℝ) (J : Sym2 V → ℝ) (S : Finset V) (o : V) :
    V → V → ℝ :=
  fun x y => Real.tanh (β * J s(x, y)) * expectationJ G β (couplingIn J S) {o, x}

Uses 2

Statement usesCoupling restricted to the edges inside a set · Correlation function with couplings

StructureSimon–Lieb type inequality for a nonnegative two-point function#✓fully proved

A Simon–Lieb type inequality for a nonnegative two-point function τ, root o, set S, weights w and boundary targets B: τ(o, z) ≤ ∑_{x ∈ S} ∑_{y ∈ B} w(x, y) τ(y, z) for every z ∉ S.

structure SimonLieb (τ : V → V → ℝ) (o : V) (S : Finset V)
    (simWeight : V → V → ℝ) (boundaryTargets : Finset V) : Prop where
  /-- The two-point function is nonnegative. -/
  τ_nonneg : ∀ a b, 0 ≤ τ a b
  /-- The weights are nonnegative. -/
  weight_nonneg : ∀ x y, 0 ≤ simWeight x y
  /-- The Simon–Lieb bound for every `z ∉ S`. -/
  simon : ∀ z, z ∉ S →
    τ o z ≤ ∑ x ∈ S, ∑ y ∈ boundaryTargets, simWeight x y * τ y z

DefinitionSimon constant of a weight function#✓fully proved

The Simon constant φ = ∑_{x ∈ S} ∑_{y ∈ B} w(x, y).

noncomputable def simonConst (S : Finset V) (simWeight : V → V → ℝ) (boundaryTargets : Finset V) :
    ℝ := ∑ x ∈ S, ∑ y ∈ boundaryTargets, simWeight x y

DefinitionSpin pair product as a bounded continuous function#✓fully proved

The bounded continuous function σ ↦ σ_x σ_y on configuration space.

noncomputable def spinPairBCF (x y : Site d) :
    ConfigSpace (Site d) →ᵇ ℝ :=
  spinBCF x * spinBCF y

Uses 3 · Used by 4

Statement usesConfiguration space of a statistical-mechanics model · Spin at a site as a bounded continuous function · Site of the hypercubic lattice

Used byInf-based and sup-based Ising critical points agree for \(d \ge 2\) · Sharpness of the Ising phase transition on \(\mathbb{Z}^d\), \(d \ge 2\) · Auxiliary critical point \(\tilde\beta_c(d)\) is positive for \(d \ge 2\) · Simon–Lieb inequality in the infinite-volume plus state

DefinitionPlus-state two-point function at zero field#✓fully proved

The plus-state two-point function ⟨σ_xσ_y⟩^+_β at zero field.

noncomputable def plusCorr (d : ℕ) (β : ℝ) (x y : Site d) : ℝ :=
  ∫ ω, spin ω x * spin ω y
    ∂(plusState d β 0 : Measure (ConfigSpace (Site d)))

Uses 4 · Used by 7

Statement usesConfiguration space of a statistical-mechanics model · Infinite-volume plus state as a subsequential weak limit · Spin of a configuration at a site · Site of the hypercubic lattice

Used byInf-based and sup-based Ising critical points agree for \(d \ge 2\) · Tail set of plus-state correlations · Window sum of plus-state correlations · Sharpness of the Ising phase transition on \(\mathbb{Z}^d\), \(d \ge 2\) · Auxiliary critical point \(\tilde\beta_c(d)\) is positive for \(d \ge 2\) · Simon–Lieb inequality in the infinite-volume plus state · Simon–Lieb boundary sum in the plus state

DefinitionSimon–Lieb boundary sum against a measure#✓fully proved

The Simon–Lieb boundary sum ∑_{(x,y) ∈ ∂S} tanh β ⟨σ_0σ_x⟩_S ∫ σ_yσ_z dμ for a measure μ.

noncomputable def simonBoundaryIntegral
    (β : ℝ) (S : Finset (Site d)) (_o z : Site d)
    (μ : Measure (ConfigSpace (Site d))) : ℝ :=
  ∑ e ∈ boundaryEdges d S,
    Real.tanh β * corrOriginInner d β S e.1 *
      (∫ ω, spin ω e.2 * spin ω z ∂μ)

Uses 5 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Spin of a configuration at a site · Site of the hypercubic lattice · Oriented edge boundary of a finite lattice set · Free origin correlation in a set, extended by zero

Used bySimon–Lieb inequality in the infinite-volume plus state

DefinitionSimon–Lieb boundary sum in the plus state#✓fully proved

The Simon–Lieb boundary sum ∑_{(x,y) ∈ ∂S} tanh β ⟨σ_0σ_x⟩_S ⟨σ_yσ_z⟩^+_β in the plus state.

noncomputable def simonBoundaryPlus
    (β : ℝ) (S : Finset (Site d)) (_o z : Site d) : ℝ :=
  ∑ e ∈ boundaryEdges d S,
    Real.tanh β * corrOriginInner d β S e.1 * plusCorr d β e.2 z

Uses 4 · Used by 4

Statement usesSite of the hypercubic lattice · Oriented edge boundary of a finite lattice set · Free origin correlation in a set, extended by zero · Plus-state two-point function at zero field

Used byInf-based and sup-based Ising critical points agree for \(d \ge 2\) · Sharpness of the Ising phase transition on \(\mathbb{Z}^d\), \(d \ge 2\) · Auxiliary critical point \(\tilde\beta_c(d)\) is positive for \(d \ge 2\) · Simon–Lieb inequality in the infinite-volume plus state

DefinitionBoundary edges of a finite volume#✓fully proved

The edges touching Λ that are not inside Λ.

noncomputable def plusBoundaryEdges (Lambda : Finset (Site d)) :
    Finset (Sym2 (Site d)) :=
  (gvBondTouch Lambda).filter (fun e ↦ ¬ edgeInside Lambda e)

Uses 3 · Used by 5

Statement usesBonds touching a set · Site of the hypercubic lattice · Unordered pair inside a set

Used byInf-based and sup-based Ising critical points agree for \(d \ge 2\) · Sharpness of the Ising phase transition on \(\mathbb{Z}^d\), \(d \ge 2\) · Auxiliary critical point \(\tilde\beta_c(d)\) is positive for \(d \ge 2\) · Field induced by the plus boundary condition · Simon–Lieb inequality in the infinite-volume plus state

DefinitionField induced by the plus boundary condition#✓fully proved

The field on x ∈ Λ induced by the plus boundary condition: the number of edges from x to sites outside Λ.

noncomputable def plusBoundaryField (Lambda : Finset (Site d))
    (x : {v // v ∈ Lambda}) : ℝ :=
  ((plusBoundaryEdges Lambda).filter (fun e ↦ x.1 ∈ e)).card

Uses 2 · Used by 4

Statement usesSite of the hypercubic lattice · Boundary edges of a finite volume

Used byInf-based and sup-based Ising critical points agree for \(d \ge 2\) · Sharpness of the Ising phase transition on \(\mathbb{Z}^d\), \(d \ge 2\) · Auxiliary critical point \(\tilde\beta_c(d)\) is positive for \(d \ge 2\) · Simon–Lieb inequality in the infinite-volume plus state

DefinitionUnit coupling on the edges of a graph#✓fully proved

The coupling equal to 1 on the edges of G and 0 elsewhere.

noncomputable def unitEdgeCoupling {V : Type*} (G : SimpleGraph V)
    (e : Sym2 V) : ℝ :=
  if e ∈ G.edgeSet then 1 else 0

Used by 4

Used byInf-based and sup-based Ising critical points agree for \(d \ge 2\) · Sharpness of the Ising phase transition on \(\mathbb{Z}^d\), \(d \ge 2\) · Auxiliary critical point \(\tilde\beta_c(d)\) is positive for \(d \ge 2\) · Simon–Lieb inequality in the infinite-volume plus state

DefinitionUnderlying lattice sites of a subset of a volume#✓fully proved

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

noncomputable def plusCutSites {Lambda : Finset (Site d)}
    (T : Finset {v // v ∈ Lambda}) : Finset (Site d) :=
  T.image Subtype.val

Uses 1 · Used by 2

Statement usesSite of the hypercubic lattice

Used bySimon–Lieb inequality in the infinite-volume plus state · Identification of volume sites with lattice sites

DefinitionIdentification of volume sites with lattice sites#✓fully proved

The identification of T (as sites of Λ) with plusCutSites T (as sites of ℤ^d).

StatMech.Sharpness.plusCutVertexEquiv · 18 lines

noncomputable def plusCutVertexEquiv {Lambda : Finset (Site d)}
    (T : Finset {v // v ∈ Lambda}) :
    {x : {v // v ∈ Lambda} // x ∈ T} ≃
      {z : Site d // z ∈ plusCutSites T} :=
  Equiv.ofBijective
    (fun x ↦ ⟨x.1.1, mem_plusCutSites.mpr x.2⟩)
    ⟨by
      intro x y h
      apply Subtype.ext
      apply Subtype.ext
      exact congrArg
        (fun z : {z : Site d // z ∈ plusCutSites 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, hval⟩ := hz
      exact ⟨⟨x, hx⟩, Subtype.ext hval⟩⟩

Uses 2 · Used by 1

Statement usesSite of the hypercubic lattice · Underlying lattice sites of a subset of a volume

Used bySimon–Lieb inequality in the infinite-volume plus state

DefinitionSites of a volume lying in a set#✓fully proved

The sites of Λ that lie in T.

noncomputable def sitesInVolume (Lambda T : Finset (Site d)) :
    Finset {v // v ∈ Lambda} :=
  Finset.univ.filter (fun x ↦ x.1 ∈ T)

Uses 1 · Used by 1

Statement usesSite of the hypercubic lattice

Used bySimon–Lieb inequality in the infinite-volume plus state

TheoremSimon–Lieb inequality in the infinite-volume plus state#✓fully proved

The Simon–Lieb inequality in the infinite-volume plus state: for β ≥ 0, a finite T ∋ 0 and z ∉ T, ⟨σ_0σ_z⟩^+_β ≤ ∑_{(x,y) ∈ ∂T} tanh β ⟨σ_0σ_x⟩_T ⟨σ_yσ_z⟩^+_β. Reference: B. Simon, "Correlation inequalities and the decay of correlations in ferromagnets", Comm. Math. Phys. 77 (1980) 111–126; E. H. Lieb, "A refinement of Simon's correlation inequality", Comm. Math. Phys. 77 (1980) 127–135.

theorem plusCorr_simon
    (beta : ℝ) (hbeta : 0 ≤ beta)
    (T : Finset (Site d)) (ho : Percolation.origin d ∈ T)
    (z : Site d) (hzT : z ∉ T) :
    plusCorr d beta (Percolation.origin d) z ≤
      simonBoundaryPlus beta T (Percolation.origin d) z

Uses 91 · Used by 3

Statement usesSite of the hypercubic lattice · Origin of the hypercubic lattice · Plus-state two-point function at zero field · Simon–Lieb boundary sum in the plus state

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 · Infinite-volume state of a sequence of measures · Bond variable of an unordered pair · Bonds touching the box · Ordered nearest-neighbour pairs touching the box · Box \((-n, n)^d\) as a finite set of sites · Existence of infinite-volume states · 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 · Configuration glued from inside spins and a boundary condition · Site with its nearest neighbours · Bonds touching a set · Set with its nearest neighbours · Energy on a set with a boundary condition · Configuration glued from a set and a boundary condition · Finite-volume Gibbs measure on a finite set · Finite-volume Gibbs measure with plus boundary condition · Gibbs probability on a set with a boundary condition · Unit vector of \(\mathbb{Z}^d\) · Boltzmann weight on a set with a boundary condition · Partition function on a set with a boundary condition · Ising Hamiltonian on a finite graph · Box sites as a set and as a finite 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-plus configuration · Plus-boundary Ising measure in a box · Infinite-volume plus state as a subsequential weak limit · Spin of a configuration at a site · Spin value of a Boolean · Spin product over a vertex set · Nearest neighbours in \(\mathbb{Z}^d\) · Box \((-n, n)^d\) in the hypercubic lattice · Every finite set of sites lies in a box · 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 · Sign of a unit lattice step · 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 · Boltzmann weight with couplings · Free origin correlation in a set, extended by zero · Coupling restricted to the edges inside a set · Unordered pair inside a set · Edges of a graph inside a set · Gibbs expectation with inhomogeneous couplings and site fields · Correlation function with couplings · Free-boundary zero-field two-point function in a finite set · Induced subgraph of \(\mathbb{Z}^d\) on a finite set · Subgraph of edges inside a vertex set · Partition function with couplings · Boundary edges of a finite volume · Field induced by the plus boundary condition · Underlying lattice sites of a subset of a volume · Identification of volume sites with lattice sites · Simon–Lieb boundary sum against a measure · Sites of a volume lying in a set · Source pair \(\{a\} \triangle \{b\}\) · Spin pair product as a bounded continuous function · Two-point function with couplings · Simon–Lieb inequality on a finite graph · Unit coupling on the edges of a graph · Gibbs expectation with a site field · Two-point function with a site field · Boltzmann weight with a site field · Partition function with a site field · Ghost-graph coupling with a site field · Boltzmann weight with inhomogeneous couplings and site fields · Graph with a ghost vertex joined to every site · Weak convergence of probability measures on configuration space · Weak convergence implies convergence of integrals

Used byInf-based and sup-based Ising critical points agree for \(d \ge 2\) · Sharpness of the Ising phase transition on \(\mathbb{Z}^d\), \(d \ge 2\) · Auxiliary critical point \(\tilde\beta_c(d)\) is positive for \(d \ge 2\)

41 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.