Increments independent of the past #
A process X adapted to a filtration ℱ has increments independent of the past if every
increment X t - X s, s ≤ t, is independent of ℱ s. This is how Brownian motion relative to a
filtration is defined, and it is the form in which a change of measure delivers independence. This
file derives the consequences that do not depend on the law of the increments.
Main declarations #
MeasureTheory.Adapted.indep_comap_sub_of_indep_comap_sub: increments independent of the past on[s, u]and on[u, t]give an increment independent of the past on[s, t].MeasureTheory.Adapted.hasIndepIncrements: increments independent of the past are independent increments in the sense ofProbabilityTheory.HasIndepIncrements.
theorem
MeasureTheory.Adapted.indep_comap_sub_of_indep_comap_sub
{Ω : Type u_1}
{ι : Type u_2}
{E : Type u_3}
{mΩ : MeasurableSpace Ω}
{μ : Measure Ω}
[Preorder ι]
{ℱ : Filtration ι mΩ}
[MeasurableSpace E]
{X : ι → Ω → E}
[AddGroup E]
[MeasurableAdd₂ E]
[MeasurableSub₂ E]
[IsZeroOrProbabilityMeasure μ]
(hX : Adapted ℱ X)
{s u t : ι}
(hsu : s ≤ u)
(h₁ : ProbabilityTheory.Indep (MeasurableSpace.comap (X u - X s) inferInstance) (↑ℱ s) μ)
(h₂ : ProbabilityTheory.Indep (MeasurableSpace.comap (X t - X u) inferInstance) (↑ℱ u) μ)
:
ProbabilityTheory.Indep (MeasurableSpace.comap (X t - X s) inferInstance) (↑ℱ s) μ
If the increment of an adapted process over [s, u] is independent of ℱ s and its
increment over [u, t] is independent of ℱ u, then its increment over [s, t] is independent
of ℱ s.
theorem
MeasureTheory.Adapted.hasIndepIncrements
{Ω : Type u_1}
{ι : Type u_2}
{E : Type u_3}
{mΩ : MeasurableSpace Ω}
{μ : Measure Ω}
[Preorder ι]
{ℱ : Filtration ι mΩ}
[MeasurableSpace E]
{X : ι → Ω → E}
[Sub E]
[MeasurableSub₂ E]
[IsProbabilityMeasure μ]
(hX : Adapted ℱ X)
(hindep : ∀ ⦃s t : ι⦄, s ≤ t → ProbabilityTheory.Indep (MeasurableSpace.comap (X t - X s) inferInstance) (↑ℱ s) μ)
:
A process adapted to ℱ whose increments X t - X s, s ≤ t, are independent of ℱ s has
independent increments.