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.

Equations

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

@[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.predictablePart_add_one {Ω : Type u_1} {E : Type u_2} {m0 : MeasurableSpace Ω} {μ : Measure Ω} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {f : ℕ → Ω → E} {ℱ : Filtration ℕ m0} (n : ℕ) : predictablePart f ℱ μ (n + 1) = predictablePart f ℱ μ n + μ[f (n + 1) - f n | ↑ℱ n]

theorem MeasureTheory.predictablePart_smul {Ω : Type u_1} {E : Type u_2} {m0 : MeasurableSpace Ω} {μ : Measure Ω} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {f : ℕ → Ω → E} {ℱ : Filtration ℕ m0} (c : ℝ) (n : ℕ) : predictablePart (c • f) ℱ μ n =ᶠ[ae μ] c • predictablePart f ℱ μ n

theorem MeasureTheory.predictablePart_add {Ω : Type u_1} {E : Type u_2} {m0 : MeasurableSpace Ω} {μ : Measure Ω} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {f g : ℕ → Ω → E} {ℱ : Filtration ℕ m0} (hfint : ∀ (n : ℕ), Integrable (f n) μ) (hgint : ∀ (n : ℕ), Integrable (g n) μ) (n : ℕ) : predictablePart (f + g) ℱ μ n =ᶠ[ae μ] predictablePart f ℱ μ n + predictablePart g ℱ μ n

theorem MeasureTheory.Martingale.predictablePart_eq_zero {Ω : Type u_1} {E : Type u_2} {m0 : MeasurableSpace Ω} {μ : Measure Ω} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {f : ℕ → Ω → E} {ℱ : Filtration ℕ m0} (hf : Martingale f ℱ μ) (n : ℕ) : predictablePart f ℱ μ n =ᶠ[ae μ] 0

theorem MeasureTheory.Submartingale.monotone_predictablePart {Ω : Type u_1} {E : Type u_2} {m0 : MeasurableSpace Ω} {μ : Measure Ω} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {f : ℕ → Ω → E} {ℱ : Filtration ℕ m0} [PartialOrder E] [IsOrderedAddMonoid E] (hf : Submartingale f ℱ μ) : ∀ᵐ (ω : Ω) ∂μ, Monotone fun (x : ℕ) => predictablePart f ℱ μ x ω

theorem MeasureTheory.Submartingale.predictablePart_nonneg {Ω : Type u_1} {E : Type u_2} {m0 : MeasurableSpace Ω} {μ : Measure Ω} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {f : ℕ → Ω → E} {ℱ : Filtration ℕ m0} [PartialOrder E] [IsOrderedAddMonoid E] (hf : Submartingale f ℱ μ) : ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), 0 ≤ predictablePart f ℱ μ n ω

theorem MeasureTheory.IsPredictable.predictablePart_eq {Ω : Type u_1} {E : Type u_2} {m0 : MeasurableSpace Ω} {μ : Measure Ω} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {f : ℕ → Ω → E} {ℱ : Filtration ℕ m0} [SecondCountableTopology E] [MeasurableSpace E] [BorelSpace E] [SigmaFiniteFiltration μ ℱ] (hf : IsPredictable ℱ f) (hfint : ∀ (n : ℕ), Integrable (f n) μ) (n : ℕ) : predictablePart f ℱ μ n =ᶠ[ae μ] f n - f 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.isPredictable_predictablePart {Ω : Type u_1} {E : Type u_2} {m0 : MeasurableSpace Ω} {μ : Measure Ω} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {f : ℕ → Ω → E} {ℱ : Filtration ℕ m0} [SecondCountableTopology E] [MeasurableSpace E] [BorelSpace E] : IsPredictable ℱ (predictablePart f ℱ μ)

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.

Equations

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

@[simp]

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

theorem MeasureTheory.martingalePart_smul {Ω : Type u_1} {E : Type u_2} {m0 : MeasurableSpace Ω} {μ : Measure Ω} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {f : ℕ → Ω → E} {ℱ : Filtration ℕ m0} (c : ℝ) (n : ℕ) : martingalePart (c • f) ℱ μ n =ᶠ[ae μ] c • martingalePart f ℱ μ n

theorem MeasureTheory.martingalePart_add {Ω : Type u_1} {E : Type u_2} {m0 : MeasurableSpace Ω} {μ : Measure Ω} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {f g : ℕ → Ω → E} {ℱ : Filtration ℕ m0} (hfint : ∀ (n : ℕ), Integrable (f n) μ) (hgint : ∀ (n : ℕ), Integrable (g n) μ) (n : ℕ) : martingalePart (f + g) ℱ μ n =ᶠ[ae μ] martingalePart f ℱ μ n + martingalePart g ℱ μ n

theorem MeasureTheory.Martingale.martingalePart_eq {Ω : Type u_1} {E : Type u_2} {m0 : MeasurableSpace Ω} {μ : Measure Ω} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {f : ℕ → Ω → E} {ℱ : Filtration ℕ m0} (hf : Martingale f ℱ μ) (n : ℕ) : martingalePart f ℱ μ n =ᶠ[ae μ] f n

theorem MeasureTheory.IsPredictable.martingalePart_eq {Ω : Type u_1} {E : Type u_2} {m0 : MeasurableSpace Ω} {μ : Measure Ω} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {f : ℕ → Ω → E} {ℱ : Filtration ℕ m0} [SecondCountableTopology E] [MeasurableSpace E] [BorelSpace E] [SigmaFiniteFiltration μ ℱ] (hf : IsPredictable ℱ f) (hfint : ∀ (n : ℕ), Integrable (f n) μ) (n : ℕ) : martingalePart f ℱ μ n =ᶠ[ae μ] f 0

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)