Adapted and progressively measurable processes #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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 #
measure_theory.adapted: a sequence of functionsuis said to be adapted to a filtrationfif at each point in timei,u iisf i-strongly measurablemeasure_theory.prog_measurable: 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 productmeasurable_spacestructure where the σ-algebra used forΩisf i.
Main results #
adapted.prog_measurable_of_continuous: a continuous adapted process is progressively measurable.
Tags #
adapted, progressively measurable
def
measure_theory.adapted
{Ω : Type u_1}
{β : Type u_2}
{ι : Type u_3}
{m : measurable_space Ω}
[topological_space β]
[preorder ι]
(f : measure_theory.filtration ι m)
(u : ι → Ω → β) :
Prop
A sequence of functions u is adapted to a filtration f if for all i,
u i is f i-measurable.
Equations
- measure_theory.adapted f u = ∀ (i : ι), measure_theory.strongly_measurable (u i)
@[protected]
theorem
measure_theory.adapted.add
{Ω : Type u_1}
{β : Type u_2}
{ι : Type u_3}
{m : measurable_space Ω}
[topological_space β]
[preorder ι]
{u v : ι → Ω → β}
{f : measure_theory.filtration ι m}
[has_add β]
[has_continuous_add β]
(hu : measure_theory.adapted f u)
(hv : measure_theory.adapted f v) :
measure_theory.adapted f (u + v)
@[protected]
theorem
measure_theory.adapted.mul
{Ω : Type u_1}
{β : Type u_2}
{ι : Type u_3}
{m : measurable_space Ω}
[topological_space β]
[preorder ι]
{u v : ι → Ω → β}
{f : measure_theory.filtration ι m}
[has_mul β]
[has_continuous_mul β]
(hu : measure_theory.adapted f u)
(hv : measure_theory.adapted f v) :
measure_theory.adapted f (u * v)
@[protected]
theorem
measure_theory.adapted.div
{Ω : Type u_1}
{β : Type u_2}
{ι : Type u_3}
{m : measurable_space Ω}
[topological_space β]
[preorder ι]
{u v : ι → Ω → β}
{f : measure_theory.filtration ι m}
[has_div β]
[has_continuous_div β]
(hu : measure_theory.adapted f u)
(hv : measure_theory.adapted f v) :
measure_theory.adapted f (u / v)
@[protected]
theorem
measure_theory.adapted.sub
{Ω : Type u_1}
{β : Type u_2}
{ι : Type u_3}
{m : measurable_space Ω}
[topological_space β]
[preorder ι]
{u v : ι → Ω → β}
{f : measure_theory.filtration ι m}
[has_sub β]
[has_continuous_sub β]
(hu : measure_theory.adapted f u)
(hv : measure_theory.adapted f v) :
measure_theory.adapted f (u - v)
@[protected]
theorem
measure_theory.adapted.inv
{Ω : Type u_1}
{β : Type u_2}
{ι : Type u_3}
{m : measurable_space Ω}
[topological_space β]
[preorder ι]
{u : ι → Ω → β}
{f : measure_theory.filtration ι m}
[group β]
[topological_group β]
(hu : measure_theory.adapted f u) :
@[protected]
theorem
measure_theory.adapted.neg
{Ω : Type u_1}
{β : Type u_2}
{ι : Type u_3}
{m : measurable_space Ω}
[topological_space β]
[preorder ι]
{u : ι → Ω → β}
{f : measure_theory.filtration ι m}
[add_group β]
[topological_add_group β]
(hu : measure_theory.adapted f u) :
measure_theory.adapted f (-u)
@[protected]
theorem
measure_theory.adapted.smul
{Ω : Type u_1}
{β : Type u_2}
{ι : Type u_3}
{m : measurable_space Ω}
[topological_space β]
[preorder ι]
{u : ι → Ω → β}
{f : measure_theory.filtration ι m}
[has_smul ℝ β]
[has_continuous_smul ℝ β]
(c : ℝ)
(hu : measure_theory.adapted f u) :
measure_theory.adapted f (c • u)
@[protected]
theorem
measure_theory.adapted.strongly_measurable
{Ω : Type u_1}
{β : Type u_2}
{ι : Type u_3}
{m : measurable_space Ω}
[topological_space β]
[preorder ι]
{u : ι → Ω → β}
{f : measure_theory.filtration ι m}
{i : ι}
(hf : measure_theory.adapted f u) :
theorem
measure_theory.adapted.strongly_measurable_le
{Ω : Type u_1}
{β : Type u_2}
{ι : Type u_3}
{m : measurable_space Ω}
[topological_space β]
[preorder ι]
{u : ι → Ω → β}
{f : measure_theory.filtration ι m}
{i j : ι}
(hf : measure_theory.adapted f u)
(hij : i ≤ j) :
theorem
measure_theory.adapted_const
{Ω : Type u_1}
{β : Type u_2}
{ι : Type u_3}
{m : measurable_space Ω}
[topological_space β]
[preorder ι]
(f : measure_theory.filtration ι m)
(x : β) :
measure_theory.adapted f (λ (_x : ι) (_x : Ω), x)
theorem
measure_theory.adapted_zero
{Ω : Type u_1}
(β : Type u_2)
{ι : Type u_3}
{m : measurable_space Ω}
[topological_space β]
[preorder ι]
[has_zero β]
(f : measure_theory.filtration ι m) :
theorem
measure_theory.filtration.adapted_natural
{Ω : Type u_1}
{β : Type u_2}
{ι : Type u_3}
{m : measurable_space Ω}
[topological_space β]
[preorder ι]
[topological_space.metrizable_space β]
[mβ : measurable_space β]
[borel_space β]
{u : ι → Ω → β}
(hum : ∀ (i : ι), measure_theory.strongly_measurable (u i)) :
def
measure_theory.prog_measurable
{Ω : Type u_1}
{β : Type u_2}
{ι : Type u_3}
{m : measurable_space Ω}
[topological_space β]
[preorder ι]
[measurable_space ι]
(f : measure_theory.filtration ι m)
(u : ι → Ω → β) :
Prop
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 measurable_space 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
- measure_theory.prog_measurable f u = ∀ (i : ι), measure_theory.strongly_measurable (λ (p : ↥(set.Iic i) × Ω), u ↑(p.fst) p.snd)
theorem
measure_theory.prog_measurable_const
{Ω : Type u_1}
{β : Type u_2}
{ι : Type u_3}
{m : measurable_space Ω}
[topological_space β]
[preorder ι]
[measurable_space ι]
(f : measure_theory.filtration ι m)
(b : β) :
measure_theory.prog_measurable f (λ (_x : ι) (_x : Ω), b)
@[protected]
theorem
measure_theory.prog_measurable.adapted
{Ω : Type u_1}
{β : Type u_2}
{ι : Type u_3}
{m : measurable_space Ω}
[topological_space β]
[preorder ι]
{u : ι → Ω → β}
{f : measure_theory.filtration ι m}
[measurable_space ι]
(h : measure_theory.prog_measurable f u) :
@[protected]
theorem
measure_theory.prog_measurable.comp
{Ω : Type u_1}
{β : Type u_2}
{ι : Type u_3}
{m : measurable_space Ω}
[topological_space β]
[preorder ι]
{u : ι → Ω → β}
{f : measure_theory.filtration ι m}
[measurable_space ι]
{t : ι → Ω → ι}
[topological_space ι]
[borel_space ι]
[topological_space.metrizable_space ι]
(h : measure_theory.prog_measurable f u)
(ht : measure_theory.prog_measurable f t)
(ht_le : ∀ (i : ι) (ω : Ω), t i ω ≤ i) :
measure_theory.prog_measurable f (λ (i : ι) (ω : Ω), u (t i ω) ω)
@[protected]
theorem
measure_theory.prog_measurable.mul
{Ω : Type u_1}
{β : Type u_2}
{ι : Type u_3}
{m : measurable_space Ω}
[topological_space β]
[preorder ι]
{u v : ι → Ω → β}
{f : measure_theory.filtration ι m}
[measurable_space ι]
[has_mul β]
[has_continuous_mul β]
(hu : measure_theory.prog_measurable f u)
(hv : measure_theory.prog_measurable f v) :
measure_theory.prog_measurable f (λ (i : ι) (ω : Ω), u i ω * v i ω)
@[protected]
theorem
measure_theory.prog_measurable.add
{Ω : Type u_1}
{β : Type u_2}
{ι : Type u_3}
{m : measurable_space Ω}
[topological_space β]
[preorder ι]
{u v : ι → Ω → β}
{f : measure_theory.filtration ι m}
[measurable_space ι]
[has_add β]
[has_continuous_add β]
(hu : measure_theory.prog_measurable f u)
(hv : measure_theory.prog_measurable f v) :
measure_theory.prog_measurable f (λ (i : ι) (ω : Ω), u i ω + v i ω)
@[protected]
theorem
measure_theory.prog_measurable.finset_sum'
{Ω : Type u_1}
{β : Type u_2}
{ι : Type u_3}
{m : measurable_space Ω}
[topological_space β]
[preorder ι]
{f : measure_theory.filtration ι m}
[measurable_space ι]
{γ : Type u_4}
[add_comm_monoid β]
[has_continuous_add β]
{U : γ → ι → Ω → β}
{s : finset γ}
(h : ∀ (c : γ), c ∈ s → measure_theory.prog_measurable f (U c)) :
measure_theory.prog_measurable f (s.sum (λ (c : γ), U c))
@[protected]
theorem
measure_theory.prog_measurable.finset_prod'
{Ω : Type u_1}
{β : Type u_2}
{ι : Type u_3}
{m : measurable_space Ω}
[topological_space β]
[preorder ι]
{f : measure_theory.filtration ι m}
[measurable_space ι]
{γ : Type u_4}
[comm_monoid β]
[has_continuous_mul β]
{U : γ → ι → Ω → β}
{s : finset γ}
(h : ∀ (c : γ), c ∈ s → measure_theory.prog_measurable f (U c)) :
measure_theory.prog_measurable f (s.prod (λ (c : γ), U c))
@[protected]
theorem
measure_theory.prog_measurable.finset_sum
{Ω : Type u_1}
{β : Type u_2}
{ι : Type u_3}
{m : measurable_space Ω}
[topological_space β]
[preorder ι]
{f : measure_theory.filtration ι m}
[measurable_space ι]
{γ : Type u_4}
[add_comm_monoid β]
[has_continuous_add β]
{U : γ → ι → Ω → β}
{s : finset γ}
(h : ∀ (c : γ), c ∈ s → measure_theory.prog_measurable f (U c)) :
measure_theory.prog_measurable f (λ (i : ι) (a : Ω), s.sum (λ (c : γ), U c i a))
@[protected]
theorem
measure_theory.prog_measurable.finset_prod
{Ω : Type u_1}
{β : Type u_2}
{ι : Type u_3}
{m : measurable_space Ω}
[topological_space β]
[preorder ι]
{f : measure_theory.filtration ι m}
[measurable_space ι]
{γ : Type u_4}
[comm_monoid β]
[has_continuous_mul β]
{U : γ → ι → Ω → β}
{s : finset γ}
(h : ∀ (c : γ), c ∈ s → measure_theory.prog_measurable f (U c)) :
measure_theory.prog_measurable f (λ (i : ι) (a : Ω), s.prod (λ (c : γ), U c i a))
@[protected]
theorem
measure_theory.prog_measurable.neg
{Ω : Type u_1}
{β : Type u_2}
{ι : Type u_3}
{m : measurable_space Ω}
[topological_space β]
[preorder ι]
{u : ι → Ω → β}
{f : measure_theory.filtration ι m}
[measurable_space ι]
[add_group β]
[topological_add_group β]
(hu : measure_theory.prog_measurable f u) :
measure_theory.prog_measurable f (λ (i : ι) (ω : Ω), -u i ω)
@[protected]
theorem
measure_theory.prog_measurable.inv
{Ω : Type u_1}
{β : Type u_2}
{ι : Type u_3}
{m : measurable_space Ω}
[topological_space β]
[preorder ι]
{u : ι → Ω → β}
{f : measure_theory.filtration ι m}
[measurable_space ι]
[group β]
[topological_group β]
(hu : measure_theory.prog_measurable f u) :
measure_theory.prog_measurable f (λ (i : ι) (ω : Ω), (u i ω)⁻¹)
@[protected]
theorem
measure_theory.prog_measurable.div
{Ω : Type u_1}
{β : Type u_2}
{ι : Type u_3}
{m : measurable_space Ω}
[topological_space β]
[preorder ι]
{u v : ι → Ω → β}
{f : measure_theory.filtration ι m}
[measurable_space ι]
[group β]
[topological_group β]
(hu : measure_theory.prog_measurable f u)
(hv : measure_theory.prog_measurable f v) :
measure_theory.prog_measurable f (λ (i : ι) (ω : Ω), u i ω / v i ω)
@[protected]
theorem
measure_theory.prog_measurable.sub
{Ω : Type u_1}
{β : Type u_2}
{ι : Type u_3}
{m : measurable_space Ω}
[topological_space β]
[preorder ι]
{u v : ι → Ω → β}
{f : measure_theory.filtration ι m}
[measurable_space ι]
[add_group β]
[topological_add_group β]
(hu : measure_theory.prog_measurable f u)
(hv : measure_theory.prog_measurable f v) :
measure_theory.prog_measurable f (λ (i : ι) (ω : Ω), u i ω - v i ω)
theorem
measure_theory.prog_measurable_of_tendsto'
{Ω : Type u_1}
{β : Type u_2}
{ι : Type u_3}
{m : measurable_space Ω}
[topological_space β]
[preorder ι]
{u : ι → Ω → β}
{f : measure_theory.filtration ι m}
{γ : Type u_4}
[measurable_space ι]
[topological_space.pseudo_metrizable_space β]
(fltr : filter γ)
[fltr.ne_bot]
[fltr.is_countably_generated]
{U : γ → ι → Ω → β}
(h : ∀ (l : γ), measure_theory.prog_measurable f (U l))
(h_tendsto : filter.tendsto U fltr (nhds u)) :
theorem
measure_theory.prog_measurable_of_tendsto
{Ω : Type u_1}
{β : Type u_2}
{ι : Type u_3}
{m : measurable_space Ω}
[topological_space β]
[preorder ι]
{u : ι → Ω → β}
{f : measure_theory.filtration ι m}
[measurable_space ι]
[topological_space.pseudo_metrizable_space β]
{U : ℕ → ι → Ω → β}
(h : ∀ (l : ℕ), measure_theory.prog_measurable f (U l))
(h_tendsto : filter.tendsto U filter.at_top (nhds u)) :
theorem
measure_theory.adapted.prog_measurable_of_continuous
{Ω : Type u_1}
{β : Type u_2}
{ι : Type u_3}
{m : measurable_space Ω}
[topological_space β]
[preorder ι]
{u : ι → Ω → β}
{f : measure_theory.filtration ι m}
[topological_space ι]
[topological_space.metrizable_space ι]
[topological_space.second_countable_topology ι]
[measurable_space ι]
[opens_measurable_space ι]
[topological_space.pseudo_metrizable_space β]
(h : measure_theory.adapted f u)
(hu_cont : ∀ (ω : Ω), continuous (λ (i : ι), u i ω)) :
A continuous and adapted process is progressively measurable.
theorem
measure_theory.adapted.prog_measurable_of_discrete
{Ω : Type u_1}
{β : Type u_2}
{ι : Type u_3}
{m : measurable_space Ω}
[topological_space β]
[preorder ι]
{u : ι → Ω → β}
{f : measure_theory.filtration ι m}
[topological_space ι]
[discrete_topology ι]
[topological_space.second_countable_topology ι]
[measurable_space ι]
[opens_measurable_space ι]
[topological_space.pseudo_metrizable_space β]
(h : measure_theory.adapted f u) :
For filtrations indexed by a discrete order, adapted and prog_measurable are equivalent.
This lemma provides adapted f u → prog_measurable f u.
See prog_measurable.adapted for the reverse direction, which is true more generally.
theorem
measure_theory.predictable.adapted
{Ω : Type u_1}
{β : Type u_2}
{m : measurable_space Ω}
[topological_space β]
{f : measure_theory.filtration ℕ m}
{u : ℕ → Ω → β}
(hu : measure_theory.adapted f (λ (n : ℕ), u (n + 1)))
(hu0 : measure_theory.strongly_measurable (u 0)) :