Translation invariance and ergodicity of the plus state

DefinitionShifted plus-boundary box measure#✓fully proved

The plus-boundary box measure on Λ_n pushed forward by the shift g.

noncomputable def pst_plusShiftedFinite (β h : ℝ) (g : Multiplicative (Site d)) (n : ℕ) :
    ProbabilityMeasure (ConfigSpace (Site d)) :=
  (plusMeasure d n β h).map (shift g)

Uses 4 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Shift of a configuration by a group element · Plus-boundary Ising measure in a box · Site of the hypercubic lattice

Used byTranslation invariance of the plus state

DefinitionShifted minus-boundary box measure#✓fully proved

The minus-boundary box measure on Λ_n pushed forward by the shift g.

noncomputable def pst_minusShiftedFinite (β h : ℝ) (g : Multiplicative (Site d)) (n : ℕ) :
    ProbabilityMeasure (ConfigSpace (Site d)) :=
  (minusMeasure d n β h).map (shift g)

Uses 4

Statement usesConfiguration space of a statistical-mechanics model · Shift of a configuration by a group element · Minus-boundary Ising measure in a box · Site of the hypercubic lattice

DefinitionDecay of shifted integrals for plus box measures#✓fully proved

Along φ, integrals of bounded continuous functions against the plus box measures and their shifts by g become equal.

def pst_PlusIntegralShiftDecay (β h : ℝ) (g : Multiplicative (Site d)) (φ : ℕ → ℕ) : Prop :=
  ∀ f : ConfigSpace (Site d) →ᵇ ℝ,
    Tendsto (fun n =>
        (∫ x, f x ∂((plusMeasure d (φ n) β h : ProbabilityMeasure _) : Measure _))
          - (∫ x, f (shift g x)
              ∂((plusMeasure d (φ n) β h : ProbabilityMeasure _) : Measure _)))
      atTop (𝓝 0)

Uses 4 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Shift of a configuration by a group element · Plus-boundary Ising measure in a box · Site of the hypercubic lattice

Used byTranslation invariance of the plus state

DefinitionDecay of shifted integrals for minus box measures#✓fully proved

Along φ, integrals of bounded continuous functions against the minus box measures and their shifts by g become equal.

def pst_MinusIntegralShiftDecay (β h : ℝ) (g : Multiplicative (Site d)) (φ : ℕ → ℕ) : Prop :=
  ∀ f : ConfigSpace (Site d) →ᵇ ℝ,
    Tendsto (fun n =>
        (∫ x, f x ∂((minusMeasure d (φ n) β h : ProbabilityMeasure _) : Measure _))
          - (∫ x, f (shift g x)
              ∂((minusMeasure d (φ n) β h : ProbabilityMeasure _) : Measure _)))
      atTop (𝓝 0)

Uses 4

Statement usesConfiguration space of a statistical-mechanics model · Shift of a configuration by a group element · Minus-boundary Ising measure in a box · Site of the hypercubic lattice

DefinitionDifference between an integral and its shifted version#✓fully proved

The difference ∫ f dμ_n - ∫ f ∘ shift_g dμ_n.

noncomputable def pstc_decayFun (μ : ℕ → ProbabilityMeasure (ConfigSpace (Site d)))
    (g : Multiplicative (Site d)) (f : (ConfigSpace (Site d)) →ᵇ ℝ) (n : ℕ) : ℝ :=
  (∫ x, f x ∂(μ n : Measure _)) - (∫ x, f (shift g x) ∂(μ n : Measure _))

Uses 3 · Used by 6

Statement usesConfiguration space of a statistical-mechanics model · Shift of a configuration by a group element · Site of the hypercubic lattice

Used byBoundary influence bound for the minus box measures · Boundary influence bound for the plus box measures · Translation invariance of the plus state · Continuous functions with decaying shifted integrals · Decay of shifted cylinder integrals for minus box measures · Decay of shifted cylinder integrals for plus box measures

DefinitionPlus-spin indicator at a site as a continuous function#✓fully proved

The coordinate ω ↦ 1_{ω_x = +} as a continuous function.

noncomputable def pstc_coordCM (x : Site d) : C(ConfigSpace (Site d), ℝ) :=
  ⟨fun ω => if ω x then (1 : ℝ) else 0,
    (continuous_of_discreteTopology (f := fun b : Bool => if b then (1 : ℝ) else 0)).comp
      (continuous_apply x)⟩

Uses 2 · Used by 4

Statement usesConfiguration space of a statistical-mechanics model · Site of the hypercubic lattice

Used byTranslation invariance of the plus state · All-plus monomial as a continuous function · Plus-spin indicator at a site as a bounded continuous function · Subalgebra of cylinder functions

DefinitionPlus-spin indicator at a site as a bounded continuous function#✓fully proved

The coordinate ω ↦ 1_{ω_x = +} as a bounded continuous function.

noncomputable def pstc_coordBcf (x : Site d) : ConfigSpace (Site d) →ᵇ ℝ :=
  BoundedContinuousFunction.mkOfCompact (pstc_coordCM x)

Uses 3 · Used by 4

Statement usesConfiguration space of a statistical-mechanics model · Plus-spin indicator at a site as a continuous function · Site of the hypercubic lattice

