progMeasurable_of_continuous — Mathlib

English

A continuous and adapted process u is progressive measurable.

Русский

Плавный и адаптированный процесс u является прогрессивно измеримым.

LaTeX

$$$\\mathrm{Adapted}(f,u) \\land \\forall \\omega\\,\\mathrm{Continuous}(i \\mapsto u(i,\\omega)) \\Rightarrow \\mathrm{ProgMeasurable}(f,u)$$$

Lean4

/-- A continuous and adapted process is progressively measurable. -/
theorem progMeasurable_of_continuous [TopologicalSpace ι] [MetrizableSpace ι] [SecondCountableTopology ι]
    [MeasurableSpace ι] [OpensMeasurableSpace ι] [PseudoMetrizableSpace β] (h : Adapted f u)
    (hu_cont : ∀ ω, Continuous fun i => u i ω) : ProgMeasurable f u := fun i =>
  @stronglyMeasurable_uncurry_of_continuous_of_stronglyMeasurable _ _ (Set.Iic i) _ _ _ _ _ _ _ (f i) _
    (fun ω => (hu_cont ω).comp continuous_induced_dom) fun j => (h j).mono (f.mono j.prop)

Похожие утверждения