Doob estimates with almost surely right-continuous paths

The countable dense-time argument is performed on one event of full measure. No change of the adapted representatives or completion of the filtration is necessary.

References

• J. Bertoin, Lévy Processes, Cambridge University Press, 1996, Chapter IV.

theorem BGW.StableTrees.aemeasurable_sup_Icc_enorm_of_ae_rightContinuous {Ω : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {M : NNReal → Ω → ℝ} (hM : ∀ (t : NNReal), Measurable (M t)) (hrc : ∀ᵐ (ω : Ω) ∂μ, ∀ (t : NNReal), ContinuousWithinAt (fun (s : NNReal) => M s ω) (Set.Ici t) t) (T : NNReal) : AEMeasurable (fun (ω : Ω) => ⨆ t ∈ Set.Icc 0 T, ‖M t ω‖ₑ) μ

The compact extended supremum is measurable up to a null set.

theorem BGW.StableTrees.lintegral_sq_sup_Icc_le_four_mul_of_ae_rightContinuous {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {ℱ : MeasureTheory.Filtration NNReal inst✝} {M : NNReal → Ω → ℝ} (hM : MeasureTheory.Martingale M ℱ μ) (hrc : ∀ᵐ (ω : Ω) ∂μ, ∀ (t : NNReal), ContinuousWithinAt (fun (s : NNReal) => M s ω) (Set.Ici t) t) (T : NNReal) : ∫⁻ (ω : Ω), (⨆ t ∈ Set.Icc 0 T, ‖M t ω‖ₑ) ^ 2 ∂μ ≤ 4 * ∫⁻ (ω : Ω), ‖M T ω‖ₑ ^ 2 ∂μ

Compact-time extended Doob inequality with almost sure right continuity.

theorem BGW.StableTrees.integral_sq_sup_Iic_le_four_mul_of_ae_rightContinuous {Ω : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {ℱ : MeasureTheory.Filtration NNReal inst✝} {M : NNReal → Ω → ℝ} (hM : MeasureTheory.Martingale M ℱ μ) (hrc : ∀ᵐ (ω : Ω) ∂μ, ∀ (t : NNReal), ContinuousWithinAt (fun (s : NNReal) => M s ω) (Set.Ici t) t) (T : NNReal) (h2 : MeasureTheory.Integrable (fun (ω : Ω) => M T ω ^ 2) μ) : MeasureTheory.Integrable (fun (ω : Ω) => (⨆ (t : ↑(Set.Iic T)), |M (↑t) ω|) ^ 2) μ ∧ ∫ (ω : Ω), (⨆ (t : ↑(Set.Iic T)), |M (↑t) ω|) ^ 2 ∂μ ≤ 4 * ∫ (ω : Ω), M T ω ^ 2 ∂μ

Real compact Doob inequality with almost sure right continuity.