SKFullSupport
DefinitionWithin the namespace ZeroTemperatureSK, Time is the interval [0,1), and extend(γ) extends a function on Time to all reals by zero outside [0,1). An OrderParameter is a function γ on [0,1) that is nonnegative, monotone, right-continuous at every point, and whose zero extension is Lebesgue integrable. A BrownianSystem on a measurable space Ω consists of a probability measure on Ω together with a real process B indexed by nonnegative reals, with each B_t measurable, satisfying Mathlib's IsBrownianReal with respect to that measure. For time t, incrementFiltration is the natural filtration generated by the shifted increments s ↦ B_{t+s} − B_t, and a Control at time t is a process α indexed by nonnegative reals that is progressively measurable for this filtration and satisfies |α_s(ω)| ≤ 1 everywhere. The controlPayoff at (t,x) for a control α is |x + B_1 − B_t + ∫t^1 γ(s) α{s−t} ds| − (1/2)∫t^1 γ(s) α{s−t}² ds, with γ extended by zero. The value(t,x) is the supremum (a real sSup) over controls of the expectation of this payoff under the Brownian law. The gradient and curvature are the first and second derivatives of the value in x, taken with Lean's deriv, which is zero where a derivative fails to exist. The parisi functional is value(0,0) − (1/2)∫_0^1 t γ(t) dt, and IsMinimizer γ means parisi(γ) ≤ parisi(η) for every order parameter η. IsStieltjesMeasure γ μ says a measure μ on [0,1) satisfies μ((−∞,t]) = γ(t) for every t in [0,1). IsDiffusion X says X is progressively measurable for the natural filtration of B and, for almost every ω, X is continuous on [0,1], X_0 = 0, and X_t = B_t + ∫_0^t γ(s) · gradient(s, X_s) ds for all t in [0,1]. squareMoment is the expectation of gradient(t, X_t)². FullSupportConclusion is a defined proposition, not a proved theorem, asserting five things for given W and γ: some Stieltjes measure for γ exists; some diffusion exists; every Stieltjes measure for γ has support equal to all of [0,1); γ is strictly increasing on [0,1); and for every diffusion X and every t in [0,1), squareMoment equals t and the expectation of curvature(t, X_t)² equals 1. Notably, the conclusion does not assume γ is a minimizer.
-- Generated from openai/math @ adc7f1241b42e322a6451854ab7e4b4c146bf78a
-- Source: lean/ComparatorChallenges/SKFullSupport.lean; bytes 16..3616
-- Kind: block; original declaration names and bodies preserved.
-- Source groups are independent. Target: Lean 4.33.1; see compilation.json.
import Mathlib
namespace OAI
open MeasureTheory ProbabilityTheory Set Filter
open scoped ENNReal NNReal Topology
noncomputable section
namespace ZeroTemperatureSK
abbrev Time := Set.Ico (0 : ℝ) 1
def extend (γ : Time → ℝ) (t : ℝ) : ℝ :=
if ht : t ∈ Set.Ico (0 : ℝ) 1 then γ ⟨t, ht⟩ else 0
structure OrderParameter where
val : Time → ℝ
nonneg : ∀ t, 0 ≤ val t
monotone : Monotone val
right_continuous : ∀ t, ContinuousWithinAt val (Set.Ici t) t
integrable : Integrable (extend val)
structure BrownianSystem (Ω : Type*) [MeasurableSpace Ω] where
law : Measure Ω
isProbability : IsProbabilityMeasure law
B : ℝ≥0 → Ω → ℝ
measurable : ∀ t, Measurable (B t)
brownian : IsBrownianReal B law
variable {Ω : Type*} [MeasurableSpace Ω]
def incrementFiltration (W : BrownianSystem Ω) (t : ℝ≥0) :
Filtration ℝ≥0 ‹MeasurableSpace Ω› :=
Filtration.natural (fun s ω => W.B (t + s) ω - W.B t ω)
(fun s => ((W.measurable (t + s)).sub (W.measurable t)).stronglyMeasurable)
structure Control (W : BrownianSystem Ω) (t : ℝ≥0) where
val : ℝ≥0 → Ω → ℝ
progressive : IsProgressive (incrementFiltration W t) val
bound : ∀ s ω, |val s ω| ≤ 1
def controlPayoff (W : BrownianSystem Ω) (γ : OrderParameter) (t x : ℝ)
(α : Control W (Real.toNNReal t)) (ω : Ω) : ℝ :=
|x + W.B 1 ω - W.B (Real.toNNReal t) ω +
∫ s in t..1, extend γ.val s * α.val (Real.toNNReal (s - t)) ω| -
(1 / 2 : ℝ) * ∫ s in t..1, extend γ.val s * (α.val (Real.toNNReal (s - t)) ω)^2
def value (W : BrownianSystem Ω) (γ : OrderParameter) (t x : ℝ) : ℝ :=
sSup (Set.range (fun α : Control W (Real.toNNReal t) =>
∫ ω, controlPayoff W γ t x α ω ∂W.law))
def gradient (W : BrownianSystem Ω) (γ : OrderParameter) (t x : ℝ) : ℝ :=
deriv (value W γ t) x
def curvature (W : BrownianSystem Ω) (γ : OrderParameter) (t x : ℝ) : ℝ :=
deriv (gradient W γ t) x
def parisi (W : BrownianSystem Ω) (γ : OrderParameter) : ℝ :=
value W γ 0 0 - (1 / 2 : ℝ) * ∫ t in (0 : ℝ)..1, t * extend γ.val t
def IsMinimizer (W : BrownianSystem Ω) (γ : OrderParameter) : Prop :=
∀ η : OrderParameter, parisi W γ ≤ parisi W η
def IsStieltjesMeasure (γ : OrderParameter) (μ : Measure Time) : Prop :=
∀ t : Time, μ (Set.Iic t) = ENNReal.ofReal (γ.val t)
def IsDiffusion (W : BrownianSystem Ω) (γ : OrderParameter)
(X : ℝ≥0 → Ω → ℝ) : Prop :=
IsProgressive (Filtration.natural W.B (fun t => (W.measurable t).stronglyMeasurable)) X ∧
(∀ᵐ ω ∂W.law, ContinuousOn (fun t : ℝ => X (Real.toNNReal t) ω) (Set.Icc 0 1) ∧
X 0 ω = 0 ∧ ∀ t ∈ Set.Icc (0 : ℝ) 1,
X (Real.toNNReal t) ω = W.B (Real.toNNReal t) ω +
∫ s in (0 : ℝ)..t, extend γ.val s *
gradient W γ s (X (Real.toNNReal s) ω))
def squareMoment (W : BrownianSystem Ω) (γ : OrderParameter)
(X : ℝ≥0 → Ω → ℝ) (t : ℝ) : ℝ :=
∫ ω, (gradient W γ t (X (Real.toNNReal t) ω))^2 ∂W.law
def FullSupportConclusion (W : BrownianSystem Ω) (γ : OrderParameter) : Prop :=
(∃ μ : Measure Time, IsStieltjesMeasure γ μ) ∧
(∃ X : ℝ≥0 → Ω → ℝ, IsDiffusion W γ X) ∧
(∀ μ : Measure Time, IsStieltjesMeasure γ μ → μ.support = Set.univ) ∧
(∀ a b : Time, a < b → γ.val a < γ.val b) ∧
∀ X : ℝ≥0 → Ω → ℝ, IsDiffusion W γ X → ∀ t : Time,
squareMoment W γ X t = (t : ℝ) ∧
(∫ ω, (curvature W γ t (X (Real.toNNReal t) ω))^2 ∂W.law) = 1
end ZeroTemperatureSK
end
end OAI
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.