Martingale convergence theorems

TheoremThe \(L^p\) martingale convergence theorem#✓fully proved

Let \((\Omega, \mu)\) be a probability space with a filtration \((\mathcal{F}_n)_{n \in \mathbb{N}}\), write \(\mathcal{F}_\infty = \bigvee_n \mathcal{F}_n\), let \(1 < p < \infty\), and let \((f_n)_{n \in \mathbb{N}}\) be a real-valued martingale with respect to \((\mathcal{F}_n)\) and \(\mu\) whose \(L^p\) norms are uniformly bounded: there is a constant \(R \ge 0\) with \(\|f_n\|_{L^p(\mu)} \le R\) for every \(n\). Let \(f_\infty\) be the limit process of \((f_n)\), that is, a chosen \(\mathcal{F}_\infty\)-measurable function to which \(f_n\) converges almost everywhere if such a function exists, and \(0\) otherwise. Then \(f_n \to f_\infty\) almost surely, and \(\|f_n - f_\infty\|_{L^p(\mu)} \to 0\) as \(n \to \infty\).

theorem Martingale.tendsto_eLpNorm_limitProcess_of_eLpNorm_bdd {p : ℝ≥0∞} {R : ℝ≥0}
    (hp : 1 < p) (hp_top : p ≠ ⊤) (hmart : Martingale f ℱ μ)
    (hbdd : ∀ n, eLpNorm (f n) p μ ≤ R) :
    (∀ᵐ ω ∂μ, Tendsto (fun n => f n ω) atTop (𝓝 (ℱ.limitProcess f μ ω))) ∧
      Tendsto (fun n => eLpNorm (f n - ℱ.limitProcess f μ) p μ) atTop (𝓝 0)

TheoremEquivalent conditions for uniform integrability of a submartingale#✓fully proved

Let \((\Omega, \mu)\) be a probability space with a filtration \((\mathcal{F}_n)_{n \in \mathbb{N}}\), and let \((X_n)_{n \in \mathbb{N}}\) be a real-valued submartingale with respect to \((\mathcal{F}_n)\) and \(\mu\). The following are equivalent: 1. \((X_n)\) is uniformly integrable. 2. There is an integrable \(X_\infty\) such that \(X_n \to X_\infty\) almost surely and \(\int |X_n - X_\infty| \, d\mu \to 0\). 3. There is an integrable \(X_\infty\) such that \(\int |X_n - X_\infty| \, d\mu \to 0\).

theorem Submartingale.uniformIntegrable_tfae
    {Ω : Type*} {m0 : MeasurableSpace Ω} {μ : Measure Ω}
    [IsProbabilityMeasure μ]
    {ℱ : Filtration ℕ m0}
    {X : ℕ → Ω → ℝ}
    (hsub : Submartingale X ℱ μ) :
    List.TFAE [
      UniformIntegrable X 1 μ,
      ∃ X_inf, Integrable X_inf μ ∧
        (∀ᵐ ω ∂μ, Filter.Tendsto (fun n => X n ω) Filter.atTop (nhds (X_inf ω))) ∧
        Filter.Tendsto (fun n => ∫ ω, ‖X n ω - X_inf ω‖ ∂μ) Filter.atTop (nhds 0),
      ∃ X_inf, Integrable X_inf μ ∧
        Filter.Tendsto (fun n => ∫ ω, ‖X n ω - X_inf ω‖ ∂μ) Filter.atTop (nhds 0)
    ]

TheoremEquivalent conditions for uniform integrability of a martingale#✓fully proved

Let \((\Omega, \mu)\) be a probability space with a filtration \((\mathcal{F}_n)_{n \in \mathbb{N}}\), and let \((X_n)_{n \in \mathbb{N}}\) be a real-valued martingale with respect to \((\mathcal{F}_n)\) and \(\mu\). The following are equivalent: 1. \((X_n)\) is uniformly integrable. 2. There is an integrable \(X_\infty\) such that \(X_n \to X_\infty\) almost surely and \(\int |X_n - X_\infty| \, d\mu \to 0\). 3. There is an integrable \(X_\infty\) such that \(\int |X_n - X_\infty| \, d\mu \to 0\). 4. There is an integrable \(X_\infty\) such that \(X_n = \mathbb{E}[X_\infty \mid \mathcal{F}_n]\) almost surely for every \(n\).

MeasureTheory.Martingale.uniformIntegrable_tfae · 15 lines

