Uniform integrability

theorem MeasureTheory.uniformIntegrable_iff' {κ : Type u_2} {Ω : Type u_3} {E : Type u_4} {mΩ : MeasurableSpace Ω} {μ : Measure Ω} [IsFiniteMeasure μ] [NormedAddCommGroup E] {X : κ → Ω → E} {p : ENNReal} (hp : 1 ≤ p) (hp' : p ≠ ⊤) : UniformIntegrable X p μ ↔ (∀ (i : κ), AEStronglyMeasurable (X i) μ) ∧ ∀ ε > 0, ∃ (C : NNReal), ∀ (i : κ), eLpNorm ({x : Ω | C < ‖X i x‖₊}.indicator (X i)) p μ ≤ ε

An analogue of uniformIntegrable_iff, but the nonstrict inequality in C ≤ ‖X i x‖₊ is replaced by a strict inequality.

theorem MeasureTheory.uniformIntegrable_iff_tendsto_iSup_eLpNorm_indicator_norm {κ : Type u_2} {Ω : Type u_3} {E : Type u_4} {mΩ : MeasurableSpace Ω} {μ : Measure Ω} [IsFiniteMeasure μ] [NormedAddCommGroup E] {X : κ → Ω → E} (hX : ∀ (k : κ), AEStronglyMeasurable (X k) μ) : UniformIntegrable X 1 μ ↔ Filter.Tendsto (fun (c : NNReal) => ⨆ (k : κ), eLpNorm ({ω : Ω | c < ‖X k ω‖₊}.indicator (X k)) 1 μ) Filter.atTop (nhds 0)

A family of random variables is uniformly integrable iff its L¹ tails above c tend to zero uniformly in the index.

theorem MeasureTheory.eLpNorm_indicator_tail_eq_setIntegral_norm {Ω : Type u_3} {E : Type u_4} {mΩ : MeasurableSpace Ω} {μ : Measure Ω} [NormedAddCommGroup E] {f : Ω → E} (hf : Integrable f μ) (c : NNReal) : eLpNorm ({ω : Ω | c < ‖f ω‖₊}.indicator f) 1 μ = ENNReal.ofReal (∫ (ω : Ω) in {ω : Ω | ↑c < ‖f ω‖}, ‖f ω‖ ∂μ)

A helper lemma for uniformIntegrable_iff_tendsto_iSup_setIntegral_norm.

theorem MeasureTheory.uniformIntegrable_iff_tendsto_nnReal_iSup_setIntegral_norm {κ : Type u_2} {Ω : Type u_3} {E : Type u_4} {mΩ : MeasurableSpace Ω} {μ : Measure Ω} [IsFiniteMeasure μ] [NormedAddCommGroup E] {X : κ → Ω → E} (hX : ∀ (k : κ), AEStronglyMeasurable (X k) μ) (hXint : ∀ (k : κ), Integrable (X k) μ) : UniformIntegrable X 1 μ ↔ Filter.Tendsto (fun (c : NNReal) => ⨆ (k : κ), ENNReal.ofReal (∫ (ω : Ω) in {ω : Ω | ↑c < ‖X k ω‖}, ‖X k ω‖ ∂μ)) Filter.atTop (nhds 0)

Use integral of norm instead of eLpNorm in the characterization of UniformIntegrable.

theorem MeasureTheory.eLpNorm_indicator_tail_eq_setIntegral_of_nonneg {Ω : Type u_3} {mΩ : MeasurableSpace Ω} {μ : Measure Ω} {f : Ω → ℝ} (hf : Integrable f μ) (hnonneg : 0 ≤ᵐ[μ] f) (c : NNReal) : eLpNorm ({ω : Ω | c < ‖f ω‖₊}.indicator f) 1 μ = ENNReal.ofReal (∫ (ω : Ω) in {ω : Ω | ↑c < f ω}, f ω ∂μ)

A helper lemma for uniformIntegrable_iff_tendsto_iSup_setIntegral_of_nonneg.

