Sharpness of the phase transition for the Ising model

• The Aizenman–Barsky–Fernández differential inequality, finite volume
• Exponential decay of the plus-state two-point function below β̃_c
• Finite susceptibility of the plus state below β̃_c
• The Duminil-Copin–Tassion point for the Ising model
• Sharpness of the phase transition for the Ising model on ℤ^d

LemmaAbstract form of the sharpness theorem#✓fully proved

Abstract form of the sharpness theorem: a magnetization satisfying the mean-field differential inequality above β_c obeys m(β) ≥ √(1 - (β_c/β)²), and correlations satisfying Simon's self-consistent bound with φ < 1 are summable with sum at most |S|/(1 - φ). The hypotheses are inputs; the unconditional statement is ising_sharp_phase_transition.

lemma ising_sharpness {V : Type*} (origin : V) (β_c : ℝ) (hβc : 0 < β_c)
    (m : ℝ → ℝ) (corr : V → V → ℝ)
    (hdiff : ∀ β ∈ Set.Ici β_c, DifferentiableAt ℝ (fun β => (m β) ^ 2) β)
    (hineq : ∀ β ∈ Set.Ioi β_c, (2 / β) * (1 - (m β) ^ 2) ≤ deriv (fun β => (m β) ^ 2) β)
    (hzero : m β_c = 0) (hmnonneg : ∀ β ∈ Set.Ici β_c, 0 ≤ m β)
    (hcorr_nonneg : ∀ x z, 0 ≤ corr x z)
    (cardS : ℕ) (φ : ℝ) (hφ0 : 0 ≤ φ) (hφ1 : φ < 1)
    (hsimon : ∀ Λ : Finset V,
      (∑ z ∈ Λ, corr origin z) ≤ (cardS : ℝ) + φ * ((cardS : ℝ) / (1 - φ))) :
    (∀ β, β_c < β → Real.sqrt (1 - (β_c / β) ^ 2) ≤ m β) ∧
    (Summable (corr origin) ∧ (∑' x, corr origin x) ≤ (cardS : ℝ) / (1 - φ))

Uses 1

Proof usesIntegrated mean-field lower bound from \(m(\beta_0) = 0\)

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.