Continuous Functionals of Continuous Adapted Processes Are Progressive
ProvedItoLemma.continuous_adapted_composition_progressiveadapted-processito-lemmaprogressive-measurabilitystochastic-calculus
If Y is a continuous-path adapted process taking values in R² and φ is a continuous map from R² to R, then the scalar process φ(Y_t) is progressively measurable relative to the same filtration. This provides the progressive-measurability hypothesis for state-dependent coefficients used in the Itô formula and product rule.
Preamble
import Definitions.Def_KLSModular_LevyStochCalc_Brownian_VectorItoVersionExists open MeasureTheory ProbabilityTheory LevyStochCalc open Filter Topology universe u
Formal statement
theorem ItoLemma.continuous_adapted_composition_progressive
{Ω : Type u} [MeasurableSpace Ω]
{ℱ : Filtration ℝ ‹MeasurableSpace Ω›}
{Y : ℝ → Ω → (Fin 2 → ℝ)}
(hYc : ∀ ω, Continuous fun t => Y t ω)
(hYa : ∀ t, Measurable[ℱ t] (Y t))
{φ : (Fin 2 → ℝ) → ℝ} (hφ : Continuous φ) :
Probability.ProgressivelyMeasurable ℱ (fun ω s => φ (Y s ω)) := by sorrySource
Reusable extraction of the accepted lemma S66.prog_comp in the full Itô chain-rule proof, accepted Prove2Me submission e4199398-3f38-4045-8e68-46254a555325. Uses the accepted progressivelyMeasurable_of_rightContinuous result.