Centering lemma for stochastic processes

Any ℕ-indexed stochastic process which is strongly adapted and integrable can be written as the sum of a martingale and a predictable process. This result is also known as Doob's decomposition theorem. From a process f, a filtration ℱ and a measure μ, we define two processes martingalePart f ℱ μ and predictablePart f ℱ μ.

Main definitions

• MeasureTheory.predictablePart f ℱ μ: a predictable process such that f = predictablePart f ℱ μ + martingalePart f ℱ μ
• MeasureTheory.martingalePart f ℱ μ: a martingale such that f = predictablePart f ℱ μ + martingalePart f ℱ μ

Main statements

• MeasureTheory.stronglyAdapted_predictablePart: (fun n => predictablePart f ℱ μ (n+1)) is strongly adapted. That is, predictablePart is predictable.
• MeasureTheory.martingale_martingalePart: martingalePart f ℱ μ is a martingale.

noncomputable def MeasureTheory.predictablePart {Ω : Type u_1} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {m0 : MeasurableSpace Ω} (f : ℕ → Ω → E) (ℱ : Filtration ℕ m0) (μ : Measure Ω) : ℕ → Ω → E

Any ℕ-indexed stochastic process can be written as the sum of a martingale and a predictable process. This is the predictable process. See martingalePart for the martingale.

@[simp]

theorem MeasureTheory.predictablePart_zero {Ω : Type u_1} {E : Type u_2} {m0 : MeasurableSpace Ω} {μ : Measure Ω} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {f : ℕ → Ω → E} {ℱ : Filtration ℕ m0} : predictablePart f ℱ μ 0 = 0

theorem MeasureTheory.stronglyAdapted_predictablePart {Ω : Type u_1} {E : Type u_2} {m0 : MeasurableSpace Ω} {μ : Measure Ω} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {f : ℕ → Ω → E} {ℱ : Filtration ℕ m0} : StronglyAdapted ℱ fun (n : ℕ) => predictablePart f ℱ μ (n + 1)

theorem MeasureTheory.stronglyAdapted_predictablePart' {Ω : Type u_1} {E : Type u_2} {m0 : MeasurableSpace Ω} {μ : Measure Ω} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {f : ℕ → Ω → E} {ℱ : Filtration ℕ m0} : StronglyAdapted ℱ fun (n : ℕ) => predictablePart f ℱ μ n

noncomputable def MeasureTheory.martingalePart {Ω : Type u_1} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {m0 : MeasurableSpace Ω} (f : ℕ → Ω → E) (ℱ : Filtration ℕ m0) (μ : Measure Ω) : ℕ → Ω → E

Any ℕ-indexed stochastic process can be written as the sum of a martingale and a predictable process. This is the martingale. See predictablePart for the predictable process.

theorem MeasureTheory.martingalePart_add_predictablePart {Ω : Type u_1} {E : Type u_2} {m0 : MeasurableSpace Ω} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (ℱ : Filtration ℕ m0) (μ : Measure Ω) (f : ℕ → Ω → E) : martingalePart f ℱ μ + predictablePart f ℱ μ = f

theorem MeasureTheory.martingalePart_eq_sum {Ω : Type u_1} {E : Type u_2} {m0 : MeasurableSpace Ω} {μ : Measure Ω} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {f : ℕ → Ω → E} {ℱ : Filtration ℕ m0} : martingalePart f ℱ μ = fun (n : ℕ) => f 0 + ∑ i ∈ Finset.range n, (f (i + 1) - f i - μ[f (i + 1) - f i | ↑ℱ i])

theorem MeasureTheory.stronglyAdapted_martingalePart {Ω : Type u_1} {E : Type u_2} {m0 : MeasurableSpace Ω} {μ : Measure Ω} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {f : ℕ → Ω → E} {ℱ : Filtration ℕ m0} (hf : StronglyAdapted ℱ f) : StronglyAdapted ℱ (martingalePart f ℱ μ)

theorem MeasureTheory.integrable_martingalePart {Ω : Type u_1} {E : Type u_2} {m0 : MeasurableSpace Ω} {μ : Measure Ω} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {f : ℕ → Ω → E} {ℱ : Filtration ℕ m0} (hf_int : ∀ (n : ℕ), Integrable (f n) μ) (n : ℕ) : Integrable (martingalePart f ℱ μ n) μ

theorem MeasureTheory.martingale_martingalePart {Ω : Type u_1} {E : Type u_2} {m0 : MeasurableSpace Ω} {μ : Measure Ω} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {f : ℕ → Ω → E} {ℱ : Filtration ℕ m0} (hf : StronglyAdapted ℱ f) (hf_int : ∀ (n : ℕ), Integrable (f n) μ) [SigmaFiniteFiltration μ ℱ] : Martingale (martingalePart f ℱ μ) ℱ μ

theorem MeasureTheory.martingalePart_add_ae_eq {Ω : Type u_1} {E : Type u_2} {m0 : MeasurableSpace Ω} {μ : Measure Ω} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {ℱ : Filtration ℕ m0} [SigmaFiniteFiltration μ ℱ] {f g : ℕ → Ω → E} (hf : Martingale f ℱ μ) (hg : StronglyAdapted ℱ fun (n : ℕ) => g (n + 1)) (hg0 : g 0 = 0) (hgint : ∀ (n : ℕ), Integrable (g n) μ) (n : ℕ) : martingalePart (f + g) ℱ μ n =ᶠ[ae μ] f n

theorem MeasureTheory.predictablePart_add_ae_eq {Ω : Type u_1} {E : Type u_2} {m0 : MeasurableSpace Ω} {μ : Measure Ω} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {ℱ : Filtration ℕ m0} [SigmaFiniteFiltration μ ℱ] {f g : ℕ → Ω → E} (hf : Martingale f ℱ μ) (hg : StronglyAdapted ℱ fun (n : ℕ) => g (n + 1)) (hg0 : g 0 = 0) (hgint : ∀ (n : ℕ), Integrable (g n) μ) (n : ℕ) : predictablePart (f + g) ℱ μ n =ᶠ[ae μ] g n

theorem MeasureTheory.predictablePart_bdd_difference {Ω : Type u_1} {m0 : MeasurableSpace Ω} {μ : Measure Ω} {R : NNReal} {f : ℕ → Ω → ℝ} (ℱ : Filtration ℕ m0) (hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R) : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |predictablePart f ℱ μ (i + 1) ω - predictablePart f ℱ μ i ω| ≤ ↑R

theorem MeasureTheory.martingalePart_bdd_difference {Ω : Type u_1} {m0 : MeasurableSpace Ω} {μ : Measure Ω} {R : NNReal} {f : ℕ → Ω → ℝ} (ℱ : Filtration ℕ m0) (hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R) : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |martingalePart f ℱ μ (i + 1) ω - martingalePart f ℱ μ i ω| ≤ ↑(2 * R)