OAI.SphericalPerceptronFreeEnergy.main
OpenThe theorem states that, for a probability measure P on continuous paths ℝ≥0→ℝ under which the evaluation process is a real Brownian motion, and for parameters α>0, β>0 and a bounded continuous function φ:ℝ→ℝ, there is a real number p with three properties. First, the variational value equals p (as an extended real). That value is the infimum over all trials m of α times the control value of βφ at m, plus the entropy of m. A trial is a nondecreasing measurable function m:[0,1]→[0,1]. Its entropy is one half of the integral over t of 1/∫ₜ¹ m(s)ds minus 1/(1−t), taken in [0,∞]. The control value of f at m is the supremum, over progressively measurable controls v with finite cost E∫ m(t)v(t)²dt, of E f(B₁+∫₀¹ m(t)v(t)dt) minus half that cost. Second, the expected spherical-perceptron pressure E[pressure(N+1)] converges to p as N→∞. For dimension n, pressure is (1/n) log ∫ exp(β Σₐ φ(⟨gₐ,x⟩/√n)) dx, with x uniform on the sphere of radius √n in ℝⁿ. The gₐ are the rows of a pattern matrix with ⌊αn⌋ rows and n i.i.d. standard Gaussian entries per row. Third, the pressure concentrates: for every ε>0, the Gaussian probability that |pressure(N+1)−p|>ε tends to 0 as N→∞.
-- Generated from openai/math @ adc7f1241b42e322a6451854ab7e4b4c146bf78a -- Source: lean/ComparatorChallenges/PerceptronFreeEnergy.lean; bytes 3753..4247 -- 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_PerceptronFreeEnergy namespace OAI noncomputable section open MeasureTheory ProbabilityTheory Filter Set open scoped ENNReal NNReal Topology BigOperators BoundedContinuousFunction namespace SphericalPerceptronFreeEnergy
theorem main (P : Measure BrownianPath) [IsProbabilityMeasure P]
(hB : IsBrownianReal brownianEval P)
(α β : ℝ) (hα : 0 < α) (hβ : 0 < β) (φ : ℝ →ᵇ ℝ) :
∃ p : ℝ, variationalValue P α β φ = (p : EReal) ∧
Tendsto (fun N : ℕ => expectedPressure α β φ (N + 1)) atTop (𝓝 p) ∧
∀ ε : ℝ, 0 < ε →
Tendsto (fun N : ℕ => patternLaw α (N + 1)
{g | ε < |pressure α β φ (N + 1) g - p|}) atTop (𝓝 0) := by
sorry
end SphericalPerceptronFreeEnergy
end
end OAI
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.