Adapted and progressively measurable processes #
This file defines some standard definition from the theory of stochastic processes including filtrations and stopping times. These definitions are used to model the amount of information at a specific time and are the first step in formalizing stochastic processes.
Main definitions #
MeasureTheory.Adapted: a sequence of functionsuis said to be adapted to a filtrationfif at each point in timei,u iisf i-strongly measurableMeasureTheory.ProgMeasurable: a sequence of functionsuis said to be progressively measurable with respect to a filtrationfif at each point in timei,urestricted toSet.Iic i × Ωis strongly measurable with respect to the productMeasurableSpacestructure where the σ-algebra used forΩisf i.
Main results #
Adapted.progMeasurable_of_continuous: a continuous adapted process is progressively measurable.
Tags #
adapted, progressively measurable
def
MeasureTheory.Adapted
{Ω : Type u_1}
{β : Type u_2}
{ι : Type u_3}
{m : MeasurableSpace Ω}
[TopologicalSpace β]
[Preorder ι]
(f : MeasureTheory.Filtration ι m)
(u : ι → Ω → β)
:
A sequence of functions u is adapted to a filtration f if for all i,
u i is f i-measurable.
Equations
- MeasureTheory.Adapted f u = ∀ (i : ι), MeasureTheory.StronglyMeasurable (u i)
Instances For
theorem
MeasureTheory.Adapted.mul
{Ω : Type u_1}
{β : Type u_2}
{ι : Type u_3}
{m : MeasurableSpace Ω}
[TopologicalSpace β]
[Preorder ι]
{u : ι → Ω → β}
{v : ι → Ω → β}
{f : MeasureTheory.Filtration ι m}
[Mul β]
[ContinuousMul β]
(hu : MeasureTheory.Adapted f u)
(hv : MeasureTheory.Adapted f v)
:
MeasureTheory.Adapted f (u * v)
theorem
MeasureTheory.Adapted.add
{Ω : Type u_1}
{β : Type u_2}
{ι : Type u_3}
{m : MeasurableSpace Ω}
[TopologicalSpace β]
[Preorder ι]
{u : ι → Ω → β}
{v : ι → Ω → β}
{f : MeasureTheory.Filtration ι m}
[Add β]
[ContinuousAdd β]
(hu : MeasureTheory.Adapted f u)
(hv : MeasureTheory.Adapted f v)
:
MeasureTheory.Adapted f (u + v)
theorem
MeasureTheory.Adapted.div
{Ω : Type u_1}
{β : Type u_2}
{ι : Type u_3}
{m : MeasurableSpace Ω}
[TopologicalSpace β]
[Preorder ι]
{u : ι → Ω → β}
{v : ι → Ω → β}
{f : MeasureTheory.Filtration ι m}
[Div β]
[ContinuousDiv β]
(hu : MeasureTheory.Adapted f u)
(hv : MeasureTheory.Adapted f v)
:
MeasureTheory.Adapted f (u / v)
theorem
MeasureTheory.Adapted.sub
{Ω : Type u_1}
{β : Type u_2}
{ι : Type u_3}
{m : MeasurableSpace Ω}
[TopologicalSpace β]
[Preorder ι]
{u : ι → Ω → β}
{v : ι → Ω → β}
{f : MeasureTheory.Filtration ι m}
[Sub β]
[ContinuousSub β]
(hu : MeasureTheory.Adapted f u)
(hv : MeasureTheory.Adapted f v)
:
MeasureTheory.Adapted f (u - v)
theorem
MeasureTheory.Adapted.inv
{Ω : Type u_1}
{β : Type u_2}
{ι : Type u_3}
{m : MeasurableSpace Ω}
[TopologicalSpace β]
[Preorder ι]
{u : ι → Ω → β}
{f : MeasureTheory.Filtration ι m}
[Group β]
[TopologicalGroup β]
(hu : MeasureTheory.Adapted f u)
:
theorem
MeasureTheory.Adapted.neg
{Ω : Type u_1}
{β : Type u_2}
{ι : Type u_3}
{m : MeasurableSpace Ω}
[TopologicalSpace β]
[Preorder ι]
{u : ι → Ω → β}
{f : MeasureTheory.Filtration ι m}
[AddGroup β]
[TopologicalAddGroup β]
(hu : MeasureTheory.Adapted f u)
:
MeasureTheory.Adapted f (-u)
theorem
MeasureTheory.Adapted.smul
{Ω : Type u_1}
{β : Type u_2}
{ι : Type u_3}
{m : MeasurableSpace Ω}
[TopologicalSpace β]
[Preorder ι]
{u : ι → Ω → β}
{f : MeasureTheory.Filtration ι m}
[SMul ℝ β]
[ContinuousSMul ℝ β]
(c : ℝ)
(hu : MeasureTheory.Adapted f u)
:
MeasureTheory.Adapted f (c • u)
theorem
MeasureTheory.Adapted.stronglyMeasurable
{Ω : Type u_1}
{β : Type u_2}
{ι : Type u_3}
{m : MeasurableSpace Ω}
[TopologicalSpace β]
[Preorder ι]
{u : ι → Ω → β}
{f : MeasureTheory.Filtration ι m}
{i : ι}
(hf : MeasureTheory.Adapted f u)
:
theorem
MeasureTheory.Adapted.stronglyMeasurable_le
{Ω : Type u_1}
{β : Type u_2}
{ι : Type u_3}
{m : MeasurableSpace Ω}
[TopologicalSpace β]
[Preorder ι]
{u : ι → Ω → β}
{f : MeasureTheory.Filtration ι m}
{i : ι}
{j : ι}
(hf : MeasureTheory.Adapted f u)
(hij : i ≤ j)
:
theorem
MeasureTheory.adapted_const
{Ω : Type u_1}
{β : Type u_2}
{ι : Type u_3}
{m : MeasurableSpace Ω}
[TopologicalSpace β]
[Preorder ι]
(f : MeasureTheory.Filtration ι m)
(x : β)
:
MeasureTheory.Adapted f fun (x_1 : ι) (x_2 : Ω) => x
theorem
MeasureTheory.adapted_zero
{Ω : Type u_1}
(β : Type u_2)
{ι : Type u_3}
{m : MeasurableSpace Ω}
[TopologicalSpace β]
[Preorder ι]
[Zero β]
(f : MeasureTheory.Filtration ι m)
:
theorem
MeasureTheory.Filtration.adapted_natural
{Ω : Type u_1}
{β : Type u_2}
{ι : Type u_3}
{m : MeasurableSpace Ω}
[TopologicalSpace β]
[Preorder ι]
[TopologicalSpace.MetrizableSpace β]
[mβ : MeasurableSpace β]
[BorelSpace β]
{u : ι → Ω → β}
(hum : ∀ (i : ι), MeasureTheory.StronglyMeasurable (u i))
:
def
MeasureTheory.ProgMeasurable
{Ω : Type u_1}
{β : Type u_2}
{ι : Type u_3}
{m : MeasurableSpace Ω}
[TopologicalSpace β]
[Preorder ι]
[MeasurableSpace ι]
(f : MeasureTheory.Filtration ι m)
(u : ι → Ω → β)
:
Progressively measurable process. A sequence of functions u is said to be progressively
measurable with respect to a filtration f if at each point in time i, u restricted to
Set.Iic i × Ω is measurable with respect to the product MeasurableSpace structure where the
σ-algebra used for Ω is f i.
The usual definition uses the interval [0,i], which we replace by Set.Iic i. We recover the
usual definition for index types ℝ≥0 or ℕ.
Equations
- MeasureTheory.ProgMeasurable f u = ∀ (i : ι), MeasureTheory.StronglyMeasurable fun (p : ↑(Set.Iic i) × Ω) => u (↑p.1) p.2
Instances For
theorem
MeasureTheory.progMeasurable_const
{Ω : Type u_1}
{β : Type u_2}
{ι : Type u_3}
{m : MeasurableSpace Ω}
[TopologicalSpace β]
[Preorder ι]
[MeasurableSpace ι]
(f : MeasureTheory.Filtration ι m)
(b : β)
:
MeasureTheory.ProgMeasurable f fun (x : ι) (x : Ω) => b
theorem
MeasureTheory.ProgMeasurable.adapted
{Ω : Type u_1}
{β : Type u_2}
{ι : Type u_3}
{m : MeasurableSpace Ω}
[TopologicalSpace β]
[Preorder ι]
{u : ι → Ω → β}
{f : MeasureTheory.Filtration ι m}
[MeasurableSpace ι]
(h : MeasureTheory.ProgMeasurable f u)
:
theorem
MeasureTheory.ProgMeasurable.comp
{Ω : Type u_1}
{β : Type u_2}
{ι : Type u_3}
{m : MeasurableSpace Ω}
[TopologicalSpace β]
[Preorder ι]
{u : ι → Ω → β}
{f : MeasureTheory.Filtration ι m}
[MeasurableSpace ι]
{t : ι → Ω → ι}
[TopologicalSpace ι]
[BorelSpace ι]
[TopologicalSpace.MetrizableSpace ι]
(h : MeasureTheory.ProgMeasurable f u)
(ht : MeasureTheory.ProgMeasurable f t)
(ht_le : ∀ (i : ι) (ω : Ω), t i ω ≤ i)
:
MeasureTheory.ProgMeasurable f fun (i : ι) (ω : Ω) => u (t i ω) ω
theorem
MeasureTheory.ProgMeasurable.mul
{Ω : Type u_1}
{β : Type u_2}
{ι : Type u_3}
{m : MeasurableSpace Ω}
[TopologicalSpace β]
[Preorder ι]
{u : ι → Ω → β}
{v : ι → Ω → β}
{f : MeasureTheory.Filtration ι m}
[MeasurableSpace ι]
[Mul β]
[ContinuousMul β]
(hu : MeasureTheory.ProgMeasurable f u)
(hv : MeasureTheory.ProgMeasurable f v)
:
MeasureTheory.ProgMeasurable f fun (i : ι) (ω : Ω) => u i ω * v i ω
theorem
MeasureTheory.ProgMeasurable.add
{Ω : Type u_1}
{β : Type u_2}
{ι : Type u_3}
{m : MeasurableSpace Ω}
[TopologicalSpace β]
[Preorder ι]
{u : ι → Ω → β}
{v : ι → Ω → β}
{f : MeasureTheory.Filtration ι m}
[MeasurableSpace ι]
[Add β]
[ContinuousAdd β]
(hu : MeasureTheory.ProgMeasurable f u)
(hv : MeasureTheory.ProgMeasurable f v)
:
MeasureTheory.ProgMeasurable f fun (i : ι) (ω : Ω) => u i ω + v i ω
theorem
MeasureTheory.ProgMeasurable.finset_prod'
{Ω : Type u_1}
{β : Type u_2}
{ι : Type u_3}
{m : MeasurableSpace Ω}
[TopologicalSpace β]
[Preorder ι]
{f : MeasureTheory.Filtration ι m}
[MeasurableSpace ι]
{γ : Type u_4}
[CommMonoid β]
[ContinuousMul β]
{U : γ → ι → Ω → β}
{s : Finset γ}
(h : ∀ c ∈ s, MeasureTheory.ProgMeasurable f (U c))
:
MeasureTheory.ProgMeasurable f (∏ c ∈ s, U c)
theorem
MeasureTheory.ProgMeasurable.finset_sum'
{Ω : Type u_1}
{β : Type u_2}
{ι : Type u_3}
{m : MeasurableSpace Ω}
[TopologicalSpace β]
[Preorder ι]
{f : MeasureTheory.Filtration ι m}
[MeasurableSpace ι]
{γ : Type u_4}
[AddCommMonoid β]
[ContinuousAdd β]
{U : γ → ι → Ω → β}
{s : Finset γ}
(h : ∀ c ∈ s, MeasureTheory.ProgMeasurable f (U c))
:
MeasureTheory.ProgMeasurable f (∑ c ∈ s, U c)
theorem
MeasureTheory.ProgMeasurable.finset_prod
{Ω : Type u_1}
{β : Type u_2}
{ι : Type u_3}
{m : MeasurableSpace Ω}
[TopologicalSpace β]
[Preorder ι]
{f : MeasureTheory.Filtration ι m}
[MeasurableSpace ι]
{γ : Type u_4}
[CommMonoid β]
[ContinuousMul β]
{U : γ → ι → Ω → β}
{s : Finset γ}
(h : ∀ c ∈ s, MeasureTheory.ProgMeasurable f (U c))
:
MeasureTheory.ProgMeasurable f fun (i : ι) (a : Ω) => ∏ c ∈ s, U c i a
theorem
MeasureTheory.ProgMeasurable.finset_sum
{Ω : Type u_1}
{β : Type u_2}
{ι : Type u_3}
{m : MeasurableSpace Ω}
[TopologicalSpace β]
[Preorder ι]
{f : MeasureTheory.Filtration ι m}
[MeasurableSpace ι]
{γ : Type u_4}
[AddCommMonoid β]
[ContinuousAdd β]
{U : γ → ι → Ω → β}
{s : Finset γ}
(h : ∀ c ∈ s, MeasureTheory.ProgMeasurable f (U c))
:
MeasureTheory.ProgMeasurable f fun (i : ι) (a : Ω) => ∑ c ∈ s, U c i a
theorem
MeasureTheory.ProgMeasurable.inv
{Ω : Type u_1}
{β : Type u_2}
{ι : Type u_3}
{m : MeasurableSpace Ω}
[TopologicalSpace β]
[Preorder ι]
{u : ι → Ω → β}
{f : MeasureTheory.Filtration ι m}
[MeasurableSpace ι]
[Group β]
[TopologicalGroup β]
(hu : MeasureTheory.ProgMeasurable f u)
:
MeasureTheory.ProgMeasurable f fun (i : ι) (ω : Ω) => (u i ω)⁻¹
theorem
MeasureTheory.ProgMeasurable.neg
{Ω : Type u_1}
{β : Type u_2}
{ι : Type u_3}
{m : MeasurableSpace Ω}
[TopologicalSpace β]
[Preorder ι]
{u : ι → Ω → β}
{f : MeasureTheory.Filtration ι m}
[MeasurableSpace ι]
[AddGroup β]
[TopologicalAddGroup β]
(hu : MeasureTheory.ProgMeasurable f u)
:
MeasureTheory.ProgMeasurable f fun (i : ι) (ω : Ω) => -u i ω
theorem
MeasureTheory.ProgMeasurable.div
{Ω : Type u_1}
{β : Type u_2}
{ι : Type u_3}
{m : MeasurableSpace Ω}
[TopologicalSpace β]
[Preorder ι]
{u : ι → Ω → β}
{v : ι → Ω → β}
{f : MeasureTheory.Filtration ι m}
[MeasurableSpace ι]
[Group β]
[TopologicalGroup β]
(hu : MeasureTheory.ProgMeasurable f u)
(hv : MeasureTheory.ProgMeasurable f v)
:
MeasureTheory.ProgMeasurable f fun (i : ι) (ω : Ω) => u i ω / v i ω
theorem
MeasureTheory.ProgMeasurable.sub
{Ω : Type u_1}
{β : Type u_2}
{ι : Type u_3}
{m : MeasurableSpace Ω}
[TopologicalSpace β]
[Preorder ι]
{u : ι → Ω → β}
{v : ι → Ω → β}
{f : MeasureTheory.Filtration ι m}
[MeasurableSpace ι]
[AddGroup β]
[TopologicalAddGroup β]
(hu : MeasureTheory.ProgMeasurable f u)
(hv : MeasureTheory.ProgMeasurable f v)
:
MeasureTheory.ProgMeasurable f fun (i : ι) (ω : Ω) => u i ω - v i ω
theorem
MeasureTheory.progMeasurable_of_tendsto'
{Ω : Type u_1}
{β : Type u_2}
{ι : Type u_3}
{m : MeasurableSpace Ω}
[TopologicalSpace β]
[Preorder ι]
{u : ι → Ω → β}
{f : MeasureTheory.Filtration ι m}
{γ : Type u_4}
[MeasurableSpace ι]
[TopologicalSpace.PseudoMetrizableSpace β]
(fltr : Filter γ)
[fltr.NeBot]
[fltr.IsCountablyGenerated]
{U : γ → ι → Ω → β}
(h : ∀ (l : γ), MeasureTheory.ProgMeasurable f (U l))
(h_tendsto : Filter.Tendsto U fltr (nhds u))
:
theorem
MeasureTheory.progMeasurable_of_tendsto
{Ω : Type u_1}
{β : Type u_2}
{ι : Type u_3}
{m : MeasurableSpace Ω}
[TopologicalSpace β]
[Preorder ι]
{u : ι → Ω → β}
{f : MeasureTheory.Filtration ι m}
[MeasurableSpace ι]
[TopologicalSpace.PseudoMetrizableSpace β]
{U : ℕ → ι → Ω → β}
(h : ∀ (l : ℕ), MeasureTheory.ProgMeasurable f (U l))
(h_tendsto : Filter.Tendsto U Filter.atTop (nhds u))
:
theorem
MeasureTheory.Adapted.progMeasurable_of_continuous
{Ω : Type u_1}
{β : Type u_2}
{ι : Type u_3}
{m : MeasurableSpace Ω}
[TopologicalSpace β]
[Preorder ι]
{u : ι → Ω → β}
{f : MeasureTheory.Filtration ι m}
[TopologicalSpace ι]
[TopologicalSpace.MetrizableSpace ι]
[SecondCountableTopology ι]
[MeasurableSpace ι]
[OpensMeasurableSpace ι]
[TopologicalSpace.PseudoMetrizableSpace β]
(h : MeasureTheory.Adapted f u)
(hu_cont : ∀ (ω : Ω), Continuous fun (i : ι) => u i ω)
:
A continuous and adapted process is progressively measurable.
theorem
MeasureTheory.Adapted.progMeasurable_of_discrete
{Ω : Type u_1}
{β : Type u_2}
{ι : Type u_3}
{m : MeasurableSpace Ω}
[TopologicalSpace β]
[Preorder ι]
{u : ι → Ω → β}
{f : MeasureTheory.Filtration ι m}
[TopologicalSpace ι]
[DiscreteTopology ι]
[SecondCountableTopology ι]
[MeasurableSpace ι]
[OpensMeasurableSpace ι]
[TopologicalSpace.PseudoMetrizableSpace β]
(h : MeasureTheory.Adapted f u)
:
For filtrations indexed by a discrete order, Adapted and ProgMeasurable are equivalent.
This lemma provides Adapted f u → ProgMeasurable f u.
See ProgMeasurable.adapted for the reverse direction, which is true more generally.
theorem
MeasureTheory.Predictable.adapted
{Ω : Type u_1}
{β : Type u_2}
{m : MeasurableSpace Ω}
[TopologicalSpace β]
{f : MeasureTheory.Filtration ℕ m}
{u : ℕ → Ω → β}
(hu : MeasureTheory.Adapted f fun (n : ℕ) => u (n + 1))
(hu0 : MeasureTheory.StronglyMeasurable (u 0))
: