Random currents and the switching lemma

AbbreviationCurrent: a multiplicity in \(\mathbb{N}\) for each unordered pair#✓fully proved

A current on the edges of V: a multiplicity n_e ∈ ℕ for every unordered pair e.

abbrev Current (V : Type*) : Type _ := Sym2 V → ℕ

Used by 35

Used byOutside part of a gated double-current summand · Cluster lower bound for double-current sums · Outside summand of a gated double-current sum · Gated double-current sum over edge-indexed currents · Random-current form of the \(\beta\)-derivative of the magnetization · 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\) · Vertices not connected to a vertex by positive current · Finite-volume mean-field inequality for the Ising model · Mean-field lower bound for the spontaneous magnetization · Canonical backbone path of a current · Connectivity through edges carrying positive current · Random-current representation · Subgraph of edges carrying positive current · Incident flux of a current at a vertex · Backbone paths along odd-current edges · Switching lemma · Current with no edge crossing a set's boundary · Subgraph of edges with odd current · Extension of an edge function to a current · Trace of a current as a bond configuration · Current with a walk removed · Restriction of a current to a set · Odd-current path as a backbone path · Least backbone path between two vertices · Odd-current paths between two vertices · Odd current on every edge of a path · Sources of a current · Weight of a random current · Current weights are nonnegative for nonnegative \(\beta\) and couplings · Indicator current of an edge set · Chosen first-exit data

DefinitionIncident flux of a current at a vertex#✓fully proved

The total multiplicity ∑_{e ∋ x} n_e of the edges of G incident to x.

noncomputable def incidentFlux (n : Current V) (x : V) : ℕ :=
  ∑ e ∈ G.edgeFinset.filter (fun e => x ∈ e), n e

Uses 1 · Used by 8

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

Used byCluster lower bound for double-current sums · Random-current form of the \(\beta\)-derivative of the magnetization · 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 · Random-current representation · Sources of a current · Chosen first-exit data

DefinitionSources of a current#✓fully proved

The sources ∂n: the vertices with odd incident flux.

noncomputable def sources (n : Current V) : Finset V :=
  Finset.univ.filter (fun x => Odd (incidentFlux G n x))

Uses 2 · Used by 19

Statement usesCurrent: a multiplicity in \(\mathbb{N}\) for each unordered pair · Incident flux of a current at a vertex

Used byOutside 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 · Gated double-current sum over edge-indexed currents · Random-current form of the \(\beta\)-derivative of the magnetization · 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 · Random-current representation · Current sum with prescribed sources · Switching lemma · Weight of currents with a given selected backbone · Double-current sum restricted to disconnection · Double-current sum with prescribed sources · Triple-current sum with prescribed sources · Sources on a graph's edge set agree with random-current sources · Weighted sum over splittings with prescribed sources · Chosen first-exit data

DefinitionWeight of a random current#✓fully proved

The current weight w(n) = ∏_{e ∈ E(G)} (βJ_e)^{n_e}/n_e!.

noncomputable def weight (β : ℝ) (J : Sym2 V → ℝ) (n : Current V) : ℝ :=
  ∏ e ∈ G.edgeFinset, (β * J e) ^ (n e) / (Nat.factorial (n e))

Uses 1 · Used by 19

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

Used byOutside 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 · Gated double-current sum over edge-indexed currents · Random-current form of the \(\beta\)-derivative of the magnetization · Gap-weighted current sum restricted to a predicate · 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 · Random-current representation · Current sum with prescribed sources · Switching lemma · Weight of currents with a given selected backbone · Double-current sum restricted to disconnection · Double-current sum with prescribed sources · Triple-current sum with prescribed sources · Weighted sum over splittings with prescribed sources · Current weights are nonnegative for nonnegative \(\beta\) and couplings

LemmaCurrent weights are nonnegative for nonnegative \(\beta\) and couplings#✓fully proved

Current weights are nonnegative for β ≥ 0 and nonnegative couplings.

lemma weight_nonneg (β : ℝ) (J : Sym2 V → ℝ) (hβ : 0 ≤ β) (hJ : ∀ e, 0 ≤ J e)
    (n : Current V) : 0 ≤ weight G β J n

Uses 2 · Used by 3

Statement usesCurrent: a multiplicity in \(\mathbb{N}\) for each unordered pair · 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

DefinitionSubgraph of edges carrying positive current#✓fully proved

The subgraph of G of edges with n_e ≥ 1.

def currentSubgraph (n : Current V) : SimpleGraph V where
  Adj x y := G.Adj x y ∧ 1 ≤ n s(x, y)
  symm := by
    constructor
    intro x y ⟨hadj, hpos⟩
    exact ⟨hadj.symm, by rwa [Sym2.eq_swap]⟩
  loopless := ⟨fun x ⟨hadj, _⟩ => hadj.ne rfl⟩

Uses 1 · Used by 6

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

Used byCluster lower bound for double-current sums · Random-current form of the \(\beta\)-derivative of the magnetization · 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 · Connectivity through edges carrying positive current

DefinitionConnectivity through edges carrying positive current#✓fully proved

x and y are joined by a path of edges carrying positive current.

def CurrentConnected (n : Current V) (x y : V) : Prop :=
  (currentSubgraph G n).Reachable x y

Uses 2 · Used by 8

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

Used byCluster lower bound for double-current sums · Random-current form of the \(\beta\)-derivative of the magnetization · Four-source lower bound for the pattern sum · Four-source double-current sum with a connection pattern · Vertices not connected to a vertex by positive current · Finite-volume mean-field inequality for the Ising model · Mean-field lower bound for the spontaneous magnetization · Double-current sum restricted to disconnection

DefinitionSubgraph of edges with odd current#✓fully proved

The subgraph of G of edges with odd multiplicity.

def oddSubgraph (n : Current V) : SimpleGraph V where
  Adj x y := G.Adj x y ∧ Odd (n s(x, y))
  symm := by
    constructor
    intro x y ⟨hadj, hodd⟩
    exact ⟨hadj.symm, by rwa [Sym2.eq_swap]⟩
  loopless := ⟨fun x ⟨hadj, _⟩ => hadj.ne rfl⟩

Uses 1 · Used by 4

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

Used byCanonical backbone path of a current · Backbone paths along odd-current edges · Odd-current path as a backbone path · Chosen first-exit data

AbbreviationBackbone paths along odd-current edges#✓fully proved

Backbone paths from x to y: paths in the subgraph of odd edges.

abbrev IsBackbonePath (n : Current V) (x y : V) : Type _ :=
  (oddSubgraph G n).Path x y

Uses 2 · Used by 3

Statement usesCurrent: a multiplicity in \(\mathbb{N}\) for each unordered pair · Subgraph of edges with odd current