theorem MeasureTheory.uniformIntegrable_iff_tendsto_nnReal_iSup_setIntegral_of_nonneg {κ : Type u_2} {Ω : Type u_3} {mΩ : MeasurableSpace Ω} {μ : Measure Ω} [IsFiniteMeasure μ] {X : κ → Ω → ℝ} (hX : ∀ (k : κ), AEStronglyMeasurable (X k) μ) (hnonneg : ∀ (k : κ), 0 ≤ᵐ[μ] X k) (hXint : ∀ (k : κ), Integrable (X k) μ) : UniformIntegrable X 1 μ ↔ Filter.Tendsto (fun (c : NNReal) => ⨆ (k : κ), ENNReal.ofReal (∫ (ω : Ω) in {ω : Ω | ↑c < X k ω}, X k ω ∂μ)) Filter.atTop (nhds 0)

Use integral instead of eLpNorm in the characterization of UniformIntegrable for nonnegative functions.

theorem MeasureTheory.UniformIntegrable.add {ι : Type u_1} {Ω : Type u_3} {E : Type u_4} {mΩ : MeasurableSpace Ω} {μ : Measure Ω} [NormedAddCommGroup E] {X Y : ι → Ω → E} {p : ENNReal} (hp : 1 ≤ p) (hX : UniformIntegrable X p μ) (hY : UniformIntegrable Y p μ) : UniformIntegrable (X + Y) p μ

theorem MeasureTheory.UniformIntegrable.neg {ι : Type u_1} {Ω : Type u_3} {E : Type u_4} {mΩ : MeasurableSpace Ω} {μ : Measure Ω} [NormedAddCommGroup E] {X : ι → Ω → E} {p : ENNReal} (hX : UniformIntegrable X p μ) : UniformIntegrable (-X) p μ

theorem MeasureTheory.UniformIntegrable.sub {ι : Type u_1} {Ω : Type u_3} {E : Type u_4} {mΩ : MeasurableSpace Ω} {μ : Measure Ω} [NormedAddCommGroup E] {X Y : ι → Ω → E} {p : ENNReal} (hp : 1 ≤ p) (hX : UniformIntegrable X p μ) (hY : UniformIntegrable Y p μ) : UniformIntegrable (X - Y) p μ

theorem MeasureTheory.uniformIntegrable_of_dominated {ι : Type u_1} {κ : Type u_2} {Ω : Type u_3} {E : Type u_4} {F : Type u_5} {mΩ : MeasurableSpace Ω} {μ : Measure Ω} [NormedAddCommGroup E] [NormedAddCommGroup F] {X : ι → Ω → E} {Y : κ → Ω → F} {p : ENNReal} (hY : UniformIntegrable Y p μ) (mX : ∀ (i : ι), AEStronglyMeasurable (X i) μ) (hX : ∀ (i : ι), ∃ (j : κ), ∀ᵐ (ω : Ω) ∂μ, ‖X i ω‖ ≤ ‖Y j ω‖) : UniformIntegrable X p μ

theorem MeasureTheory.UniformIntegrable.norm {ι : Type u_1} {Ω : Type u_3} {E : Type u_4} {mΩ : MeasurableSpace Ω} {μ : Measure Ω} [NormedAddCommGroup E] {X : ι → Ω → E} {p : ENNReal} (hY : UniformIntegrable X p μ) : UniformIntegrable (fun (t : ι) (ω : Ω) => ‖X t ω‖) p μ

theorem MeasureTheory.uniformIntegrable_iff_norm {ι : Type u_1} {Ω : Type u_3} {E : Type u_4} {mΩ : MeasurableSpace Ω} {μ : Measure Ω} [NormedAddCommGroup E] {X : ι → Ω → E} {p : ENNReal} (mX : ∀ (i : ι), AEStronglyMeasurable (X i) μ) : UniformIntegrable X p μ ↔ UniformIntegrable (fun (t : ι) (ω : Ω) => ‖X t ω‖) p μ

