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 thatf = predictable_part f ℱ μ + martingale_part f ℱ μmeasure_theory.martingale_part f ℱ μ: a martingale such thatf = predictable_part f ℱ μ + martingale_part f ℱ μ
Main statements #
measure_theory.adapted_predictable_part:(λ n, predictable_part f ℱ μ (n+1))is adapted. That is,predictable_partis 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}
[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") :
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
- measure_theory.predictable_part f ℱ μ = λ (n : ℕ), (finset.range n).sum (λ (i : ℕ), measure_theory.condexp (⇑ℱ i) μ (f (i + 1) - f i))
@[simp]
theorem
measure_theory.predictable_part_zero
{Ω : 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.predictable_part f ℱ μ 0 = 0
theorem
measure_theory.adapted_predictable_part
{Ω : 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.adapted ℱ (λ (n : ℕ), measure_theory.predictable_part f ℱ μ (n + 1))
theorem
measure_theory.adapted_predictable_part'
{Ω : 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.adapted ℱ (λ (n : ℕ), measure_theory.predictable_part f ℱ μ n)
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") :
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
- measure_theory.martingale_part f ℱ μ = λ (n : ℕ), f n - measure_theory.predictable_part f ℱ μ n
theorem
measure_theory.martingale_part_add_predictable_part
{Ω : Type u_1}
{E : Type u_2}
{m0 : measurable_space Ω}
[normed_add_comm_group E]
[normed_space ℝ E]
[complete_space E]
(ℱ : measure_theory.filtration ℕ m0)
(μ : measure_theory.measure Ω)
(f : ℕ → Ω → E) :
measure_theory.martingale_part f ℱ μ + measure_theory.predictable_part f ℱ μ = f
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.adapted_martingale_part
{Ω : 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}
(hf : measure_theory.adapted ℱ f) :
theorem
measure_theory.integrable_martingale_part
{Ω : 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}
(hf_int : ∀ (n : ℕ), measure_theory.integrable (f n) μ)
(n : ℕ) :
theorem
measure_theory.martingale_martingale_part
{Ω : 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}
(hf : measure_theory.adapted ℱ f)
(hf_int : ∀ (n : ℕ), measure_theory.integrable (f n) μ)
[measure_theory.sigma_finite_filtration μ ℱ] :
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 : ℕ) :
measure_theory.martingale_part (f + g) ℱ μ n =ᵐ[μ] f 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 : ℕ) :
measure_theory.predictable_part (f + g) ℱ μ n =ᵐ[μ] g n