Used byCanonical backbone path of a current · Odd-current path as a backbone path · Chosen first-exit data

DefinitionCanonical backbone path of a current#✓fully proved

A canonical backbone path: the least one for a given linear order on backbone paths.

noncomputable def backbone (n : Current V) (x y : V)
    [LinearOrder (IsBackbonePath G n x y)]
    (h : Nonempty (IsBackbonePath G n x y)) : IsBackbonePath G n x y :=
  (Finset.univ : Finset (IsBackbonePath G n x y)).min'
    (Finset.univ_nonempty_iff.mpr h)

Uses 3

Statement usesCurrent: a multiplicity in \(\mathbb{N}\) for each unordered pair · Backbone paths along odd-current edges · Subgraph of edges with odd current

DefinitionTrace of a current as a bond configuration#✓fully proved

The trace of a current: the bond configuration with e open iff n_e ≥ 1.

def percolationField (n : Current V) : Sym2 V → Bool :=
  fun e => decide (1 ≤ n e)

Uses 1

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

DefinitionGhost vertex of the extended vertex set#✓fully proved

The ghost vertex none of Option V.

def ghost : Option V := none

Used by 2

Used byAizenman–Barsky inequality on a finite graph · Aizenman–Barsky inequality on infinite vertex-transitive graphs

DefinitionGraph with a ghost vertex joined to every site#✓fully proved

The graph on V ⊔ {ghost} with the edges of G and an edge from every site to the ghost.

StatMech.Sharpness.withGhost · 18 lines

def withGhost : SimpleGraph (Option V) where
  Adj a b :=
    match a, b with
    | some x, some y => G.Adj x y
    | some _, none => True
    | none, some _ => True
    | none, none => False
  symm := by
    constructor
    rintro (_ | x) (_ | y) h
    · exact h
    · exact h
    · exact h
    · exact G.symm.symm _ _ h
  loopless := ⟨by
    rintro (_ | x) h
    · exact h
    · exact G.loopless.irrefl x h⟩

Used by 24

Used byAizenman–Barsky inequality on a finite graph · Finite-volume percolation magnetization · Sites connected to \(o\) with ghost edges closed · Aizenman–Barsky inequality on infinite vertex-transitive graphs · Infinite-volume percolation magnetization · Griffiths–Hurst–Sherman inequality · FKG lattice condition for the agreement law when \(\beta, h \ge 0\) · Griffiths–Hurst–Sherman inequality · Inhomogeneous weight of an agreement set · Griffiths–Hurst–Sherman inequality · Weight of an agreement set in the duplicated system · Inf-based and sup-based Ising critical points agree for \(d \ge 2\) · Bond term \(\Delta_e\) of the magnetization derivative · Random-current form of the \(\beta\)-derivative of the magnetization · Field term \(\Delta_z\) of the magnetization derivative · Cut 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 · Bond term: ghost-graph disconnection sum for a bond covariance · Field term: ghost-graph disconnection sum for a site covariance · Random-current representation with a field for even source sets · 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

DefinitionNumber of walk edges at a vertex#✓fully proved

The number of edges of the walk p incident to x.

def walkDeg {a b : V} (p : H.Walk a b) (x : V) : ℕ :=
  (p.edges.filter (fun e => x ∈ e)).length

Used by 1

Used byChosen first-exit data

DefinitionCurrent with a walk removed#✓fully proved

The current n with one unit removed from each traversal of an edge of p.

def removeWalk {a b : V} (n : Current V) (p : H.Walk a b) : Current V :=
  fun e => n e - p.edges.count e

Uses 1

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

DefinitionExtension of an edge function to a current#✓fully proved

Extension of a function on the edges of G to a current, zero off E(G).

noncomputable def ofEdgeFun (m : ↥G.edgeFinset → ℕ) : Current V :=
  fun e => if h : e ∈ G.edgeFinset then m ⟨e, h⟩ else 0

Uses 1 · Used by 16

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

Used byOutside 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 · Gated double-current sum over edge-indexed currents · Random-current form of the \(\beta\)-derivative of the magnetization · Gap-weighted current sum restricted to a predicate · 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 · Random-current representation · Current sum with prescribed sources · Weight of currents with a given selected backbone · Double-current sum restricted to disconnection · Double-current sum with prescribed sources · Triple-current sum with prescribed sources

DefinitionCurrent sum with prescribed sources#✓fully proved

The current sum Z(∂ = A) = ∑_{∂n = A} w(n) over currents on the edges of G.

noncomputable def currentSum (β : ℝ) (J : Sym2 V → ℝ) (A : Finset V) : ℝ :=
  ∑' m : ↥G.edgeFinset → ℕ,
    if sources G (ofEdgeFun G m) = A then weight G β J (ofEdgeFun G m) else 0

Uses 3 · Used by 10

Statement usesExtension 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 form of the \(\beta\)-derivative of the magnetization · Random-current cut mass of a vertex set · 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 · Sourced current sum as correlation times sourceless sum · Random-current representation · Random-current representation with a field for even source sets · Backbone weight \(\rho(\omega)\)

DefinitionTerm of the exponential expansion of an edge weight#✓fully proved

The k-th term (βJ_e σ_e)^k / k! of the expansion of exp(βJ_e σ_e).

noncomputable def gEdge (β : ℝ) (J : Sym2 V → ℝ) (s : ConfigSpace V)
    (e : Sym2 V) (k : ℕ) : ℝ := (β * J e) ^ k * (bond s e) ^ k / k.factorial

Uses 2 · Used by 6

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

Used byCluster lower bound for double-current sums · Random-current form of the \(\beta\)-derivative of the magnetization · 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 · Random-current representation

DefinitionBoltzmann weight with couplings#✓fully proved

The Boltzmann weight exp(β ∑_e J_e σ_e) with couplings J.

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

Uses 2 · Used by 14

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

Used byInf-based and sup-based Ising critical points agree for \(d \ge 2\) · Cluster lower bound for double-current sums · Random-current form of the \(\beta\)-derivative of the magnetization · 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 · Random-current representation · Correlation function with couplings · Random-current representation with a field for even source sets · Partition function with couplings · 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 inequality on a finite graph

DefinitionPartition function with couplings#✓fully proved

The partition function with couplings J.

noncomputable def partitionJ (β : ℝ) (J : Sym2 V → ℝ) : ℝ :=
  ∑ s : ConfigSpace V, boltzmannJ G β J s

Uses 2 · Used by 13

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

Used byInf-based and sup-based Ising critical points agree for \(d \ge 2\) · Cluster lower bound for double-current sums · Random-current form of the \(\beta\)-derivative of the magnetization · 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 · Random-current representation · Correlation function with couplings · Random-current representation with a field for even source sets · 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 inequality on a finite graph

