Stochastic processes with independent increments #
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.
Equivalently, for any monotone sequence (tₙ), the random variables (X tₙ₊₁ - X tₙ)
are independent.
Main definition #
HasIndepIncrements: A stochastic processX : T → Ω → Ehas independent increments if for anyn ≥ 1andt₁ ≤ ... ≤ tₙ, the random variablesX t₂ - X t₁, ..., X tₙ - X tₙ₋₁are independent.
Main statement #
hasIndepIncrements_iff_nat: A stochastic processX : T → Ω → Ehas independent increments if and only if for any monotone sequence(tₙ), the random variables(X tₙ₊₁ - X tₙ)are independent.
Tags #
independent increments
def
ProbabilityTheory.HasIndepIncrements
{T : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
{mΩ : MeasurableSpace Ω}
[Preorder T]
[MeasurableSpace E]
[Sub E]
(X : T → Ω → E)
(P : MeasureTheory.Measure Ω := by volume_tac)
:
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.
Equations
Instances For
theorem
ProbabilityTheory.HasIndepIncrements.nat
{T : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
{X : T → Ω → E}
[Preorder T]
[MeasurableSpace E]
[Sub E]
(hX : HasIndepIncrements X P)
{t : ℕ → T}
(ht : Monotone t)
:
theorem
ProbabilityTheory.HasIndepIncrements.of_nat
{T : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
{X : T → Ω → E}
[Preorder T]
[MeasurableSpace E]
[Sub E]
(h :
∀ (t : ℕ → T),
Monotone t →
Filter.EventuallyConst t Filter.atTop → iIndepFun (fun (i : ℕ) (ω : Ω) => X (t (i + 1)) ω - X (t i) ω) P)
:
theorem
ProbabilityTheory.hasIndepIncrements_iff_nat
{T : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
{X : T → Ω → E}
[Preorder T]
[MeasurableSpace E]
[Sub E]
:
theorem
ProbabilityTheory.HasIndepIncrements.indepFun_sub_sub
{T : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
{X : T → Ω → E}
[Preorder T]
[MeasurableSpace E]
[Sub E]
(hX : HasIndepIncrements X P)
{r s t : T}
(hrs : r ≤ s)
(hst : s ≤ t)
:
theorem
ProbabilityTheory.HasIndepIncrements.indepFun_eval_sub
{T : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
{X : T → Ω → E}
[Preorder T]
[MeasurableSpace E]
[SubNegZeroMonoid E]
(hX : HasIndepIncrements X P)
{r s t : T}
(hrs : r ≤ s)
(hst : s ≤ t)
(h : ∀ᵐ (ω : Ω) ∂P, X r ω = 0)
:
theorem
ProbabilityTheory.HasIndepIncrements.map'
{T : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
{X : T → Ω → E}
[Preorder T]
[MeasurableSpace E]
{F : Type u_4}
{G : Type u_5}
[MeasurableSpace G]
[FunLike F E G]
[AddGroup E]
[SubtractionMonoid G]
[AddMonoidHomClass F E G]
{f : F}
(hf : Measurable ⇑f)
(hX : HasIndepIncrements X P)
:
HasIndepIncrements (fun (t : T) (ω : Ω) => f (X t ω)) P
theorem
ProbabilityTheory.HasIndepIncrements.map
{T : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
{X : T → Ω → E}
[Preorder T]
[MeasurableSpace E]
{R : Type u_4}
{F : Type u_5}
[Semiring R]
[SeminormedAddCommGroup E]
[Module R E]
[OpensMeasurableSpace E]
[SeminormedAddCommGroup F]
[Module R F]
[MeasurableSpace F]
[BorelSpace F]
(L : E →L[R] F)
(hX : HasIndepIncrements X P)
:
HasIndepIncrements (fun (t : T) (ω : Ω) => L (X t ω)) P
theorem
ProbabilityTheory.HasIndepIncrements.smul
{T : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
{X : T → Ω → E}
[Preorder T]
[MeasurableSpace E]
{R : Type u_4}
[AddGroup E]
[DistribSMul R E]
[MeasurableConstSMul R E]
(hX : HasIndepIncrements X P)
(c : R)
:
HasIndepIncrements (fun (t : T) (ω : Ω) => c • X t ω) P
theorem
ProbabilityTheory.HasIndepIncrements.neg
{T : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
{X : T → Ω → E}
[Preorder T]
[MeasurableSpace E]
[AddCommGroup E]
[MeasurableNeg E]
(hX : HasIndepIncrements X P)
:
HasIndepIncrements (-X) P