theorem MeasureTheory.uniformIntegrable_of_dominated_singleton {ι : Type u_1} {Ω : Type u_3} {E : Type u_4} {mΩ : MeasurableSpace Ω} {μ : Measure Ω} [NormedAddCommGroup E] {X : ι → Ω → E} {Y : Ω → ℝ} {p : ENNReal} (hp : 1 ≤ p) (hp_ne_top : p ≠ ⊤) (hY : MemLp Y p μ) (mX : ∀ (i : ι), AEStronglyMeasurable (X i) μ) (hX : ∀ (i : ι), ∀ᵐ (ω : Ω) ∂μ, ‖X i ω‖ ≤ Y ω) : UniformIntegrable X p μ

theorem MeasureTheory.norm_le_toReal_of_enorm_le {E : Type u_4} [NormedAddCommGroup E] {r : ENNReal} (hr : r ≠ ⊤) {x : E} (hle : ‖x‖ₑ ≤ r) : ‖x‖ ≤ r.toReal

theorem MeasureTheory.MemLp.enorm_ae_lt_top {Ω : Type u_3} {E : Type u_4} {mΩ : MeasurableSpace Ω} {μ : Measure Ω} [TopologicalSpace E] [ContinuousENorm E] {f : Ω → E} {p : ENNReal} (hlp : MemLp f p μ) (hp_ne_zero : p ≠ 0) (hp_ne_top : p ≠ ⊤) : ∀ᵐ (x : Ω) ∂μ, ‖f x‖ₑ < ⊤

theorem MeasureTheory.uniformIntegrable_of_dominated_enorm_singleton {ι : Type u_1} {Ω : Type u_3} {E : Type u_4} {mΩ : MeasurableSpace Ω} {μ : Measure Ω} [NormedAddCommGroup E] {X : ι → Ω → E} {Y : Ω → ENNReal} (hY : MemLp Y 1 μ) (mX : ∀ (i : ι), AEStronglyMeasurable (X i) μ) (hX : ∀ (i : ι), ∀ᵐ (ω : Ω) ∂μ, ‖X i ω‖ₑ ≤ Y ω) : UniformIntegrable X 1 μ

theorem MeasureTheory.UniformIntegrable.condExp' {ι : Type u_1} {κ : Type u_2} {Ω : Type u_3} {E : Type u_4} {mΩ : MeasurableSpace Ω} {μ : Measure Ω} {X : ι → Ω → E} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (hX : UniformIntegrable X 1 μ) {𝓕 : κ → MeasurableSpace Ω} (h𝓕 : ∀ (i : κ), 𝓕 i ≤ mΩ) : UniformIntegrable (fun (p : ι × κ) => μ[X p.1 | 𝓕 p.2]) 1 μ

theorem MeasureTheory.UniformIntegrable.comp {ι : Type u_1} {Ω : Type u_3} {E : Type u_4} {mΩ : MeasurableSpace Ω} {μ : Measure Ω} {κ : Type u_6} [NormedAddCommGroup E] {X : ι → Ω → E} {p : ENNReal} (hX : UniformIntegrable X p μ) (f : κ → ι) : UniformIntegrable (X ∘ f) p μ

theorem MeasureTheory.UniformIntegrable.condExp {ι : Type u_1} {Ω : Type u_3} {E : Type u_4} {mΩ : MeasurableSpace Ω} {μ : Measure Ω} {X : ι → Ω → E} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (hX : UniformIntegrable X 1 μ) {𝓕 : ι → MeasurableSpace Ω} (h𝓕 : ∀ (i : ι), 𝓕 i ≤ mΩ) : UniformIntegrable (fun (i : ι) => μ[X i | 𝓕 i]) 1 μ

theorem MeasureTheory.uniformIntegrable_of_eLpNorm_le {ι : Type u_1} {Ω : Type u_3} {E : Type u_4} {mΩ : MeasurableSpace Ω} {μ : Measure Ω} {X : ι → Ω → E} [NormedAddCommGroup E] [NormedSpace ℝ E] [IsFiniteMeasure μ] (p q : ENNReal) (hp : q < p) (hq : 1 ≤ q) (C : ENNReal) (hC : C ≠ ⊤) (hX2 : ∀ (i : ι), eLpNorm (X i) p μ ≤ C) : UniformIntegrable X q μ

