theorem
DoobDecomposition.predictablePart_mono_of_submartingale
{Ω : Type u_1}
{m0 : MeasurableSpace Ω}
{μ : MeasureTheory.Measure Ω}
{f : ℕ → Ω → ℝ}
{ℱ : MeasureTheory.Filtration ℕ m0}
(hf : MeasureTheory.Submartingale f ℱ μ)
(n : ℕ)
:
For a submartingale f, the predictable part A_n is almost-everywhere
nondecreasing: A_n ≤ A_{n+1} a.e. This uses that E[f_{n+1} - f_n | ℱ n] ≥ 0 for a
submartingale.
theorem
DoobDecomposition.doob_decomposition
{Ω : Type u_1}
{m0 : MeasurableSpace Ω}
{μ : MeasureTheory.Measure Ω}
{f : ℕ → Ω → ℝ}
{ℱ : MeasureTheory.Filtration ℕ m0}
[MeasureTheory.SigmaFiniteFiltration μ ℱ]
(hf : MeasureTheory.Submartingale f ℱ μ)
:
MeasureTheory.Martingale (MeasureTheory.martingalePart f ℱ μ) ℱ μ ∧ MeasureTheory.predictablePart f ℱ μ 0 = 0 ∧ (MeasureTheory.StronglyAdapted ℱ fun (n : ℕ) => MeasureTheory.predictablePart f ℱ μ (n + 1)) ∧ (∀ (n : ℕ), MeasureTheory.predictablePart f ℱ μ n ≤ᵐ[μ] MeasureTheory.predictablePart f ℱ μ (n + 1)) ∧ MeasureTheory.martingalePart f ℱ μ + MeasureTheory.predictablePart f ℱ μ = f
Doob's decomposition theorem. Any submartingale f admits the decomposition
f = M + A where M = martingalePart f ℱ μ is a martingale and
A = predictablePart f ℱ μ is a predictable, almost-everywhere nondecreasing process
with A 0 = 0.