theorem Martingale.uniformIntegrable_tfae
    {Ω : Type*} {m0 : MeasurableSpace Ω} {μ : Measure Ω}
    [IsProbabilityMeasure μ]
    {ℱ : Filtration ℕ m0}
    {X : ℕ → Ω → ℝ}
    (hmart : Martingale X ℱ μ) :
    List.TFAE [
      UniformIntegrable X 1 μ,
      ∃ X_inf, Integrable X_inf μ ∧
        (∀ᵐ ω ∂μ, Filter.Tendsto (fun n => X n ω) Filter.atTop (nhds (X_inf ω))) ∧
        Filter.Tendsto (fun n => ∫ ω, ‖X n ω - X_inf ω‖ ∂μ) Filter.atTop (nhds 0),
      ∃ X_inf, Integrable X_inf μ ∧
        Filter.Tendsto (fun n => ∫ ω, ‖X n ω - X_inf ω‖ ∂μ) Filter.atTop (nhds 0),
      ∃ X_inf, Integrable X_inf μ ∧ ∀ n, X n =ᵐ[μ] μ[X_inf | ℱ n]
    ]

TheoremSquare-integrable martingale convergence#✓fully proved

Let \((X_n)_{n \in \mathbb{N}}\) be a real-valued martingale with respect to a filtration \((\mathcal{F}_n)\) on a probability space, with \(E[X_n^2] < \infty\) for every \(n\), and let \((A_n)\) be its predictable quadratic variation. Then for almost every \(\omega\): if \(A_n(\omega)\) converges to a real limit as \(n \to \infty\), then \(X_n(\omega)\) converges to a real limit as well.

In particular, \(X_n\) converges almost surely on the event \(\{\sup_n A_n < \infty\}\), since \(A_n\) is almost surely non-decreasing in \(n\).

theorem Martingale.ae_tendsto_of_tendsto_predictableQuadVar [IsProbabilityMeasure μ]
    (hmart : Martingale f ℱ μ) (hinteg : ∀ n, Integrable (fun ω => (f n ω) ^ 2) μ) :
    ∀ᵐ ω ∂μ, (∃ l, Tendsto (fun n => predictableQuadraticVariation μ ℱ f n ω) atTop (𝓝 l)) →
      ∃ l, Tendsto (fun n => f n ω) atTop (𝓝 l)

Uses 2

Statement usesPredictable quadratic variation

Proof usesExpectation of the predictable quadratic variation

TheoremExpectations increase along a submartingale#✓fully proved

Let \((X_n)_{n \ge 0}\) be a real-valued submartingale with respect to a filtration \((\mathcal F_n)_{n \ge 0}\) on a probability space \((\Omega, \mu)\). Then \(\int X_i \, d\mu \le \int X_j \, d\mu\) for all natural numbers \(i \le j\).

theorem Submartingale.integral_mono
    {Ω : Type*} {m0 : MeasurableSpace Ω} {μ : Measure Ω} [IsProbabilityMeasure μ]
    {ℱ : Filtration ℕ m0} {X : ℕ → Ω → ℝ}
    (hsub : Submartingale X ℱ μ) {i j : ℕ} (hij : i ≤ j) :
    ∫ ω, X i ω ∂μ ≤ ∫ ω, X j ω ∂μ

Used by 1

Used byL¹ bound for a submartingale with bounded positive parts

TheoremL¹ bound for a submartingale with bounded positive parts#✓fully proved

Let \((X_n)_{n \ge 0}\) be a real-valued submartingale with respect to a filtration \((\mathcal F_n)_{n \ge 0}\) on a probability space \((\Omega, \mu)\), and let \(C\) be a real number with \(\int X_n^+ \, d\mu \le C\) for every \(n\), where \(X_n^+\) is the positive part of \(X_n\). Then for every \(n\), \(\int |X_n| \, d\mu \le 2C - \int X_0 \, d\mu\).

The proof uses the identity \(|x| = 2x^+ - x\) together with the monotonicity of \(n \mapsto \int X_n \, d\mu\).

theorem Submartingale.integral_norm_le
    {Ω : Type*} {m0 : MeasurableSpace Ω} {μ : Measure Ω} [IsProbabilityMeasure μ]
    {ℱ : Filtration ℕ m0} {X : ℕ → Ω → ℝ} {C : ℝ}
    (hsub : Submartingale X ℱ μ)
    (hbdd : ∀ n, ∫ ω, (X n ω)⁺ ∂μ ≤ C) (n : ℕ) :
    ∫ ω, ‖X n ω‖ ∂μ ≤ 2 * C - ∫ ω, X 0 ω ∂μ

Uses 1 · Used by 1

Proof usesExpectations increase along a submartingale

