ComparatorChallenges/InvariantIsing.lean

GitHub source file

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL
Lean4 Domain Explanation Language

Credit: OpenAI's pinned repository says an unreleased internal model produced the manuscripts and supporting proof artifacts. The collection builds on the mathematics community's accumulated problems, results, language, and formal libraries; each manuscript's BibTeX and bibliography are the authority for individual scholarly credit.

Project sources: Pinned openai/math documentation, Pinned formalization catalogue

80 declarations, 11 contain sorry, 0 declared as axioms

All-temperature invariant Ising pressure and its magnetic, random-spectral, ground-state, and Gaussian-pattern extensions.

  1. abbrev OAI.InvariantIsing.Spin line 14

    Also declared: OAI/Probability/InvariantIsing/Core/Model.lean:20 (same declaration text).

  2. def OAI.InvariantIsing.spinValue line 16

    Also declared: OAI/Probability/InvariantIsing/Core/Model.lean:23 (same declaration text).

  3. def OAI.InvariantIsing.logPartition line 18

    Also declared: OAI/Probability/InvariantIsing/Core/Model.lean:32 (same declaration text).

  4. def OAI.InvariantIsing.fieldEnergy line 21

    Also declared: OAI/Probability/InvariantIsing/Core/Model.lean:80 (same declaration text).

  5. abbrev OAI.InvariantIsing.Rotation line 24

    Also declared: OAI/Probability/InvariantIsing/Haar/Rotation.lean:20 (same declaration text).

  6. abbrev OAI.InvariantIsing.Orthogonal line 27

    Also declared: OAI/Probability/InvariantIsing/Haar/HaarDerivative.lean:19 (same declaration text).

  7. def OAI.InvariantIsing.spinVector line 29

    Also declared: OAI/Probability/InvariantIsing/Haar/Rotation.lean:23 (same declaration text).

  8. def OAI.InvariantIsing.rotatedEnergy line 32

    Also declared: OAI/Probability/InvariantIsing/Haar/Rotation.lean:40 (same declaration text).

  9. def OAI.InvariantIsing.rotatedPressure line 35

    Distinct definitions of this name: OAI/Probability/InvariantIsing/Haar/Rotation.lean:44 (same statement text; different proof or body). Qualify references as OAI.InvariantIsing.rotatedPressure@path.

  10. lemma OAI.InvariantIsing.orthogonal_mulVec_norm_sq line 41

    Also declared: OAI/Probability/InvariantIsing/Haar/MatrixRotation.lean:15 (same declaration text).

  11. def OAI.InvariantIsing.matrixRotation line 54

    Also declared: OAI/Probability/InvariantIsing/Haar/MatrixRotation.lean:29 (same declaration text).

  12. structure OAI.InvariantIsing.OverlapPath line 61

    Also declared: OAI/Probability/InvariantIsing/Core/Variational.lean:21 (same declaration text).

  13. instance OAI.InvariantIsing.(instance at line 67) line 67
  14. def OAI.InvariantIsing.pathMeasure line 69

    Distinct definitions of this name: OAI/Probability/InvariantIsing/Core/Variational.lean:29 (same statement text; different proof or body). Qualify references as OAI.InvariantIsing.pathMeasure@path.

  15. def OAI.InvariantIsing.deficit line 71

    Distinct definitions of this name: OAI/Probability/InvariantIsing/Core/Variational.lean:53 (same statement text; different proof or body). Qualify references as OAI.InvariantIsing.deficit@path.

  16. def OAI.InvariantIsing.gaussianOperator line 76

    Also declared: OAI/Probability/InvariantIsing/Fields/Field.lean:21 (same declaration text).

  17. structure OAI.InvariantIsing.FieldStep line 80

    Also declared: OAI/Probability/InvariantIsing/Fields/Field.lean:33 (same declaration text).

  18. def OAI.InvariantIsing.fieldFunction line 90

    Also declared: OAI/Probability/InvariantIsing/Fields/Field.lean:44 (same declaration text).

  19. def OAI.InvariantIsing.fieldIncrement line 94

    Also declared: OAI/Probability/InvariantIsing/Fields/Field.lean:49 (same declaration text).

  20. def OAI.InvariantIsing.fieldValue line 98

    Also declared: OAI/Probability/InvariantIsing/Fields/Field.lean:54 (same declaration text).

  21. def OAI.InvariantIsing.fieldPairing line 103

    Also declared: OAI/Probability/InvariantIsing/Fields/Field.lean:60 (same declaration text).

  22. def OAI.InvariantIsing.entropyFunctional line 106

    Also declared: OAI/Probability/InvariantIsing/Fields/Field.lean:64 (same declaration text).

  23. def OAI.InvariantIsing.spectralFunctional line 109

    Also declared: OAI/Probability/InvariantIsing/Fields/Field.lean:68 (same declaration text).

  24. def OAI.InvariantIsing.variationalFunctional line 112

    Also declared: OAI/Probability/InvariantIsing/Fields/Field.lean:72 (same declaration text).

  25. def OAI.InvariantIsing.measureResolvent line 115

    Also declared: OAI/Probability/InvariantIsing/Spectral/MeasureResolvent.lean:15 (same declaration text).

  26. def OAI.InvariantIsing.measureInverse line 117

    Also declared: OAI/Probability/InvariantIsing/Spectral/MeasureResolvent.lean:17 (same declaration text).

  27. def OAI.InvariantIsing.measureR line 120

    Also declared: OAI/Probability/InvariantIsing/Spectral/MeasureResolvent.lean:20 (same declaration text).

  28. def OAI.InvariantIsing.finiteSpectralMeasure line 123

    Distinct definitions of this name: OAI/Probability/InvariantIsing/Spectral/FiniteSpectralMeasure.lean:16 (different declaration text). Qualify references as OAI.InvariantIsing.finiteSpectralMeasure@path.

  29. theorem OAI.InvariantIsing.finiteSpectralMeasure_probability line 126

    Distinct definitions of this name: OAI/Probability/InvariantIsing/Spectral/FiniteSpectralMeasure.lean:19 (different declaration text). Qualify references as OAI.InvariantIsing.finiteSpectralMeasure_probability@path.

  30. lemma OAI.InvariantIsing.empiricalSpectralWeight_sum line 134

    Also declared: OAI/Probability/InvariantIsing/Spectral/EmpiricalSpectralLaw.lean:14 (same declaration text).

  31. def OAI.InvariantIsing.empiricalSpectralLaw line 139

    Also declared: OAI/Probability/InvariantIsing/Spectral/EmpiricalSpectralLaw.lean:19 (same declaration text).

  32. def OAI.InvariantIsing.spectralMinimum line 143

    Also declared: OAI/Probability/InvariantIsing/Spectral/SpectralExtremeLimits.lean:14 (same declaration text).

  33. def OAI.InvariantIsing.spectralMaximum line 146

    Also declared: OAI/Probability/InvariantIsing/Spectral/SpectralExtremeLimits.lean:17 (same declaration text).

  34. def OAI.InvariantIsing.magneticBiasObjective line 149

    Also declared: OAI/Probability/InvariantIsing/Magnetic/MagneticFieldMinimum.lean:16 (same declaration text).

  35. def OAI.InvariantIsing.constrainedFieldValue line 151

    Distinct definitions of this name: OAI/Probability/InvariantIsing/Magnetic/MagneticFieldMinimum.lean:20 (same statement text; different proof or body). Qualify references as OAI.InvariantIsing.constrainedFieldValue@path.

  36. def OAI.InvariantIsing.magneticGroupValue line 154

    Distinct definitions of this name: OAI/Probability/InvariantIsing/Magnetic/MagneticVariational.lean:14 (same statement text; different proof or body). Qualify references as OAI.InvariantIsing.magneticGroupValue@path.

  37. def OAI.InvariantIsing.magneticEntropyFunctional line 159

    Also declared: OAI/Probability/InvariantIsing/Magnetic/MagneticVariational.lean:17 (same declaration text).

  38. def OAI.InvariantIsing.magneticVariationalFunctional line 163

    Also declared: OAI/Probability/InvariantIsing/Magnetic/MagneticVariational.lean:21 (same declaration text).

  39. def OAI.InvariantIsing.RationalMagnetization line 166

    Also declared: OAI/Probability/InvariantIsing/Magnetic/MagneticVariational.lean:24 (same declaration text).

  40. def OAI.InvariantIsing.finiteMagneticFunctional line 168

    Also declared: OAI/Probability/InvariantIsing/Magnetic/MagneticVariational.lean:29 (same declaration text).

  41. def OAI.InvariantIsing.finiteIndexWeight line 173

    Distinct definitions of this name: OAI/Probability/InvariantIsing/Core/FiniteIndexDistribution.lean:15 (different declaration text). Qualify references as OAI.InvariantIsing.finiteIndexWeight@path.

  42. def OAI.InvariantIsing.simpleFieldIndex line 176

    Distinct definitions of this name: OAI/Probability/InvariantIsing/Fields/SimpleFieldData.lean:16 (different declaration text). Qualify references as OAI.InvariantIsing.simpleFieldIndex@path.

  43. def OAI.InvariantIsing.simpleFieldWeight line 179

    Distinct definitions of this name: OAI/Probability/InvariantIsing/Fields/SimpleFieldData.lean:22 (different declaration text). Qualify references as OAI.InvariantIsing.simpleFieldWeight@path.

  44. abbrev OAI.InvariantIsing.SimpleFieldPositive line 182

    Distinct definitions of this name: OAI/Probability/InvariantIsing/Fields/SimpleFieldData.lean:25 (different declaration text). Qualify references as OAI.InvariantIsing.SimpleFieldPositive@path.

  45. def OAI.InvariantIsing.simpleFieldValue line 185

    Distinct definitions of this name: OAI/Probability/InvariantIsing/Fields/SimpleFieldData.lean:45 (different declaration text). Qualify references as OAI.InvariantIsing.simpleFieldValue@path.

  46. def OAI.InvariantIsing.fieldSimpleApproximation line 190

    Also declared: OAI/Probability/InvariantIsing/Fields/FieldSimpleApproximation.lean:11 (same declaration text).

  47. def OAI.InvariantIsing.magneticFieldFunctional line 193

    Also declared: OAI/Probability/InvariantIsing/Magnetic/MagneticFieldExtension.lean:11 (same declaration text).

  48. structure OAI.InvariantIsing.FieldLawCoupling line 197

    Distinct definitions of this name: OAI/Probability/InvariantIsing/Fields/FieldWasserstein.lean:12 (same statement text; different proof or body). Qualify references as OAI.InvariantIsing.FieldLawCoupling@path.

  49. def OAI.InvariantIsing.FieldLawCoupling.cost line 202

    Distinct definitions of this name: OAI/Probability/InvariantIsing/Fields/FieldWasserstein.lean:21 (different declaration text). Qualify references as OAI.InvariantIsing.FieldLawCoupling.cost@path.

  50. def OAI.InvariantIsing.fieldWassersteinOne line 205

    Also declared: OAI/Probability/InvariantIsing/Fields/FieldWasserstein.lean:46 (same declaration text).

  51. def OAI.InvariantIsing.scaledSpectralLaw line 208

    Also declared: OAI/Probability/InvariantIsing/Spectral/ScaledSpectralLaw.lean:13 (same declaration text).

  52. def OAI.InvariantIsing.groundStateEnergy line 211

    Also declared: OAI/Probability/InvariantIsing/Pressure/GroundStateFinite.lean:14 (same declaration text).

  53. def OAI.InvariantIsing.thermalVariationalValue line 214

    Also declared: OAI/Probability/InvariantIsing/Pressure/GroundStateLimit.lean:16 (same declaration text).

  54. abbrev OAI.InvariantIsing.FieldSpectralData line 217

    Also declared: OAI/Probability/InvariantIsing/Pressure/RandomOrbitLaw.lean:13 (same declaration text).

  55. def OAI.InvariantIsing.dataPhysicalPressure line 219

    Also declared: OAI/Probability/InvariantIsing/Pressure/RandomOrbitLaw.lean:15 (same declaration text).

  56. def OAI.InvariantIsing.ConditionalFieldOrbitLaw line 222

    Distinct definitions of this name: OAI/Probability/InvariantIsing/Pressure/RandomOrbitLaw.lean:52 (same statement text; different proof or body). Qualify references as OAI.InvariantIsing.ConditionalFieldOrbitLaw@path.

  57. def OAI.InvariantIsing.spectralExcess line 228

    Distinct definitions of this name: OAI/Probability/InvariantIsing/Spectral/SpectralExcess.lean:13 (same statement text; different proof or body). Qualify references as OAI.InvariantIsing.spectralExcess@path.

  58. def OAI.InvariantIsing.gaussianPatternCount line 234

    Also declared: OAI/Probability/InvariantIsing/Gaussian/GaussianPatternPublishedInputs.lean:17 (same declaration text).

  59. def OAI.InvariantIsing.marchenkoPasturA line 236

    Also declared: OAI/Probability/InvariantIsing/Gaussian/GaussianPatternPublishedInputs.lean:18 (same declaration text).

  60. def OAI.InvariantIsing.marchenkoPasturB line 238

    Also declared: OAI/Probability/InvariantIsing/Gaussian/GaussianPatternPublishedInputs.lean:19 (same declaration text).

  61. def OAI.InvariantIsing.marchenkoPasturLower line 240

    Also declared: OAI/Probability/InvariantIsing/Gaussian/GaussianPatternPublishedInputs.lean:20 (same declaration text).

  62. def OAI.InvariantIsing.marchenkoPasturMeasure line 242

    Also declared: OAI/Probability/InvariantIsing/Gaussian/GaussianPatternPublishedInputs.lean:22 (same declaration text).

  63. def OAI.InvariantIsing.gaussianPatternLimit line 248

    Distinct definitions of this name: OAI/Probability/InvariantIsing/Gaussian/GaussianPatternPressureLimit.lean:15 (same statement text; different proof or body). Qualify references as OAI.InvariantIsing.gaussianPatternLimit@path.

  64. def OAI.InvariantIsing.gaussianPatternArray line 254

    Also declared: OAI/Probability/InvariantIsing/Gaussian/GaussianPatternModel.lean:13 (same declaration text).

  65. def OAI.InvariantIsing.gaussianPatternSum line 257

    Also declared: OAI/Probability/InvariantIsing/Gaussian/GaussianPatternModel.lean:20 (same declaration text).

  66. def OAI.InvariantIsing.gaussianPatternPressure line 261

    Distinct definitions of this name: OAI/Probability/InvariantIsing/Gaussian/GaussianPatternModel.lean:24 (same statement text; different proof or body). Qualify references as OAI.InvariantIsing.gaussianPatternPressure@path.

  67. def OAI.InvariantIsing.gaussianPatternGroundEnergy line 267

    Distinct definitions of this name: OAI/Probability/InvariantIsing/Gaussian/GaussianPatternGroundFinite.lean:13 (same statement text; different proof or body). Qualify references as OAI.InvariantIsing.gaussianPatternGroundEnergy@path.

  68. def OAI.InvariantIsing.gaussianPatternColumn line 274

    Also declared: OAI/Probability/InvariantIsing/Gaussian/GaussianPatternNorms.lean:14 (same declaration text).

  69. def OAI.InvariantIsing.gaussianPatternOperator line 277

    Also declared: OAI/Probability/InvariantIsing/Gaussian/GaussianPatternNorms.lean:23 (same declaration text).

  70. theorem OAI.InvariantIsing.limiting_pressure_of_extreme_limits_unconditional Challenge statement: All-temperature pressure of orthogonally invariant Ising spin glasses sorry line 282

    L4DEL explanation

    The formalization gives variational limits for orthogonally invariant Ising spin glasses whose eigenvectors have Haar law and whose empirical eigenvalue distributions converge to a compactly supported law with the stated control of extreme eigenvalues. The pressure converges both in expectation and almost surely to an explicit functional of the limiting spectral law. A version with external fields assumes convergence of their empirical laws in Wasserstein distance and gives the corresponding magnetic-field functional. The formalization also covers every positive temperature, a ground-state limit, random spectral data with the stated conditional Haar law, and Gaussian-pattern specializations. These hypotheses identify the invariant models to which the limits apply.

    1. This is an exact comparator target linked by the pinned repository's formalization note for this result.
    2. The repository's comparator configuration selects OAI.Probability.InvariantIsing.Unconditional as the released solution module checked against this declaration.

    Sources and attribution: Pinned Lean source (fd4aeeb2ee4f)

    Distinct definitions of this name: OAI/Probability/InvariantIsing/Unconditional.lean:27 (same statement text; different proof or body). Qualify references as OAI.InvariantIsing.limiting_pressure_of_extreme_limits_unconditional@path.

    theorem limiting_pressure_of_extreme_limits_unconditional :
  ∀ {Ω : Type*} [MeasurableSpace Ω] (P : Measure Ω) [IsProbabilityMeasure P]
    (U : (N : ℕ) → Ω → Orthogonal N) (_hU : ∀ N, Measurable (U N))
    (_hHaar : ∀ N, (P.map (U N)).IsMulRightInvariant)
    (eig : (N : ℕ) → Fin N → ℝ) (ν : ProbabilityMeasure ℝ) (a b : ℝ)
    (_hcompact : IsCompact (ν : Measure ℝ).support)
    (_hbound : (ν : Measure ℝ).support ⊆ Icc a b)
    (_ha : a∈(ν : Measure ℝ).support) (_hb : b∈(ν : Measure ℝ).support)
    (_hmin : Tendsto (fun k => spectralMinimum (eig (k+1))) atTop (𝓝 a))
    (_hmax : Tendsto (fun k => spectralMaximum (eig (k+1))) atTop (𝓝 b))
    (_hweak : Tendsto (fun k => empiricalSpectralLaw (Nat.succ_pos k) (eig (k+1)))
      atTop (𝓝 ν)),
