mathlib documentation

probability.process.adapted

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 #

Main results #

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
@[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) :
@[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) :
@[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) :
@[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) :
@[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) :
@[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) :
@[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) :
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
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]
@[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)) :

A continuous and adapted process is progressively measurable.

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.