OAI.ZeroTemperatureSK.full_support
OpenThe theorem states that, for any probability space carrying a real Brownian motion B (a BrownianSystem W) and any order parameter γ on [0,1), if γ minimizes the Parisi functional over all order parameters, then a five-part full-support conclusion holds. An order parameter γ:[0,1)→ℝ is nonnegative, monotone, right-continuous and integrable (extended by zero outside [0,1)). For a time t and position x, the value is the supremum, over controls α progressive for the filtration generated by the Brownian increments after t and bounded by 1 in absolute value, of the expected payoff |x + B₁ − B_t + ∫_t^1 γ(s)α(s−t)ds| − ½∫_t^1 γ(s)α(s−t)²ds. The gradient and curvature are its first and second derivatives in x, and the Parisi functional is value at (0,0) minus ½∫_0^1 tγ(t)dt. Being a minimizer means the functional at γ is at most its value at every order parameter η. The conclusion says: (1) there is a measure μ on [0,1) with μ((−∞,t]) = γ(t) for every t in [0,1); (2) there is a diffusion X, a process progressive for the Brownian filtration that almost surely is continuous on [0,1], starts at 0, and satisfies X_t = B_t + ∫_0^t γ(s)·gradient(s,X_s)ds; (3) every such measure μ has full support, equal to all of [0,1); (4) γ is strictly increasing, γ(a)<γ(b) whenever a<b; and (5) for every such diffusion X and every t in [0,1), the expected square of the gradient at X_t equals t, and the expected square of the curvature at X_t equals 1.
-- Generated from openai/math @ adc7f1241b42e322a6451854ab7e4b4c146bf78a
-- Source: lean/ComparatorChallenges/SKFullSupport.lean; bytes 3616..3755
-- 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_SKFullSupport
namespace OAI
open MeasureTheory ProbabilityTheory Set Filter
open scoped ENNReal NNReal Topology
noncomputable section
namespace ZeroTemperatureSK
variable {Ω : Type*} [MeasurableSpace Ω]
theorem full_support (W : BrownianSystem Ω) (γ : OrderParameter)
(hmin : IsMinimizer W γ) : FullSupportConclusion W γ := by
sorry
end ZeroTemperatureSK
end
end OAI
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.