Aizenman–Barsky inequality

DefinitionEndpoint sum on unordered pairs#✓fully proved

The function s(x, y) ↦ F(x) + F(y) on unordered pairs.

noncomputable def abcrEndpointSum (F : V → ℝ) : Sym2 V → ℝ :=
  Sym2.lift ⟨fun x y => F x + F y, fun x y => by ring⟩

Used by 2

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

DefinitionIncident coupling of a vertex#✓fully proved

The incident coupling ∑_{y ∼ x} J_{xy} of x, as a sum over darts starting at x.

noncomputable def abcrIncidentCoupling (J : Sym2 V → ℝ) (x : V) : ℝ :=
  ∑ d : {d : G.Dart // d.fst = x}, J d.1.edge

Used by 2

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

DefinitionEdge weight under an inhomogeneous product measure#✓fully proved

The probability p_e or 1 - p_e of the state of edge e in ω.

noncomputable def edgeWeightV (p : E → ℝ) (ω : ConfigSpace E) (e : E) : ℝ :=
  if ω e then p e else 1 - p e

Uses 1 · Used by 4

Statement usesConfiguration space of a statistical-mechanics model

Used byAizenman–Barsky inequality on a finite graph · Aizenman–Barsky inequality on infinite vertex-transitive graphs · Product weight of a configuration · Product weight of a configuration off one edge

DefinitionProduct weight of a configuration#✓fully proved

The product weight ∏_e (p_e or 1 - p_e) of a configuration.

noncomputable def configWeightV (p : E → ℝ) (ω : ConfigSpace E) : ℝ :=
  ∏ e, edgeWeightV p ω e

Uses 2 · Used by 4

Statement usesConfiguration space of a statistical-mechanics model · Edge weight under an inhomogeneous product measure

Used byAizenman–Barsky inequality on a finite graph · Aizenman–Barsky inequality on infinite vertex-transitive graphs · Pivotal probability of an edge · Probability under an inhomogeneous product measure

DefinitionProduct weight of a configuration off one edge#✓fully proved

The product weight of a configuration over all edges other than e.

noncomputable def weightOffV (p : E → ℝ) (e : E) (ω : ConfigSpace E) : ℝ :=
  ∏ j ∈ univ.erase e, edgeWeightV p ω j

Uses 2 · Used by 2

Statement usesConfiguration space of a statistical-mechanics model · Edge weight under an inhomogeneous product measure

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

DefinitionProbability under an inhomogeneous product measure#✓fully proved

The probability ∑_ω 1_A(ω) ∏_e (p_e or 1 - p_e) of A under the inhomogeneous product measure.

noncomputable def probV (p : E → ℝ) (A : Set (ConfigSpace E)) : ℝ :=
  ∑ ω, A.indicator (fun _ => (1 : ℝ)) ω * configWeightV p ω

Uses 2 · Used by 3

Statement usesConfiguration space of a statistical-mechanics model · Product weight of a configuration

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

DefinitionPivotal probability of an edge#✓fully proved

The probability that e is pivotal for A.

noncomputable def pivotalProbV (p : E → ℝ) (A : Set (ConfigSpace E)) (e : E) : ℝ :=
  ∑ ω, (Set.indicator {ω | IsPivotal e A ω} (fun _ => (1 : ℝ)) ω) * configWeightV p ω

Uses 3 · Used by 2

Statement usesConfiguration space of a statistical-mechanics model · Pivotal coordinate for an event · Product weight of a configuration

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

DefinitionEdge parameters set to a common value on a subset#✓fully proved

The parameters p with the value c on the edges of s.

noncomputable def paramOn (s : Finset E) (c : ℝ) (p : E → ℝ) : E → ℝ :=
  fun e => if e ∈ s then c else p e

Used by 3

Used byAizenman–Barsky inequality on a finite graph · Aizenman–Barsky inequality on infinite vertex-transitive graphs · Edge parameters with a field value on a subset

DefinitionGhost-edge probability \(1 - e^{-h}\)#✓fully proved

The ghost-edge probability 1 - e^{-h}.

noncomputable def qField (h : ℝ) : ℝ := 1 - Real.exp (-h)

Used by 5

Used byAizenman–Barsky inequality on a finite graph · Edge parameters with a ghost field · Aizenman–Barsky inequality on infinite vertex-transitive graphs · Bond percolation measure on the ghost graph · Real edge parameters with a ghost field

DefinitionExtension of a vertex permutation to the ghost graph#✓fully proved

The extension of a vertex permutation to the ghost graph fixing the ghost.

def abfsOptionEquiv (sigma : V ≃ V) : Option V ≃ Option V := sigma.optionCongr

Used by 2

Used byInduced permutation of ghost-graph edges · Aizenman–Barsky inequality on infinite vertex-transitive graphs

DefinitionInduced permutation of ghost-graph edges#✓fully proved

The induced permutation of unordered pairs of the ghost graph.

def abfsEdgeEquiv (sigma : V ≃ V) :
    Sym2 (Option V) ≃ Sym2 (Option V) :=
  StatMech.Lattice.sym2Congr (abfsOptionEquiv sigma)

Uses 2 · Used by 1

Statement usesUnordered pairs under an equivalence · Extension of a vertex permutation to the ghost graph

Used byAizenman–Barsky inequality on infinite vertex-transitive graphs

DefinitionConfigurations with an edge closed and pivotal#✓fully proved

Configurations in which e is closed and pivotal for A.

def abgiClosedPivotal (e : E) (A : Set (ConfigSpace E)) : Set (ConfigSpace E) :=
  {omega | IsPivotal e A omega ∧ omega e = false}

Uses 2 · Used by 2

Statement usesConfiguration space of a statistical-mechanics model · Pivotal coordinate for an event

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

DefinitionEdge parameters with a field value on a subset#✓fully proved

Edge parameters 1 - e^{-βJ_e} off s and q on s.

noncomputable def abpdBetaFieldParams (s : Finset E) (q : ℝ) (J : E → ℝ)
    (beta : ℝ) : E → ℝ :=
  paramOn s q (fun e => pBeta (J e) beta)

Uses 2 · Used by 3

Statement usesBond probability \(p(\beta) = 1 - e^{-\beta J}\) · Edge parameters set to a common value on a subset

Used byAizenman–Barsky inequality on a finite graph · Edge parameters with a ghost field · Aizenman–Barsky inequality on infinite vertex-transitive graphs

DefinitionEdges used by an open walk in an induced subgraph#✓fully proved

The edges of V used by a walk in the open subgraph induced on A.

def sab_inducedEdgeSet (G : SimpleGraph V) (ω : ConfigSpace (Sym2 V)) (A : Set V) {x y : A}
    (w : ((openSub G ω).induce A).Walk x y) : Set (Sym2 V) :=
  {e | ∃ z ∈ w.edges, e = Sym2.map Subtype.val z}

Uses 2 · Used by 4

Statement usesConfiguration space of a statistical-mechanics model · Open subgraph of a configuration

Used byAizenman–Barsky inequality on a finite graph · Aizenman–Barsky inequality on infinite vertex-transitive graphs · Transfer of an open walk between agreeing configurations · Transfer of an open walk avoiding a fixed edge

DefinitionTransfer of an open walk between agreeing configurations#✓fully proved

An open walk in A for ω, read as an open walk for ω' when ω and ω' agree on its edges.

StatMech.Sharpness.sab_inducedWalkTransfer · 18 lines

noncomputable def sab_inducedWalkTransfer (G : SimpleGraph V) {ω ω' : ConfigSpace (Sym2 V)}
    {A : Set V} {x y : A}
    (w : ((openSub G ω).induce A).Walk x y)
    (hagree : ∀ e ∈ sab_inducedEdgeSet G ω A w, ω e = ω' e) :
    ((openSub G ω').induce A).Walk x y := by
  induction w with
  | nil => exact Walk.nil
  | @cons a b c hadj p ih =>
    have hedges : ∀ e ∈ sab_inducedEdgeSet G ω A p, ω e = ω' e := by
      intro e he
      obtain ⟨z, hz, rfl⟩ := he
      exact hagree _ ⟨z, by simp [Walk.edges_cons, hz], rfl⟩
    have hadj' : ((openSub G ω').induce A).Adj a b := by
      have hcoord : ω s((a:V),(b:V)) = ω' s((a:V),(b:V)) := by
        apply hagree; exact ⟨s(a,b), by simp [Walk.edges_cons], by simp [Sym2.map_mk]⟩
      have : (openSub G ω').Adj (a:V) (b:V) := ⟨hadj.1, by rw [← hcoord]; exact hadj.2⟩
      exact induce_adj.2 this
    exact Walk.cons hadj' (ih hedges)

Uses 3 · Used by 3

Statement usesConfiguration space of a statistical-mechanics model · Open subgraph of a configuration · Edges used by an open walk in an induced subgraph

Used byAizenman–Barsky inequality on a finite graph · Aizenman–Barsky inequality on infinite vertex-transitive graphs · Transfer of an open walk avoiding a fixed edge

DefinitionTransfer of an open walk avoiding a fixed edge#✓fully proved

An open walk for ω_S avoiding the edge xy, read as an open walk for ω when the two agree off xy.

noncomputable def sab_transfer_avoid (G : SimpleGraph V) {ωS ω : ConfigSpace (Sym2 V)}
    (A : Set V) (x y : V) (hx : x ∈ A) (hy : y ∈ A) {u a : A}
    (hagreeOff : ∀ e, e ≠ s(x, y) → ωS e = ω e)
    (w : ((openSub G ωS).induce A).Walk u a)
    (hav : s((⟨x, hx⟩ : A), (⟨y, hy⟩ : A)) ∉ w.edges) :
    ((openSub G ω).induce A).Walk u a := by
  apply sab_inducedWalkTransfer G w
  intro e he
  have hne : e ≠ s(x,y) := by
    intro hcon; subst hcon; exact sab_inducedEdgeSet_avoid w hav he
  exact hagreeOff e hne

Uses 4 · Used by 2

Statement usesConfiguration space of a statistical-mechanics model · Open subgraph of a configuration · Edges used by an open walk in an induced subgraph · Transfer of an open walk between agreeing configurations

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

DefinitionCoupling restricted to the edges of a graph#✓fully proved

The coupling J restricted to the edges of G.

noncomputable def abfaBaseCoupling (J : Sym2 V → ℝ) (e : Sym2 V) : ℝ :=
  if e ∈ G.edgeFinset then J e else 0

Used by 2

Used byCoupling lifted to the ghost graph · Aizenman–Barsky inequality on infinite vertex-transitive graphs

DefinitionCoupling lifted to the ghost graph#✓fully proved

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

noncomputable def abfaLiftCoupling (J : Sym2 V → ℝ) : Sym2 (Option V) → ℝ :=
  FieldGhostDict.ghostCoupling 0 1 (abfaBaseCoupling G J)

Uses 2 · Used by 4

Statement usesCoupling on the ghost graph with uniform field · Coupling restricted to the edges of a graph

Used byAizenman–Barsky inequality on a finite graph · Edge parameters with a ghost field · Probability of a physical configuration · Aizenman–Barsky inequality on infinite vertex-transitive graphs

DefinitionEdge parameters with a ghost field#✓fully proved

Edge parameters 1 - e^{-βJ_e} on the edges of G and 1 - e^{-h} on the ghost edges.

noncomputable def abfaParams (J : Sym2 V → ℝ) (beta h : ℝ) :
    Sym2 (Option V) → ℝ :=
  abpdBetaFieldParams (FieldGhostDict.ghostEdges V) (qField h)
    (abfaLiftCoupling G J) beta

Uses 4 · Used by 3

Statement usesGhost edges · Coupling lifted to the ghost graph · Edge parameters with a field value on a subset · Ghost-edge probability \(1 - e^{-h}\)

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

DefinitionFinite-volume percolation magnetization#✓fully proved

The percolation magnetization M(β, h) = P(o ↔ ghost).

noncomputable def abfaMag (J : Sym2 V → ℝ) (o : V) (beta h : ℝ) : ℝ :=
  probV (abfaParams G J beta h)
    (connEvent (withGhost G) Set.univ (some o) {none})

Uses 4 · Used by 3

Statement usesEdge parameters with a ghost field · Connection event inside a set · Probability under an inhomogeneous product measure · Graph with a ghost vertex joined to every site

Used byAizenman–Barsky inequality on a finite graph · Aizenman–Barsky inequality on infinite vertex-transitive graphs · Largest site magnetization in a window

TheoremAizenman–Barsky inequality on a finite graph#✓fully proved

The Aizenman–Barsky inequality on a finite graph: if all row sums equal J₀ and all sites have the same magnetization, then ∂_β M ≤ J₀ M ∂_h M for β, h ≥ 0. Reference: M. Aizenman, D. J. Barsky, "Sharpness of the phase transition in percolation models", Comm. Math. Phys. 108 (1987) 489–526.

theorem abfa_aizenmanBarsky (J : Sym2 V → ℝ) (o : V) (beta h J0 : ℝ)
    (hJ : ∀ e ∈ G.edgeFinset, 0 ≤ J e)
    (hrow : ∀ x, abcrIncidentCoupling G J x = J0)
    (hbeta : 0 ≤ beta) (hh : 0 ≤ h)
    (hmag : ∀ x : V,
      probV (abfaParams G J beta h)
        (connEvent (withGhost G) Set.univ (some x) {none}) =
          abfaMag G J o beta h) :
    deriv (fun b => abfaMag G J o b h) beta ≤
      J0 * abfaMag G J o beta h * deriv (fun t => abfaMag G J o beta t) h

Uses 48

Statement usesIncident coupling of a vertex · Finite-volume percolation magnetization · Edge parameters with a ghost field · Connection event inside a set · Probability under an inhomogeneous product measure · Graph with a ghost vertex joined to every site

Proof usesConfiguration space of a statistical-mechanics model · Event determined by a set of coordinates · Increasing event · Pivotal coordinate for an event · Occurrence of an event on a coordinate set · Open connection inside a set to a target set · Open connection between two vertices inside a set · Ghost edges · Graph edges as ghost-graph edges · Endpoint sum on unordered pairs · Coupling lifted to the ghost graph · Configurations with an edge closed and pivotal · Edge parameters with a field value on a subset · Product weight of a configuration · Event that an edge is open · Edge weight under an inhomogeneous product measure · Ghost vertex of the extended vertex set · Vertices not connected to a target set · Edges with both endpoints in a vertex set · Event that the set of vertices not connected to \(B\) is \(S\) · Open subgraph of a configuration · Bond probability \(p(\beta) = 1 - e^{-\beta J}\) · Edge parameters set to a common value on a subset · Pivotal probability of an edge · Ghost-edge probability \(1 - e^{-h}\) · Edges used by an open walk in an induced subgraph · Transfer of an open walk between agreeing configurations · Transfer of an open walk avoiding a fixed edge · Product weight of a configuration off one edge · Agreement of configurations on a set · Agreement on a set restricts to subsets · Transitivity of agreement on a set · Disjoint occurrence of events · Disjoint occurrence lies in the intersection · Pivotality depends only on the other coordinates · Pivotal coordinates of an increasing event · Product weight of a configuration · Closing a coordinate of a configuration · Closed configuration lies below the opened one · Opening a coordinate of a configuration · Weighted probability of an event · Independence of events determined by disjoint coordinate sets

DefinitionMerging configurations on and off a set#✓fully proved

The configuration equal to γ on s and to η off s.

noncomputable def abgrMerge (s : Finset E) (gamma : {e // e ∈ s} -> Bool)
    (eta : {e // e ∉ s} -> Bool) : ConfigSpace E :=
  (Equiv.piEquivPiSubtypeProd (fun e : E => e ∈ s) (fun _ => Bool)).symm (gamma, eta)

Uses 1 · Used by 2

Statement usesConfiguration space of a statistical-mechanics model

Used byGhost edges at the physical cluster of \(o\) · Aizenman–Barsky inequality on infinite vertex-transitive graphs

DefinitionClosing all ghost edges but one#✓fully proved

Close all ghost edges except {x, ghost}.

noncomputable def abgrKeepGhost (x : V) (omega : ConfigSpace (Sym2 (Option V))) :
    ConfigSpace (Sym2 (Option V)) := fun e =>
  if e = s(some x, none) then omega e
  else if e ∈ FieldGhostDict.ghostEdges V then false else omega e

Uses 2

Statement usesConfiguration space of a statistical-mechanics model · Ghost edges

DefinitionClosing all ghost edges#✓fully proved

Close all ghost edges.

noncomputable def abgrCloseGhost (omega : ConfigSpace (Sym2 (Option V))) :
    ConfigSpace (Sym2 (Option V)) := fun e =>
  if e ∈ FieldGhostDict.ghostEdges V then false else omega e

Uses 2 · Used by 2

Statement usesConfiguration space of a statistical-mechanics model · Ghost edges

Used bySites connected to \(o\) with ghost edges closed · Aizenman–Barsky inequality on infinite vertex-transitive graphs

DefinitionSites connected to \(o\) with ghost edges closed#✓fully proved

The sites connected to o when all ghost edges are closed.

noncomputable def abgrActive (o : V) (omega : ConfigSpace (Sym2 (Option V))) : Finset V :=
  by
    classical
    exact Finset.univ.filter fun x =>
      abgrCloseGhost omega ∈ connEvent (withGhost G) Set.univ (some o) {some x}

Uses 4 · Used by 2

Statement usesConfiguration space of a statistical-mechanics model · Closing all ghost edges · Connection event inside a set · Graph with a ghost vertex joined to every site

Used byGhost edges at the physical cluster of \(o\) · Aizenman–Barsky inequality on infinite vertex-transitive graphs

DefinitionCorrespondence between sites and ghost edges#✓fully proved

Sites correspond to ghost edges.

StatMech.Sharpness.abgrGhostEdgeEquiv · 20 lines

noncomputable def abgrGhostEdgeEquiv :
    V ≃ {e : Sym2 (Option V) // e ∈ FieldGhostDict.ghostEdges V} :=
  Equiv.ofBijective
    (fun x : V => (⟨s(some x, none), by
      simp [FieldGhostDict.ghostEdges]⟩ :
        {e : Sym2 (Option V) // e ∈ FieldGhostDict.ghostEdges V}))
    ⟨by
      intro x y hxy
      replace hxy : s(some x, none) = s(some y, none) := congrArg Subtype.val hxy
      rw [Sym2.eq_iff] at hxy
      rcases hxy with hxy | hxy
      · exact Option.some.inj hxy.1
      · simp at hxy,
    by
      intro e
      rcases e with ⟨e, he⟩
      simp only [FieldGhostDict.ghostEdges, Finset.mem_image,
        Finset.mem_univ, true_and] at he
      obtain ⟨x, rfl⟩ := he
      exact ⟨x, rfl⟩⟩

Uses 1 · Used by 2

Statement usesGhost edges

Used byGhost edges at the physical cluster of \(o\) · Aizenman–Barsky inequality on infinite vertex-transitive graphs

DefinitionGhost edges at the physical cluster of \(o\)#✓fully proved

The ghost edges at sites of the cluster of o in the physical configuration η.

noncomputable def abgrActiveGhost (o : V)
    (eta : {e // e ∉ FieldGhostDict.ghostEdges V} -> Bool) :
    Finset {e // e ∈ FieldGhostDict.ghostEdges V} :=
  (abgrActive (G := G) o
    (abgrMerge (FieldGhostDict.ghostEdges V) (fun _ => false) eta)).map
      (abgrGhostEdgeEquiv (V := V)).toEmbedding

Uses 4 · Used by 1

Statement usesGhost edges · Sites connected to \(o\) with ghost edges closed · Correspondence between sites and ghost edges · Merging configurations on and off a set

Used byAizenman–Barsky inequality on infinite vertex-transitive graphs

DefinitionProbability of a physical configuration#✓fully proved

The probability of the physical configuration η.

noncomputable def abgrOffWeight (J : Sym2 V -> Real) (beta : Real)
    (eta : {e // e ∉ FieldGhostDict.ghostEdges V} -> Bool) : Real :=
  ∏ e : {e // e ∉ FieldGhostDict.ghostEdges V},
    if eta e then pBeta (abfaLiftCoupling G J e) beta
    else 1 - pBeta (abfaLiftCoupling G J e) beta

Uses 3 · Used by 1

Statement usesGhost edges · Coupling lifted to the ghost graph · Bond probability \(p(\beta) = 1 - e^{-\beta J}\)

Used byAizenman–Barsky inequality on infinite vertex-transitive graphs

DefinitionAizenman–Barsky inequality for all \(\beta\) and \(h\)#✓fully proved

The Aizenman–Barsky inequality ∂_β M(β, h) ≤ J M(β, h) ∂_h M(β, h) for all β, h.

def AizenmanBarskyInequality (M : ℝ → ℝ → ℝ) (J : ℝ) : Prop :=
  ∀ β h, deriv (fun β => M β h) β ≤ J * (M β h * deriv (fun h => M β h) h)

Used by 1

Used byAizenman–Barsky critical bound \(M(\beta_c, h) \ge c\sqrt{h}\)

DefinitionSecond Aizenman–Barsky inequality#✓fully proved

The second Aizenman–Barsky inequality M ≤ h ∂_h M + M² + β M ∂_β M.

def AizenmanBarskyPDI (M : ℝ → ℝ → ℝ) : Prop :=
  ∀ β h, M β h ≤
      h * deriv (fun h => M β h) h + (M β h) ^ 2 + β * (M β h * deriv (fun β => M β h) β)

TheoremAizenman–Barsky critical bound \(M(\beta_c, h) \ge c\sqrt{h}\)#✓fully proved

The Aizenman–Barsky critical bound: from ∂_β M ≤ J M ∂_h M and 1 - M(β_c, h) ≤ β_c ∂_β M(β_c, h) with M(β_c, 0) = 0, M(β_c, h) ≥ c √h for 0 < h ≤ β_c J/4. Reference: M. Aizenman, D. J. Barsky, "Sharpness of the phase transition in percolation models", Comm. Math. Phys. 108 (1987) 489–526.

theorem ab_perco_meanfield_sqrt (M : ℝ → ℝ → ℝ) (J : ℝ) (βc : ℝ)
    (hβc : 0 < βc) (hJ : 0 < J)
    (hAB : AizenmanBarskyInequality M J)
    (hdiff : ∀ h ∈ Ici (0 : ℝ), DifferentiableAt ℝ (fun h => M βc h) h)
    (hmono : ∀ h ∈ Ici (0 : ℝ), 0 ≤ deriv (fun h => M βc h) h)
    (hmnn : ∀ h, 0 ≤ M βc h)
    (hm0 : M βc 0 = 0)
    (heq6 : ∀ h ∈ Ici (0 : ℝ),
      1 - M βc h ≤ βc * deriv (fun β => M β h) βc) :
    ∃ c > 0, ∀ h ∈ Ioc (0 : ℝ) (βc * J / 4),
      c * Real.sqrt h ≤ M βc h

Uses 1

Statement usesAizenman–Barsky inequality for all \(\beta\) and \(h\)

DefinitionAizenman–Barsky inequality for \(\beta \ge 0\) and \(h > 0\)#✓fully proved

The Aizenman–Barsky inequality ∂_β M ≤ J M ∂_h M for β ≥ 0 and h > 0.

def AizenmanBarskyInequalityPhysical (M : ℝ → ℝ → ℝ) (J : ℝ) : Prop :=
  ∀ β, 0 ≤ β → ∀ h, 0 < h →
    deriv (fun b => M b h) β ≤
      J * (M β h * deriv (fun t => M β t) h)

Used by 3

Used byAizenman–Barsky inequality on infinite vertex-transitive graphs · Aizenman–Barsky inequality on \(\mathbb{Z}^d\) · Aizenman–Barsky inequality on \(\mathbb{Z}^d\) with neighbour row sum

DefinitionReal edge parameters with a ghost field#✓fully proved

The real edge parameters: 1 - e^{-βJ_e} on physical edges and 1 - e^{-h} on ghost edges.

noncomputable def abigRealParam (J : Sym2 V -> Real) (beta h : Real) :
    Sym2 (Option V) -> Real :=
  FieldGhostDict.ghostCoupling (qField h) 1
    (fun e => pBeta (J e) beta)

Uses 3 · Used by 2

Statement usesCoupling on the ghost graph with uniform field · Bond probability \(p(\beta) = 1 - e^{-\beta J}\) · Ghost-edge probability \(1 - e^{-h}\)

Used byAizenman–Barsky inequality on infinite vertex-transitive graphs · Edge parameters as nonnegative reals

DefinitionEdge parameters as nonnegative reals#✓fully proved

The edge parameters as elements of ℝ≥0.

noncomputable def abigParam (J : Sym2 V -> Real) (beta h : Real) :
    Sym2 (Option V) -> NNReal :=
  fun e => (abigRealParam J beta h e).toNNReal

Uses 1 · Used by 2

Statement usesReal edge parameters with a ghost field

Used byAizenman–Barsky inequality on infinite vertex-transitive graphs · Bond percolation measure on the ghost graph

DefinitionBond percolation measure on the ghost graph#✓fully proved

Independent bond percolation on the ghost graph with parameters abigParam.

noncomputable def abigMeasure (J : Sym2 V -> Real) (beta h : Real) :
    Measure (ConfigSpace (Sym2 (Option V))) :=
  inhomBernoulliProductMeasure (abigParam J beta h)
    (abigParam_le_one J beta h)

Uses 5 · Used by 2

Statement usesConfiguration space of a statistical-mechanics model · Edge parameters as nonnegative reals · Bond probability \(p(\beta) = 1 - e^{-\beta J}\) · Ghost-edge probability \(1 - e^{-h}\) · Inhomogeneous Bernoulli product measure

Used byAizenman–Barsky inequality on infinite vertex-transitive graphs · Infinite-volume percolation magnetization

DefinitionInfinite-volume percolation magnetization#✓fully proved

The percolation magnetization M(β, h) = P(o ↔ ghost).

noncomputable def abigMag (G : SimpleGraph V) (J : Sym2 V -> Real) (o : V)
    (beta h : Real) : Real :=
  (abigMeasure J beta h).real
    (connEvent (withGhost G) Set.univ (some o) {none})

Uses 4 · Used by 3

Statement usesConfiguration space of a statistical-mechanics model · Bond percolation measure on the ghost graph · Connection event inside a set · Graph with a ghost vertex joined to every site

Used byAizenman–Barsky inequality on infinite vertex-transitive graphs · Aizenman–Barsky inequality on \(\mathbb{Z}^d\) · Aizenman–Barsky inequality on \(\mathbb{Z}^d\) with neighbour row sum

DefinitionInternal edges of a finite set#✓fully proved

The unordered pairs with both endpoints in T.

noncomputable def abigInternalEdges [DecidableEq W] (T : Finset W) :
    Finset (Sym2 W) :=
  (T ×ˢ T).image (fun p => s(p.1, p.2))

Used by 3

Used byAizenman–Barsky inequality on infinite vertex-transitive graphs · Unordered pairs of a set as its internal edges · Unordered pairs of the extended set as window edges

DefinitionUnordered pairs of a set as its internal edges#✓fully proved

Unordered pairs of T correspond to abigInternalEdges T.

StatMech.Sharpness.abigInternalEdgeEquiv · 21 lines

noncomputable def abigInternalEdgeEquiv [DecidableEq W] (T : Finset W) :
    Sym2 T ≃ abigInternalEdges T :=
  Equiv.ofBijective
    (fun e => ⟨Sym2.map (Subtype.val : T -> W) e, by
      induction e using Sym2.inductionOn with
      | _ x y =>
          rw [Sym2.map_mk]
          exact (mem_abigInternalEdges).2
            ⟨x, x.property, y, y.property, rfl⟩⟩)
    ⟨by
      intro e f hef
      apply Sym2.map.injective Subtype.val_injective
      exact congrArg Subtype.val hef,
    by
      rintro ⟨e, he⟩
      obtain ⟨x, hx, y, hy, rfl⟩ := (mem_abigInternalEdges).1 he
      refine ⟨s((⟨x, hx⟩ : T), (⟨y, hy⟩ : T)), ?_⟩
      apply Subtype.ext
      change Sym2.map (Subtype.val : T -> W)
        s((⟨x, hx⟩ : T), (⟨y, hy⟩ : T)) = s(x, y)
      rw [Sym2.map_mk]⟩

Uses 1 · Used by 2

Statement usesInternal edges of a finite set

Used byAizenman–Barsky inequality on infinite vertex-transitive graphs · Unordered pairs of the extended set as window edges

DefinitionGhost window of a finite set#✓fully proved

The window S ∪ {ghost} in the ghost graph.

noncomputable def abigGhostWindow [DecidableEq V] (S : Finset V) :
    Finset (Option V) :=
  S.image some ∪ {none}

Used by 4

Used byAizenman–Barsky inequality on infinite vertex-transitive graphs · Ghost window as a set with one added point · Unordered pairs of the extended set as window edges · Aizenman–Barsky inequality on \(\mathbb{Z}^d\) with neighbour row sum

DefinitionGhost window as a set with one added point#✓fully proved

Option S corresponds to the window S ∪ {ghost}.

StatMech.Sharpness.abigGhostWindowEquiv · 15 lines

noncomputable def abigGhostWindowEquiv [DecidableEq V] (S : Finset V) :
    Option S ≃ abigGhostWindow S :=
  Equiv.ofBijective
    (fun z => match z with
      | none => ⟨none, by simp [abigGhostWindow]⟩
      | some x => ⟨some (x : V), by simp [abigGhostWindow, x.property]⟩)
    ⟨by
      intro a b hab
      rcases a with _ | a <;> rcases b with _ | b <;> simp_all,
    by
      rintro ⟨z, hz⟩
      rcases z with _ | x
      · exact ⟨none, rfl⟩
      · have hx : x ∈ S := by simpa [abigGhostWindow] using hz
        exact ⟨some ⟨x, hx⟩, rfl⟩⟩

Uses 1 · Used by 2

Statement usesGhost window of a finite set

Used byAizenman–Barsky inequality on infinite vertex-transitive graphs · Unordered pairs of the extended set as window edges

DefinitionUnordered pairs of the extended set as window edges#✓fully proved

Unordered pairs of Option S correspond to the internal edges of the window.

noncomputable def abigWindowEdgeEquiv [DecidableEq V] (S : Finset V) :
    Sym2 (Option S) ≃ abigInternalEdges (abigGhostWindow S) :=
  (StatMech.Lattice.sym2Congr (abigGhostWindowEquiv S)).trans
    (abigInternalEdgeEquiv (abigGhostWindow S))

Uses 5 · Used by 1

Statement usesUnordered pairs under an equivalence · Ghost window of a finite set · Ghost window as a set with one added point · Unordered pairs of a set as its internal edges · Internal edges of a finite set

Used byAizenman–Barsky inequality on infinite vertex-transitive graphs

DefinitionSubgraph induced on a window#✓fully proved

The subgraph of G induced on S.

def abigWindowGraph (G : SimpleGraph V) (S : Finset V) : SimpleGraph S :=
  G.induce (S : Set V)

Used by 2

Used byAizenman–Barsky inequality on infinite vertex-transitive graphs · Largest site magnetization in a window

DefinitionCoupling restricted to a window#✓fully proved

The coupling restricted to the window.

noncomputable def abigWindowCoupling (J : Sym2 V -> Real) (S : Finset V) :
    Sym2 S -> Real :=
  fun e => J (Sym2.map (Subtype.val : S -> V) e)

Used by 2

Used byAizenman–Barsky inequality on infinite vertex-transitive graphs · Largest site magnetization in a window

DefinitionDarts at a vertex as its neighbours#✓fully proved

Darts starting at x correspond to neighbours of x.

def abigDartFiberEquivNeighbor {W : Type*} (H : SimpleGraph W) (x : W) :
    {d : H.Dart // d.fst = x} ≃ H.neighborSet x where
  toFun d := ⟨d.1.snd, by simpa only [d.2, SimpleGraph.mem_neighborSet] using d.1.adj⟩
  invFun y := ⟨H.dartOfNeighborSet x y, rfl⟩
  left_inv d := by
    rcases d with ⟨⟨⟨a, b⟩, hab⟩, ha⟩
    simp only at ha
    subst a
    rfl
  right_inv y := by
    apply Subtype.ext
    rfl

Used by 1

Used byAizenman–Barsky inequality on infinite vertex-transitive graphs

DefinitionUniform row-sum bound in finite windows#✓fully proved

All row sums of J in all finite windows are at most J₀.

def abigUniformFiniteRowBound (G : SimpleGraph V) [DecidableRel G.Adj]
    (J : Sym2 V -> Real) (J0 : Real) : Prop :=
  forall (S : Finset V) (x : S),
    (∑ y : S, if G.Adj (x : V) (y : V)
      then J s((x : V), (y : V)) else 0) <= J0

Used by 1

Used byAizenman–Barsky inequality on infinite vertex-transitive graphs

DefinitionLargest site magnetization in a window#✓fully proved

The largest site magnetization in the window.

noncomputable def abigWindowEnvelope [DecidableEq V]
    (G : SimpleGraph V) [DecidableRel G.Adj]
    (J : Sym2 V -> Real) (S : Finset V) (o : S) (beta h : Real) : Real :=
  (Finset.univ.image (fun x : S =>
    abfaMag (abigWindowGraph G S) (abigWindowCoupling J S) x beta h)).max'
      (by exact Finset.image_nonempty.mpr ⟨o, Finset.mem_univ o⟩)

Uses 3 · Used by 1

Statement usesFinite-volume percolation magnetization · Coupling restricted to a window · Subgraph induced on a window

Used byAizenman–Barsky inequality on infinite vertex-transitive graphs

TheoremAizenman–Barsky inequality on infinite vertex-transitive graphs#✓fully proved

The Aizenman–Barsky inequality on infinite vertex-transitive graphs with translation-invariant couplings supported on edges and row sums at most J₀: ∂_β M ≤ J₀ M ∂_h M for β ≥ 0, h > 0. Reference: M. Aizenman, D. J. Barsky, "Sharpness of the phase transition in percolation models", Comm. Math. Phys. 108 (1987) 489–526.

StatMech.Sharpness.abig_aizenmanBarskyPhysical_of_tsum_transitive · 18 lines

theorem abig_aizenmanBarskyPhysical_of_tsum_transitive
    [DecidableEq V]
    (G : SimpleGraph V) [DecidableRel G.Adj]
    (J : Sym2 V -> Real) (o : V) (J0 : Real)
    (hJ0 : 0 <= J0) (hJ : forall e, 0 <= J e)
    (hJsupport : forall x y, ¬ G.Adj x y -> J s(x, y) = 0)
    (hsum : forall x, Summable (fun y =>
      if G.Adj x y then J s(x, y) else 0))
    (hrow : forall x, (∑' y,
      if G.Adj x y then J s(x, y) else 0) <= J0)
    (move : V -> (V ≃ V)) (hmove : forall x, move x o = x)
    (hG : forall x u v, G.Adj (move x u) (move x v) <-> G.Adj u v)
    (hJinv : forall x u v, J s(move x u, move x v) = J s(u, v))
    (S : Nat -> Finset V) (ho : forall n, o ∈ S n)
    (hmonoWindow : Monotone (fun n => abigGhostWindow (S n)))
    (hcover : forall F : Finset (Option V),
      exists n, F ⊆ abigGhostWindow (S n)) :
    AizenmanBarskyInequalityPhysical (abigMag G J o) J0

Uses 81 · Used by 1

Statement usesAizenman–Barsky inequality for \(\beta \ge 0\) and \(h > 0\) · Ghost window of a finite set · Infinite-volume percolation magnetization

Proof usesConfiguration space of a statistical-mechanics model · Event depending only on a set of coordinates · Event determined by a set of coordinates · Increasing event · Pivotal coordinate for an event · Unordered pairs under an equivalence · Occurrence of an event on a coordinate set · Open connection inside a set to a target set · Open connection between two vertices inside a set · Ghost edges · Graph edges as ghost-graph edges · Endpoint sum on unordered pairs · Incident coupling of a vertex · Coupling restricted to the edges of a graph · Coupling lifted to the ghost graph · Finite-volume percolation magnetization · Edge parameters with a ghost field · Induced permutation of ghost-graph edges · Extension of a vertex permutation to the ghost graph · Configurations with an edge closed and pivotal · Sites connected to \(o\) with ghost edges closed · Ghost edges at the physical cluster of \(o\) · Closing all ghost edges · Correspondence between sites and ghost edges · Merging configurations on and off a set · Probability of a physical configuration · Darts at a vertex as its neighbours · Ghost window as a set with one added point · Unordered pairs of a set as its internal edges · Internal edges of a finite set · Bond percolation measure on the ghost graph · Edge parameters as nonnegative reals · Real edge parameters with a ghost field · Uniform row-sum bound in finite windows · Coupling restricted to a window · Unordered pairs of the extended set as window edges · Largest site magnetization in a window · Subgraph induced on a window · Edge parameters with a field value on a subset · Product weight of a configuration · Connection event inside a set · Event that an edge is open · Edge weight under an inhomogeneous product measure · Ghost vertex of the extended vertex set · Vertices not connected to a target set · Edges with both endpoints in a vertex set · Event that the set of vertices not connected to \(B\) is \(S\) · Open subgraph of a configuration · Bond probability \(p(\beta) = 1 - e^{-\beta J}\) · Edge parameters set to a common value on a subset · Pivotal probability of an edge · Probability under an inhomogeneous product measure · Ghost-edge probability \(1 - e^{-h}\) · Edges used by an open walk in an induced subgraph · Transfer of an open walk between agreeing configurations · Transfer of an open walk avoiding a fixed edge · Product weight of a configuration off one edge · Graph with a ghost vertex joined to every site · Agreement of configurations on a set · Agreement on a set restricts to subsets · Transitivity of agreement on a set · Bernoulli distribution on the Booleans · Relabeling configurations along a bijection · Disjoint occurrence of events · Disjoint occurrence lies in the intersection · Finitely dependent event is a cylinder over its section · Filling a finite configuration with closed coordinates · Section of an event on a finite coordinate set · Inhomogeneous Bernoulli product measure · Pivotality depends only on the other coordinates · Pivotal coordinates of an increasing event · Product weight of a configuration · Closing a coordinate of a configuration · Closed configuration lies below the opened one · Opening a coordinate of a configuration · Weighted probability of an event · Independence of events determined by disjoint coordinate sets · Weighted probability is invariant under relabeling coordinates

Used byAizenman–Barsky inequality on \(\mathbb{Z}^d\) with neighbour row sum

DefinitionBox as a finite set of sites#✓fully proved

The box Λ_n as a finite set of sites.

noncomputable def ablBoxFinset (d n : Nat) : Finset (Site d) :=
  (box_finite d n).toFinset

Uses 2 · Used by 1

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

Used byAizenman–Barsky inequality on \(\mathbb{Z}^d\) with neighbour row sum

TheoremAizenman–Barsky inequality on \(\mathbb{Z}^d\) with neighbour row sum#✓fully proved

The Aizenman–Barsky inequality on ℤ^d with the row sum written over lattice neighbours. Reference: M. Aizenman, D. J. Barsky, "Sharpness of the phase transition in percolation models", Comm. Math. Phys. 108 (1987) 489–526. Scope and fidelity: this is the first Aizenman–Barsky differential inequality ∂_β M ≤ |J| M ∂_h M for independent bond percolation on ℤ^d with nearest-neighbour, translation-invariant couplings J ≥ 0 (edge probability 1 - e^{-βJ_e}) and a ghost field (ghost-edge probability 1 - e^{-h}), for β ≥ 0, h > 0; M(β, h) is the probability that the origin is connected to the ghost. Aizenman–Barsky allow general summable translation-invariant couplings; here J vanishes off lattice edges. A derivative is taken to be \(0\) where the function is not differentiable: M is differentiable in h, and at a point where β ↦ M(β, h) is not differentiable the inequality holds trivially.

theorem abl_aizenmanBarsky_hypercubic_neighbourSum {d : Nat}
    (J : Sym2 (Site d) → Real)
    (hJ : ∀ e, 0 ≤ J e)
    (hJsupport : ∀ x y, ¬ (hypercubicLattice d).Adj x y → J s(x, y) = 0)
    (hJinv : ∀ x u v,
      J s(FK.fktc_translate x u, FK.fktc_translate x v) = J s(u, v))
    (hsum0 : Summable (fun y =>
      if (hypercubicLattice d).Adj (0 : Site d) y then J s(0, y) else 0)) :
    AizenmanBarskyInequalityPhysical
      (abigMag (hypercubicLattice d) J (0 : Site d))
      (∑' y, if (hypercubicLattice d).Adj (0 : Site d) y
        then J s(0, y) else 0)

Uses 9 · Used by 1

Statement usesTranslation of \(\mathbb{Z}^d\) by a vector · Site of the hypercubic lattice · Hypercubic lattice \(\mathbb{Z}^d\) · Aizenman–Barsky inequality for \(\beta \ge 0\) and \(h > 0\) · Infinite-volume percolation magnetization

Proof usesBox \((-n, n)^d\) in the hypercubic lattice · Ghost window of a finite set · Aizenman–Barsky inequality on infinite vertex-transitive graphs · Box as a finite set of sites

Used byAizenman–Barsky inequality on \(\mathbb{Z}^d\)

TheoremAizenman–Barsky inequality on \(\mathbb{Z}^d\)#✓fully proved

The Aizenman–Barsky inequality on ℤ^d: ∂_β M ≤ |J| M ∂_h M with |J| = ∑_y J_{0y}. Reference: M. Aizenman, D. J. Barsky, "Sharpness of the phase transition in percolation models", Comm. Math. Phys. 108 (1987) 489–526. Scope and fidelity: this is the first Aizenman–Barsky differential inequality ∂_β M ≤ |J| M ∂_h M for independent bond percolation on ℤ^d with nearest-neighbour, translation-invariant couplings J ≥ 0 (edge probability 1 - e^{-βJ_e}) and a ghost field (ghost-edge probability 1 - e^{-h}), for β ≥ 0, h > 0; M(β, h) is the probability that the origin is connected to the ghost. Aizenman–Barsky allow general summable translation-invariant couplings; here J vanishes off lattice edges. A derivative is taken to be \(0\) where the function is not differentiable: M is differentiable in h, and at a point where β ↦ M(β, h) is not differentiable the inequality holds trivially.

theorem abl_aizenmanBarsky_hypercubic {d : Nat}
    (J : Sym2 (Site d) → Real)
    (hJ : ∀ e, 0 ≤ J e)
    (hJsupport : ∀ x y, ¬ (hypercubicLattice d).Adj x y → J s(x, y) = 0)
    (hJinv : ∀ x u v,
      J s(FK.fktc_translate x u, FK.fktc_translate x v) = J s(u, v))
    (hsum0 : Summable (fun y => J s((0 : Site d), y))) :
    AizenmanBarskyInequalityPhysical
      (abigMag (hypercubicLattice d) J (0 : Site d))
      (∑' y, J s((0 : Site d), y))

Uses 6

Statement usesTranslation of \(\mathbb{Z}^d\) by a vector · Site of the hypercubic lattice · Hypercubic lattice \(\mathbb{Z}^d\) · Aizenman–Barsky inequality for \(\beta \ge 0\) and \(h > 0\) · Infinite-volume percolation magnetization

Proof usesAizenman–Barsky inequality on \(\mathbb{Z}^d\) with neighbour row sum

50 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.