Pressure of the Ising model

DefinitionPartition function of a finite system#✓fully proved

The partition function Z(β) = ∑_s e^{-βE(s)} of a finite system.

noncomputable def Z {Ω : Type*} [Fintype Ω] (β : ℝ) (E : Ω → ℝ) : ℝ :=
  ∑ s : Ω, Real.exp (-β * E s)

Used by 4

Used byOnsager's formula from the spin Kac-Ward identities · Onsager's formula · Pressure from independent copies · Partition function of independent copies

DefinitionPartition function of independent copies#✓fully proved

The partition function of n independent copies of the system.

noncomputable def Zpow {Ω : Type*} [Fintype Ω] (β : ℝ) (E : Ω → ℝ) (n : ℕ) : ℝ :=
  Z β (fun c : Fin n → Ω => ∑ i, E (c i))

Uses 1 · Used by 2

Statement usesPartition function of a finite system

Used byLog-partition sequence of independent copies · Pressure from independent copies

DefinitionLog-partition sequence of independent copies#✓fully proved

The sequence log Z_n for n independent copies.

noncomputable def logZSeq {Ω : Type*} [Fintype Ω] (β : ℝ) (E : Ω → ℝ) (n : ℕ) : ℝ :=
  Real.log (Zpow β E n)

Uses 1 · Used by 1

Statement usesPartition function of independent copies

Used byPressure from independent copies

DefinitionPressure from independent copies#✓fully proved

The pressure: the limit of log Z_n / n for independent copies, obtained from subadditivity.

noncomputable def pressure {Ω : Type*} [Fintype Ω] [Nonempty Ω] (β : ℝ) (E : Ω → ℝ) : ℝ :=
  (logZSeq_subadditive β E).lim

Uses 3

Statement usesPartition function of a finite system · Partition function of independent copies · Log-partition sequence of independent copies

DefinitionOuter vertex boundary of a box#✓fully proved

The outer vertex boundary Λ_{n+1} ∖ Λ_n of the box.

noncomputable def psv_Bdry (d n : ℕ) : Finset (Site d) :=
  (vertexBoundary_finite d (n + 1)).toFinset

Uses 3

Statement usesSite of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice · Inner vertex boundary of a box

5 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.