…

    Mentions: OAI.InvariantIsing.Orthogonal, OAI.InvariantIsing.spectralMinimum, OAI.InvariantIsing.spectralMaximum, OAI.InvariantIsing.empiricalSpectralLaw

  71. theorem OAI.InvariantIsing.limiting_wasserstein_field_pressure_of_extreme_limits_unconditional Challenge statement: All-temperature pressure of orthogonally invariant Ising spin glasses sorry line 300

    L4DEL explanation

    The formalization gives variational limits for orthogonally invariant Ising spin glasses whose eigenvectors have Haar law and whose empirical eigenvalue distributions converge to a compactly supported law with the stated control of extreme eigenvalues. The pressure converges both in expectation and almost surely to an explicit functional of the limiting spectral law. A version with external fields assumes convergence of their empirical laws in Wasserstein distance and gives the corresponding magnetic-field functional. The formalization also covers every positive temperature, a ground-state limit, random spectral data with the stated conditional Haar law, and Gaussian-pattern specializations. These hypotheses identify the invariant models to which the limits apply.

    1. This is an exact comparator target linked by the pinned repository's formalization note for this result.
    2. The repository's comparator configuration selects OAI.Probability.InvariantIsing.Unconditional as the released solution module checked against this declaration.

    Sources and attribution: Pinned Lean source (fd4aeeb2ee4f)

    Distinct definitions of this name: OAI/Probability/InvariantIsing/Unconditional.lean:45 (same statement text; different proof or body). Qualify references as OAI.InvariantIsing.limiting_wasserstein_field_pressure_of_extreme_limits_unconditional@path.

    theorem limiting_wasserstein_field_pressure_of_extreme_limits_unconditional :
  ∀ {Ω : Type*} [MeasurableSpace Ω] (P : Measure Ω) [IsProbabilityMeasure P]
    (U : (N : ℕ) → Ω → Orthogonal N) (_hU : ∀ N, Measurable (U N))
    (_hHaar : ∀ N, (P.map (U N)).IsMulRightInvariant)
    (eig : (N : ℕ) → Fin N → ℝ) (ν : ProbabilityMeasure ℝ) (a b : ℝ)
    (_hcompact : IsCompact (ν : Measure ℝ).support)
    (_hbound : (ν : Measure ℝ).support ⊆ Icc a b)
    (_ha : a∈(ν : Measure ℝ).support) (_hb : b∈(ν : Measure ℝ).support)
    (_hmin : Tendsto (fun k => spectralMinimum (eig (k+1))) atTop (𝓝 a))
    (_hmax : Tendsto (fun k => spectralMaximum (eig (k+1))) atTop (𝓝 b))
    (_hweak : Tendsto (fun k => empiricalSpectralLaw (Nat.succ_pos k) (eig (k+1)))
      atTop (𝓝 ν))