Used byInf-based and sup-based Ising critical points agree for \(d \ge 2\) · Mean-field lower bound for the spontaneous magnetization · 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\)

DefinitionSubalgebra of cylinder functions#✓fully proved

The subalgebra generated by the spin coordinates (cylinder functions).

noncomputable def pstc_cylinderAlg (d : ℕ) : Subalgebra ℝ C(ConfigSpace (Site d), ℝ) :=
  Algebra.adjoin ℝ (Set.range (pstc_coordCM (d := d)))

Uses 3 · Used by 2

Statement usesConfiguration space of a statistical-mechanics model · Plus-spin indicator at a site as a continuous function · Site of the hypercubic lattice

Used byTranslation invariance of the plus state · Cylinder functions as bounded continuous functions

DefinitionCylinder functions as bounded continuous functions#✓fully proved

The cylinder functions as bounded continuous functions.

noncomputable def pstc_cylinderBcfSet (d : ℕ) : Set (ConfigSpace (Site d) →ᵇ ℝ) :=
  BoundedContinuousFunction.mkOfCompact ''
    (pstc_cylinderAlg d : Set C(ConfigSpace (Site d), ℝ))

Uses 3 · Used by 5

Statement usesConfiguration space of a statistical-mechanics model · Subalgebra of cylinder functions · Site of the hypercubic lattice

Used byBoundary influence bound for the minus box measures · Boundary influence bound for the plus box measures · Translation invariance of the plus state · Decay of shifted cylinder integrals for minus box measures · Decay of shifted cylinder integrals for plus box measures

DefinitionDecay of shifted cylinder integrals for plus box measures#✓fully proved

Shifted integrals of cylinder functions against the plus box measures decay along φ.

def pstc_PlusCylinderDecay (β h : ℝ) (g : Multiplicative (Site d)) (φ : ℕ → ℕ) : Prop :=
  ∀ f ∈ pstc_cylinderBcfSet d,
    Tendsto (pstc_decayFun (fun n => plusMeasure d (φ n) β h) g f) atTop (𝓝 0)

Uses 5 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Plus-boundary Ising measure in a box · Cylinder functions as bounded continuous functions · Difference between an integral and its shifted version · Site of the hypercubic lattice

Used byTranslation invariance of the plus state

DefinitionDecay of shifted cylinder integrals for minus box measures#✓fully proved

Shifted integrals of cylinder functions against the minus box measures decay along φ.

def pstc_MinusCylinderDecay (β h : ℝ) (g : Multiplicative (Site d)) (φ : ℕ → ℕ) : Prop :=
  ∀ f ∈ pstc_cylinderBcfSet d,
    Tendsto (pstc_decayFun (fun n => minusMeasure d (φ n) β h) g f) atTop (𝓝 0)

Uses 5

Statement usesConfiguration space of a statistical-mechanics model · Minus-boundary Ising measure in a box · Cylinder functions as bounded continuous functions · Difference between an integral and its shifted version · Site of the hypercubic lattice

DefinitionBoundary bond fraction of a box#✓fully proved

The number of bonds touching but not inside Λ_n, divided by the number of sites of Λ_n.

noncomputable def ibs_boundaryFraction (d n : ℕ) : ℝ :=
  ((bondFinsetTouch d n \ bondFinsetInternal d n).card : ℝ) / ((boxFinset d n).card : ℝ)

Uses 4 · Used by 2

Statement usesBonds inside the box · Bonds touching the box · Box \((-n, n)^d\) as a finite set of sites · Site of the hypercubic lattice

Used byBoundary influence bound for the minus box measures · Boundary influence bound for the plus box measures

DefinitionBoundary influence bound for the plus box measures#✓fully proved

Shift differences of cylinder-function integrals against the plus box measures are O(boundary fraction).

def ibs_PlusBoundaryInfluence (β h : ℝ) (g : Multiplicative (Site d)) (φ : ℕ → ℕ) : Prop :=
  ∀ f ∈ pstc_cylinderBcfSet d, ∃ C : ℝ, ∀ n,
    |pstc_decayFun (fun n => plusMeasure d (φ n) β h) g f n|
      ≤ C * ibs_boundaryFraction d (φ n)

Uses 6

Statement usesConfiguration space of a statistical-mechanics model · Boundary bond fraction of a box · Plus-boundary Ising measure in a box · Cylinder functions as bounded continuous functions · Difference between an integral and its shifted version · Site of the hypercubic lattice

DefinitionBoundary influence bound for the minus box measures#✓fully proved

Shift differences of cylinder-function integrals against the minus box measures are O(boundary fraction).

def ibs_MinusBoundaryInfluence (β h : ℝ) (g : Multiplicative (Site d)) (φ : ℕ → ℕ) : Prop :=
  ∀ f ∈ pstc_cylinderBcfSet d, ∃ C : ℝ, ∀ n,
    |pstc_decayFun (fun n => minusMeasure d (φ n) β h) g f n|
      ≤ C * ibs_boundaryFraction d (φ n)

Uses 6

Statement usesConfiguration space of a statistical-mechanics model · Boundary bond fraction of a box · Minus-boundary Ising measure in a box · Cylinder functions as bounded continuous functions · Difference between an integral and its shifted version · Site of the hypercubic lattice

DefinitionAll-plus monomial as a continuous function#✓fully proved