DefinitionCorrelation function with couplings#✓fully proved

The correlation ⟨σ_A⟩_{β,J} with couplings J.

noncomputable def expectationJ (β : ℝ) (J : Sym2 V → ℝ) (A : Finset V) : ℝ :=
  (∑ s : ConfigSpace V, spinProd A s * boltzmannJ G β J s) / partitionJ G β J

Uses 4 · Used by 16

Statement usesConfiguration space of a statistical-mechanics model · Spin product over a vertex set · Boltzmann weight with couplings · Partition function with couplings

Used byInf-based and sup-based Ising critical points agree for \(d \ge 2\) · Cluster lower bound for double-current sums · Random-current form of the \(\beta\)-derivative of the magnetization · 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 · Sourced current sum as correlation times sourceless sum · Random-current representation · Random-current representation with a field for even source sets · 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 weight of a boundary pair · Two-point function with couplings · Simon–Lieb inequality on a finite graph

TheoremRandom-current representation#✓fully proved

The random-current representation: ⟨σ_A⟩_{β,J} = Z(∂ = A)/Z(∂ = ∅). Reference: M. Aizenman, "Geometric analysis of φ⁴ fields and Ising models", Comm. Math. Phys. 86 (1982) 1–48; J. Ginibre (1970); H. Duminil-Copin, "Random currents expansion of the Ising model", lecture notes (2016), arXiv:1607.06933.

theorem current_representation (β : ℝ) (J : Sym2 V → ℝ) (A : Finset V) :
    expectationJ G β J A = currentSum G β J A / currentSum G β J ∅

Uses 15 · Used by 7

Statement usesCurrent sum with prescribed sources · Correlation function with couplings

Proof usesConfiguration space of a statistical-mechanics model · Bond variable of an unordered pair · Spin of a configuration at a site · Spin value of a Boolean · Spin product over a vertex set · Current: a multiplicity in \(\mathbb{N}\) for each unordered pair · Boltzmann weight 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 · Partition function with couplings · Sources of a current · Weight of a random current

Used byCluster lower bound for double-current sums · Random-current form of the \(\beta\)-derivative of the magnetization · 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 · Sourced current sum as correlation times sourceless sum · Random-current representation with a field for even source sets

DefinitionOdd current on every edge of a path#✓fully proved

Every edge of the path carries odd current.

def shb_IsBackboneOf (n : Current V) (x y : V) (ω : G.Path x y) : Prop :=
  ∀ e ∈ ω.1.edges, Odd (n e)

Uses 1 · Used by 2

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

Used byOdd-current path as a backbone path · Odd-current paths between two vertices

DefinitionOdd-current paths between two vertices#✓fully proved

The paths from x to y all of whose edges carry odd current.

noncomputable def shb_backboneSet (n : Current V) (x y : V) : Finset (G.Path x y) :=
  Finset.univ.filter (fun ω => shb_IsBackboneOf G n x y ω)

Uses 2 · Used by 1

Statement usesCurrent: a multiplicity in \(\mathbb{N}\) for each unordered pair · Odd current on every edge of a path

Used byLeast backbone path between two vertices

DefinitionOdd-current path as a backbone path#✓fully proved

A path with odd current on every edge as a backbone path.

noncomputable def shb_backboneOf_imp_isBackbonePath (n : Current V) (x y : V) (ω : G.Path x y)
    (h : shb_IsBackboneOf G n x y ω) : IsBackbonePath G n x y := by
  refine ⟨ω.1.transfer (oddSubgraph G n) ?_, ω.2.transfer _⟩
  intro e he
  have hG : e ∈ G.edgeSet := ω.1.edges_subset_edgeSet he
  have hodd : Odd (n e) := h e he
  revert hG hodd
  refine Sym2.ind (fun a b => ?_) e
  intro hG hodd
  rw [SimpleGraph.mem_edgeSet] at hG ⊢
  exact ⟨hG, hodd⟩

Uses 4

Statement usesCurrent: a multiplicity in \(\mathbb{N}\) for each unordered pair · Backbone paths along odd-current edges · Subgraph of edges with odd current · Odd current on every edge of a path

DefinitionLeast backbone path between two vertices#✓fully proved

The least backbone path from x to y, if any.

