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) (ℱ : MeasureTheory.Filtration m0) (μ : MeasureTheory.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]
    noncomputable def MeasureTheory.martingalePart {Ω : Type u_1} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace E] [CompleteSpace E] {m0 : MeasurableSpace Ω} (f : ΩE) (ℱ : MeasureTheory.Filtration m0) (μ : MeasureTheory.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_eq_sum {Ω : Type u_1} {E : Type u_2} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [NormedAddCommGroup E] [NormedSpace E] [CompleteSpace E] {f : ΩE} {ℱ : MeasureTheory.Filtration m0} :
      MeasureTheory.martingalePart f μ = fun (n : ) => f 0 + (Finset.range n).sum fun (i : ) => f (i + 1) - f i - MeasureTheory.condexp ( i) μ (f (i + 1) - f i)
      theorem MeasureTheory.martingalePart_add_ae_eq {Ω : Type u_1} {E : Type u_2} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [NormedAddCommGroup E] [NormedSpace E] [CompleteSpace E] {ℱ : MeasureTheory.Filtration m0} [MeasureTheory.SigmaFiniteFiltration μ ] {f : ΩE} {g : ΩE} (hf : MeasureTheory.Martingale f μ) (hg : MeasureTheory.Adapted fun (n : ) => g (n + 1)) (hg0 : g 0 = 0) (hgint : ∀ (n : ), MeasureTheory.Integrable (g n) μ) (n : ) :
      MeasureTheory.martingalePart (f + g) μ n =ᶠ[μ.ae] f n
      theorem MeasureTheory.predictablePart_add_ae_eq {Ω : Type u_1} {E : Type u_2} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [NormedAddCommGroup E] [NormedSpace E] [CompleteSpace E] {ℱ : MeasureTheory.Filtration m0} [MeasureTheory.SigmaFiniteFiltration μ ] {f : ΩE} {g : ΩE} (hf : MeasureTheory.Martingale f μ) (hg : MeasureTheory.Adapted fun (n : ) => g (n + 1)) (hg0 : g 0 = 0) (hgint : ∀ (n : ), MeasureTheory.Integrable (g n) μ) (n : ) :
      MeasureTheory.predictablePart (f + g) μ n =ᶠ[μ.ae] g n
      theorem MeasureTheory.predictablePart_bdd_difference {Ω : Type u_1} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {R : NNReal} {f : Ω} (ℱ : MeasureTheory.Filtration m0) (hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ), |f (i + 1) ω - f i ω| R) :
      ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ), |MeasureTheory.predictablePart f μ (i + 1) ω - MeasureTheory.predictablePart f μ i ω| R
      theorem MeasureTheory.martingalePart_bdd_difference {Ω : Type u_1} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {R : NNReal} {f : Ω} (ℱ : MeasureTheory.Filtration m0) (hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ), |f (i + 1) ω - f i ω| R) :
      ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ), |MeasureTheory.martingalePart f μ (i + 1) ω - MeasureTheory.martingalePart f μ i ω| (2 * R)