The monomial ω ↦ ∏_{x ∈ T} 1_{ω_x = +} as a continuous function.

noncomputable def iti_monomialCM (T : Finset (Site d)) : C(ConfigSpace (Site d), ℝ) :=
  ∏ x ∈ T, pstc_coordCM x

Uses 3 · Used by 2

Statement usesConfiguration space of a statistical-mechanics model · Plus-spin indicator at a site as a continuous function · Site of the hypercubic lattice

Used byTranslation invariance of the plus state · All-plus monomial as a bounded continuous function

DefinitionAll-plus monomial as a bounded continuous function#✓fully proved

The monomial ω ↦ ∏_{x ∈ T} 1_{ω_x = +} as a bounded continuous function.

noncomputable def iti_monomialBcf (T : Finset (Site d)) : ConfigSpace (Site d) →ᵇ ℝ :=
  BoundedContinuousFunction.mkOfCompact (iti_monomialCM T)

Uses 3 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · All-plus monomial as a continuous function · Site of the hypercubic lattice

Used byTranslation invariance of the plus state

DefinitionShift homogeneity of all-plus events in the plus state#✓fully proved

The plus state gives the all-plus events on T and on g⁻¹ T the same probability, for every finite T.

def iti_PlusMultiHomogeneous (β h : ℝ) (g : Multiplicative (Site d)) : Prop :=
  ∀ T : Finset (Site d),
    (plusState d β h : Measure (ConfigSpace (Site d))).real (fmu_multiOpen (E := Site d) T)
      = (plusState d β h : Measure (ConfigSpace (Site d))).real
          (fmu_multiOpen (E := Site d) (T.image (fun x => g⁻¹ • x)))

Uses 4 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Event that every coordinate of a finite set is open · Infinite-volume plus state as a subsequential weak limit · Site of the hypercubic lattice

Used byTranslation invariance of the plus state

DefinitionContinuous functions with decaying shifted integrals#✓fully proved

The continuous functions whose shifted integrals against the plus box measures decay along φ.

StatMech.Ising.iti_decaySet · 23 lines

noncomputable def iti_decaySet (β h : ℝ) (g : Multiplicative (Site d)) (φ : ℕ → ℕ) :
    Submodule ℝ C(ConfigSpace (Site d), ℝ) where
  carrier := {hh | Tendsto (pstc_decayFun (fun n => plusMeasure d (φ n) β h) g
      (BoundedContinuousFunction.mkOfCompact hh)) atTop (𝓝 0)}
  add_mem' {hh hh'} h1 h2 := by
    simp only [Set.mem_ofPred_eq] at h1 h2 ⊢
    have hsum := h1.add h2; rw [add_zero] at hsum
    refine hsum.congr (fun n => ?_)
    rw [BoundedContinuousFunction.mkOfCompact_add, iti_decayFun_add]
  zero_mem' := by
    simp only [Set.mem_ofPred_eq]
    have hz : pstc_decayFun (fun n => plusMeasure d (φ n) β h) g
        (BoundedContinuousFunction.mkOfCompact (0 : C(ConfigSpace (Site d), ℝ)))
      = fun _ => (0:ℝ) := by
      funext n; rw [BoundedContinuousFunction.mkOfCompact_zero, iti_decayFun_zero]
    rw [hz]; exact tendsto_const_nhds
  smul_mem' c hh h1 := by
    simp only [Set.mem_ofPred_eq] at h1 ⊢
    have hsmul := h1.const_mul c; rw [mul_zero] at hsmul
    refine hsmul.congr (fun n => ?_)
    have hms : BoundedContinuousFunction.mkOfCompact (c • hh)
        = c • BoundedContinuousFunction.mkOfCompact hh := rfl
    rw [hms, iti_decayFun_smul]

Uses 5 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Shift of a configuration by a group element · Plus-boundary Ising measure in a box · Difference between an integral and its shifted version · Site of the hypercubic lattice

Used byTranslation invariance of the plus state

DefinitionAsymptotic shift homogeneity of all-plus events in plus boxes#✓fully proved

Along φ, the plus box measures give the all-plus events on T and on g⁻¹ T asymptotically equal probabilities.

def itb_PlusMultiBoundaryDecay (β h : ℝ) (g : Multiplicative (Site d)) (φ : ℕ → ℕ) : Prop :=
  ∀ T : Finset (Site d),
    Tendsto (fun n =>
      ((plusMeasure d (φ n) β h : Measure (ConfigSpace (Site d))).real
          (fmu_multiOpen (E := Site d) T))
        - ((plusMeasure d (φ n) β h : Measure (ConfigSpace (Site d))).real
            (fmu_multiOpen (E := Site d) (T.image (fun x => g⁻¹ • x)))))
      atTop (𝓝 0)

Uses 4

Statement usesConfiguration space of a statistical-mechanics model · Event that every coordinate of a finite set is open · Plus-boundary Ising measure in a box · Site of the hypercubic lattice

DefinitionOff-centre domination of all-plus events#✓fully proved

For every finite T there is c such that plus measures on boxes of sizes m + c and m compare the all-plus events on T and g⁻¹ T in both directions.

