Doob's maximal inequalities

TheoremDoob's L² maximal inequality, finite horizon#✓fully proved

Let \(\mu\) be a probability measure and let \((f_k)_{k \in \mathbb{N}}\) be a real-valued martingale with respect to a filtration \((\mathcal{F}_k)\) and \(\mu\) such that every \(f_k\) is in \(L^2(\mu)\). Then for every \(n \in \mathbb{N}\), \(\int (\max_{k \le n} |f_k|)^2 \, d\mu \le 4 \int f_n^2 \, d\mu\).

theorem Martingale.doob_sq_maximal_ineq [IsProbabilityMeasure μ] (hmart : Martingale f ℱ μ)
    (hL2 : ∀ n, MemLp (f n) 2 μ) (n : ℕ) :
    ∫ ω, ((Finset.range (n + 1)).sup' Finset.nonempty_range_add_one
      fun k => |f k ω|) ^ 2 ∂μ ≤
    4 * ∫ ω, (f n ω) ^ 2 ∂μ

Used by 3

Used byDoob's L² maximal inequality in terms of the predictable quadratic variation, finite horizon · Square-integrability of the maximal stopped partial sum · Square-integrability of a stopped partial sum

DefinitionPredictable quadratic variation#✓fully proved

Let \(\mu\) be a measure on \(\Omega\), let \((\mathcal{F}_k)_{k \in \mathbb{N}}\) be a filtration and let \((f_k)_{k \in \mathbb{N}}\) be a real-valued process. The predictable quadratic variation of \(f\) with respect to \((\mathcal{F}_k)\) and \(\mu\) is the process defined pointwise by \(A_n(\omega) = \sum_{k=0}^{n-1} \mathbb{E}_\mu[(f_{k+1} - f_k)^2 \mid \mathcal{F}_k](\omega)\), so \(A_0 = 0\). For a square-integrable martingale this is the predictable part of \(f^2\) in Doob's decomposition.

noncomputable def predictableQuadraticVariation (μ : Measure Ω) (ℱ : Filtration ℕ m0)
    (f : ℕ → Ω → ℝ) (n : ℕ) (ω : Ω) : ℝ :=
  (Finset.range n).sum (fun k =>
    (μ[(fun ω' => (f (k + 1) ω' - f k ω') ^ 2) | ℱ k]) ω)

Used by 4

Used byDoob's L² maximal inequality, infinite horizon · Doob's L² maximal inequality in terms of the predictable quadratic variation, finite horizon · Expectation of the predictable quadratic variation · Square-integrable martingale convergence

TheoremExpectation of the predictable quadratic variation#✓fully proved

Let \(\mu\) be a probability measure and let \((f_k)_{k \in \mathbb{N}}\) be a real-valued martingale with respect to a filtration \((\mathcal{F}_k)\) and \(\mu\) such that every \(f_k\) is in \(L^2(\mu)\), and let \(A_n\) be its predictable quadratic variation. Then for every \(n \in \mathbb{N}\), \(\int A_n \, d\mu = \int f_n^2 \, d\mu - \int f_0^2 \, d\mu\).

The proof telescopes, using the orthogonality of martingale increments.

theorem Martingale.integral_predictableQuadraticVariation [IsProbabilityMeasure μ]
    (hmart : Martingale f ℱ μ) (hL2 : ∀ n, MemLp (f n) 2 μ) (n : ℕ) :
    ∫ ω, predictableQuadraticVariation μ ℱ f n ω ∂μ =
      ∫ ω, (f n ω) ^ 2 ∂μ - ∫ ω, (f 0 ω) ^ 2 ∂μ

Uses 1 · Used by 2

Statement usesPredictable quadratic variation

Used byDoob's L² maximal inequality in terms of the predictable quadratic variation, finite horizon · Square-integrable martingale convergence

TheoremDoob's L² maximal inequality in terms of the predictable quadratic variation, finite horizon#✓fully proved

Doob's L² maximal inequality in terms of the predictable quadratic variation, finite horizon. Let \(\mu\) be a probability measure and let \((f_k)_{k \in \mathbb{N}}\) be a real-valued martingale with respect to a filtration \((\mathcal{F}_k)\) and \(\mu\) such that every \(f_k\) is in \(L^2(\mu)\) and \(f_0 = 0\) almost everywhere, and let \(A_n\) be its predictable quadratic variation. Then for every \(n \in \mathbb{N}\), \(\int (\max_{k \le n} |f_k|)^2 \, d\mu \le 4 \int A_n \, d\mu\).

theorem Martingale.doob_sq_maximal_ineq_predictableQuadraticVariation
    [IsProbabilityMeasure μ] (hmart : Martingale f ℱ μ) (hL2 : ∀ n, MemLp (f n) 2 μ)
    (hf0 : f 0 =ᵐ[μ] 0) (n : ℕ) :
    ∫ ω, ((Finset.range (n + 1)).sup' Finset.nonempty_range_add_one
      fun k => |f k ω|) ^ 2 ∂μ ≤
    4 * ∫ ω, predictableQuadraticVariation μ ℱ f n ω ∂μ

Uses 3 · Used by 1

Statement usesPredictable quadratic variation

Proof usesDoob's L² maximal inequality, finite horizon · Expectation of the predictable quadratic variation

Used byDoob's L² maximal inequality, infinite horizon

TheoremDoob's L² maximal inequality, infinite horizon#✓fully proved

Let \(\mu\) be a probability measure, let \((f_n)_{n \in \mathbb{N}}\) be a real-valued martingale with respect to a filtration \((\mathcal{F}_n)\) and \(\mu\) such that every \(f_n\) is in \(L^2(\mu)\) and \(f_0 = 0\) almost everywhere, and let \(A_n\) be its predictable quadratic variation. Then \(\int \sup_n |f_n|^2 \, d\mu \le 4 \int \sup_n \max(A_n, 0) \, d\mu\), where both integrals are of \([0, \infty]\)-valued functions and may be infinite.

Since each \(A_n\) is nonnegative almost everywhere, the right side is \(4\,\mathbb{E}[A_\infty]\) with \(A_\infty = \sup_n A_n\).

theorem Martingale.doob_sq_maximal_ineq_iSup [IsProbabilityMeasure μ]
    (hmart : Martingale f ℱ μ) (hL2 : ∀ n, MemLp (f n) 2 μ) (hf0 : f 0 =ᵐ[μ] 0) :
    ∫⁻ ω, ⨆ n, ENNReal.ofReal (|f n ω| ^ 2) ∂μ ≤
      4 * ∫⁻ ω, ⨆ n, ENNReal.ofReal (predictableQuadraticVariation μ ℱ f n ω) ∂μ

Uses 2

Statement usesPredictable quadratic variation

Proof usesDoob's L² maximal inequality in terms of the predictable quadratic variation, finite horizon

5 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.