Continuity of Onsager's pressure at the critical point

2 fully proved

A. The integrand near the critical point

DefinitionIntegrable dominating function for log g near the critical point#✓fully proved

The dominating function log 9 + log 2 + |log (1 - cos y)| for log g near β_c.

noncomputable def ons_criticalLogBound (y : ℝ) : ℝ :=
  Real.log 9 + Real.log 2 + |Real.log (1 - Real.cos y)|

Used by 4

Used byUniform bound constant for the inner integrals near β_c · Onsager's formula from the spin Kac-Ward identities · Continuity of Onsager's pressure at the critical point · Onsager's formula

B. Inner integrals

DefinitionUniform bound constant for the inner integrals near β_c#✓fully proved

A uniform bound for the inner integrals ∫ log g dk₂ near β_c.

noncomputable def ons_criticalInnerBound : ℝ :=
  |∫ k2 in (-Real.pi)..Real.pi, ons_criticalLogBound k2|

Uses 1 · Used by 3

Statement usesIntegrable dominating function for log g near the critical point

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

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.