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}
{m : MeasurableSpace Ω}
[Preorder ι]
{β : ι → Type u_3}
[(i : ι) → TopologicalSpace (β i)]
(f : Filtration ι m)
(u : (i : ι) → Ω → β i)
:
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}
{m : MeasurableSpace Ω}
[Preorder ι]
{f : Filtration ι m}
{β : ι → Type u_3}
[(i : ι) → TopologicalSpace (β i)]
{u v : (i : ι) → Ω → β i}
[(i : ι) → Mul (β i)]
[∀ (i : ι), ContinuousMul (β i)]
(hu : Adapted f u)
(hv : Adapted f v)
:
theorem
MeasureTheory.Adapted.add
{Ω : Type u_1}
{ι : Type u_2}
{m : MeasurableSpace Ω}
[Preorder ι]
{f : Filtration ι m}
{β : ι → Type u_3}
[(i : ι) → TopologicalSpace (β i)]
{u v : (i : ι) → Ω → β i}
[(i : ι) → Add (β i)]
[∀ (i : ι), ContinuousAdd (β i)]
(hu : Adapted f u)
(hv : Adapted f v)
:
theorem
MeasureTheory.Adapted.div
{Ω : Type u_1}
{ι : Type u_2}
{m : MeasurableSpace Ω}
[Preorder ι]
{f : Filtration ι m}
{β : ι → Type u_3}
[(i : ι) → TopologicalSpace (β i)]
{u v : (i : ι) → Ω → β i}
[(i : ι) → Div (β i)]
[∀ (i : ι), ContinuousDiv (β i)]
(hu : Adapted f u)
(hv : Adapted f v)
:
theorem
MeasureTheory.Adapted.sub
{Ω : Type u_1}
{ι : Type u_2}
{m : MeasurableSpace Ω}
[Preorder ι]
{f : Filtration ι m}
{β : ι → Type u_3}
[(i : ι) → TopologicalSpace (β i)]
{u v : (i : ι) → Ω → β i}
[(i : ι) → Sub (β i)]
[∀ (i : ι), ContinuousSub (β i)]
(hu : Adapted f u)
(hv : Adapted f v)
:
theorem
MeasureTheory.Adapted.inv
{Ω : Type u_1}
{ι : Type u_2}
{m : MeasurableSpace Ω}
[Preorder ι]
{f : Filtration ι m}
{β : ι → Type u_3}
[(i : ι) → TopologicalSpace (β i)]
{u : (i : ι) → Ω → β i}
[(i : ι) → Group (β i)]
[∀ (i : ι), ContinuousInv (β i)]
(hu : Adapted f u)
:
theorem
MeasureTheory.Adapted.neg
{Ω : Type u_1}
{ι : Type u_2}
{m : MeasurableSpace Ω}
[Preorder ι]
{f : Filtration ι m}
{β : ι → Type u_3}
[(i : ι) → TopologicalSpace (β i)]
{u : (i : ι) → Ω → β i}
[(i : ι) → AddGroup (β i)]
[∀ (i : ι), ContinuousNeg (β i)]
(hu : Adapted f u)
:
theorem
MeasureTheory.Adapted.smul
{Ω : Type u_1}
{ι : Type u_2}
{m : MeasurableSpace Ω}
[Preorder ι]
{f : Filtration ι m}
{β : ι → Type u_3}
[(i : ι) → TopologicalSpace (β i)]
{u : (i : ι) → Ω → β i}
[(i : ι) → SMul ℝ (β i)]
[∀ (i : ι), ContinuousConstSMul ℝ (β i)]
(c : ℝ)
(hu : Adapted f u)
:
theorem
MeasureTheory.Adapted.stronglyMeasurable
{Ω : Type u_1}
{ι : Type u_2}
{m : MeasurableSpace Ω}
[Preorder ι]
{f : Filtration ι m}
{β : ι → Type u_3}
[(i : ι) → TopologicalSpace (β i)]
{u : (i : ι) → Ω → β i}
{i : ι}
(hf : Adapted f u)
:
StronglyMeasurable (u i)
theorem
MeasureTheory.Adapted.stronglyMeasurable_le
{Ω : Type u_1}
{ι : Type u_2}
{m : MeasurableSpace Ω}
[Preorder ι]
{f : Filtration ι m}
{β : ι → Type u_3}
[(i : ι) → TopologicalSpace (β i)]
{u : (i : ι) → Ω → β i}
{i j : ι}
(hf : Adapted f u)
(hij : i ≤ j)
:
StronglyMeasurable (u i)
theorem
MeasureTheory.adapted_const'
{Ω : Type u_1}
{ι : Type u_2}
{m : MeasurableSpace Ω}
[Preorder ι]
{β : ι → Type u_3}
[(i : ι) → TopologicalSpace (β i)]
(f : Filtration ι m)
(x : (i : ι) → β i)
:
Adapted f fun (i : ι) (x_1 : Ω) => x i
theorem
MeasureTheory.adapted_const
{Ω : Type u_1}
{ι : Type u_2}
{m : MeasurableSpace Ω}
[Preorder ι]
{β : Type u_4}
[TopologicalSpace β]
(f : Filtration ι m)
(x : β)
:
Adapted f fun (x_1 : ι) (x_2 : Ω) => x
theorem
MeasureTheory.adapted_zero'
{Ω : Type u_1}
{ι : Type u_2}
{m : MeasurableSpace Ω}
[Preorder ι]
(β : ι → Type u_3)
[(i : ι) → TopologicalSpace (β i)]
[(i : ι) → Zero (β i)]
(f : Filtration ι m)
:
Adapted f 0
theorem
MeasureTheory.adapted_zero
{Ω : Type u_1}
{ι : Type u_2}
{m : MeasurableSpace Ω}
[Preorder ι]
(β : Type u_4)
[TopologicalSpace β]
[Zero β]
(f : Filtration ι m)
:
Adapted f 0
theorem
MeasureTheory.Filtration.adapted_natural
{Ω : Type u_1}
{ι : Type u_2}
{m : MeasurableSpace Ω}
[Preorder ι]
{β : ι → Type u_3}
[(i : ι) → TopologicalSpace (β i)]
{u : (i : ι) → Ω → β i}
[∀ (i : ι), TopologicalSpace.MetrizableSpace (β i)]
[mβ : (i : ι) → MeasurableSpace (β i)]
[∀ (i : ι), BorelSpace (β i)]
(hum : ∀ (i : ι), StronglyMeasurable (u i))
:
def
MeasureTheory.ProgMeasurable
{Ω : Type u_1}
{ι : Type u_2}
{m : MeasurableSpace Ω}
[Preorder ι]
{β : Type u_3}
[TopologicalSpace β]
[MeasurableSpace ι]
(f : 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}
{m : MeasurableSpace Ω}
[Preorder ι]
{β : Type u_3}
[TopologicalSpace β]
[MeasurableSpace ι]
(f : Filtration ι m)
(b : β)
:
ProgMeasurable f fun (x : ι) (x_1 : Ω) => b
theorem
MeasureTheory.ProgMeasurable.adapted
{Ω : Type u_1}
{ι : Type u_2}
{m : MeasurableSpace Ω}
[Preorder ι]
{f : Filtration ι m}
{β : Type u_3}
[TopologicalSpace β]
{u : ι → Ω → β}
[MeasurableSpace ι]
(h : ProgMeasurable f u)
:
Adapted f u
theorem
MeasureTheory.ProgMeasurable.comp
{Ω : Type u_1}
{ι : Type u_2}
{m : MeasurableSpace Ω}
[Preorder ι]
{f : Filtration ι m}
{β : Type u_3}
[TopologicalSpace β]
{u : ι → Ω → β}
[MeasurableSpace ι]
{t : ι → Ω → ι}
[TopologicalSpace ι]
[BorelSpace ι]
[TopologicalSpace.PseudoMetrizableSpace ι]
(h : ProgMeasurable f u)
(ht : ProgMeasurable f t)
(ht_le : ∀ (i : ι) (ω : Ω), t i ω ≤ i)
:
ProgMeasurable f fun (i : ι) (ω : Ω) => u (t i ω) ω
theorem
MeasureTheory.ProgMeasurable.mul
{Ω : Type u_1}
{ι : Type u_2}
{m : MeasurableSpace Ω}
[Preorder ι]
{f : Filtration ι m}
{β : Type u_3}
[TopologicalSpace β]
{u v : ι → Ω → β}
[MeasurableSpace ι]
[Mul β]
[ContinuousMul β]
(hu : ProgMeasurable f u)
(hv : ProgMeasurable f v)
:
ProgMeasurable f fun (i : ι) (ω : Ω) => u i ω * v i ω
theorem
MeasureTheory.ProgMeasurable.add
{Ω : Type u_1}
{ι : Type u_2}
{m : MeasurableSpace Ω}
[Preorder ι]
{f : Filtration ι m}
{β : Type u_3}
[TopologicalSpace β]
{u v : ι → Ω → β}
[MeasurableSpace ι]
[Add β]
[ContinuousAdd β]
(hu : ProgMeasurable f u)
(hv : ProgMeasurable f v)
:
ProgMeasurable f fun (i : ι) (ω : Ω) => u i ω + v i ω
theorem
MeasureTheory.ProgMeasurable.finset_prod'
{Ω : Type u_1}
{ι : Type u_2}
{m : MeasurableSpace Ω}
[Preorder ι]
{f : Filtration ι m}
{β : Type u_3}
[TopologicalSpace β]
[MeasurableSpace ι]
{γ : Type u_4}
[CommMonoid β]
[ContinuousMul β]
{U : γ → ι → Ω → β}
{s : Finset γ}
(h : ∀ c ∈ s, ProgMeasurable f (U c))
:
ProgMeasurable f (∏ c ∈ s, U c)
theorem
MeasureTheory.ProgMeasurable.finset_sum'
{Ω : Type u_1}
{ι : Type u_2}
{m : MeasurableSpace Ω}
[Preorder ι]
{f : Filtration ι m}
{β : Type u_3}
[TopologicalSpace β]
[MeasurableSpace ι]
{γ : Type u_4}
[AddCommMonoid β]
[ContinuousAdd β]
{U : γ → ι → Ω → β}
{s : Finset γ}
(h : ∀ c ∈ s, ProgMeasurable f (U c))
:
ProgMeasurable f (∑ c ∈ s, U c)
theorem
MeasureTheory.ProgMeasurable.finset_prod
{Ω : Type u_1}
{ι : Type u_2}
{m : MeasurableSpace Ω}
[Preorder ι]
{f : Filtration ι m}
{β : Type u_3}
[TopologicalSpace β]
[MeasurableSpace ι]
{γ : Type u_4}
[CommMonoid β]
[ContinuousMul β]
{U : γ → ι → Ω → β}
{s : Finset γ}
(h : ∀ c ∈ s, ProgMeasurable f (U c))
:
ProgMeasurable f fun (i : ι) (a : Ω) => ∏ c ∈ s, U c i a
theorem
MeasureTheory.ProgMeasurable.finset_sum
{Ω : Type u_1}
{ι : Type u_2}
{m : MeasurableSpace Ω}
[Preorder ι]
{f : Filtration ι m}
{β : Type u_3}
[TopologicalSpace β]
[MeasurableSpace ι]
{γ : Type u_4}
[AddCommMonoid β]
[ContinuousAdd β]
{U : γ → ι → Ω → β}
{s : Finset γ}
(h : ∀ c ∈ s, ProgMeasurable f (U c))
:
ProgMeasurable f fun (i : ι) (a : Ω) => ∑ c ∈ s, U c i a
theorem
MeasureTheory.ProgMeasurable.inv
{Ω : Type u_1}
{ι : Type u_2}
{m : MeasurableSpace Ω}
[Preorder ι]
{f : Filtration ι m}
{β : Type u_3}
[TopologicalSpace β]
{u : ι → Ω → β}
[MeasurableSpace ι]
[Group β]
[ContinuousInv β]
(hu : ProgMeasurable f u)
:
ProgMeasurable f fun (i : ι) (ω : Ω) => (u i ω)⁻¹
theorem
MeasureTheory.ProgMeasurable.neg
{Ω : Type u_1}
{ι : Type u_2}
{m : MeasurableSpace Ω}
[Preorder ι]
{f : Filtration ι m}
{β : Type u_3}
[TopologicalSpace β]
{u : ι → Ω → β}
[MeasurableSpace ι]
[AddGroup β]
[ContinuousNeg β]
(hu : ProgMeasurable f u)
:
ProgMeasurable f fun (i : ι) (ω : Ω) => -u i ω
theorem
MeasureTheory.ProgMeasurable.div
{Ω : Type u_1}
{ι : Type u_2}
{m : MeasurableSpace Ω}
[Preorder ι]
{f : Filtration ι m}
{β : Type u_3}
[TopologicalSpace β]
{u v : ι → Ω → β}
[MeasurableSpace ι]
[Group β]
[ContinuousDiv β]
(hu : ProgMeasurable f u)
(hv : ProgMeasurable f v)
:
ProgMeasurable f fun (i : ι) (ω : Ω) => u i ω / v i ω
theorem
MeasureTheory.ProgMeasurable.sub
{Ω : Type u_1}
{ι : Type u_2}
{m : MeasurableSpace Ω}
[Preorder ι]
{f : Filtration ι m}
{β : Type u_3}
[TopologicalSpace β]
{u v : ι → Ω → β}
[MeasurableSpace ι]
[AddGroup β]
[ContinuousSub β]
(hu : ProgMeasurable f u)
(hv : ProgMeasurable f v)
:
ProgMeasurable f fun (i : ι) (ω : Ω) => u i ω - v i ω
theorem
MeasureTheory.progMeasurable_of_tendsto'
{Ω : Type u_1}
{ι : Type u_2}
{m : MeasurableSpace Ω}
[Preorder ι]
{f : Filtration ι m}
{β : Type u_3}
[TopologicalSpace β]
{u : ι → Ω → β}
{γ : Type u_4}
[MeasurableSpace ι]
[TopologicalSpace.PseudoMetrizableSpace β]
(fltr : Filter γ)
[fltr.NeBot]
[fltr.IsCountablyGenerated]
{U : γ → ι → Ω → β}
(h : ∀ (l : γ), ProgMeasurable f (U l))
(h_tendsto : Filter.Tendsto U fltr (nhds u))
:
ProgMeasurable f u
theorem
MeasureTheory.progMeasurable_of_tendsto
{Ω : Type u_1}
{ι : Type u_2}
{m : MeasurableSpace Ω}
[Preorder ι]
{f : Filtration ι m}
{β : Type u_3}
[TopologicalSpace β]
{u : ι → Ω → β}
[MeasurableSpace ι]
[TopologicalSpace.PseudoMetrizableSpace β]
{U : ℕ → ι → Ω → β}
(h : ∀ (l : ℕ), ProgMeasurable f (U l))
(h_tendsto : Filter.Tendsto U Filter.atTop (nhds u))
:
ProgMeasurable f u
theorem
MeasureTheory.Adapted.progMeasurable_of_continuous
{Ω : Type u_1}
{ι : Type u_2}
{m : MeasurableSpace Ω}
[Preorder ι]
{f : Filtration ι m}
{β : Type u_3}
[TopologicalSpace β]
{u : ι → Ω → β}
[TopologicalSpace ι]
[TopologicalSpace.MetrizableSpace ι]
[SecondCountableTopology ι]
[MeasurableSpace ι]
[OpensMeasurableSpace ι]
[TopologicalSpace.PseudoMetrizableSpace β]
(h : Adapted f u)
(hu_cont : ∀ (ω : Ω), Continuous fun (i : ι) => u i ω)
:
ProgMeasurable f u
A continuous and adapted process is progressively measurable.
theorem
MeasureTheory.Adapted.progMeasurable_of_discrete
{Ω : Type u_1}
{ι : Type u_2}
{m : MeasurableSpace Ω}
[Preorder ι]
{f : Filtration ι m}
{β : Type u_3}
[TopologicalSpace β]
{u : ι → Ω → β}
[TopologicalSpace ι]
[DiscreteTopology ι]
[SecondCountableTopology ι]
[MeasurableSpace ι]
[OpensMeasurableSpace ι]
[TopologicalSpace.PseudoMetrizableSpace β]
(h : Adapted f u)
:
ProgMeasurable 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}
{m : MeasurableSpace Ω}
{β : Type u_3}
[TopologicalSpace β]
{f : Filtration ℕ m}
{u : ℕ → Ω → β}
(hu : Adapted f fun (n : ℕ) => u (n + 1))
(hu0 : StronglyMeasurable (u 0))
:
Adapted f u