Theorems · Definition · probability

MeasureTheory.predictablePart

{Ω : Type u_1} →
  {E : Type u_2} →
    [inst : NormedAddCommGroup E] →
      [NormedSpace ℝ E] →
        {m0 : MeasurableSpace Ω} → (ℕ → Ω → 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.

Defined in

Mathlib.Probability.Martingale.Centering

Cited by

23 results in Mathlib

Foundations

Depth 294 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedAddCommGroupNormedSpace