Documentation

Mathlib.Probability.Martingale.Centering

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 #

Main statements #

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
Instances For
    @[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.adapted_predictablePart {Ω : Type u_1} {E : Type u_2} {m0 : MeasurableSpace Ω} {μ : Measure Ω} [NormedAddCommGroup E] [NormedSpace E] [CompleteSpace E] {f : ΩE} {ℱ : Filtration m0} :
    Adapted fun (n : ) => predictablePart f μ (n + 1)
    theorem MeasureTheory.adapted_predictablePart' {Ω : Type u_1} {E : Type u_2} {m0 : MeasurableSpace Ω} {μ : Measure Ω} [NormedAddCommGroup E] [NormedSpace E] [CompleteSpace E] {f : ΩE} {ℱ : Filtration m0} :
    Adapted 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
    Instances For
      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 + iFinset.range n, (f (i + 1) - f i - condexp ( i) μ (f (i + 1) - f i))
      theorem MeasureTheory.adapted_martingalePart {Ω : Type u_1} {E : Type u_2} {m0 : MeasurableSpace Ω} {μ : Measure Ω} [NormedAddCommGroup E] [NormedSpace E] [CompleteSpace E] {f : ΩE} {ℱ : Filtration m0} (hf : Adapted f) :
      Adapted (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 : Adapted 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 : Adapted 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 : Adapted 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)