…

    Mentions: OAI.InvariantIsing.Orthogonal, OAI.InvariantIsing.spectralMinimum, OAI.InvariantIsing.spectralMaximum, OAI.InvariantIsing.empiricalSpectralLaw

  72. theorem OAI.InvariantIsing.positive_temperature_pressure_unconditional Challenge statement: All-temperature pressure of orthogonally invariant Ising spin glasses sorry line 322

    L4DEL explanation

    The formalization gives variational limits for orthogonally invariant Ising spin glasses whose eigenvectors have Haar law and whose empirical eigenvalue distributions converge to a compactly supported law with the stated control of extreme eigenvalues. The pressure converges both in expectation and almost surely to an explicit functional of the limiting spectral law. A version with external fields assumes convergence of their empirical laws in Wasserstein distance and gives the corresponding magnetic-field functional. The formalization also covers every positive temperature, a ground-state limit, random spectral data with the stated conditional Haar law, and Gaussian-pattern specializations. These hypotheses identify the invariant models to which the limits apply.

    1. This is an exact comparator target linked by the pinned repository's formalization note for this result.
    2. The repository's comparator configuration selects OAI.Probability.InvariantIsing.Unconditional as the released solution module checked against this declaration.

    Sources and attribution: Pinned Lean source (fd4aeeb2ee4f)

    Distinct definitions of this name: OAI/Probability/InvariantIsing/Unconditional.lean:67 (same statement text; different proof or body). Qualify references as OAI.InvariantIsing.positive_temperature_pressure_unconditional@path.

    theorem positive_temperature_pressure_unconditional :
  ∀ {Ω : Type*} [MeasurableSpace Ω] (P : Measure Ω) [IsProbabilityMeasure P]
    (U : (N : ℕ) → Ω → Orthogonal N) (_hU : ∀ N, Measurable (U N))
    (_hHaar : ∀ N, (P.map (U N)).IsMulRightInvariant)
    (eig : (N : ℕ) → Fin N → ℝ) (ν : ProbabilityMeasure ℝ) (a b : ℝ)
    (_hbound : (ν : Measure ℝ).support ⊆ Icc a b)
    (_ha : a∈(ν : Measure ℝ).support) (_hb : b∈(ν : Measure ℝ).support)
    (_hno : ∀ ε : ℝ, 0 < ε → ∀ᶠ N in atTop, ∀ i, a-ε ≤ eig N i ∧ eig N i ≤ b+ε)
    (β : ℝ) (_hβ : 0 < β)
    (_hweak : Tendsto (fun k => empiricalSpectralLaw (Nat.succ_pos k) (eig (k+1)))
      atTop (𝓝 ν)),
    Tendsto (fun N => ∫ ω, rotatedPressure (fun i => β*eig N i) (matrixRotation (U N ω)⁻¹) (fun _ => 0) ∂P)