If a a family of random variables in bounded in Lp for p > q ≥ 1, then it is uniformly integrable in Lq.

theorem MeasureTheory.Martingale.uniformIntegrable_stoppedValue {Ω : Type u_3} {E : Type u_4} {mΩ : MeasurableSpace Ω} {μ : Measure Ω} {ι : Type u_6} [LinearOrder ι] [OrderBot ι] [Countable ι] [TopologicalSpace ι] [OrderTopology ι] [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {X : ι → Ω → E} {𝓕 : Filtration ι mΩ} [SigmaFiniteFiltration μ 𝓕] (hX : Martingale X 𝓕 μ) (τ : ℕ → Ω → WithTop ι) (hτ : ∀ (i : ℕ), IsStoppingTime 𝓕 (τ i)) {n : ι} (hτ_le : ∀ (i : ℕ) (ω : Ω), τ i ω ≤ ↑n) : UniformIntegrable (fun (i : ℕ) => stoppedValue X (τ i)) 1 μ

theorem MeasureTheory.Submartingale.uniformIntegrable_stoppedValue {Ω : Type u_3} {mΩ : MeasurableSpace Ω} {μ : Measure Ω} {ι : Type u_6} [LinearOrder ι] [OrderBot ι] [Countable ι] [TopologicalSpace ι] [OrderTopology ι] {X : ι → Ω → ℝ} {𝓕 : Filtration ι mΩ} [SigmaFiniteFiltration μ 𝓕] (hX : Submartingale X 𝓕 μ) (τ : ℕ → Ω → WithTop ι) (hτ : ∀ (i : ℕ), IsStoppingTime 𝓕 (τ i)) {n : ι} (hτ_le : ∀ (i : ℕ) (ω : Ω), τ i ω ≤ ↑n) : UniformIntegrable (fun (i : ℕ) => stoppedValue X (τ i)) 1 μ

theorem MeasureTheory.Martingale.uniformIntegrable_stoppedValue_of_countable_range {Ω : Type u_3} {E : Type u_4} {mΩ : MeasurableSpace Ω} {μ : Measure Ω} {ι : Type u_6} [LinearOrder ι] [OrderBot ι] [TopologicalSpace ι] [OrderTopology ι] [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] [FirstCountableTopology ι] {X : ι → Ω → E} {𝓕 : Filtration ι mΩ} [SigmaFiniteFiltration μ 𝓕] (hX : Martingale X 𝓕 μ) (τ : ℕ → Ω → WithTop ι) (hτ : ∀ (i : ℕ), IsStoppingTime 𝓕 (τ i)) {n : ι} (hτ_le : ∀ (i : ℕ) (ω : Ω), τ i ω ≤ ↑n) (hτ_countable : ∀ (i : ℕ), (Set.range (τ i)).Countable) : UniformIntegrable (fun (i : ℕ) => stoppedValue X (τ i)) 1 μ

theorem MeasureTheory.Martingale.integrable_stoppedValue_of_countable_range {Ω : Type u_3} {E : Type u_4} {mΩ : MeasurableSpace Ω} {μ : Measure Ω} {ι : Type u_6} [LinearOrder ι] [OrderBot ι] [TopologicalSpace ι] [OrderTopology ι] [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] [FirstCountableTopology ι] {X : ι → Ω → E} {𝓕 : Filtration ι mΩ} [SigmaFiniteFiltration μ 𝓕] (hX : Martingale X 𝓕 μ) (τ : Ω → WithTop ι) (hτ : IsStoppingTime 𝓕 τ) {n : ι} (hτ_le : ∀ (ω : Ω), τ ω ≤ ↑n) (hτ_countable : (Set.range τ).Countable) : Integrable (stoppedValue X τ) μ

theorem MeasureTheory.seq_tendsto_ae_bounded {α : Type u_7} {β : Type u_8} {m : MeasurableSpace α} {μ : Measure α} [NormedAddCommGroup β] {f : ℕ → α → β} {g : α → β} {C : ENNReal} (p : ENNReal) (bound : ∀ (n : ℕ), eLpNorm (f n) p μ ≤ C) (h_tendsto : ∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun (n : ℕ) => f n x) Filter.atTop (nhds (g x))) (hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ) : eLpNorm g p μ ≤ C

