Theorems · Definition · probability

ProbabilityTheory.HasIndepIncrements

{T : Type u_1} →
  {Ω : Type u_2} →
    {E : Type u_3} →
      {mΩ : MeasurableSpace Ω} →
        [Preorder T] →
          [MeasurableSpace E] →
            [Sub E] →
              (T → Ω → E) → autoParam (MeasureTheory.Measure Ω) ProbabilityTheory.HasIndepIncrements._auto_1 → Prop

A stochastic process X : T → Ω → E has independent increments if for any n ≥ 1 and t₁ ≤ ... ≤ tₙ, the random variables X t₂ - X t₁, ..., X tₙ - X tₙ₋₁ are independent. Although this corresponds to the standard definition, dealing with Fin might make things complicated in some cases. Therefore we provide HasIndepIncrements.of_nat which instead requires to prove that for any monotone sequence (tₙ) that is eventually constant, the random variables X tₙ₊₁ - X tₙ are independent.

Defined in

Mathlib.Probability.Independence.Process.HasIndepIncrements.Basic

Cited by

12 results in Mathlib

Foundations

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

Assumes

PreorderMeasurableSpaceSub