def itb_OffCentreDomination (β h : ℝ) (g : Multiplicative (Site d)) : Prop :=
  ∀ T : Finset (Site d), ∃ c : ℕ, ∀ m : ℕ,
    (plusMeasure d (m + c) β h : Measure (ConfigSpace (Site d))).real
        (fmu_multiOpen (E := Site d) T)
      ≤ (plusMeasure d m β h : Measure (ConfigSpace (Site d))).real
          (fmu_multiOpen (E := Site d) (T.image (fun x => g⁻¹ • x)))
    ∧ (plusMeasure d m β h : Measure (ConfigSpace (Site d))).real
          (fmu_multiOpen (E := Site d) (T.image (fun x => g⁻¹ • x)))
      ≤ (plusMeasure d (m - c) β h : Measure (ConfigSpace (Site d))).real
          (fmu_multiOpen (E := Site d) T)

Uses 4

Statement usesConfiguration space of a statistical-mechanics model · Event that every coordinate of a finite set is open · Plus-boundary Ising measure in a box · Site of the hypercubic lattice

DefinitionShift vector \(R e_{i_0}\)#✓fully proved

The vector R e_{i₀} of ℤ^d.

noncomputable def icb_shiftVec {d : ℕ} (i₀ : Fin d) (R : ℤ) : Site d :=
  fun i => if i = i₀ then R else 0

Uses 1 · Used by 2

Statement usesSite of the hypercubic lattice

Used byErgodicity of the plus state · Extremality of the plus state

DefinitionUnit vector of \(\mathbb{Z}^d\)#✓fully proved

The unit vector e_i of ℤ^d.

def gvUnit (d : ℕ) (i : Fin d) : Site d := fun j => if j = i then 1 else 0

Uses 1 · Used by 6

Statement usesSite of the hypercubic lattice

Used byInf-based and sup-based Ising critical points agree for \(d \ge 2\) · Site with its nearest neighbours · Translation invariance of the plus state · 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

DefinitionSite with its nearest neighbours#✓fully proved

The site x and its nearest neighbours.

noncomputable def gvBall (x : Site d) : Finset (Site d) :=
  insert x ((Finset.univ : Finset (Fin d)).biUnion
    (fun i => {x + gvUnit d i, x - gvUnit d i}))

Uses 2 · Used by 6

Statement usesUnit vector of \(\mathbb{Z}^d\) · Site of the hypercubic lattice

Used byInf-based and sup-based Ising critical points agree for \(d \ge 2\) · Set with its nearest neighbours · Translation invariance of the plus state · 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

DefinitionSet with its nearest neighbours#✓fully proved

The sites of S together with their nearest neighbours.

noncomputable def gvCand (S : Finset (Site d)) : Finset (Site d) := S.biUnion gvBall

Uses 2 · Used by 6

Statement usesSite with its nearest neighbours · Site of the hypercubic lattice

Used byInf-based and sup-based Ising critical points agree for \(d \ge 2\) · Bonds touching a set · Translation invariance of the plus state · 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

DefinitionBonds touching a set#✓fully proved

The bonds with at least one endpoint in S.

noncomputable def gvBondTouch (S : Finset (Site d)) : Finset (Sym2 (Site d)) :=
  (((gvCand S) ×ˢ (gvCand S)).filter
    (fun p => (hypercubicLattice d).Adj p.1 p.2 ∧ (p.1 ∈ S ∨ p.2 ∈ S))).image (fun p => s(p.1, p.2))

Uses 4 · Used by 7

Statement usesSet with its nearest neighbours · Nearest neighbours in \(\mathbb{Z}^d\) · Site of the hypercubic lattice · Hypercubic lattice \(\mathbb{Z}^d\)

Used byInf-based and sup-based Ising critical points agree for \(d \ge 2\) · Energy on a set with a boundary condition · Translation invariance of the plus state · 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\) · Boundary edges of a finite volume · Simon–Lieb inequality in the infinite-volume plus state

DefinitionConfiguration glued from a set and a boundary condition#✓fully proved

The configuration equal to τ on S and to η off S.

