Cadlag modification stochastic processes

theorem ProbabilityTheory.exists_modification_left_right_limit {ι : Type u_1} {Ω : Type u_2} [TopologicalSpace ι] [LinearOrder ι] [OrderBot ι] [OrderTopology ι] [FirstCountableTopology ι] [DenselyOrdered ι] [NoMaxOrder ι] {mΩ : MeasurableSpace Ω} {𝓕 : MeasureTheory.Filtration ι mΩ} {μ : MeasureTheory.Measure Ω} {X : ι → Ω → ℝ} [MeasureTheory.Approximable 𝓕 μ] [MeasureTheory.IsFiniteMeasure μ] (hX : MeasureTheory.StronglyAdapted 𝓕 X) (hXint : ∀ (t : ι), MeasureTheory.Integrable (X t) μ) (hXbdd : ∀ (t : ι), ∃ (C : ℝ), ∀ (S : ElementaryPredictableSet 𝓕), ∫ (x : Ω), SimpleProcess.integral (ContinuousLinearMap.mul ℝ ℝ) (S.indicator 1) X (↑t) x ∂μ ≤ C) : ∃ (Y : ι → Ω → ℝ), (∀ (t : ι), Y t =ᵐ[μ] X t) ∧ (∀ (x : ι) (ω : Ω), ∃ (l : ℝ), Filter.Tendsto (fun (x : ι) => Y x ω) (nhdsWithin x (Set.Iio x)) (nhds l)) ∧ (∀ (x : ι) (ω : Ω), ∃ (l : ℝ), Filter.Tendsto (fun (x : ι) => Y x ω) (nhdsWithin x (Set.Ioi x)) (nhds l)) ∧ ∃ (s : Set ι), s.Countable ∧ ∀ x ∉ s, ∀ (ω : Ω), ContinuousWithinAt (fun (x : ι) => Y x ω) (Set.Ioi x) x

If X is an adapted integrable stochastic process such that the sets {𝔼[(𝟙_A ● X) t] | A elementary predicatable} is bounded for any t, then it has a modification Y which has left and right limits everywhere and is right continuous on a co-countable set s : Set ι.

theorem ProbabilityTheory.exists_modification_isCadlag {ι : Type u_1} {Ω : Type u_2} [TopologicalSpace ι] [LinearOrder ι] [OrderBot ι] [OrderTopology ι] [FirstCountableTopology ι] [DenselyOrdered ι] [NoMaxOrder ι] {mΩ : MeasurableSpace Ω} {𝓕 : MeasureTheory.Filtration ι mΩ} {μ : MeasureTheory.Measure Ω} {X : ι → Ω → ℝ} [MeasureTheory.Approximable 𝓕 μ] [MeasureTheory.IsFiniteMeasure μ] (hX : MeasureTheory.StronglyAdapted 𝓕 X) (hXint : ∀ (t : ι), MeasureTheory.Integrable (X t) μ) (hXRC : ∀ (t : ι), MeasureTheory.TendstoInMeasure μ X (nhdsWithin t (Set.Ioi t)) (X t)) (hXbdd : ∀ (t : ι), ∃ (C : ℝ), ∀ (S : ElementaryPredictableSet 𝓕), ∫ (x : Ω), SimpleProcess.integral (ContinuousLinearMap.mul ℝ ℝ) (S.indicator 1) X (↑t) x ∂μ ≤ C) : ∃ (Y : ι → Ω → ℝ), (∀ (t : ι), Y t =ᵐ[μ] X t) ∧ (∀ (t : ι), MeasureTheory.Integrable (Y t) μ) ∧ ∀ (ω : Ω), IsCadlag fun (x : ι) => Y x ω

If X is an adapted integrable stochastic process which is right continuous in probability, and is such that the set {𝔼[(𝟙_A ● X) t] | A elementary predicatable} is bounded for any t, then it admits a cadlag modification.