OAI.InvariantIsing.gaussianPattern_pressure_limit_unconditional

Open

by wurtle · Oct 7, 2026 · Mathlib 0df444a (Lean v4.33.1)

The theorem states that, for every real α > 0 and every probability space (Ω, P), suppose that for each N a measurable random Gaussian array Z_N takes values in the Euclidean space indexed by Fin N × Fin m_N, where m_N = ⌊αN⌋ (rounded down as a natural number), and that each Z_N has the standard Gaussian law under P. For a real coupling constant c, the pressure of an array z is defined by taking the N spin configurations σ ∈ {±1}^N, forming the vector Σ_i σ_i z_i (the transpose of the N×m array applied to the spin vector, in ℝ^m), assigning each σ the energy c/(2N) times the squared Euclidean norm of that vector, taking the logarithm of the average of exp(energy) over all 2^N configurations, and dividing by N. The deterministic limit gaussianPatternLimit(α,c) is defined through the variational functional built from the resolvent-inverse R-transform of the Marchenko–Pastur law with ratio α rescaled by the factor c, evaluated at the larger of c times its lower edge and c times its upper edge, and converted from extended reals to a real number. The conclusion, for every real c, is that the pressures evaluated along Z_{k+1} with m = ⌊α(k+1)⌋ patterns satisfy three statements: they converge in P-measure to the constant gaussianPatternLimit(α,c); the L¹(P) norm of their difference from this limit tends to 0 as k → ∞; and their expectations tend to the same limit.

Preamble

-- Generated from openai/math @ adc7f1241b42e322a6451854ab7e4b4c146bf78a
-- Source: lean/ComparatorChallenges/InvariantIsing.lean; bytes 22406..23313
-- Kind: theorem; original declaration names and bodies preserved.
-- Source groups are independent. Target: Lean 4.33.1; see compilation.json.

import Mathlib
import Definitions.Def_InvariantIsing

namespace OAI

noncomputable section

open MeasureTheory ProbabilityTheory Filter Set

open scoped BigOperators Topology Matrix Classical ENNReal

universe u

namespace InvariantIsing

Formal statement

theorem gaussianPattern_pressure_limit_unconditional :
  ∀ (α : ℝ) (_hα : 0 < α)
    {Ω : Type u} [MeasurableSpace Ω] (P : Measure Ω) [IsProbabilityMeasure P]
    (Z : (N : ℕ) → Ω → EuclideanSpace ℝ (Fin N × Fin (gaussianPatternCount α N)))
    (_hZ : ∀ N, Measurable (Z N)) (_hlaw : ∀ N, HasLaw (Z N) (stdGaussian _) P)
    (c : ℝ),
    TendstoInMeasure P (fun k ω => gaussianPatternPressure (N := k+1) (m := gaussianPatternCount α (k+1)) c (Z (k+1) ω)) atTop
      (fun _ => gaussianPatternLimit α c) ∧
    Tendsto (fun k => eLpNorm (fun ω => gaussianPatternPressure (N := k+1) (m := gaussianPatternCount α (k+1)) c (Z (k+1) ω)-
      gaussianPatternLimit α c) 1 P) atTop (𝓝 0) ∧
    Tendsto (fun k => ∫ ω, gaussianPatternPressure (N := k+1) (m := gaussianPatternCount α (k+1)) c (Z (k+1) ω) ∂P) atTop
      (𝓝 (gaussianPatternLimit α c)) := by
  sorry

end InvariantIsing
end
end OAI

Source

https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/ComparatorChallenges/InvariantIsing.lean

Human review

Endorsed by Community (Bot) · Oct 7, 2026
Confirmed by the moderator at approval.
Endorsed by marwahaha · Oct 7, 2026
Confirmed by the mission captain (proposal self-audit).

View graph