# 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 functions u is said to be adapted to a filtration f if at each point in time i, u i is f i-strongly measurable
• measure_theory.prog_measurable: 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 strongly measurable with respect to the product measurable_space structure where the σ-algebra used for Ω is f i.

## Main results #

• adapted.prog_measurable_of_continuous: a continuous adapted process is progressively measurable.

## Tags #

def measure_theory.adapted {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} {m : measurable_space Ω} [preorder ι] (f : 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 Ω} [preorder ι] {u v : ι Ω β} {f : m} [has_add β] (hu : u) (hv : v) :
(u + v)
@[protected]
theorem measure_theory.adapted.mul {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} {m : measurable_space Ω} [preorder ι] {u v : ι Ω β} {f : m} [has_mul β] (hu : u) (hv : v) :
(u * v)
@[protected]
theorem measure_theory.adapted.div {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} {m : measurable_space Ω} [preorder ι] {u v : ι Ω β} {f : m} [has_div β] (hu : u) (hv : v) :
(u / v)
@[protected]
theorem measure_theory.adapted.sub {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} {m : measurable_space Ω} [preorder ι] {u v : ι Ω β} {f : m} [has_sub β] (hu : u) (hv : v) :
(u - v)
@[protected]
theorem measure_theory.adapted.inv {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} {m : measurable_space Ω} [preorder ι] {u : ι Ω β} {f : m} [group β] (hu : u) :
@[protected]
theorem measure_theory.adapted.neg {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} {m : measurable_space Ω} [preorder ι] {u : ι Ω β} {f : m} [add_group β] (hu : u) :
@[protected]
theorem measure_theory.adapted.smul {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} {m : measurable_space Ω} [preorder ι] {u : ι Ω β} {f : m} [ β] (c : ) (hu : u) :
(c u)
@[protected]
theorem measure_theory.adapted.strongly_measurable {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} {m : measurable_space Ω} [preorder ι] {u : ι Ω β} {f : m} {i : ι} (hf : u) :
theorem measure_theory.adapted.strongly_measurable_le {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} {m : measurable_space Ω} [preorder ι] {u : ι Ω β} {f : m} {i j : ι} (hf : u) (hij : i j) :
theorem measure_theory.adapted_const {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} {m : measurable_space Ω} [preorder ι] (f : m) (x : β) :
(λ (_x : ι) (_x : Ω), x)
theorem measure_theory.adapted_zero {Ω : Type u_1} (β : Type u_2) {ι : Type u_3} {m : measurable_space Ω} [preorder ι] [has_zero β] (f : m) :
theorem measure_theory.filtration.adapted_natural {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} {m : measurable_space Ω} [preorder ι] [mβ : measurable_space β] [borel_space β] {u : ι Ω β} (hum : (i : ι), ) :
def measure_theory.prog_measurable {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} {m : measurable_space Ω} [preorder ι] (f : 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 Ω} [preorder ι] (f : m) (b : β) :
(λ (_x : ι) (_x : Ω), b)
@[protected]
theorem measure_theory.prog_measurable.adapted {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} {m : measurable_space Ω} [preorder ι] {u : ι Ω β} {f : m} (h : u) :
@[protected]
theorem measure_theory.prog_measurable.comp {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} {m : measurable_space Ω} [preorder ι] {u : ι Ω β} {f : m} {t : ι Ω ι} [borel_space ι] (h : u) (ht : t) (ht_le : (i : ι) (ω : Ω), t i ω i) :
(λ (i : ι) (ω : Ω), u (t i ω) ω)
@[protected]
theorem measure_theory.prog_measurable.mul {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} {m : measurable_space Ω} [preorder ι] {u v : ι Ω β} {f : m} [has_mul β] (hu : u) (hv : v) :
(λ (i : ι) (ω : Ω), u i ω * v i ω)
@[protected]
theorem measure_theory.prog_measurable.add {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} {m : measurable_space Ω} [preorder ι] {u v : ι Ω β} {f : m} [has_add β] (hu : u) (hv : v) :
(λ (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 Ω} [preorder ι] {f : m} {γ : Type u_4} {U : γ ι Ω β} {s : finset γ} (h : (c : γ), c s ) :
(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 Ω} [preorder ι] {f : m} {γ : Type u_4} [comm_monoid β] {U : γ ι Ω β} {s : finset γ} (h : (c : γ), c s ) :
(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 Ω} [preorder ι] {f : m} {γ : Type u_4} {U : γ ι Ω β} {s : finset γ} (h : (c : γ), c s ) :
(λ (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 Ω} [preorder ι] {f : m} {γ : Type u_4} [comm_monoid β] {U : γ ι Ω β} {s : finset γ} (h : (c : γ), c s ) :
(λ (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 Ω} [preorder ι] {u : ι Ω β} {f : m} [add_group β] (hu : u) :
(λ (i : ι) (ω : Ω), -u i ω)
@[protected]
theorem measure_theory.prog_measurable.inv {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} {m : measurable_space Ω} [preorder ι] {u : ι Ω β} {f : m} [group β] (hu : u) :
(λ (i : ι) (ω : Ω), (u i ω)⁻¹)
@[protected]
theorem measure_theory.prog_measurable.div {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} {m : measurable_space Ω} [preorder ι] {u v : ι Ω β} {f : m} [group β] (hu : u) (hv : v) :
(λ (i : ι) (ω : Ω), u i ω / v i ω)
@[protected]
theorem measure_theory.prog_measurable.sub {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} {m : measurable_space Ω} [preorder ι] {u v : ι Ω β} {f : m} [add_group β] (hu : u) (hv : v) :
(λ (i : ι) (ω : Ω), u i ω - v i ω)
theorem measure_theory.prog_measurable_of_tendsto' {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} {m : measurable_space Ω} [preorder ι] {u : ι Ω β} {f : m} {γ : Type u_4} (fltr : filter γ) [fltr.ne_bot] [fltr.is_countably_generated] {U : γ ι Ω β} (h : (l : γ), ) (h_tendsto : fltr (nhds u)) :
theorem measure_theory.prog_measurable_of_tendsto {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} {m : measurable_space Ω} [preorder ι] {u : ι Ω β} {f : m} {U : ι Ω β} (h : (l : ), ) (h_tendsto : (nhds u)) :
theorem measure_theory.adapted.prog_measurable_of_continuous {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} {m : measurable_space Ω} [preorder ι] {u : ι Ω β} {f : m} (h : 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 Ω} [preorder ι] {u : ι Ω β} {f : m} (h : 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 Ω} {f : m} {u : Ω β} (hu : (λ (n : ), u (n + 1))) (hu0 : measure_theory.strongly_measurable (u 0)) :