…

    Mentions: OAI.InvariantIsing.Orthogonal, OAI.InvariantIsing.empiricalSpectralLaw, OAI.InvariantIsing.matrixRotation

  73. theorem OAI.InvariantIsing.ground_state_limit_unconditional Challenge statement: All-temperature pressure of orthogonally invariant Ising spin glasses sorry line 339

    L4DEL explanation

    The formalization gives variational limits for orthogonally invariant Ising spin glasses whose eigenvectors have Haar law and whose empirical eigenvalue distributions converge to a compactly supported law with the stated control of extreme eigenvalues. The pressure converges both in expectation and almost surely to an explicit functional of the limiting spectral law. A version with external fields assumes convergence of their empirical laws in Wasserstein distance and gives the corresponding magnetic-field functional. The formalization also covers every positive temperature, a ground-state limit, random spectral data with the stated conditional Haar law, and Gaussian-pattern specializations. These hypotheses identify the invariant models to which the limits apply.

    1. This is an exact comparator target linked by the pinned repository's formalization note for this result.
    2. The repository's comparator configuration selects OAI.Probability.InvariantIsing.Unconditional as the released solution module checked against this declaration.

    Sources and attribution: Pinned Lean source (fd4aeeb2ee4f)

    Distinct definitions of this name: OAI/Probability/InvariantIsing/Unconditional.lean:84 (same statement text; different proof or body). Qualify references as OAI.InvariantIsing.ground_state_limit_unconditional@path.

    theorem ground_state_limit_unconditional :
  ∀ {Ω : Type*} [MeasurableSpace Ω] (P : Measure Ω) [IsProbabilityMeasure P]
    (U : (N : ℕ) → Ω → Orthogonal N) (_hU : ∀ N, Measurable (U N))
    (_hHaar : ∀ N, (P.map (U N)).IsMulRightInvariant)
    (eig : (N : ℕ) → Fin N → ℝ) (ν : ProbabilityMeasure ℝ) (a b : ℝ)
    (_hbound : (ν : Measure ℝ).support ⊆ Icc a b)
    (_ha : a∈(ν : Measure ℝ).support) (_hb : b∈(ν : Measure ℝ).support)
    (_hno : ∀ ε : ℝ, 0 < ε → ∀ᶠ N in atTop, ∀ i, a-ε ≤ eig N i ∧ eig N i ≤ b+ε)
    (_hweak : Tendsto (fun k => empiricalSpectralLaw (Nat.succ_pos k) (eig (k+1)))
      atTop (𝓝 ν)),
    ∃ M : ℝ,
      Tendsto (fun N => ∫ ω, groundStateEnergy (eig N) (matrixRotation (U N ω)⁻¹) ∂P)
