Strong measurability of the path map of a right-continuous process

A process X : ι → Ω → E can be seen as a path-valued random variable Ω → (ι → E), where ι → E carries the product topology. We show that if each X i is strongly measurable and every path X · ω is right-continuous, then that path map is strongly measurable.

Main results

• stronglyMeasurable_path_of_isRightContinuous: the path map of a right-continuous process with strongly measurable marginals is strongly measurable.
• MeasureTheory.StronglyAdapted.stronglyMeasurable_path: the same statement for a strongly adapted process with right-continuous paths.

theorem MeasureTheory.SimpleFunc.coe_finset_sum {α : Type u_1} {β : Type u_2} {γ : Type u_3} {x✝ : MeasurableSpace α} [AddCommMonoid β] (f : γ → SimpleFunc α β) (s : Finset γ) : ⇑(∑ t ∈ s, f t) = ∑ t ∈ s, ⇑(f t)

theorem MeasureTheory.nhdsWithin_inter_Ioi_neBot {ι : Type u_1} [LinearOrder ι] [TopologicalSpace ι] [OrderTopology ι] {d : Set ι} (hd : Dense d) {i : ι} (hi : (nhdsWithin i (Set.Ioi i)).NeBot) : (nhdsWithin i (d ∩ Set.Ioi i)).NeBot

theorem MeasureTheory.isSeparable_iUnion_range_of_stronglyMeasurable_of_isRightContinuous {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [LinearOrder ι] [TopologicalSpace ι] [SecondCountableTopology ι] [OrderTopology ι] [MeasurableSpace Ω] [TopologicalSpace E] {X : ι → Ω → E} (hX : ∀ (i : ι), StronglyMeasurable (X i)) (hX_cont : ∀ (ω : Ω), IsRightContinuous fun (x : ι) => X x ω) : TopologicalSpace.IsSeparable (⋃ (t : ι), Set.range (X t))

The set of values taken by a right-continuous process with strongly measurable marginals is separable.

theorem MeasureTheory.stronglyMeasurable_path_of_isRightContinuous {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [LinearOrder ι] [TopologicalSpace ι] [OrderTopology ι] [SecondCountableTopology ι] {mΩ : MeasurableSpace Ω} [NormedAddCommGroup E] {X : ι → Ω → E} (hX : ∀ (i : ι), StronglyMeasurable (X i)) (hX_cont : ∀ (ω : Ω), IsRightContinuous fun (x : ι) => X x ω) : StronglyMeasurable fun (ω : Ω) (x : ι) => X x ω

A process whose paths are right-continuous and whose marginals X i are strongly measurable is strongly measurable as a map Ω → (ι → E) into the path space with the product topology.

theorem MeasureTheory.StronglyAdapted.stronglyMeasurable_path {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [LinearOrder ι] [TopologicalSpace ι] [OrderTopology ι] [SecondCountableTopology ι] {mΩ : MeasurableSpace Ω} [NormedAddCommGroup E] {X : ι → Ω → E} {𝓕 : Filtration ι mΩ} (hX : StronglyAdapted 𝓕 X) (hX_cont : ∀ (ω : Ω), IsRightContinuous fun (x : ι) => X x ω) : StronglyMeasurable fun (ω : Ω) (x : ι) => X x ω

A strongly adapted process with right-continuous paths is strongly measurable as a path-valued random variable Ω → (ι → E).