mathlib3 documentation

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 #

Main statements #

noncomputable def measure_theory.predictable_part {Ω : Type u_1} {E : Type u_2} [normed_add_comm_group E] [normed_space E] [complete_space E] {m0 : measurable_space Ω} (f : Ω E) (ℱ : measure_theory.filtration m0) (μ : measure_theory.measure Ω . "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
noncomputable def measure_theory.martingale_part {Ω : Type u_1} {E : Type u_2} [normed_add_comm_group E] [normed_space E] [complete_space E] {m0 : measurable_space Ω} (f : Ω E) (ℱ : measure_theory.filtration m0) (μ : measure_theory.measure Ω . "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_eq_sum {Ω : Type u_1} {E : Type u_2} {m0 : measurable_space Ω} {μ : measure_theory.measure Ω} [normed_add_comm_group E] [normed_space E] [complete_space E] {f : Ω E} {ℱ : measure_theory.filtration m0} :
measure_theory.martingale_part f μ = λ (n : ), f 0 + (finset.range n).sum (λ (i : ), f (i + 1) - f i - measure_theory.condexp (ℱ i) μ (f (i + 1) - f i))
theorem measure_theory.martingale_part_add_ae_eq {Ω : Type u_1} {E : Type u_2} {m0 : measurable_space Ω} {μ : measure_theory.measure Ω} [normed_add_comm_group E] [normed_space E] [complete_space E] {ℱ : measure_theory.filtration m0} [measure_theory.sigma_finite_filtration μ ℱ] {f g : Ω E} (hf : measure_theory.martingale f μ) (hg : measure_theory.adapted (λ (n : ), g (n + 1))) (hg0 : g 0 = 0) (hgint : (n : ), measure_theory.integrable (g n) μ) (n : ) :
theorem measure_theory.predictable_part_add_ae_eq {Ω : Type u_1} {E : Type u_2} {m0 : measurable_space Ω} {μ : measure_theory.measure Ω} [normed_add_comm_group E] [normed_space E] [complete_space E] {ℱ : measure_theory.filtration m0} [measure_theory.sigma_finite_filtration μ ℱ] {f g : Ω E} (hf : measure_theory.martingale f μ) (hg : measure_theory.adapted (λ (n : ), g (n + 1))) (hg0 : g 0 = 0) (hgint : (n : ), measure_theory.integrable (g n) μ) (n : ) :
theorem measure_theory.predictable_part_bdd_difference {Ω : Type u_1} {m0 : measurable_space Ω} {μ : measure_theory.measure Ω} {R : nnreal} {f : Ω } (ℱ : measure_theory.filtration m0) (hbdd : ∀ᵐ (ω : Ω) μ, (i : ), |f (i + 1) ω - f i ω| R) :
∀ᵐ (ω : Ω) μ, (i : ), |measure_theory.predictable_part f μ (i + 1) ω - measure_theory.predictable_part f μ i ω| R
theorem measure_theory.martingale_part_bdd_difference {Ω : Type u_1} {m0 : measurable_space Ω} {μ : measure_theory.measure Ω} {R : nnreal} {f : Ω } (ℱ : measure_theory.filtration m0) (hbdd : ∀ᵐ (ω : Ω) μ, (i : ), |f (i + 1) ω - f i ω| R) :
∀ᵐ (ω : Ω) μ, (i : ), |measure_theory.martingale_part f μ (i + 1) ω - measure_theory.martingale_part f μ i ω| (2 * R)