noncomputable def gvGlue (η : ConfigSpace (Site d)) (S : Finset (Site d))
    (τ : {x // x ∈ S} → Bool) : ConfigSpace (Site d) :=
  fun x => if h : x ∈ S then τ ⟨x, h⟩ else η x

Uses 2 · Used by 7

Statement usesConfiguration space of a statistical-mechanics model · Site of the hypercubic lattice

Used byInf-based and sup-based Ising critical points agree for \(d \ge 2\) · Energy on a set with a boundary condition · Finite-volume Gibbs measure on a finite set · Translation invariance of the plus state · 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

DefinitionEnergy on a set with a boundary condition#✓fully proved

The energy -∑_{e touching S} σ_e - h ∑_{x ∈ S} σ_x of gvGlue η S τ.

noncomputable def gvEnergy (η : ConfigSpace (Site d)) (S : Finset (Site d)) (h : ℝ)
    (τ : {x // x ∈ S} → Bool) : ℝ :=
  - (∑ e ∈ gvBondTouch S, bond (gvGlue η S τ) e) - h * ∑ x ∈ S, spin (gvGlue η S τ) x

Uses 6 · Used by 6

Statement usesConfiguration space of a statistical-mechanics model · Bond variable of an unordered pair · Bonds touching a set · Configuration glued from a set and a boundary condition · Spin of a configuration at a site · Site of the hypercubic lattice

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

DefinitionBoltzmann weight on a set with a boundary condition#✓fully proved

The Boltzmann weight of the configuration τ on S with boundary condition η.

noncomputable def gvWeight (η : ConfigSpace (Site d)) (S : Finset (Site d)) (β h : ℝ)
    (τ : {x // x ∈ S} → Bool) : ℝ :=
  Real.exp (-β * gvEnergy η S h τ)

Uses 3 · Used by 7

Statement usesConfiguration space of a statistical-mechanics model · Energy on a set with a boundary condition · Site of the hypercubic lattice

Used byInf-based and sup-based Ising critical points agree for \(d \ge 2\) · Gibbs probability on a set with a boundary condition · Partition function on a set with a boundary condition · Translation invariance of the plus state · 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

DefinitionPartition function on a set with a boundary condition#✓fully proved

The partition function on S with boundary condition η.

noncomputable def gvZ (η : ConfigSpace (Site d)) (S : Finset (Site d)) (β h : ℝ) : ℝ :=
  ∑ τ : {x // x ∈ S} → Bool, gvWeight η S β h τ

Uses 3 · Used by 6

Statement usesConfiguration space of a statistical-mechanics model · Boltzmann weight on a set with a boundary condition · Site of the hypercubic lattice

Used byInf-based and sup-based Ising critical points agree for \(d \ge 2\) · Gibbs probability on a set with a boundary condition · Translation invariance of the plus state · 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

DefinitionGibbs probability on a set with a boundary condition#✓fully proved

The Gibbs probability of τ on S with boundary condition η.

noncomputable def gvProb (η : ConfigSpace (Site d)) (S : Finset (Site d)) (β h : ℝ)
    (τ : {x // x ∈ S} → Bool) : ℝ :=
  gvWeight η S β h τ / gvZ η S β h

Uses 4 · Used by 6

Statement usesConfiguration space of a statistical-mechanics model · Boltzmann weight on a set with a boundary condition · Partition function on a set with a boundary condition · Site of the hypercubic lattice

Used byInf-based and sup-based Ising critical points agree for \(d \ge 2\) · Finite-volume Gibbs measure on a finite set · Translation invariance of the plus state · 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

DefinitionFinite-volume Gibbs measure on a finite set#✓fully proved

The finite-volume Gibbs measure on the finite set S with boundary condition η.

noncomputable def gvMeasure (η : ConfigSpace (Site d)) (S : Finset (Site d)) (β h : ℝ) :
    Measure (ConfigSpace (Site d)) :=
  ∑ τ : {x // x ∈ S} → Bool,
    ENNReal.ofReal (gvProb η S β h τ) • Measure.dirac (gvGlue η S τ)

Uses 4 · Used by 6

Statement usesConfiguration space of a statistical-mechanics model · Configuration glued from a set and a boundary condition · Gibbs probability on a set with a boundary condition · Site of the hypercubic lattice

Used byInf-based and sup-based Ising critical points agree for \(d \ge 2\) · Finite-volume Gibbs measure with plus boundary condition · Translation invariance of the plus state · 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

DefinitionFinite-volume Gibbs measure with plus boundary condition#✓fully proved

The finite-volume Gibbs measure on S with plus boundary condition.

noncomputable def gvPlusMeasure (S : Finset (Site d)) (β h : ℝ) : Measure (ConfigSpace (Site d)) :=
  gvMeasure (plusField d) S β h

Uses 4 · Used by 5

Statement usesConfiguration space of a statistical-mechanics model · Finite-volume Gibbs measure on a finite set · All-plus configuration · Site of the hypercubic lattice

Used byInf-based and sup-based Ising critical points agree for \(d \ge 2\) · Translation invariance of the plus state · 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

DefinitionOverwriting a configuration on an inner set#✓fully proved

The configuration on Sout obtained by overwriting its spins in Sin with τ.

noncomputable def gvOvr {Sin Sout : Finset (Site d)} (_hsub : Sin ⊆ Sout)
    (σ : {x // x ∈ Sout} → Bool) (τ : {x // x ∈ Sin} → Bool) : {x // x ∈ Sout} → Bool :=
  fun x => if hn : (x : Site d) ∈ Sin then τ ⟨x, hn⟩ else σ x

Uses 1 · Used by 2

Statement usesSite of the hypercubic lattice

Used byInvolution swapping inner-set parts of configuration pairs · Translation invariance of the plus state

DefinitionRestriction of a configuration to an inner set#✓fully proved

The restriction of a configuration on Sout to Sin.

noncomputable def gvRes {Sin Sout : Finset (Site d)} (hsub : Sin ⊆ Sout)
    (σ : {x // x ∈ Sout} → Bool) : {x // x ∈ Sin} → Bool :=
  fun x => σ ⟨x, hsub x.2⟩

Uses 1 · Used by 2

Statement usesSite of the hypercubic lattice

Used byInvolution swapping inner-set parts of configuration pairs · Translation invariance of the plus state

DefinitionInvolution swapping inner-set parts of configuration pairs#✓fully proved

The involution exchanging the Sin parts of a configuration on Sout and a configuration on Sin.

noncomputable def gvSwapPair {Sin Sout : Finset (Site d)} (hsub : Sin ⊆ Sout) :
    (({x // x ∈ Sout} → Bool) × ({x // x ∈ Sin} → Bool))
      → (({x // x ∈ Sout} → Bool) × ({x // x ∈ Sin} → Bool)) :=
  fun p => (gvOvr hsub p.1 p.2, gvRes hsub p.1)

Uses 3 · Used by 1

Statement usesOverwriting a configuration on an inner set · Restriction of a configuration to an inner set · Site of the hypercubic lattice

Used byTranslation invariance of the plus state

DefinitionBox sites as a set and as a finite set#✓fully proved

The sites of the box Λ_n as a set and as a finset.

noncomputable def iptp_boxEquiv (d n : ℕ) :
    {x : Site d // x ∈ box d n} ≃ {x : Site d // x ∈ boxFinset d n} :=
  Equiv.subtypeEquivProp (by ext x; rw [mem_boxFinset])

Uses 3 · Used by 5

Statement usesBox \((-n, n)^d\) as a finite set of sites · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice

Used byInf-based and sup-based Ising critical points agree for \(d \ge 2\) · Translation invariance of the plus state · 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

DefinitionTranslation as an equivalence onto a translate#✓fully proved

Translation by g as an equivalence between S and its translate.

noncomputable def iptp_transInteriorEquiv (g : Multiplicative (Site d)) (S : Finset (Site d)) :
    {x : Site d // x ∈ S} ≃ {x : Site d // x ∈ S.image (fun x => g • x)} where
  toFun x := ⟨g • (x : Site d), Finset.mem_image_of_mem _ x.2⟩
  invFun y := ⟨g⁻¹ • (y : Site d), by
    obtain ⟨z, hz, hzeq⟩ := Finset.mem_image.mp y.2
    rw [← hzeq, inv_smul_smul]; exact hz⟩
  left_inv x := by ext; simp [inv_smul_smul]
  right_inv y := by ext; simp [smul_inv_smul]

Uses 1 · Used by 1

Statement usesSite of the hypercubic lattice

Used byTranslation invariance of the plus state

TheoremTranslation invariance of the plus state#✓fully proved

For β, h ≥ 0, the plus state of the Ising model on ℤ^d is invariant under all lattice translations.

S. Friedli and Y. Velenik, Statistical Mechanics of Lattice Systems, Cambridge University Press (2017), Chapter 3.

theorem iptp_plusState_isTranslationInvariant {β : ℝ} (hβ : 0 ≤ β) {h : ℝ} (hh : 0 ≤ h) :
    ConfigSpace.IsTranslationInvariant (G := Multiplicative (Site d))
      (plusState d β h : Measure (ConfigSpace (Site d)))

Uses 64 · Used by 5

Statement usesConfiguration space of a statistical-mechanics model · Translation-invariant measure on configuration space · Infinite-volume plus state as a subsequential weak limit · Site of the hypercubic lattice

Proof usesShift of a configuration by a group element · Sup norm of a site of \(\mathbb{Z}^d\) · Event that every coordinate of a finite set is open · Increasing event · Infinite-volume state of a sequence of measures · Bond variable of an unordered pair · Bonds touching the box · Ordered nearest-neighbour pairs touching the box · Box \((-n, n)^d\) as a finite set of sites · Existence of infinite-volume states · Box energy with a boundary condition · Finite-volume Gibbs measure on configurations of \(\mathbb{Z}^d\) · Finite-volume Gibbs probability with a boundary condition · Finite-volume Boltzmann weight with a boundary condition · Finite-volume partition function with a boundary condition · Configuration glued from inside spins and a boundary condition · Site with its nearest neighbours · Bonds touching a set · Set with its nearest neighbours · Energy on a set with a boundary condition · Configuration glued from a set and a boundary condition · Finite-volume Gibbs measure on a finite set · Overwriting a configuration on an inner set · Finite-volume Gibbs measure with plus boundary condition · Gibbs probability on a set with a boundary condition · Restriction of a configuration to an inner set · Involution swapping inner-set parts of configuration pairs · Unit vector of \(\mathbb{Z}^d\) · Boltzmann weight on a set with a boundary condition · Partition function on a set with a boundary condition · Box sites as a set and as a finite set · Translation as an equivalence onto a translate · Shift homogeneity of all-plus events in the plus state · Continuous functions with decaying shifted integrals · All-plus monomial as a bounded continuous function · All-plus monomial as a continuous function · Chosen subsequential weak limit of a sequence of measures · Overwriting a configuration on an inner box · All-plus configuration · Plus-boundary Ising measure in a box · Decay of shifted integrals for plus box measures · Shifted plus-boundary box measure · Decay of shifted cylinder integrals for plus box measures · Plus-spin indicator at a site as a continuous function · Subalgebra of cylinder functions · Cylinder functions as bounded continuous functions · Difference between an integral and its shifted version · Restriction of a configuration to an inner box · Spin of a configuration at a site · Involution swapping inner-box parts of configuration pairs · Nearest neighbours in \(\mathbb{Z}^d\) · Box \((-n, n)^d\) in the hypercubic lattice · Hypercubic lattice \(\mathbb{Z}^d\) · Stochastic domination of measures on configurations · Stochastic domination compares real-valued masses · Weak convergence of probability measures on configuration space · Weak convergence implies convergence of integrals · Portmanteau theorem for clopen events · Holley inequality for increasing events · Convergence of integrals implies weak convergence

Used byInf-based and sup-based Ising critical points agree for \(d \ge 2\) · Ergodicity of the plus state · Extremality of the plus state · 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\)

TheoremExtremality of the plus state#✓fully proved

For d ≥ 1 and β, h ≥ 0, the plus state is an extreme point of the translation-invariant probability measures.

H.-O. Georgii, Gibbs Measures and Phase Transitions, de Gruyter (1988), Chapter 14.

theorem ising_plus_extreme (hd : 1 ≤ d) {β : ℝ} (hβ : 0 ≤ β) {h : ℝ} (hh : 0 ≤ h) :
    StatMech.FK.IsInvariantExtremePoint (G := Multiplicative (Site d))
      (plusState d β h : Measure (ConfigSpace (Site d)))

Uses 48

Statement usesConfiguration space of a statistical-mechanics model · Extreme point of the invariant probability measures · Infinite-volume plus state as a subsequential weak limit · Site of the hypercubic lattice

Proof usesErgodic measure on configuration space · Translation-invariant measure on configuration space · Almost-invariant events are trivial under an ergodic measure · Shift of a configuration by a group element · Self-mixing on cylinder events · Translation-invariant self-mixing measures are ergodic · Pair mixing of multi-open events · Upper decay of correlations of multi-open events · Product indicator of a multi-open event · Event that every coordinate of a finite set is open · Inclusion–exclusion coefficient of a multi-open event · Indicator of agreeing with a pattern on a finite set · Coordinate state as a real number · FKG lattice condition · Increasing event · Infinite-volume state of a sequence of measures · Bond variable of an unordered pair · Bonds touching the box · Ordered nearest-neighbour pairs touching the box · Box \((-n, n)^d\) as a finite set of sites · Existence of infinite-volume states · Box energy with a boundary condition · Finite-volume Gibbs measure on configurations of \(\mathbb{Z}^d\) · Finite-volume Gibbs probability with a boundary condition · Finite-volume Boltzmann weight with a boundary condition · Finite-volume partition function with a boundary condition · Configuration glued from inside spins and a boundary condition · Shift vector \(R e_{i_0}\) · Translation invariance of the plus state · Chosen subsequential weak limit of a sequence of measures · Overwriting a configuration on an inner box · All-plus configuration · Plus-boundary Ising measure in a box · Restriction of a configuration to an inner box · Spin of a configuration at a site · Involution swapping inner-box parts of configuration pairs · Box \((-n, n)^d\) in the hypercubic lattice · Hypercubic lattice \(\mathbb{Z}^d\) · Stochastic domination of measures on configurations · Stochastic domination compares real-valued masses · Weak convergence of probability measures on configuration space · Portmanteau theorem for clopen events · FKG inequality for increasing events · Holley inequality for increasing events

TheoremErgodicity of the plus state#✓fully proved

For d ≥ 1 and β, h ≥ 0, the plus state is ergodic under lattice translations.

H.-O. Georgii, Gibbs Measures and Phase Transitions, de Gruyter (1988), Chapter 14.

theorem iptp_plusState_isErgodic (hd : 1 ≤ d) {β : ℝ} (hβ : 0 ≤ β) {h : ℝ} (hh : 0 ≤ h) :
    IsErgodic (G := Multiplicative (Site d))
      (plusState d β h : Measure (ConfigSpace (Site d)))

Uses 46

Statement usesConfiguration space of a statistical-mechanics model · Ergodic measure on configuration space · Infinite-volume plus state as a subsequential weak limit · Site of the hypercubic lattice

Proof usesTranslation-invariant measure on configuration space · Shift of a configuration by a group element · Self-mixing on cylinder events · Translation-invariant self-mixing measures are ergodic · Pair mixing of multi-open events · Upper decay of correlations of multi-open events · Product indicator of a multi-open event · Event that every coordinate of a finite set is open · Inclusion–exclusion coefficient of a multi-open event · Indicator of agreeing with a pattern on a finite set · Coordinate state as a real number · FKG lattice condition · Increasing event · Infinite-volume state of a sequence of measures · Bond variable of an unordered pair · Bonds touching the box · Ordered nearest-neighbour pairs touching the box · Box \((-n, n)^d\) as a finite set of sites · Existence of infinite-volume states · Box energy with a boundary condition · Finite-volume Gibbs measure on configurations of \(\mathbb{Z}^d\) · Finite-volume Gibbs probability with a boundary condition · Finite-volume Boltzmann weight with a boundary condition · Finite-volume partition function with a boundary condition · Configuration glued from inside spins and a boundary condition · Shift vector \(R e_{i_0}\) · Translation invariance of the plus state · Chosen subsequential weak limit of a sequence of measures · Overwriting a configuration on an inner box · All-plus configuration · Plus-boundary Ising measure in a box · Restriction of a configuration to an inner box · Spin of a configuration at a site · Involution swapping inner-box parts of configuration pairs · Box \((-n, n)^d\) in the hypercubic lattice · Hypercubic lattice \(\mathbb{Z}^d\) · Stochastic domination of measures on configurations · Stochastic domination compares real-valued masses · Weak convergence of probability measures on configuration space · Portmanteau theorem for clopen events · FKG inequality for increasing events · Holley inequality for increasing events

DefinitionExtreme point of the DLR states#✓fully proved

μ is an extreme point of the DLR states: a proper convex decomposition into DLR probability measures is trivial.

def IsDLRExtremePoint (β h : ℝ) (μ : Measure (ConfigSpace (Site d))) : Prop :=
  ∀ (ν₁ ν₂ : Measure (ConfigSpace (Site d))) [IsProbabilityMeasure ν₁] [IsProbabilityMeasure ν₂],
    IsDLRState d β h ν₁ → IsDLRState d β h ν₂ →
    ∀ (a b : ℝ≥0∞), 0 < a → 0 < b → a + b = 1 → a ≠ ⊤ → b ≠ ⊤ →
      μ = a • ν₁ + b • ν₂ → ν₁ = ν₂

Uses 3

Statement usesConfiguration space of a statistical-mechanics model · DLR state of the Ising model on \(\mathbb{Z}^d\) · Site of the hypercubic lattice

LemmaAll-plus Dirac mass gives the all-plus event probability one#✓fully proved

A nonvacuity check: the Dirac mass at the all-plus configuration gives the all-plus event probability one.

lemma atip2_ergodic_zeroOne_nonvacuous :
    (Measure.dirac (fun _ => true) : Measure (ConfigSpace (Site 1)))
        {ω : ConfigSpace (Site 1) | ∀ e, ω e = true} = 1

Uses 5

Statement usesConfiguration space of a statistical-mechanics model · Site of the hypercubic lattice

Proof usesErgodic measure on configuration space · Translation-invariant measure on configuration space · Shift of a configuration by a group element

DefinitionTail event for lattice spin configurations#✓fully proved

A tail event: measurable with respect to the spins outside Λ_n, for every n.

def IsTailEvent (s : Set (ConfigSpace (Site d))) : Prop :=
  ∀ n : ℕ, @MeasurableSet _ (outsideSigma (box d n)) s

Uses 4 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice · σ-algebra of the configuration outside a region

Used byNonvacuity of the a.s.-tail theorem via the all-plus Dirac mass

Definitionσ-algebra generated by the spins in a finite set#✓fully proved

The σ-algebra generated by the spins in the finite set F.

@[reducible] noncomputable def aetc_finSig (F : Finset (Site d)) :
    MeasurableSpace (ConfigSpace (Site d)) :=
  ⨆ e ∈ F, MeasurableSpace.comap (ConfigSpace.eval e) inferInstance

Uses 3 · Used by 2

Statement usesConfiguration space of a statistical-mechanics model · Coordinate projection of a configuration · Site of the hypercubic lattice

Used byCylinder events of the Ising configuration space · Nonvacuity of the a.s.-tail theorem via the all-plus Dirac mass

DefinitionCylinder events of the Ising configuration space#✓fully proved

The cylinder events: events depending on the spins in some box.

def aetc_Cring (d : ℕ) : Set (Set (ConfigSpace (Site d))) :=
  {A | ∃ F : Finset (Site d), MeasurableSet[aetc_finSig F] A}

Uses 3 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · σ-algebra generated by the spins in a finite set · Site of the hypercubic lattice

Used byNonvacuity of the a.s.-tail theorem via the all-plus Dirac mass

DefinitionApproximation in measure by events measurable outside every box#✓fully proved

For every box Λ_k and ε > 0, s is ε-approximated in μ-measure by an event measurable outside Λ_k.

def AeApproxFarOut (μ : Measure (ConfigSpace (Site d))) (s : Set (ConfigSpace (Site d))) : Prop :=
  ∀ (k : ℕ) (ε : ℝ≥0∞), 0 < ε →
    ∃ A : Set (ConfigSpace (Site d)), @MeasurableSet _ (outsideSigma (box d k)) A ∧ μ (s ∆ A) < ε

Uses 4 · Used by 1

Statement usesConfiguration space of a statistical-mechanics model · Site of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice · σ-algebra of the configuration outside a region

Used byNonvacuity of the a.s.-tail theorem via the all-plus Dirac mass

LemmaNonvacuity of the a.s.-tail theorem via the all-plus Dirac mass#✓fully proved

The hypotheses of aetc_haeTail are satisfiable: the Dirac mass at the all-plus configuration.

lemma aetc_haeTail_nonvacuous :
    ∃ s' : Set (ConfigSpace (Site 1)), IsTailEvent (d := 1) s'
      ∧ (Set.univ : Set (ConfigSpace (Site 1)))
          =ᵐ[(Measure.dirac (fun _ => true) : Measure (ConfigSpace (Site 1)))] s'

Uses 13

Statement usesConfiguration space of a statistical-mechanics model · Tail event for lattice spin configurations · Site of the hypercubic lattice

Proof usesTranslation-invariant measure on configuration space · Coordinate projection of a configuration · Product σ-algebra on configuration space is generated by the coordinates · Shift of a configuration by a group element · Approximation in measure by events measurable outside every box · Cylinder events of the Ising configuration space · σ-algebra generated by the spins in a finite set · Box \((-n, n)^d\) in the hypercubic lattice · σ-algebra of the configuration outside a region · Outside σ-algebra is a sub-σ-algebra of the product σ-algebra

47 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.