# Centering lemma for stochastic processes #

Any ℕ-indexed stochastic process which is 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.adapted_predictablePart: (fun n => predictablePart f ℱ μ (n+1)) is 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} [] [] {m0 : } (f : ΩE) (ℱ : ) (μ : ) :
Ω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.

Equations
Instances For
@[simp]
theorem MeasureTheory.predictablePart_zero {Ω : Type u_1} {E : Type u_2} {m0 : } {μ : } [] [] {f : ΩE} {ℱ : } :
= 0
theorem MeasureTheory.adapted_predictablePart {Ω : Type u_1} {E : Type u_2} {m0 : } {μ : } [] [] {f : ΩE} {ℱ : } :
theorem MeasureTheory.adapted_predictablePart' {Ω : Type u_1} {E : Type u_2} {m0 : } {μ : } [] [] {f : ΩE} {ℱ : } :
MeasureTheory.Adapted fun (n : ) =>
noncomputable def MeasureTheory.martingalePart {Ω : Type u_1} {E : Type u_2} [] [] {m0 : } (f : ΩE) (ℱ : ) (μ : ) :
Ω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.

Equations
Instances For
theorem MeasureTheory.martingalePart_add_predictablePart {Ω : Type u_1} {E : Type u_2} {m0 : } [] [] (ℱ : ) (μ : ) (f : ΩE) :
= f
theorem MeasureTheory.martingalePart_eq_sum {Ω : Type u_1} {E : Type u_2} {m0 : } {μ : } [] [] {f : ΩE} {ℱ : } :
= fun (n : ) => f 0 + ().sum fun (i : ) => f (i + 1) - f i - MeasureTheory.condexp ( i) μ (f (i + 1) - f i)
theorem MeasureTheory.adapted_martingalePart {Ω : Type u_1} {E : Type u_2} {m0 : } {μ : } [] [] {f : ΩE} {ℱ : } (hf : ) :
theorem MeasureTheory.integrable_martingalePart {Ω : Type u_1} {E : Type u_2} {m0 : } {μ : } [] [] {f : ΩE} {ℱ : } (hf_int : ∀ (n : ), MeasureTheory.Integrable (f n) μ) (n : ) :
theorem MeasureTheory.martingale_martingalePart {Ω : Type u_1} {E : Type u_2} {m0 : } {μ : } [] [] {f : ΩE} {ℱ : } (hf : ) (hf_int : ∀ (n : ), MeasureTheory.Integrable (f n) μ) :
theorem MeasureTheory.martingalePart_add_ae_eq {Ω : Type u_1} {E : Type u_2} {m0 : } {μ : } [] [] {ℱ : } {f : ΩE} {g : ΩE} (hf : ) (hg : MeasureTheory.Adapted fun (n : ) => g (n + 1)) (hg0 : g 0 = 0) (hgint : ∀ (n : ), MeasureTheory.Integrable (g n) μ) (n : ) :
MeasureTheory.martingalePart (f + g) μ n =ᶠ[μ.ae] f n
theorem MeasureTheory.predictablePart_add_ae_eq {Ω : Type u_1} {E : Type u_2} {m0 : } {μ : } [] [] {ℱ : } {f : ΩE} {g : ΩE} (hf : ) (hg : MeasureTheory.Adapted fun (n : ) => g (n + 1)) (hg0 : g 0 = 0) (hgint : ∀ (n : ), MeasureTheory.Integrable (g n) μ) (n : ) :
MeasureTheory.predictablePart (f + g) μ n =ᶠ[μ.ae] g n
theorem MeasureTheory.predictablePart_bdd_difference {Ω : Type u_1} {m0 : } {μ : } {R : NNReal} {f : Ω} (ℱ : ) (hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ), |f (i + 1) ω - f i ω| R) :
∀ᵐ (ω : Ω) ∂μ, ∀ (i : ), |MeasureTheory.predictablePart f μ (i + 1) ω - | R
theorem MeasureTheory.martingalePart_bdd_difference {Ω : Type u_1} {m0 : } {μ : } {R : NNReal} {f : Ω} (ℱ : ) (hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ), |f (i + 1) ω - f i ω| R) :
∀ᵐ (ω : Ω) ∂μ, ∀ (i : ), |MeasureTheory.martingalePart f μ (i + 1) ω - | (2 * R)