…

    Mentions: OAI.InvariantIsing.Orthogonal, OAI.InvariantIsing.empiricalSpectralLaw, OAI.InvariantIsing.groundStateEnergy, OAI.InvariantIsing.matrixRotation

  74. theorem OAI.InvariantIsing.random_pressure_tendsto_in_measure_unconditional Challenge statement: All-temperature pressure of orthogonally invariant Ising spin glasses sorry line 357

    L4DEL explanation

    The formalization gives variational limits for orthogonally invariant Ising spin glasses whose eigenvectors have Haar law and whose empirical eigenvalue distributions converge to a compactly supported law with the stated control of extreme eigenvalues. The pressure converges both in expectation and almost surely to an explicit functional of the limiting spectral law. A version with external fields assumes convergence of their empirical laws in Wasserstein distance and gives the corresponding magnetic-field functional. The formalization also covers every positive temperature, a ground-state limit, random spectral data with the stated conditional Haar law, and Gaussian-pattern specializations. These hypotheses identify the invariant models to which the limits apply.

    1. This is an exact comparator target linked by the pinned repository's formalization note for this result.
    2. The repository's comparator configuration selects OAI.Probability.InvariantIsing.Unconditional as the released solution module checked against this declaration.

    Sources and attribution: Pinned Lean source (fd4aeeb2ee4f)

    Distinct definitions of this name: OAI/Probability/InvariantIsing/Unconditional.lean:102 (same statement text; different proof or body). Qualify references as OAI.InvariantIsing.random_pressure_tendsto_in_measure_unconditional@path.

    theorem random_pressure_tendsto_in_measure_unconditional
    {Ω : Type*} [MeasurableSpace Ω] (P : Measure Ω) [IsProbabilityMeasure P]
    (eig : (N : ℕ) → Ω → Fin N → ℝ) (Y : ℕ → Ω → ℝ)
    (heig : ∀ N, Measurable (eig N)) (hY : ∀ N, Measurable (Y N))
    (H : (N : ℕ) → Measure (Orthogonal N)) [∀ N, IsProbabilityMeasure (H N)]
    [∀ N, (H N).IsMulRightInvariant]
    (hlaw : ∀ N, ConditionalFieldOrbitLaw P (fun ω => (eig N ω,fun _ => 0)) (Y N) (H N))
    (ν : ProbabilityMeasure ℝ) (a b : ℝ)
    (hcompact : IsCompact (ν : Measure ℝ).support)
    (hbound : (ν : Measure ℝ).support ⊆ Icc a b)
    (ha : a∈(ν : Measure ℝ).support) (hb : b∈(ν : Measure ℝ).support)
    (hweak : TendstoInMeasure P (fun k ω => LevyProkhorov.ofMeasure
…

    Mentions: OAI.InvariantIsing.Orthogonal

  75. theorem OAI.InvariantIsing.random_pressure_limit_unconditional Challenge statement: All-temperature pressure of orthogonally invariant Ising spin glasses sorry line 377

    L4DEL explanation

    The formalization gives variational limits for orthogonally invariant Ising spin glasses whose eigenvectors have Haar law and whose empirical eigenvalue distributions converge to a compactly supported law with the stated control of extreme eigenvalues. The pressure converges both in expectation and almost surely to an explicit functional of the limiting spectral law. A version with external fields assumes convergence of their empirical laws in Wasserstein distance and gives the corresponding magnetic-field functional. The formalization also covers every positive temperature, a ground-state limit, random spectral data with the stated conditional Haar law, and Gaussian-pattern specializations. These hypotheses identify the invariant models to which the limits apply.

    1. This is an exact comparator target linked by the pinned repository's formalization note for this result.
    2. The repository's comparator configuration selects OAI.Probability.InvariantIsing.Unconditional as the released solution module checked against this declaration.

    Sources and attribution: Pinned Lean source (fd4aeeb2ee4f)

    Distinct definitions of this name: OAI/Probability/InvariantIsing/Unconditional.lean:124 (same statement text; different proof or body). Qualify references as OAI.InvariantIsing.random_pressure_limit_unconditional@path.

    theorem random_pressure_limit_unconditional :
  ∀ {Ω : Type*} [MeasurableSpace Ω] (P : Measure Ω) [IsProbabilityMeasure P]
    (eig : (N : ℕ) → Ω → Fin N → ℝ) (Y : ℕ → Ω → ℝ)
    (_heig : ∀ N, Measurable (eig N)) (_hY : ∀ N, Measurable (Y N))
    (H : (N : ℕ) → Measure (Orthogonal N)) [∀ N, IsProbabilityMeasure (H N)]
    [∀ N, (H N).IsMulRightInvariant]
    (_hlaw : ∀ N, ConditionalFieldOrbitLaw P (fun ω => (eig N ω,fun _ => 0)) (Y N) (H N))
    (ν : ProbabilityMeasure ℝ) (a b : ℝ)
    (_hcompact : IsCompact (ν : Measure ℝ).support)
    (_hbound : (ν : Measure ℝ).support ⊆ Icc a b)
    (_ha : a∈(ν : Measure ℝ).support) (_hb : b∈(ν : Measure ℝ).support)
    (_hweak : TendstoInMeasure P (fun k ω => LevyProkhorov.ofMeasure
…

    Mentions: OAI.InvariantIsing.Orthogonal

  76. theorem OAI.InvariantIsing.random_pressure_tendsto_ae_unconditional Challenge statement: All-temperature pressure of orthogonally invariant Ising spin glasses sorry line 402

    L4DEL explanation

    The formalization gives variational limits for orthogonally invariant Ising spin glasses whose eigenvectors have Haar law and whose empirical eigenvalue distributions converge to a compactly supported law with the stated control of extreme eigenvalues. The pressure converges both in expectation and almost surely to an explicit functional of the limiting spectral law. A version with external fields assumes convergence of their empirical laws in Wasserstein distance and gives the corresponding magnetic-field functional. The formalization also covers every positive temperature, a ground-state limit, random spectral data with the stated conditional Haar law, and Gaussian-pattern specializations. These hypotheses identify the invariant models to which the limits apply.

    1. This is an exact comparator target linked by the pinned repository's formalization note for this result.
    2. The repository's comparator configuration selects OAI.Probability.InvariantIsing.Unconditional as the released solution module checked against this declaration.

    Sources and attribution: Pinned Lean source (fd4aeeb2ee4f)

    Distinct definitions of this name: OAI/Probability/InvariantIsing/Unconditional.lean:149 (same statement text; different proof or body). Qualify references as OAI.InvariantIsing.random_pressure_tendsto_ae_unconditional@path.

    theorem random_pressure_tendsto_ae_unconditional :
  ∀ {Ω : Type*} [MeasurableSpace Ω] (P : Measure Ω) [IsProbabilityMeasure P]
    (eig : (N : ℕ) → Ω → Fin N → ℝ) (Y : ℕ → Ω → ℝ)
    (_heig : ∀ N, Measurable (eig N)) (_hY : ∀ N, Measurable (Y N))
    (H : (N : ℕ) → Measure (Orthogonal N)) [∀ N, IsProbabilityMeasure (H N)]
    [∀ N, (H N).IsMulRightInvariant]
    (_hlaw : ∀ N, ConditionalFieldOrbitLaw P (fun ω => (eig N ω,fun _ => 0)) (Y N) (H N))
    (ν : ProbabilityMeasure ℝ) (a b : ℝ)
    (_hcompact : IsCompact (ν : Measure ℝ).support)
    (_hbound : (ν : Measure ℝ).support ⊆ Icc a b)
    (_ha : a∈(ν : Measure ℝ).support) (_hb : b∈(ν : Measure ℝ).support)
    (_hno : ∀ᵐ ω ∂P, ∀ ε : ℝ, 0 < ε → ∀ᶠ N in atTop,
…

    Mentions: OAI.InvariantIsing.Orthogonal

  77. theorem OAI.InvariantIsing.random_field_pressure_tendsto_ae_unconditional Challenge statement: All-temperature pressure of orthogonally invariant Ising spin glasses sorry line 421

    L4DEL explanation

    The formalization gives variational limits for orthogonally invariant Ising spin glasses whose eigenvectors have Haar law and whose empirical eigenvalue distributions converge to a compactly supported law with the stated control of extreme eigenvalues. The pressure converges both in expectation and almost surely to an explicit functional of the limiting spectral law. A version with external fields assumes convergence of their empirical laws in Wasserstein distance and gives the corresponding magnetic-field functional. The formalization also covers every positive temperature, a ground-state limit, random spectral data with the stated conditional Haar law, and Gaussian-pattern specializations. These hypotheses identify the invariant models to which the limits apply.

    1. This is an exact comparator target linked by the pinned repository's formalization note for this result.
    2. The repository's comparator configuration selects OAI.Probability.InvariantIsing.Unconditional as the released solution module checked against this declaration.

    Sources and attribution: Pinned Lean source (fd4aeeb2ee4f)

    Distinct definitions of this name: OAI/Probability/InvariantIsing/Unconditional.lean:168 (same statement text; different proof or body). Qualify references as OAI.InvariantIsing.random_field_pressure_tendsto_ae_unconditional@path.

    theorem random_field_pressure_tendsto_ae_unconditional :
  ∀ {Ω : Type*} [MeasurableSpace Ω] (P : Measure Ω) [IsProbabilityMeasure P]
    (d : (N : ℕ) → Ω → FieldSpectralData N) (Y : ℕ → Ω → ℝ)
    (_hd : ∀ N, Measurable (d N)) (_hY : ∀ N, Measurable (Y N))
    (H : (N : ℕ) → Measure (Orthogonal N)) [∀ N, IsProbabilityMeasure (H N)]
    [∀ N, (H N).IsMulRightInvariant]
    (_hlaw : ∀ N, ConditionalFieldOrbitLaw P (d N) (Y N) (H N))
    (ν : ProbabilityMeasure ℝ) (a b : ℝ)
    (_hcompact : IsCompact (ν : Measure ℝ).support)
    (_hbound : (ν : Measure ℝ).support ⊆ Icc a b)
    (_ha : a∈(ν : Measure ℝ).support) (_hb : b∈(ν : Measure ℝ).support)
    (_hno : ∀ᵐ ω ∂P, ∀ ε : ℝ, 0 < ε → ∀ᶠ N in atTop,
…

    Mentions: OAI.InvariantIsing.FieldSpectralData, OAI.InvariantIsing.Orthogonal

  78. theorem OAI.InvariantIsing.gaussianPattern_pressure_limit_unconditional Challenge statement: All-temperature pressure of orthogonally invariant Ising spin glasses sorry line 443

    L4DEL explanation

    The formalization gives variational limits for orthogonally invariant Ising spin glasses whose eigenvectors have Haar law and whose empirical eigenvalue distributions converge to a compactly supported law with the stated control of extreme eigenvalues. The pressure converges both in expectation and almost surely to an explicit functional of the limiting spectral law. A version with external fields assumes convergence of their empirical laws in Wasserstein distance and gives the corresponding magnetic-field functional. The formalization also covers every positive temperature, a ground-state limit, random spectral data with the stated conditional Haar law, and Gaussian-pattern specializations. These hypotheses identify the invariant models to which the limits apply.

    1. This is an exact comparator target linked by the pinned repository's formalization note for this result.
    2. The repository's comparator configuration selects OAI.Probability.InvariantIsing.Unconditional as the released solution module checked against this declaration.

    Sources and attribution: Pinned Lean source (fd4aeeb2ee4f)

    Distinct definitions of this name: OAI/Probability/InvariantIsing/Unconditional.lean:190 (same statement text; different proof or body). Qualify references as OAI.InvariantIsing.gaussianPattern_pressure_limit_unconditional@path.

    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
…

    Mentions: OAI.InvariantIsing.gaussianPatternCount

  79. theorem OAI.InvariantIsing.gaussianPattern_ground_limit_unconditional Challenge statement: All-temperature pressure of orthogonally invariant Ising spin glasses sorry line 457

    L4DEL explanation

    The formalization gives variational limits for orthogonally invariant Ising spin glasses whose eigenvectors have Haar law and whose empirical eigenvalue distributions converge to a compactly supported law with the stated control of extreme eigenvalues. The pressure converges both in expectation and almost surely to an explicit functional of the limiting spectral law. A version with external fields assumes convergence of their empirical laws in Wasserstein distance and gives the corresponding magnetic-field functional. The formalization also covers every positive temperature, a ground-state limit, random spectral data with the stated conditional Haar law, and Gaussian-pattern specializations. These hypotheses identify the invariant models to which the limits apply.

    1. This is an exact comparator target linked by the pinned repository's formalization note for this result.
    2. The repository's comparator configuration selects OAI.Probability.InvariantIsing.Unconditional as the released solution module checked against this declaration.

    Sources and attribution: Pinned Lean source (fd4aeeb2ee4f)

    Distinct definitions of this name: OAI/Probability/InvariantIsing/Unconditional.lean:204 (same statement text; different proof or body). Qualify references as OAI.InvariantIsing.gaussianPattern_ground_limit_unconditional@path.

    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
…

    Mentions: OAI.InvariantIsing.gaussianPatternCount

  80. theorem OAI.InvariantIsing.gaussianPattern_norm_limits_unconditional Challenge statement: All-temperature pressure of orthogonally invariant Ising spin glasses sorry line 471

    L4DEL explanation

    The formalization gives variational limits for orthogonally invariant Ising spin glasses whose eigenvectors have Haar law and whose empirical eigenvalue distributions converge to a compactly supported law with the stated control of extreme eigenvalues. The pressure converges both in expectation and almost surely to an explicit functional of the limiting spectral law. A version with external fields assumes convergence of their empirical laws in Wasserstein distance and gives the corresponding magnetic-field functional. The formalization also covers every positive temperature, a ground-state limit, random spectral data with the stated conditional Haar law, and Gaussian-pattern specializations. These hypotheses identify the invariant models to which the limits apply.

    1. This is an exact comparator target linked by the pinned repository's formalization note for this result.
    2. The repository's comparator configuration selects OAI.Probability.InvariantIsing.Unconditional as the released solution module checked against this declaration.

    Sources and attribution: Pinned Lean source (fd4aeeb2ee4f)

    Distinct definitions of this name: OAI/Probability/InvariantIsing/Unconditional.lean:218 (same statement text; different proof or body). Qualify references as OAI.InvariantIsing.gaussianPattern_norm_limits_unconditional@path.

    theorem gaussianPattern_norm_limits_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),
    ∃ eplus eminus : ℝ, 0 ≤ eplus ∧ eminus ≤ 0 ∧
      Tendsto (fun β => gaussianPatternLimit α β/β) atTop (𝓝 eplus) ∧
      Tendsto (fun β => gaussianPatternLimit α (-β)/β) atTop (𝓝 eminus) ∧
      (TendstoInMeasure P (fun k ω => ‖gaussianPatternOperator (Z (k+1) ω)‖/(k+1)) atTop
        (fun _ => Real.sqrt (2*eplus)) ∧
       Tendsto (fun k => eLpNorm (fun ω => ‖gaussianPatternOperator (Z (k+1) ω)‖/(k+1)-
        Real.sqrt (2*eplus)) 1 P) atTop (𝓝 0)) ∧
…

    Mentions: OAI.InvariantIsing.gaussianPatternCount, OAI.InvariantIsing.gaussianPatternOperator