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} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {m0 : MeasurableSpace Ω} (f : ℕ → Ω → E) (ℱ : MeasureTheory.Filtration ℕ m0) (μ : MeasureTheory.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.

Equations

• MeasureTheory.predictablePart f ℱ μ n = ∑ i ∈ Finset.range n, MeasureTheory.condexp (↑ℱ i) μ (f (i + 1) - f i)

@[simp]

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

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

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

noncomputable def MeasureTheory.martingalePart {Ω : Type u_1} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {m0 : MeasurableSpace Ω} (f : ℕ → Ω → E) (ℱ : MeasureTheory.Filtration ℕ m0) (μ : MeasureTheory.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.

Equations

• MeasureTheory.martingalePart f ℱ μ n = f n - MeasureTheory.predictablePart f ℱ μ n

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

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

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

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

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

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

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

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