# 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 #

adapted, progressively measurable

source
def MeasureTheory.Adapted {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [Preorder ι] {β : ι → Type u_3} [(i : ι) → TopologicalSpace (β i)] (f : Filtration ι m) (u : (i : ι) → Ω → β i) :
Prop

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

source
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) :
Adapted f (u * v)
source
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) :
Adapted f (u + v)
source
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) :
Adapted f (u / v)
source
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) :
Adapted f (u - v)
source
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) :
Adapted f u⁻¹
source
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) :
Adapted f (-u)
source
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) :
Adapted f (c • u)
source
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)
source
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)
source
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
source
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
source
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
source
theorem MeasureTheory.adapted_zero {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [Preorder ι] (β : Type u_4) [TopologicalSpace β] [Zero β] (f : Filtration ι m) :
Adapted f 0
source
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)) :
Adapted (natural u hum) u
source
def MeasureTheory.ProgMeasurable {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [Preorder ι] {β : Type u_3} [TopologicalSpace β] [MeasurableSpace ι] (f : 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 `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

source
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
source
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
source
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 ω) ω
source
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 ω
source
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 ω
source
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)
source
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)
source
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
source
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
source
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 ω)⁻¹
source
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 ω
source
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 ω
source
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 ω
source
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
source
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
source
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.

source
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.

source
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