noncomputable def shb_backboneSelect (n : Current V) (x y : V) : Option (G.Path x y) :=
  if h : (shb_backboneSet G n x y).Nonempty then
    some ((shb_backboneSet G n x y).min' h) else none

Uses 2 · Used by 1

Statement usesCurrent: a multiplicity in \(\mathbb{N}\) for each unordered pair · Odd-current paths between two vertices

Used byWeight of currents with a given selected backbone

DefinitionWeight of currents with a given selected backbone#✓fully proved

Z_ω: the total weight of currents with sources {x, y} whose selected backbone is ω.

noncomputable def shb_backboneNum (β : ℝ) (J : Sym2 V → ℝ) (x y : V) (ω : G.Path x y) : ℝ :=
  ∑' m : ↥G.edgeFinset → ℕ,
    if Sharpness.sources G (ofEdgeFun G m) = {x, y}
        ∧ shb_backboneSelect G (ofEdgeFun G m) x y = some ω then
      weight G β J (ofEdgeFun G m) else 0

Uses 4 · Used by 1

Statement usesExtension of an edge function to a current · Least backbone path between two vertices · Sources of a current · Weight of a random current

Used byBackbone weight \(\rho(\omega)\)

DefinitionBackbone weight \(\rho(\omega)\)#✓fully proved

The backbone weight ρ(ω) = Z_ω/Z(∂ = ∅).

noncomputable def shb_rho (β : ℝ) (J : Sym2 V → ℝ) (x y : V) (ω : G.Path x y) : ℝ :=
  shb_backboneNum G β J x y ω / currentSum G β J ∅

Uses 2

Statement usesCurrent sum with prescribed sources · Weight of currents with a given selected backbone

DefinitionUnordered pair inside a set#✓fully proved

An unordered pair e is inside S if both of its endpoints lie in S.

def edgeInside (S : Finset V) (e : Sym2 V) : Prop := ∀ v ∈ e, v ∈ S

Used by 28

Used byGriffiths–Hurst–Sherman inequality · FKG lattice condition for the agreement law when \(\beta, h \ge 0\) · Griffiths–Hurst–Sherman inequality · Griffiths–Hurst–Sherman inequality · Edges of the induced subgraph on a vertex set · Inf-based and sup-based Ising critical points agree for \(d \ge 2\) · Extension by zero of a current inside a set · Extension by zero of a current outside a set · Cluster lower bound for double-current sums · Coupling restricted to the edges inside a set · Edges of a graph inside a set · Edge lying inside a set · Four-source lower bound for the pattern sum · 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 · Current with no edge crossing a set's boundary · Restriction of a current to a set · 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 · Edges of a graph inside a set · High-temperature switching map · Switching map between valid inputs and outputs · Boundary edges of a finite volume · Simon–Lieb inequality in the infinite-volume plus state · Simon–Lieb inequality on a finite graph

DefinitionCurrent with no edge crossing a set's boundary#✓fully proved

The current n uses no edge joining S to Sᶜ: every edge with n e ≥ 1 is inside S or inside Sᶜ.

def NoCrossing (n : Current V) (S : Finset V) : Prop :=
  ∀ e ∈ G.edgeFinset, 1 ≤ n e → edgeInside S e ∨ edgeInside Sᶜ e

Uses 2 · Used by 4

Statement usesCurrent: a multiplicity in \(\mathbb{N}\) for each unordered pair · Unordered pair 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

DefinitionRestriction of a current to a set#✓fully proved

The restriction n|_S of a current to the edges inside S, zero elsewhere.

noncomputable def restrictTo (n : Current V) (S : Finset V) : Current V :=
  fun e => if edgeInside S e then n e else 0

Uses 2 · Used by 4

Statement usesCurrent: a multiplicity in \(\mathbb{N}\) for each unordered pair · Unordered pair 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

DefinitionSubsets of a sigma type as families of fibre subsets#✓fully proved

Subsets of Σ e, β e correspond to families of subsets of the fibres.

noncomputable def sigmaFinsetEquivPi : Finset (Σ e : E, β e) ≃ Π e : E, Finset (β e) where
  toFun S := fun e => (univ : Finset (β e)).filter (fun b => (⟨e, b⟩ : Σ e, β e) ∈ S)
  invFun f := univ.filter (fun i : Σ e, β e => i.2 ∈ f i.1)
  left_inv := by intro S; ext i; obtain ⟨e, b⟩ := i; simp
  right_inv := by intro f; ext e b; simp

Used by 5

Used byCluster lower bound for double-current sums · Random-current form of the \(\beta\)-derivative of the magnetization · 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

AbbreviationEdge copies of a current#✓fully proved

The edge copies of a current m: m_e copies of each edge e.

abbrev Copy (m : ↥G.edgeFinset → ℕ) : Type _ := Σ e : ↥G.edgeFinset, Fin (m e)

Used by 8

Used byCluster lower bound for double-current sums · Random-current form of the \(\beta\)-derivative of the magnetization · Switching gap of a current · 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 · Endpoints of an edge copy · Profile of a set of edge copies

DefinitionEndpoints of an edge copy#✓fully proved

The endpoints of an edge copy.

def endsM (m : ↥G.edgeFinset → ℕ) : Copy G m → Sym2 V := fun i => i.1.1

Uses 1 · Used by 6

Statement usesEdge copies of a current

Used byCluster lower bound for double-current sums · Random-current form of the \(\beta\)-derivative of the magnetization · Switching gap of a current · 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

DefinitionProfile of a set of edge copies#✓fully proved

The profile of a set of copies: the number of copies of each edge it contains.

noncomputable def profileFlux (m : ↥G.edgeFinset → ℕ) (S : Finset (Copy G m)) :
    ↥G.edgeFinset → ℕ :=
  fun e => #(S.filter (fun i : Copy G m => i.1 = e))

Uses 1 · Used by 5

Statement usesEdge copies of a current

Used byCluster lower bound for double-current sums · Random-current form of the \(\beta\)-derivative of the magnetization · 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

DefinitionDouble-current sum restricted to disconnection#✓fully proved

The double-current sum ∑_{∂n₁ = A, ∂n₂ = B} w(n₁) w(n₂) 1_{u ↮ v in n₁ + n₂}.

noncomputable def sourcePairDisconnSum (β : ℝ) (J : Sym2 V → ℝ) (A B : Finset V) (u v : V) : ℝ :=
  ∑' 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 ¬ CurrentConnected G (ofEdgeFun G (fun e => pq.1 e + pq.2 e)) u v then 1 else 0)

Uses 4 · Used by 7

Statement usesConnectivity through edges carrying positive current · Extension of an edge function to a current · Sources of a current · Weight of a random current

Used byBond term \(\Delta_e\) of the magnetization derivative · Random-current form of the \(\beta\)-derivative of the magnetization · Field term \(\Delta_z\) of the magnetization derivative · Finite-volume mean-field inequality for the Ising model · Mean-field lower bound for the spontaneous magnetization · Bond term: ghost-graph disconnection sum for a bond covariance · Field term: ghost-graph disconnection sum for a site covariance

DefinitionGraph edges as ghost-graph edges#✓fully proved

The edges of G, as edges of the ghost graph.

noncomputable def origEdges : Finset (Sym2 (Option V)) := G.edgeFinset.image (Sym2.map some)

Used by 14

Used byAizenman–Barsky inequality on a finite graph · Aizenman–Barsky inequality on infinite vertex-transitive graphs · Griffiths–Hurst–Sherman inequality · FKG lattice condition for the agreement law when \(\beta, h \ge 0\) · Griffiths–Hurst–Sherman inequality · Griffiths–Hurst–Sherman inequality · Inf-based and sup-based Ising critical points agree for \(d \ge 2\) · Random-current form of the \(\beta\)-derivative of the magnetization · Finite-volume mean-field inequality for the Ising model · Mean-field lower bound for the spontaneous magnetization · Random-current representation with a field for even source sets · 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

DefinitionGhost edges#✓fully proved

The ghost edges {x, ghost}.

noncomputable def ghostEdges (V : Type*) [Fintype V] [DecidableEq V] :
    Finset (Sym2 (Option V)) := (univ : Finset V).image (fun x => s(some x, none))

Used by 20

Used byAizenman–Barsky inequality on a finite graph · Edge parameters with a ghost field · Ghost edges at the physical cluster of \(o\) · Closing all ghost edges · Correspondence between sites and ghost edges · Closing all ghost edges but one · Probability of a physical configuration · Aizenman–Barsky inequality on infinite vertex-transitive graphs · Griffiths–Hurst–Sherman inequality · FKG lattice condition for the agreement law when \(\beta, h \ge 0\) · Griffiths–Hurst–Sherman inequality · Griffiths–Hurst–Sherman inequality · Inf-based and sup-based Ising critical points agree for \(d \ge 2\) · Random-current form of the \(\beta\)-derivative of the magnetization · Finite-volume mean-field inequality for the Ising model · Mean-field lower bound for the spontaneous magnetization · Random-current representation with a field for even source sets · 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

DefinitionCoupling on the ghost graph with uniform field#✓fully proved

The coupling on the ghost graph: J on the edges of G and h on the ghost edges.

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

Used by 15

Used byCoupling lifted to the ghost graph · Real edge parameters with a ghost field · Griffiths–Hurst–Sherman inequality · FKG lattice condition for the agreement law when \(\beta, h \ge 0\) · Griffiths–Hurst–Sherman inequality · Weight of an agreement set in the duplicated system · Bond term \(\Delta_e\) of the magnetization derivative · Random-current form of the \(\beta\)-derivative of the magnetization · Field term \(\Delta_z\) of the magnetization derivative · Cut 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 · Bond term: ghost-graph disconnection sum for a bond covariance · Field term: ghost-graph disconnection sum for a site covariance · Random-current representation with a field for even source sets

DefinitionGlobal spin flip#✓fully proved

The global spin flip σ ↦ -σ.

def flipV (s : ConfigSpace V) : ConfigSpace V := fun v => ! s v

Uses 1 · Used by 12

Statement usesConfiguration space of a statistical-mechanics model

Used byGriffiths–Hurst–Sherman inequality · FKG lattice condition for the agreement law when \(\beta, h \ge 0\) · Griffiths–Hurst–Sherman inequality · Griffiths–Hurst–Sherman inequality · Inf-based and sup-based Ising critical points agree for \(d \ge 2\) · Random-current form of the \(\beta\)-derivative of the magnetization · Finite-volume mean-field inequality for the Ising model · Mean-field lower bound for the spontaneous magnetization · Random-current representation with a field for even source sets · 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

DefinitionEmbedding of vertices into the ghost graph#✓fully proved

The embedding V ↪ Option V.

def someEmb : V ↪ Option V := ⟨some, Option.some_injective V⟩

Used by 17

Used byGriffiths–Hurst–Sherman inequality · FKG lattice condition for the agreement law when \(\beta, h \ge 0\) · Griffiths–Hurst–Sherman inequality · Griffiths–Hurst–Sherman inequality · Image of a vertex set among non-ghost vertices · Inf-based and sup-based Ising critical points agree for \(d \ge 2\) · Vertex subsets as ghost-free subsets of the extended vertex set · Ghost source set of a bond covariance · Random-current form of the \(\beta\)-derivative of the magnetization · Ghost source set of a field covariance · Cut 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 · Random-current representation with a field for even source sets · 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

LemmaRandom-current representation with a field for even source sets#✓fully proved

The random-current representation with a field: for |A| even, ⟨σ_A⟩_{β,h} = Z_ghost(∂ = A)/Z_ghost(∂ = ∅) on the ghost graph. 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; H. Duminil-Copin, "Random currents expansion of the Ising model", lecture notes (2016), arXiv:1607.06933.

lemma fgd_isingExpectation_eq_currentSum_ratio (β h : ℝ) (A : Finset V) (hA : Even A.card) :
    isingExpectation G β h (spinProd A)
      = currentSum (withGhost G) β (ghostCoupling h β (fun _ => 1)) (A.map someEmb)
          / currentSum (withGhost G) β (ghostCoupling h β (fun _ => 1)) ∅

Uses 22 · Used by 1

Statement usesFinite-volume Ising expectation · Spin product over a vertex set · Coupling on the ghost graph with uniform field · Embedding of vertices into the ghost graph · Current sum with prescribed sources · Graph with a ghost vertex joined to every site

Proof usesConfiguration space of a statistical-mechanics model · Bond 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 of a configuration at a site · Spin value of a Boolean · Global spin flip · Ghost edges · Graph edges as ghost-graph edges · Boltzmann weight with couplings · Random-current representation · Correlation function with couplings · Partition function with couplings

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

DefinitionReparametrizing triples of functions by their sum and two summands#✓fully proved

Triples of functions to ℕ correspond to a sum m together with two functions with pointwise sum ≤ m.

StatMech.Sharpness.tripleEquivSigma · 16 lines

def tripleEquivSigma {E : Type*} :
    ((E → ℕ) × (E → ℕ) × (E → ℕ)) ≃
      Σ m : (E → ℕ), {pq : (E → ℕ) × (E → ℕ) // ∀ e, pq.1 e + pq.2 e ≤ m e} where
  toFun klm :=
    ⟨fun e => klm.1 e + klm.2.1 e + klm.2.2 e,
      ⟨(klm.1, klm.2.1), fun e => by simp only; omega⟩⟩
  invFun s := (s.2.1.1, s.2.1.2, fun e => s.1 e - s.2.1.1 e - s.2.1.2 e)
  left_inv := by
    rintro ⟨k, l, m⟩
    refine Prod.ext rfl (Prod.ext rfl ?_)
    funext e; simp only []; omega
  right_inv := by
    rintro ⟨m, ⟨⟨p, q⟩, hpq⟩⟩
    have h1 : (fun e => p e + q e + (m e - p e - q e)) = m := by
      ext e; have h := hpq e; simp only at h; omega
    exact Sigma.subtype_ext h1 (by simp only)

DefinitionTriple-current sum with prescribed sources#✓fully proved

The triple-current sum ∑_{∂n₁ = A, ∂n₂ = B, ∂n₃ = C} w(n₁) w(n₂) w(n₃).

noncomputable def sourceTripleSum (β : ℝ) (J : Sym2 V → ℝ) (A B C : Finset V) : ℝ :=
  ∑' z : (↥G.edgeFinset → ℕ) × (↥G.edgeFinset → ℕ) × (↥G.edgeFinset → ℕ),
    (if sources G (ofEdgeFun G z.1) = A then weight G β J (ofEdgeFun G z.1) else 0)
    * (if sources G (ofEdgeFun G z.2.1) = B then weight G β J (ofEdgeFun G z.2.1) else 0)
    * (if sources G (ofEdgeFun G z.2.2) = C then weight G β J (ofEdgeFun G z.2.2) else 0)

Uses 3

Statement usesExtension of an edge function to a current · Sources of a current · Weight of a random current

DefinitionDegree of a vertex in a multigraph edge set#✓fully proved

The degree of x in the multigraph edge set T.

def degK (ends : ι → Sym2 V) (T : Finset ι) (x : V) : ℕ :=
  #(T.filter (fun i => x ∈ ends i))

Used by 8

Used byCluster lower bound for double-current sums · Random-current form of the \(\beta\)-derivative of the magnetization · 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 · Odd-degree vertices in a cluster · Sources of a multigraph edge set · Switching lemma for multigraph currents

DefinitionSources of a multigraph edge set#✓fully proved

The odd-degree vertices of the multigraph edge set T.

def sources (ends : ι → Sym2 V) (T : Finset ι) : Finset V :=
  (Finset.univ : Finset V).filter (fun x => Odd (degK ends T x))

Uses 1 · Used by 11

Statement usesDegree of a vertex in a multigraph edge set

Used byDomination condition fails on the triangle · Mass of sub-currents with a given source set · Cluster lower bound for double-current sums · Random-current form of the \(\beta\)-derivative of the magnetization · Switching gap of a current · 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 · Sub-subset-weighted pair sum on a multigraph · Sum over edge sets split into parts with sources \(A\) and \(B\) · Switching lemma for multigraph currents

DefinitionAdjacency through an edge of a multigraph edge set#✓fully proved

a ≠ b are the endpoints of an edge of K.

def adjStep (ends : ι → Sym2 V) (K : Finset ι) (a b : V) : Prop :=
  ∃ i ∈ K, a ∈ ends i ∧ b ∈ ends i ∧ a ≠ b

Used by 8

Used byDomination condition fails on the triangle · Cluster lower bound for double-current sums · Random-current form of the \(\beta\)-derivative of the magnetization · 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 · Connectivity in a multigraph edge set · Switching lemma for multigraph currents

DefinitionConnectivity in a multigraph edge set#✓fully proved

Connectivity in K: the reflexive transitive closure of adjStep.

def connK (ends : ι → Sym2 V) (K : Finset ι) : V → V → Prop :=
  Relation.ReflTransGen (adjStep ends K)

Uses 1 · Used by 12

Statement usesAdjacency through an edge of a multigraph edge set

Used byDomination condition fails on the triangle · Current connecting all three site pairs · Current connecting none of the three site pairs · Three-site backbone factor · Cluster lower bound for double-current sums · Random-current form of the \(\beta\)-derivative of the magnetization · 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 · Cluster of a vertex in a multigraph edge set · Vertices not connected to a root through a multigraph edge set · Switching lemma for multigraph currents

DefinitionCluster of a vertex in a multigraph edge set#✓fully proved

The cluster of u in K.

noncomputable def compOf (ends : ι → Sym2 V) (K : Finset ι) (u : V) : Finset V :=
  (Finset.univ : Finset V).filter (fun x => connK ends K u x)

Uses 1 · Used by 7

Statement usesConnectivity in a multigraph edge set

Used byBackbone cluster of a site in a current · Random-current form of the \(\beta\)-derivative of the magnetization · 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 · Odd-degree vertices in a cluster · Switching lemma for multigraph currents

TheoremSwitching lemma for multigraph currents#✓fully proved

The switching lemma: for m with sources A and u ≠ v, ∑_{K ⊆ m, ∂K = A ∆ {u, v}} F(m) = ∑_{K ⊆ m, ∂K = A} F(m) 1_{u ↔ v in m}. Reference: M. Aizenman, "Geometric analysis of φ⁴ fields and Ising models", Comm. Math. Phys. 86 (1982) 1–48; H. Duminil-Copin, "Random currents expansion of the Ising model", lecture notes (2016), arXiv:1607.06933.

theorem switching_lemma (ends : ι → Sym2 V) (m : Finset ι)
    (hnd : ∀ i ∈ m, ¬ (ends i).IsDiag) (A : Finset V) (hm : sources ends m = A)
    {u v : V} (huv : u ≠ v) (F : Finset ι → ℝ) :
    ∑ _K ∈ m.powerset.filter (fun K => sources ends K = A ∆ {u, v}), F m
      = ∑ _K ∈ m.powerset.filter (fun K => sources ends K = A),
          F m * (if connK ends m u v then 1 else 0)

Uses 5 · Used by 3

Statement usesConnectivity in a multigraph edge set · Sources of a multigraph edge set

Proof usesAdjacency through an edge of a multigraph edge set · Cluster of a vertex in a multigraph edge set · Degree of a vertex in a multigraph edge 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

DefinitionSub-subset-weighted pair sum on a multigraph#✓fully proved

For a multigraph ends, the sum over edge subsets m with sources A of F m times the number of sub-subsets K ⊆ m with sources A, restricted to m satisfying P.

noncomputable def drd_pairSum (ends : ι → Sym2 V) (A : Finset V) (F : Finset ι → ℝ)
    (P : Finset ι → Prop) : ℝ :=
  ∑ m ∈ (Finset.univ.powerset.filter (fun m => RandomCurrent.sources ends m = A)),
    (∑ _K ∈ m.powerset.filter (fun K => RandomCurrent.sources ends K = A),
        F m * (if P m then 1 else 0))

Uses 1

Statement usesSources of a multigraph edge set

DefinitionVertices not connected to a root through a multigraph edge set#✓fully proved

The vertices not connected to o using edges of m in the multigraph ends.

noncomputable def notConnCompK (ends : ι → Sym2 V) (m : Finset ι) (o : V) : Finset V :=
  (Finset.univ : Finset V).filter (fun w => ¬ connK ends m o w)

Uses 1

Statement usesConnectivity in a multigraph edge set

DefinitionMultigraph edge lying inside a vertex set#✓fully proved

Both endpoints of the multigraph edge i lie in S.

def edgeInsideK (ends : ι → Sym2 V) (S : Finset V) (i : ι) : Prop := ∀ w ∈ ends i, w ∈ S

Used by 1

Used byMultigraph edge set with no edge crossing a vertex set

DefinitionMultigraph edge set with no edge crossing a vertex set#✓fully proved

Every edge of m lies inside S or inside Sᶜ.

def NoCrossingK (ends : ι → Sym2 V) (m : Finset ι) (S : Finset V) : Prop :=
  ∀ i ∈ m, edgeInsideK ends S i ∨ edgeInsideK ends Sᶜ i

Uses 1

Statement usesMultigraph edge lying inside a vertex set

DefinitionSum over edge sets split into parts with sources \(A\) and \(B\)#✓fully proved

The sum over edge sets m with sources A ∆ B and over splittings m = K ⊔ (m \ K) with sources A and B of F m.

noncomputable def srcPairFamily (ends : ι → Sym2 V) (A B : Finset V) (F : Finset ι → ℝ) : ℝ :=
  ∑ m ∈ (Finset.univ.powerset.filter (fun m => sources ends m = A ∆ B)),
    (∑ _K ∈ m.powerset.filter
        (fun K => sources ends K = A ∧ sources ends (m \ K) = B), F m)

Uses 1

Statement usesSources of a multigraph edge set

DefinitionOdd-degree vertices in a cluster#✓fully proved

The odd-degree vertices of m in the cluster of u.

noncomputable def compOddVertices (ends : ι → Sym2 V) (m : Finset ι) (u : V) : Finset V :=
  (compOf ends m u).filter (fun x => Odd (degK ends m x))

Uses 2 · Used by 2

Statement usesCluster of a vertex in a multigraph edge set · Degree of a vertex in a multigraph edge set

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

DefinitionFour-vertex multigraph with edges \(\{0, 1\}\) and \(\{2, 3\}\)#✓fully proved

A multigraph on Fin 4 with the two edges {0, 1} and {2, 3}.

def witEnds : Fin 2 → Sym2 (Fin 4)
  | 0 => s(0, 1)
  | 1 => s(2, 3)

DefinitionFull edge set of the four-vertex multigraph#✓fully proved

All edges of witEnds.

def witM : Finset (Fin 2) := Finset.univ

DefinitionSingle-edge current weight \((\beta J_e)^k/k!\)#✓fully proved

The single-edge weight (βJ_e)^k / k!.

noncomputable def wEdge (β : ℝ) (J : Sym2 V → ℝ) (e : Sym2 V) (k : ℕ) : ℝ :=
  (β * J e) ^ k / k.factorial

Used by 5

Used byCluster lower bound for double-current sums · Random-current form of the \(\beta\)-derivative of the magnetization · 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

DefinitionReparametrizing pairs of functions by their sum and one summand#✓fully proved

Pairs (p, q) of functions to ℕ correspond to a sum m = p + q together with p ≤ m.

def pairEquivSigma {E : Type*} :
    ((E → ℕ) × (E → ℕ)) ≃ Σ m : (E → ℕ), {p : E → ℕ // p ≤ m} where
  toFun pq := ⟨fun e => pq.1 e + pq.2 e, ⟨pq.1, fun e => Nat.le_add_right _ _⟩⟩
  invFun mp := (mp.2.1, fun e => mp.1 e - mp.2.1 e)
  left_inv := by rintro ⟨p, q⟩; ext e <;> simp
  right_inv := by
    rintro ⟨m, ⟨p, hp⟩⟩
    have hm : (fun e => p e + (m e - p e)) = m := by
      ext e; exact Nat.add_sub_cancel' (hp e)
    simp only
    exact Sigma.subtype_ext hm rfl

Used by 5

Used byCluster lower bound for double-current sums · Random-current form of the \(\beta\)-derivative of the magnetization · 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

DefinitionDouble-current sum with prescribed sources#✓fully proved

The double-current sum ∑_{∂n₁ = A, ∂n₂ = B} w(n₁) w(n₂).

noncomputable def sourcePairSum (β : ℝ) (J : Sym2 V → ℝ) (A B : Finset V) : ℝ :=
  ∑' 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)

Uses 3 · Used by 3

Statement usesExtension of an edge function to a current · Sources of a current · Weight of a random current

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

AbbreviationCurrent as a multiplicity on unordered pairs#✓fully proved

A current: a multiplicity in ℕ on every unordered pair. See also StatMech.Sharpness.Current.

abbrev Current (V : Type*) : Type _ := Sym2 V → ℕ

Used by 15

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 · Restriction of a current to an edge predicate · Incident flux of a current on an edge set · Switching lemma · Switching lemma · Edges of an edge set with odd multiplicity · Edges of an edge set with positive multiplicity · Reflection of a sub-current along an edge set · Reflection as an involution of the sub-currents of a current · Source set of a current on an edge set · Sources on a graph's edge set agree with random-current sources · Weighted sum over splittings with prescribed sources · Chosen first-exit data

DefinitionIncident flux of a current on an edge set#✓fully proved

The total multiplicity of the edges of E incident to x.

def incidentFlux (n : Current V) (x : V) : ℕ :=
  ∑ e ∈ E.filter (fun e => x ∈ e), n e

Uses 1 · Used by 7

Statement usesCurrent as a multiplicity on unordered pairs

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 · Switching lemma · Switching lemma · Source set of a current on an edge set · Chosen first-exit data

DefinitionSource set of a current on an edge set#✓fully proved

The source set of a current: the sites with odd incident flux. See also StatMech.Sharpness.sources and StatMech.Ising.sources_edgeFinset_eq.

def sources (n : Current V) : Finset V :=
  Finset.univ.filter (fun x => Odd (incidentFlux E n x))

Uses 2 · Used by 7

Statement usesCurrent as a multiplicity on unordered pairs · Incident flux of a current on an edge set

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 · Switching lemma · Switching lemma · Sources on a graph's edge set agree with random-current sources · Chosen first-exit data

DefinitionAdjacency through an edge of an edge set#✓fully proved

a and b are distinct endpoints of an edge in P.

def adjP (P : Finset (Sym2 V)) (a b : V) : Prop :=
  ∃ e ∈ P, a ∈ e ∧ b ∈ e ∧ a ≠ b

Used by 7

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 · Connectivity through the edges of an edge set · Switching lemma · Switching lemma · Chosen first-exit data

DefinitionConnectivity through the edges of an edge set#✓fully proved

Connectivity through the edges of P: the reflexive-transitive closure of adjP P.

def connP (P : Finset (Sym2 V)) : V → V → Prop :=
  Relation.ReflTransGen (adjP P)

Uses 1 · Used by 7

Statement usesAdjacency through an edge of an edge set

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 · Cluster of a site in an edge set · Switching lemma · Switching lemma · Chosen first-exit data

DefinitionEdges of an edge set with positive multiplicity#✓fully proved

The edges of E with positive multiplicity.

def posEdges (m : Current V) : Finset (Sym2 V) := E.filter (fun e => 1 ≤ m e)

Uses 1 · Used by 3

Statement usesCurrent as a multiplicity on unordered pairs

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

DefinitionEdges of an edge set with odd multiplicity#✓fully proved

The edges of E with odd multiplicity.

def oddEdges (m : Current V) : Finset (Sym2 V) := E.filter (fun e => Odd (m e))

Uses 1 · Used by 6

Statement usesCurrent as a multiplicity on unordered pairs

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 · Switching lemma · Switching lemma · Chosen first-exit data

DefinitionDegree of a site in an edge set#✓fully proved

The number of edges of P incident to x.

def degP (P : Finset (Sym2 V)) (x : V) : ℕ := #(P.filter (fun e => x ∈ e))

Used by 10

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 · Switching lemma · Switching lemma · Odd-degree sites of an edge set · Chosen first-exit data · High-temperature switching map · Switching map between valid inputs and outputs · Simon–Lieb inequality on a finite graph

DefinitionOdd-degree sites of an edge set#✓fully proved

The sites of odd degree in the edge set P.

def srcP (P : Finset (Sym2 V)) : Finset V :=
  Finset.univ.filter (fun x => Odd (degP P x))

Uses 1 · Used by 9

Statement usesDegree of a site in an edge set

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 · Switching lemma · Switching lemma · Chosen first-exit data · High-temperature switching map · Switching map between valid inputs and outputs · Simon–Lieb inequality on a finite graph

DefinitionCluster of a site in an edge set#✓fully proved

The cluster of u in the edge set P.

noncomputable def compOf (P : Finset (Sym2 V)) (u : V) : Finset V :=
  Finset.univ.filter (fun x => connP P u x)

Uses 1 · Used by 4

Statement usesConnectivity through the edges of an edge set

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 · Chosen first-exit data

DefinitionReflection of a sub-current along an edge set#✓fully proved

The reflection of a sub-current n ≤ m along P: m e - n e on P and n e elsewhere.

def reflect (m : Current V) (P : Finset (Sym2 V)) (n : Current V) : Current V :=
  fun e => if e ∈ P then m e - n e else n e

Uses 1 · Used by 3

Statement usesCurrent as a multiplicity on unordered pairs

Used bySwitching lemma · Switching lemma · Reflection as an involution of the sub-currents of a current

TheoremSwitching lemma#✓fully proved

Switching lemma (counting form). If u ≠ v are connected by the odd edges of n₁ + n₂, the sub-currents of n₁ + n₂ with sources A ∆ {u, v} and with sources A are equinumerous.

R. B. Griffiths, C. A. Hurst and S. Sherman, J. Math. Phys. 11 (1970); M. Aizenman, Geometric analysis of φ⁴ fields and Ising models, Comm. Math. Phys. 86 (1982).

theorem ising_switching_lemma_pair (n₁ n₂ : Current V)
    {u v : V} (huv : u ≠ v)
    (hconn : connP (oddEdges E (fun e => n₁ e + n₂ e)) u v) (A : Finset V) :
    Nat.card {n : Current V //
        (∀ e, n e ≤ n₁ e + n₂ e) ∧ sources E n = A ∆ {u, v}}
      = Nat.card {n : Current V //
        (∀ e, n e ≤ n₁ e + n₂ e) ∧ sources E n = A}

Uses 9

Statement usesCurrent as a multiplicity on unordered pairs · Connectivity through the edges of an edge set · Edges of an edge set with odd multiplicity · Source set of a current on an edge set

Proof usesAdjacency through an edge of an edge set · Degree of a site in an edge set · Incident flux of a current on an edge set · Reflection of a sub-current along an edge set · Odd-degree sites of an edge set

DefinitionRestriction of a current to an edge predicate#✓fully proved

The restriction of the current n to the edges satisfying p (zero elsewhere).

noncomputable def acwRestrict (p : Sym2 V → Prop) [DecidablePred p] (n : Current V) : Current V :=
  fun e => if p e then n e else 0

Uses 1

Statement usesCurrent as a multiplicity on unordered pairs

DefinitionInternal edge of a vertex set#✓fully proved

Both endpoints of e lie in S.

def acwInternal (S : Finset V) (e : Sym2 V) : Prop := ∀ z ∈ e, z ∈ S

Used by 1

Used byVertex set that no edge of the graph crosses

DefinitionVertex set that no edge of the graph crosses#✓fully proved

Every edge of G lies inside S or inside its complement.

def acwClosedCut (S : Finset V) : Prop :=
  ∀ e ∈ G.edgeFinset, acwInternal S e ∨ acwInternal Sᶜ e

Uses 1

Statement usesInternal edge of a vertex set

LemmaSourced current sum as correlation times sourceless sum#✓fully proved

Z_A = ⟨σ_A⟩ Z_∅.

lemma acw_currentSum_eq_expectation (β : ℝ) (J : Sym2 V → ℝ) (A : Finset V)
    (h0 : Sharpness.currentSum G β J ∅ ≠ 0) :
    Sharpness.currentSum G β J A = Sharpness.expectationJ G β J A * Sharpness.currentSum G β J ∅

Uses 3 · Used by 3

Statement usesCurrent sum with prescribed sources · Correlation function with couplings

Proof usesRandom-current representation

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

LemmaSources on a graph's edge set agree with random-current sources#✓fully proved

The source set of a current on the edges of G is Sharpness.sources G.

lemma sources_edgeFinset_eq (n : Current V) : sources G.edgeFinset n = Sharpness.sources G n

Uses 3

Statement usesCurrent as a multiplicity on unordered pairs · Source set of a current on an edge set · Sources of a current

DefinitionReflection as an involution of the sub-currents of a current#✓fully proved

Reflection along P as an involutive equivalence of the sub-currents of m.

noncomputable def reflectEquiv (m : Current V) (P : Finset (Sym2 V)) :
    {K : Current V // ∀ e, K e ≤ m e} ≃ {K : Current V // ∀ e, K e ≤ m e} where
  toFun K := ⟨reflect m P K.1, reflect_le m P K.2⟩
  invFun K := ⟨reflect m P K.1, reflect_le m P K.2⟩
  left_inv K := Subtype.ext (reflect_involutive m P K.2)
  right_inv K := Subtype.ext (reflect_involutive m P K.2)

Uses 2 · Used by 1

Statement usesCurrent as a multiplicity on unordered pairs · Reflection of a sub-current along an edge set

Used bySwitching lemma

DefinitionWeighted sum over splittings with prescribed sources#✓fully proved

The weighted sum F ∑_K w(K) w(m - K) over sub-currents K ≤ m with sources A.

noncomputable def splitWeightedSum (β : ℝ) (J : Sym2 V → ℝ) (m : Current V) (F : ℝ)
    (A : Finset V) : ℝ :=
  ∑ K : {K : Current V // ∀ e, K e ≤ m e},
    (if Sharpness.sources G K.1 = A
      then F * (Sharpness.weight G β J K.1 * Sharpness.weight G β J (fun e => m e - K.1 e))
      else 0)

Uses 3 · Used by 1

Statement usesCurrent as a multiplicity on unordered pairs · Sources of a current · Weight of a random current

Used bySwitching lemma

TheoremSwitching lemma#✓fully proved

Switching lemma (weighted form). If u ≠ v are connected by odd edges of m, the weighted sums over splittings with sources A ∆ {u, v} and A agree.

M. Aizenman, Geometric analysis of φ⁴ fields and Ising models, Comm. Math. Phys. 86 (1982).

theorem ising_switching_weighted (β : ℝ) (J : Sym2 V → ℝ) (m : Current V)
    {u v : V} (huv : u ≠ v) (hconn : connP (oddEdges G.edgeFinset m) u v)
    (F : ℝ) (A : Finset V) :
    splitWeightedSum G β J m F (A ∆ {u, v}) = splitWeightedSum G β J m F A

Uses 14

Statement usesCurrent as a multiplicity on unordered pairs · Connectivity through the edges of an edge set · Edges of an edge set with odd multiplicity · Weighted sum over splittings with prescribed sources

Proof usesAdjacency through an edge of an edge set · Degree of a site in an edge set · Incident flux of a current on an edge set · Reflection of a sub-current along an edge set · Reflection as an involution of the sub-currents of a current · 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 · Sources of a current · Weight of a random current

81 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.