mathlib3documentation

probability.martingale.centering

Centering lemma for stochastic processes #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 martingale_part f ℱ μ and predictable_part f ℱ μ.

Main definitions #

• measure_theory.predictable_part f ℱ μ: a predictable process such that f = predictable_part f ℱ μ + martingale_part f ℱ μ
• measure_theory.martingale_part f ℱ μ: a martingale such that f = predictable_part f ℱ μ + martingale_part f ℱ μ

Main statements #

• measure_theory.adapted_predictable_part: (λ n, predictable_part f ℱ μ (n+1)) is adapted. That is, predictable_part is predictable.
• measure_theory.martingale_martingale_part: martingale_part f ℱ μ is a martingale.
noncomputable def measure_theory.predictable_part {Ω : Type u_1} {E : Type u_2} [ E] {m0 : measurable_space Ω} (f : Ω E) (ℱ : m0) (μ : . "volume_tac") :
Ω E

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

Equations
@[simp]
theorem measure_theory.predictable_part_zero {Ω : Type u_1} {E : Type u_2} {m0 : measurable_space Ω} {μ : measure_theory.measure Ω} [ E] {f : Ω E} {ℱ : m0} :
= 0
theorem measure_theory.adapted_predictable_part {Ω : Type u_1} {E : Type u_2} {m0 : measurable_space Ω} {μ : measure_theory.measure Ω} [ E] {f : Ω E} {ℱ : m0} :
(λ (n : ), (n + 1))
theorem measure_theory.adapted_predictable_part' {Ω : Type u_1} {E : Type u_2} {m0 : measurable_space Ω} {μ : measure_theory.measure Ω} [ E] {f : Ω E} {ℱ : m0} :
(λ (n : ), n)
noncomputable def measure_theory.martingale_part {Ω : Type u_1} {E : Type u_2} [ E] {m0 : measurable_space Ω} (f : Ω E) (ℱ : m0) (μ : . "volume_tac") :
Ω E

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

Equations
theorem measure_theory.martingale_part_add_predictable_part {Ω : Type u_1} {E : Type u_2} {m0 : measurable_space Ω} [ E] (ℱ : m0) (μ : measure_theory.measure Ω) (f : Ω E) :
theorem measure_theory.martingale_part_eq_sum {Ω : Type u_1} {E : Type u_2} {m0 : measurable_space Ω} {μ : measure_theory.measure Ω} [ E] {f : Ω E} {ℱ : m0} :
= λ (n : ), f 0 + (finset.range n).sum (λ (i : ), f (i + 1) - f i - μ (f (i + 1) - f i))
theorem measure_theory.adapted_martingale_part {Ω : Type u_1} {E : Type u_2} {m0 : measurable_space Ω} {μ : measure_theory.measure Ω} [ E] {f : Ω E} {ℱ : m0} (hf : f) :
theorem measure_theory.integrable_martingale_part {Ω : Type u_1} {E : Type u_2} {m0 : measurable_space Ω} {μ : measure_theory.measure Ω} [ E] {f : Ω E} {ℱ : m0} (hf_int : (n : ), μ) (n : ) :
theorem measure_theory.martingale_martingale_part {Ω : Type u_1} {E : Type u_2} {m0 : measurable_space Ω} {μ : measure_theory.measure Ω} [ E] {f : Ω E} {ℱ : m0} (hf : f) (hf_int : (n : ), μ)  :
theorem measure_theory.martingale_part_add_ae_eq {Ω : Type u_1} {E : Type u_2} {m0 : measurable_space Ω} {μ : measure_theory.measure Ω} [ E] {ℱ : m0} {f g : Ω E} (hf : μ) (hg : (λ (n : ), g (n + 1))) (hg0 : g 0 = 0) (hgint : (n : ), μ) (n : ) :
μ n =ᵐ[μ] f n
theorem measure_theory.predictable_part_add_ae_eq {Ω : Type u_1} {E : Type u_2} {m0 : measurable_space Ω} {μ : measure_theory.measure Ω} [ E] {ℱ : m0} {f g : Ω E} (hf : μ) (hg : (λ (n : ), g (n + 1))) (hg0 : g 0 = 0) (hgint : (n : ), μ) (n : ) :
μ n =ᵐ[μ] g n
theorem measure_theory.predictable_part_bdd_difference {Ω : Type u_1} {m0 : measurable_space Ω} {μ : measure_theory.measure Ω} {R : nnreal} {f : Ω } (ℱ : m0) (hbdd : ∀ᵐ (ω : Ω) μ, (i : ), |f (i + 1) ω - f i ω| R) :
∀ᵐ (ω : Ω) μ, (i : ), | (i + 1) ω - ω| R
theorem measure_theory.martingale_part_bdd_difference {Ω : Type u_1} {m0 : measurable_space Ω} {μ : measure_theory.measure Ω} {R : nnreal} {f : Ω } (ℱ : m0) (hbdd : ∀ᵐ (ω : Ω) μ, (i : ), |f (i + 1) ω - f i ω| R) :
∀ᵐ (ω : Ω) μ, (i : ), | (i + 1) ω - ω| (2 * R)