# 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 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
• MeasureTheory.ProgMeasurable: 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 MeasurableSpace structure where the σ-algebra used for Ω is f i.

## Main results #

• Adapted.progMeasurable_of_continuous: a continuous adapted process is progressively measurable.

## Tags #

def MeasureTheory.Adapted {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} {m : } [] [] (f : ) (u : ιΩβ) :

A sequence of functions u is adapted to a filtration f if for all i, u i is f i-measurable.

Equations
• = ∀ (i : ι),
Instances For
theorem MeasureTheory.Adapted.add {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} {m : } [] [] {u : ιΩβ} {v : ιΩβ} {f : } [Add β] [] (hu : ) (hv : ) :
theorem MeasureTheory.Adapted.mul {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} {m : } [] [] {u : ιΩβ} {v : ιΩβ} {f : } [Mul β] [] (hu : ) (hv : ) :
theorem MeasureTheory.Adapted.sub {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} {m : } [] [] {u : ιΩβ} {v : ιΩβ} {f : } [Sub β] [] (hu : ) (hv : ) :
theorem MeasureTheory.Adapted.div {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} {m : } [] [] {u : ιΩβ} {v : ιΩβ} {f : } [Div β] [] (hu : ) (hv : ) :
theorem MeasureTheory.Adapted.neg {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} {m : } [] [] {u : ιΩβ} {f : } [] (hu : ) :
theorem MeasureTheory.Adapted.inv {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} {m : } [] [] {u : ιΩβ} {f : } [] [] (hu : ) :
theorem MeasureTheory.Adapted.smul {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} {m : } [] [] {u : ιΩβ} {f : } [] [] (c : ) (hu : ) :
theorem MeasureTheory.Adapted.stronglyMeasurable {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} {m : } [] [] {u : ιΩβ} {f : } {i : ι} (hf : ) :
theorem MeasureTheory.Adapted.stronglyMeasurable_le {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} {m : } [] [] {u : ιΩβ} {f : } {i : ι} {j : ι} (hf : ) (hij : i j) :
theorem MeasureTheory.adapted_const {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} {m : } [] [] (f : ) (x : β) :
MeasureTheory.Adapted f fun (x_1 : ι) (x_2 : Ω) => x
theorem MeasureTheory.adapted_zero {Ω : Type u_1} (β : Type u_2) {ι : Type u_3} {m : } [] [] [Zero β] (f : ) :
theorem MeasureTheory.Filtration.adapted_natural {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} {m : } [] [] [mβ : ] [] {u : ιΩβ} (hum : ∀ (i : ι), ) :
def MeasureTheory.ProgMeasurable {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} {m : } [] [] [] (f : ) (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
Instances For
theorem MeasureTheory.progMeasurable_const {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} {m : } [] [] [] (f : ) (b : β) :
MeasureTheory.ProgMeasurable f fun (x : ι) (x : Ω) => b
theorem MeasureTheory.ProgMeasurable.adapted {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} {m : } [] [] {u : ιΩβ} {f : } [] (h : ) :
theorem MeasureTheory.ProgMeasurable.comp {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} {m : } [] [] {u : ιΩβ} {f : } [] {t : ιΩι} [] [] (h : ) (ht : ) (ht_le : ∀ (i : ι) (ω : Ω), t i ω i) :
MeasureTheory.ProgMeasurable f fun (i : ι) (ω : Ω) => u (t i ω) ω
theorem MeasureTheory.ProgMeasurable.add {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} {m : } [] [] {u : ιΩβ} {v : ιΩβ} {f : } [] [Add β] [] (hu : ) (hv : ) :
MeasureTheory.ProgMeasurable f fun (i : ι) (ω : Ω) => u i ω + v i ω
theorem MeasureTheory.ProgMeasurable.mul {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} {m : } [] [] {u : ιΩβ} {v : ιΩβ} {f : } [] [Mul β] [] (hu : ) (hv : ) :
MeasureTheory.ProgMeasurable f fun (i : ι) (ω : Ω) => u i ω * v i ω
theorem MeasureTheory.ProgMeasurable.finset_sum' {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} {m : } [] [] {f : } [] {γ : Type u_4} [] [] {U : γιΩβ} {s : } (h : cs, ) :
MeasureTheory.ProgMeasurable f (cs, U c)
theorem MeasureTheory.ProgMeasurable.finset_prod' {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} {m : } [] [] {f : } [] {γ : Type u_4} [] [] {U : γιΩβ} {s : } (h : cs, ) :
MeasureTheory.ProgMeasurable f (cs, U c)
theorem MeasureTheory.ProgMeasurable.finset_sum {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} {m : } [] [] {f : } [] {γ : Type u_4} [] [] {U : γιΩβ} {s : } (h : cs, ) :
MeasureTheory.ProgMeasurable f fun (i : ι) (a : Ω) => cs, U c i a
theorem MeasureTheory.ProgMeasurable.finset_prod {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} {m : } [] [] {f : } [] {γ : Type u_4} [] [] {U : γιΩβ} {s : } (h : cs, ) :
MeasureTheory.ProgMeasurable f fun (i : ι) (a : Ω) => cs, U c i a
theorem MeasureTheory.ProgMeasurable.neg {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} {m : } [] [] {u : ιΩβ} {f : } [] [] (hu : ) :
MeasureTheory.ProgMeasurable f fun (i : ι) (ω : Ω) => -u i ω
theorem MeasureTheory.ProgMeasurable.inv {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} {m : } [] [] {u : ιΩβ} {f : } [] [] [] (hu : ) :
MeasureTheory.ProgMeasurable f fun (i : ι) (ω : Ω) => (u i ω)⁻¹
theorem MeasureTheory.ProgMeasurable.sub {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} {m : } [] [] {u : ιΩβ} {v : ιΩβ} {f : } [] [] (hu : ) (hv : ) :
MeasureTheory.ProgMeasurable f fun (i : ι) (ω : Ω) => u i ω - v i ω
theorem MeasureTheory.ProgMeasurable.div {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} {m : } [] [] {u : ιΩβ} {v : ιΩβ} {f : } [] [] [] (hu : ) (hv : ) :
MeasureTheory.ProgMeasurable f fun (i : ι) (ω : Ω) => u i ω / v i ω
theorem MeasureTheory.progMeasurable_of_tendsto' {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} {m : } [] [] {u : ιΩβ} {f : } {γ : Type u_4} [] (fltr : ) [fltr.NeBot] [fltr.IsCountablyGenerated] {U : γιΩβ} (h : ∀ (l : γ), ) (h_tendsto : Filter.Tendsto U fltr (nhds u)) :
theorem MeasureTheory.progMeasurable_of_tendsto {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} {m : } [] [] {u : ιΩβ} {f : } [] {U : ιΩβ} (h : ∀ (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 : } [] [] {u : ιΩβ} {f : } [] [] (h : ) (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 : } [] [] {u : ιΩβ} {f : } [] [] [] (h : ) :

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 : } [] {f : } {u : Ωβ} (hu : MeasureTheory.Adapted f fun (n : ) => u (n + 1)) (hu0 : ) :