Onsager's free energy and the torus pressure

DefinitionOnsager's free-energy double integral#✓fully proved

The integral (1 / (8π²)) ∫_{-π}^{π} ∫_{-π}^{π} log (cosh² 2β - sinh 2β (cos k₁ + cos k₂)) dk₁ dk₂ in Onsager's formula.

noncomputable def ons_freeEnergyIntegral (β : ℝ) : ℝ :=
  (1 / (8 * Real.pi ^ 2)) *
    ∫ k₁ in (-Real.pi)..Real.pi, ∫ k₂ in (-Real.pi)..Real.pi, Real.log (ons_gInt β k₁ k₂)

Uses 1 · Used by 6

Statement usesOnsager integrand of the square-lattice Ising model

Used byLimit statement for \(\log X_L(\tanh\beta)/L^2\) on the torus · Onsager's pressure of the square-lattice Ising model · Onsager's formula · Onsager's formula from the spin Kac-Ward identities · Continuity of Onsager's pressure at the critical point · Onsager's formula

DefinitionOnsager's pressure of the square-lattice Ising model#✓fully proved

Onsager's pressure (minus β times the free energy per site) of the square-lattice Ising model: log 2 plus ons_freeEnergyIntegral β.

noncomputable def ons_pressure (β : ℝ) : ℝ := Real.log 2 + ons_freeEnergyIntegral β

Uses 1 · Used by 4

Statement usesOnsager's free-energy double integral

Used byOnsager's formula · Onsager's formula from the spin Kac-Ward identities · Continuity of Onsager's pressure at the critical point · Onsager's formula

DefinitionLimit statement for \(\log X_L(\tanh\beta)/L^2\) on the torus#✓fully proved

The statement that log X_L(tanh β) / L² on the L × L torus converges to ons_freeEnergyIntegral β - 2 log cosh β as L → ∞.

def ons_KacWardResidue (β : ℝ) : Prop :=
  Filter.Tendsto
    (fun L : ℕ => if h : 2 < L then
        (letI : Fact (2 < L) := ⟨h⟩
         Real.log (ons_X (onsTorusGraph L) (Real.tanh β)) / ((L : ℝ) ^ 2))
      else 0)
    Filter.atTop
    (nhds (ons_freeEnergyIntegral β - 2 * Real.log (Real.cosh β)))

Uses 4 · Used by 2

Statement usesNearest-neighbor adjacency on the discrete torus · The \(L \times L\) square-lattice torus graph · Even-subgraph generating function of a graph · Onsager's free-energy double integral

Used byOnsager's formula from the spin Kac-Ward identities · Onsager's formula

3 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.