English
If u and t are progMeasurable and t(i,ω) ≤ i, then the time-changed process i,ω ↦ u(t(i,ω),ω) is progMeasurable.
Русский
Если u и t прогрессивно измеримы, и t(i,ω) ≤ i, то процесс, заданный как u(t(i,ω),ω), прогрессивно измерим.
LaTeX
$$$\\mathrm{ProgMeasurable}(f,u) \\land \\mathrm{ProgMeasurable}(f,t) \\land \\forall i\\,\\omega\\; t(i,\\omega) \\le i \\Rightarrow \\mathrm{ProgMeasurable}(f, (\\lambda i\\,\\omega. u (t i \\omega) \\omega))$$$
Lean4
protected theorem comp {t : ι → Ω → ι} [TopologicalSpace ι] [BorelSpace ι] [PseudoMetrizableSpace ι]
(h : ProgMeasurable f u) (ht : ProgMeasurable f t) (ht_le : ∀ i ω, t i ω ≤ i) :
ProgMeasurable f fun i ω => u (t i ω) ω := by
intro i
have :
(fun p : ↥(Set.Iic i) × Ω => u (t (p.fst : ι) p.snd) p.snd) =
(fun p : ↥(Set.Iic i) × Ω => u (p.fst : ι) p.snd) ∘ fun p : ↥(Set.Iic i) × Ω =>
(⟨t (p.fst : ι) p.snd, Set.mem_Iic.mpr ((ht_le _ _).trans p.fst.prop)⟩, p.snd) :=
rfl
rw [this]
exact (h i).comp_measurable ((ht i).measurable.subtype_mk.prodMk measurable_snd)