Uniformly integrable martingales

theorem MeasureTheory.Martingale.ae_tendsto_limitProcess {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [LinearOrder ι] {mΩ : MeasurableSpace Ω} {P : Measure Ω} {𝓕 : Filtration ι mΩ} {X : ι → Ω → E} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace ι] (hX1 : Martingale X 𝓕 P) (hX2 : UniformIntegrable X 1 P) (hX3 : ∀ (ω : Ω), IsRightContinuous fun (x : ι) => X x ω) : ∀ᵐ (ω : Ω) ∂P, Filter.Tendsto (fun (x : ι) => X x ω) Filter.atTop (nhds (Filtration.limitProcess X 𝓕 P ω))

A càdlàg uniformly integrable martingale converges.

theorem MeasureTheory.Martingale.limitProcess_add {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [LinearOrder ι] {mΩ : MeasurableSpace Ω} {P : Measure Ω} {𝓕 : Filtration ι mΩ} {X Y : ι → Ω → E} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace ι] [Nonempty ι] (hX1 : Martingale X 𝓕 P) (hX2 : UniformIntegrable X 1 P) (hX3 : ∀ (ω : Ω), IsRightContinuous fun (x : ι) => X x ω) (hY1 : Martingale Y 𝓕 P) (hY2 : UniformIntegrable Y 1 P) (hY3 : ∀ (ω : Ω), IsRightContinuous fun (x : ι) => Y x ω) : Filtration.limitProcess (X + Y) 𝓕 P =ᵐ[P] Filtration.limitProcess X 𝓕 P + Filtration.limitProcess Y 𝓕 P

theorem MeasureTheory.Martingale.limitProcess_fun_add {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [LinearOrder ι] {mΩ : MeasurableSpace Ω} {P : Measure Ω} {𝓕 : Filtration ι mΩ} {X Y : ι → Ω → E} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace ι] [Nonempty ι] (hX1 : Martingale X 𝓕 P) (hX2 : UniformIntegrable X 1 P) (hX3 : ∀ (ω : Ω), IsRightContinuous fun (x : ι) => X x ω) (hY1 : Martingale Y 𝓕 P) (hY2 : UniformIntegrable Y 1 P) (hY3 : ∀ (ω : Ω), IsRightContinuous fun (x : ι) => Y x ω) : Filtration.limitProcess (fun (i : ι) (i_1 : Ω) => X i i_1 + Y i i_1) 𝓕 P =ᵐ[P] fun (i : Ω) => Filtration.limitProcess X 𝓕 P i + Filtration.limitProcess Y 𝓕 P i

Eta-expanded form of MeasureTheory.Martingale.limitProcess_add

theorem MeasureTheory.Martingale.limitProcess_sub {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [LinearOrder ι] {mΩ : MeasurableSpace Ω} {P : Measure Ω} {𝓕 : Filtration ι mΩ} {X Y : ι → Ω → E} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace ι] [Nonempty ι] (hX1 : Martingale X 𝓕 P) (hX2 : UniformIntegrable X 1 P) (hX3 : ∀ (ω : Ω), IsRightContinuous fun (x : ι) => X x ω) (hY1 : Martingale Y 𝓕 P) (hY2 : UniformIntegrable Y 1 P) (hY3 : ∀ (ω : Ω), IsRightContinuous fun (x : ι) => Y x ω) : Filtration.limitProcess (X - Y) 𝓕 P =ᵐ[P] Filtration.limitProcess X 𝓕 P - Filtration.limitProcess Y 𝓕 P

