OAI.InvariantIsing.gaussianPattern_ground_limit_unconditional

Open

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

The theorem states that, for every real α>0, every probability space (Ω,P), and every sequence of measurable random vectors Z_N on Ω, N=0,1,2,..., each with the standard Gaussian law on Euclidean space indexed by Fin N × Fin m_N, where m_N=⌊αN⌋ is the pattern count, and for every real ε, there exists a real number e with four properties. Reading Z_{k+1}(ω) as an (k+1)×m_{k+1} Gaussian array and a spin configuration σ∈{±1}^{k+1} as acting on it by the transpose, let the ground energy gaussianPatternGroundEnergy ε be (1/N) times the maximum over σ of (ε/(2N))·‖Zᵀσ‖², with N=k+1. Then this ground energy, as k→∞, converges in probability to the constant e; its L¹(P) distance to e tends to 0; its expectation tends to e; and, in addition, gaussianPatternLimit α (εβ)/β tends to e as β→∞, where gaussianPatternLimit α c is the real value of the variational functional applied to the pushforward of the Marchenko–Pastur measure of parameter α under x↦cx, with the associated measureR parameter max(c·lower edge, c·upper edge).

Preamble

-- Generated from openai/math @ adc7f1241b42e322a6451854ab7e4b4c146bf78a
-- Source: lean/ComparatorChallenges/InvariantIsing.lean; bytes 23315..24110
-- 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_ground_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)
    (ε : ℝ),
    ∃ e : ℝ,
      TendstoInMeasure P (fun k ω => gaussianPatternGroundEnergy ε (Z (k+1) ω)) atTop (fun _ => e) ∧
      Tendsto (fun k => eLpNorm (fun ω => gaussianPatternGroundEnergy ε (Z (k+1) ω)-e) 1 P)
        atTop (𝓝 0) ∧
      Tendsto (fun k => ∫ ω, gaussianPatternGroundEnergy ε (Z (k+1) ω) ∂P) atTop (𝓝 e) ∧
      Tendsto (fun β => gaussianPatternLimit α (ε*β)/β) atTop (𝓝 e) := 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