Used bySubmartingale almost-sure convergence theorem

TheoremSubmartingale almost-sure convergence theorem#✓fully proved

Let \((X_n)_{n \ge 0}\) be a real-valued submartingale with respect to a filtration \((\mathcal F_n)_{n \ge 0}\) on a probability space \((\Omega, \mu)\), and let \(C\) be a real number with \(\int X_n^+ \, d\mu \le C\) for every \(n\), where \(X_n^+\) is the positive part of \(X_n\). Then there is an integrable function \(X_\infty : \Omega \to \mathbb R\) such that \(X_n(\omega) \to X_\infty(\omega)\) as \(n \to \infty\) for \(\mu\)-almost every \(\omega\).

theorem Submartingale.exists_ae_tendsto_of_posPart_bdd
    {Ω : Type*} {m0 : MeasurableSpace Ω} {μ : Measure Ω} [IsProbabilityMeasure μ]
    {ℱ : Filtration ℕ m0} {X : ℕ → Ω → ℝ} {C : ℝ}
    (hsub : Submartingale X ℱ μ)
    (hbdd : ∀ n, ∫ ω, (X n ω)⁺ ∂μ ≤ C) :
    ∃ X_inf : Ω → ℝ, Integrable X_inf μ ∧
      ∀ᵐ ω ∂μ, Tendsto (fun n => X n ω) atTop (𝓝 (X_inf ω))

Uses 1 · Used by 2

Proof usesL¹ bound for a submartingale with bounded positive parts

Used bySupermartingale almost-sure convergence theorem · Martingale almost-sure convergence theorem

TheoremSupermartingale almost-sure convergence theorem#✓fully proved

Let \((X_n)_{n \ge 0}\) be a real-valued supermartingale with respect to a filtration \((\mathcal F_n)_{n \ge 0}\) on a probability space \((\Omega, \mu)\), and let \(C\) be a real number with \(\int X_n^- \, d\mu \le C\) for every \(n\), where \(X_n^-\) is the negative part of \(X_n\). Then there is an integrable function \(X_\infty : \Omega \to \mathbb R\) such that \(X_n(\omega) \to X_\infty(\omega)\) as \(n \to \infty\) for \(\mu\)-almost every \(\omega\).

This follows from the submartingale theorem applied to \(-X\), since \((-X_n)^+ = X_n^-\).

theorem Supermartingale.exists_ae_tendsto_of_negPart_bdd
    {Ω : Type*} {m0 : MeasurableSpace Ω} {μ : Measure Ω} [IsProbabilityMeasure μ]
    {ℱ : Filtration ℕ m0} {X : ℕ → Ω → ℝ} {C : ℝ}
    (hsuper : Supermartingale X ℱ μ)
    (hbdd : ∀ n, ∫ ω, (X n ω)⁻ ∂μ ≤ C) :
    ∃ X_inf : Ω → ℝ, Integrable X_inf μ ∧
      ∀ᵐ ω ∂μ, Tendsto (fun n => X n ω) atTop (𝓝 (X_inf ω))

Uses 1

Proof usesSubmartingale almost-sure convergence theorem

TheoremMartingale almost-sure convergence theorem#✓fully proved

Let \((X_n)_{n \ge 0}\) be a real-valued martingale with respect to a filtration \((\mathcal F_n)_{n \ge 0}\) on a probability space \((\Omega, \mu)\), and let \(C\) be a real number with \(\int X_n^+ \, d\mu \le C\) for every \(n\), where \(X_n^+\) is the positive part of \(X_n\). Then there is an integrable function \(X_\infty : \Omega \to \mathbb R\) such that \(X_n(\omega) \to X_\infty(\omega)\) as \(n \to \infty\) for \(\mu\)-almost every \(\omega\).

This is the submartingale theorem, since every martingale is a submartingale.

theorem Martingale.exists_ae_tendsto_of_posPart_bdd
    {Ω : Type*} {m0 : MeasurableSpace Ω} {μ : Measure Ω} [IsProbabilityMeasure μ]
    {ℱ : Filtration ℕ m0} {X : ℕ → Ω → ℝ} {C : ℝ}
    (hmart : Martingale X ℱ μ)
    (hbdd : ∀ n, ∫ ω, (X n ω)⁺ ∂μ ≤ C) :
    ∃ X_inf : Ω → ℝ, Integrable X_inf μ ∧
      ∀ᵐ ω ∂μ, Tendsto (fun n => X n ω) atTop (𝓝 (X_inf ω))

Uses 1

Proof usesSubmartingale almost-sure convergence theorem

9 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.