noncomputable def predictableQuadVar {Ω : Type u_1} {m0 : MeasurableSpace Ω} (f : ℕ → Ω → ℝ) (ℱ : MeasureTheory.Filtration ℕ m0) (μ : MeasureTheory.Measure Ω) : ℕ → Ω → ℝ

The predictable quadratic variation Aₙ of a process f with respect to a filtration ℱ, defined as Aₙ = ∑_{i=0}^{n-1} E[(f_{i+1} - f_i)² | ℱ_i]. For a square-integrable martingale this is the predictable increasing process arising from Doob's decomposition of f².

theorem stopped_martingale_L1_bound {Ω : Type u_1} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {ℱ : MeasureTheory.Filtration ℕ m0} {f : ℕ → Ω → ℝ} (hmart : MeasureTheory.Martingale f ℱ μ) (hinteg : ∀ (n : ℕ), MeasureTheory.Integrable (fun (ω : Ω) => f n ω ^ 2) μ) (M : ℕ) : have A := predictableQuadVar f ℱ μ; have τ := MeasureTheory.leastGE (fun (n : ℕ) => A (n + 1)) (↑M + 1); have g := MeasureTheory.stoppedProcess f τ; ∃ (R : NNReal), ∀ (n : ℕ), MeasureTheory.eLpNorm (g n) 1 μ ≤ ↑R

Helper bound used in the square-integrable martingale convergence proof: if f is a square-integrable martingale and τ is the first time the predictable quadratic variation exceeds M + 1, then the stopped process g = f^τ is L¹-bounded uniformly in n.

theorem ae_convergent_of_bounded_predictable_quadvar {Ω : Type u_1} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {ℱ : MeasureTheory.Filtration ℕ m0} {f : ℕ → Ω → ℝ} (hmart : MeasureTheory.Martingale f ℱ μ) (hinteg : ∀ (n : ℕ), MeasureTheory.Integrable (fun (ω : Ω) => f n ω ^ 2) μ) (M : ℕ) : ∀ᵐ (ω : Ω) ∂μ, (∀ (n : ℕ), predictableQuadVar f ℱ μ n ω ≤ ↑M) → ∃ (l : ℝ), Filter.Tendsto (fun (n : ℕ) => f n ω) Filter.atTop (nhds l)

If a square-integrable martingale f has predictable quadratic variation bounded by a constant M along the trajectory of ω, then f n ω converges as n → ∞, for almost every such ω. This is the discrete analogue of bounded variation ensuring convergence of a martingale.

theorem sq_martingale_convergence_on_predictable_quadvar_finite {Ω : Type u_1} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {ℱ : MeasureTheory.Filtration ℕ m0} {f : ℕ → Ω → ℝ} (hmart : MeasureTheory.Martingale f ℱ μ) (hinteg : ∀ (n : ℕ), MeasureTheory.Integrable (fun (ω : Ω) => f n ω ^ 2) μ) : ∀ᵐ (ω : Ω) ∂μ, (∃ (l : ℝ), Filter.Tendsto (fun (n : ℕ) => predictableQuadVar f ℱ μ n ω) Filter.atTop (nhds l)) → ∃ (l : ℝ), Filter.Tendsto (fun (n : ℕ) => f n ω) Filter.atTop (nhds l)

Square integrable martingale convergence. Suppose Xₙ is a martingale with E[Xₙ²] < ∞ for all n and let Aₙ be the associated predictable quadratic variation. Then lim_{n→∞} Xₙ exists and is finite almost surely on the event {A_∞ < ∞}.