theorem MeasureTheory.Martingale.limitProcess_fun_sub {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [LinearOrder ι] {mΩ : MeasurableSpace Ω} {P : Measure Ω} {𝓕 : Filtration ι mΩ} {X Y : ι → Ω → E} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace ι] [Nonempty ι] (hX1 : Martingale X 𝓕 P) (hX2 : UniformIntegrable X 1 P) (hX3 : ∀ (ω : Ω), IsRightContinuous fun (x : ι) => X x ω) (hY1 : Martingale Y 𝓕 P) (hY2 : UniformIntegrable Y 1 P) (hY3 : ∀ (ω : Ω), IsRightContinuous fun (x : ι) => Y x ω) : Filtration.limitProcess (fun (i : ι) (i_1 : Ω) => X i i_1 - Y i i_1) 𝓕 P =ᵐ[P] fun (i : Ω) => Filtration.limitProcess X 𝓕 P i - Filtration.limitProcess Y 𝓕 P i

Eta-expanded form of MeasureTheory.Martingale.limitProcess_sub

theorem MeasureTheory.Martingale.condExp_limitProcess_ae_eq {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [LinearOrder ι] {mΩ : MeasurableSpace Ω} {P : Measure Ω} {𝓕 : Filtration ι mΩ} {X : ι → Ω → E} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace ι] (hX1 : Martingale X 𝓕 P) (hX2 : UniformIntegrable X 1 P) (hX3 : ∀ (ω : Ω), IsRightContinuous fun (x : ι) => X x ω) (t : ι) : P[Filtration.limitProcess X 𝓕 P | ↑𝓕 t] =ᵐ[P] X t

For a càdlàg uniformly integrable martingale, P[X ∞ | 𝓕 t] = X t.

theorem MeasureTheory.Martingale.condExp_limitProcess_ae_eq' {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [LinearOrder ι] {mΩ : MeasurableSpace Ω} {P : Measure Ω} {𝓕 : Filtration ι mΩ} {X : ι → Ω → E} {τ : Ω → WithTop ι} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace ι] (hX1 : Martingale X 𝓕 P) (hX2 : UniformIntegrable X 1 P) (hX3 : ∀ (ω : Ω), IsRightContinuous fun (x : ι) => X x ω) (hτ : IsStoppingTime 𝓕 τ) : P[Filtration.limitProcess X 𝓕 P | hτ.measurableSpace] =ᵐ[P] Filtration.stoppedValue' X τ 𝓕 P

For a càdlàg uniformly integrable martingale and a stopping time τ, P[X ∞ | 𝓕 τ] = X τ.

theorem MeasureTheory.iSup_eLpNorm_le_eLpNorm_limitProcess {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [LinearOrder ι] {mΩ : MeasurableSpace Ω} {P : Measure Ω} {𝓕 : Filtration ι mΩ} {X : ι → Ω → E} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace ι] [CompleteSpace E] (hX1 : Martingale X 𝓕 P) (hX2 : UniformIntegrable X 1 P) (hX3 : ∀ (ω : Ω), IsRightContinuous fun (x : ι) => X x ω) {p : ENNReal} (hp : 1 ≤ p) : ⨆ (t : ι), eLpNorm (X t) p P ≤ eLpNorm (Filtration.limitProcess X 𝓕 P) p P

For a càdlàg uniformly integrable martingale, ⨆ t, ‖X t‖ₑ ≤ ‖X ∞‖ₑ.

theorem MeasureTheory.Filtration.limitProcess_stoppedProcess {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [LinearOrder ι] {mΩ : MeasurableSpace Ω} {P : Measure Ω} {𝓕 : Filtration ι mΩ} {X : ι → Ω → E} {τ : Ω → WithTop ι} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace ι] [OrderBot ι] [OrderTopology ι] [SecondCountableTopology ι] (hX1 : Martingale X 𝓕 P) (hX2 : UniformIntegrable X 1 P) (hX3 : ∀ (ω : Ω), _root_.IsRightContinuous fun (x : ι) => X x ω) (hτ : IsStoppingTime 𝓕 τ) : limitProcess (stoppedProcess X τ) 𝓕 P =ᵐ[P] stoppedValue' X τ 𝓕 P