Documentation

Mathlib.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 MeasureTheory.Adapted {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} {m : MeasurableSpace Ω} [TopologicalSpace β] [Preorder ι] (f : MeasureTheory.Filtration ι m) (u : ιΩβ) :

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

Equations
Instances For
    theorem MeasureTheory.Adapted.add {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} {m : MeasurableSpace Ω} [TopologicalSpace β] [Preorder ι] {u : ιΩβ} {v : ιΩβ} {f : MeasureTheory.Filtration ι m} [Add β] [ContinuousAdd β] (hu : MeasureTheory.Adapted f u) (hv : MeasureTheory.Adapted f v) :
    theorem MeasureTheory.Adapted.mul {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} {m : MeasurableSpace Ω} [TopologicalSpace β] [Preorder ι] {u : ιΩβ} {v : ιΩβ} {f : MeasureTheory.Filtration ι m} [Mul β] [ContinuousMul β] (hu : MeasureTheory.Adapted f u) (hv : MeasureTheory.Adapted f v) :
    theorem MeasureTheory.Adapted.sub {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} {m : MeasurableSpace Ω} [TopologicalSpace β] [Preorder ι] {u : ιΩβ} {v : ιΩβ} {f : MeasureTheory.Filtration ι m} [Sub β] [ContinuousSub β] (hu : MeasureTheory.Adapted f u) (hv : MeasureTheory.Adapted f v) :
    theorem MeasureTheory.Adapted.div {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} {m : MeasurableSpace Ω} [TopologicalSpace β] [Preorder ι] {u : ιΩβ} {v : ιΩβ} {f : MeasureTheory.Filtration ι m} [Div β] [ContinuousDiv β] (hu : MeasureTheory.Adapted f u) (hv : MeasureTheory.Adapted f v) :
    theorem MeasureTheory.Adapted.neg {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} {m : MeasurableSpace Ω} [TopologicalSpace β] [Preorder ι] {u : ιΩβ} {f : MeasureTheory.Filtration ι m} [AddGroup β] [TopologicalAddGroup β] (hu : MeasureTheory.Adapted f u) :
    theorem MeasureTheory.Adapted.inv {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} {m : MeasurableSpace Ω} [TopologicalSpace β] [Preorder ι] {u : ιΩβ} {f : MeasureTheory.Filtration ι m} [Group β] [TopologicalGroup β] (hu : MeasureTheory.Adapted f u) :
    theorem MeasureTheory.Adapted.smul {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} {m : MeasurableSpace Ω} [TopologicalSpace β] [Preorder ι] {u : ιΩβ} {f : MeasureTheory.Filtration ι m} [SMul β] [ContinuousSMul β] (c : ) (hu : MeasureTheory.Adapted f u) :
    theorem MeasureTheory.Adapted.stronglyMeasurable {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} {m : MeasurableSpace Ω} [TopologicalSpace β] [Preorder ι] {u : ιΩβ} {f : MeasureTheory.Filtration ι m} {i : ι} (hf : MeasureTheory.Adapted f u) :
    theorem MeasureTheory.Adapted.stronglyMeasurable_le {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} {m : MeasurableSpace Ω} [TopologicalSpace β] [Preorder ι] {u : ιΩβ} {f : MeasureTheory.Filtration ι m} {i : ι} {j : ι} (hf : MeasureTheory.Adapted f u) (hij : i j) :
    theorem MeasureTheory.adapted_const {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} {m : MeasurableSpace Ω} [TopologicalSpace β] [Preorder ι] (f : MeasureTheory.Filtration ι m) (x : β) :
    MeasureTheory.Adapted f fun (x_1 : ι) (x_2 : Ω) => x
    theorem MeasureTheory.adapted_zero {Ω : Type u_1} (β : Type u_2) {ι : Type u_3} {m : MeasurableSpace Ω} [TopologicalSpace β] [Preorder ι] [Zero β] (f : MeasureTheory.Filtration ι m) :
    def MeasureTheory.ProgMeasurable {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} {m : MeasurableSpace Ω} [TopologicalSpace β] [Preorder ι] [MeasurableSpace ι] (f : MeasureTheory.Filtration ι m) (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 : MeasurableSpace Ω} [TopologicalSpace β] [Preorder ι] [MeasurableSpace ι] (f : MeasureTheory.Filtration ι m) (b : β) :
      MeasureTheory.ProgMeasurable f fun (x : ι) (x : Ω) => b
      theorem MeasureTheory.ProgMeasurable.adapted {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} {m : MeasurableSpace Ω} [TopologicalSpace β] [Preorder ι] {u : ιΩβ} {f : MeasureTheory.Filtration ι m} [MeasurableSpace ι] (h : MeasureTheory.ProgMeasurable f u) :
      theorem MeasureTheory.ProgMeasurable.comp {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} {m : MeasurableSpace Ω} [TopologicalSpace β] [Preorder ι] {u : ιΩβ} {f : MeasureTheory.Filtration ι m} [MeasurableSpace ι] {t : ιΩι} [TopologicalSpace ι] [BorelSpace ι] [TopologicalSpace.MetrizableSpace ι] (h : MeasureTheory.ProgMeasurable f u) (ht : MeasureTheory.ProgMeasurable f t) (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 : MeasurableSpace Ω} [TopologicalSpace β] [Preorder ι] {u : ιΩβ} {v : ιΩβ} {f : MeasureTheory.Filtration ι m} [MeasurableSpace ι] [Add β] [ContinuousAdd β] (hu : MeasureTheory.ProgMeasurable f u) (hv : MeasureTheory.ProgMeasurable f v) :
      MeasureTheory.ProgMeasurable f fun (i : ι) (ω : Ω) => u i ω + v i ω
      theorem MeasureTheory.ProgMeasurable.mul {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} {m : MeasurableSpace Ω} [TopologicalSpace β] [Preorder ι] {u : ιΩβ} {v : ιΩβ} {f : MeasureTheory.Filtration ι m} [MeasurableSpace ι] [Mul β] [ContinuousMul β] (hu : MeasureTheory.ProgMeasurable f u) (hv : MeasureTheory.ProgMeasurable f v) :
      MeasureTheory.ProgMeasurable f fun (i : ι) (ω : Ω) => u i ω * v i ω
      theorem MeasureTheory.ProgMeasurable.finset_sum' {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} {m : MeasurableSpace Ω} [TopologicalSpace β] [Preorder ι] {f : MeasureTheory.Filtration ι m} [MeasurableSpace ι] {γ : Type u_4} [AddCommMonoid β] [ContinuousAdd β] {U : γιΩβ} {s : Finset γ} (h : cs, MeasureTheory.ProgMeasurable f (U c)) :
      MeasureTheory.ProgMeasurable f (∑ cs, U c)
      theorem MeasureTheory.ProgMeasurable.finset_prod' {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} {m : MeasurableSpace Ω} [TopologicalSpace β] [Preorder ι] {f : MeasureTheory.Filtration ι m} [MeasurableSpace ι] {γ : Type u_4} [CommMonoid β] [ContinuousMul β] {U : γιΩβ} {s : Finset γ} (h : cs, MeasureTheory.ProgMeasurable f (U c)) :
      MeasureTheory.ProgMeasurable f (∏ cs, U c)
      theorem MeasureTheory.ProgMeasurable.finset_sum {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} {m : MeasurableSpace Ω} [TopologicalSpace β] [Preorder ι] {f : MeasureTheory.Filtration ι m} [MeasurableSpace ι] {γ : Type u_4} [AddCommMonoid β] [ContinuousAdd β] {U : γιΩβ} {s : Finset γ} (h : cs, MeasureTheory.ProgMeasurable f (U c)) :
      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 : MeasurableSpace Ω} [TopologicalSpace β] [Preorder ι] {f : MeasureTheory.Filtration ι m} [MeasurableSpace ι] {γ : Type u_4} [CommMonoid β] [ContinuousMul β] {U : γιΩβ} {s : Finset γ} (h : cs, MeasureTheory.ProgMeasurable f (U c)) :
      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 : MeasurableSpace Ω} [TopologicalSpace β] [Preorder ι] {u : ιΩβ} {f : MeasureTheory.Filtration ι m} [MeasurableSpace ι] [AddGroup β] [TopologicalAddGroup β] (hu : MeasureTheory.ProgMeasurable f u) :
      MeasureTheory.ProgMeasurable f fun (i : ι) (ω : Ω) => -u i ω
      theorem MeasureTheory.ProgMeasurable.inv {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} {m : MeasurableSpace Ω} [TopologicalSpace β] [Preorder ι] {u : ιΩβ} {f : MeasureTheory.Filtration ι m} [MeasurableSpace ι] [Group β] [TopologicalGroup β] (hu : MeasureTheory.ProgMeasurable f u) :
      MeasureTheory.ProgMeasurable f fun (i : ι) (ω : Ω) => (u i ω)⁻¹
      theorem MeasureTheory.ProgMeasurable.sub {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} {m : MeasurableSpace Ω} [TopologicalSpace β] [Preorder ι] {u : ιΩβ} {v : ιΩβ} {f : MeasureTheory.Filtration ι m} [MeasurableSpace ι] [AddGroup β] [TopologicalAddGroup β] (hu : MeasureTheory.ProgMeasurable f u) (hv : MeasureTheory.ProgMeasurable f v) :
      MeasureTheory.ProgMeasurable f fun (i : ι) (ω : Ω) => u i ω - v i ω
      theorem MeasureTheory.ProgMeasurable.div {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} {m : MeasurableSpace Ω} [TopologicalSpace β] [Preorder ι] {u : ιΩβ} {v : ιΩβ} {f : MeasureTheory.Filtration ι m} [MeasurableSpace ι] [Group β] [TopologicalGroup β] (hu : MeasureTheory.ProgMeasurable f u) (hv : MeasureTheory.ProgMeasurable f v) :
      MeasureTheory.ProgMeasurable f fun (i : ι) (ω : Ω) => u i ω / v i ω
      theorem MeasureTheory.progMeasurable_of_tendsto' {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} {m : MeasurableSpace Ω} [TopologicalSpace β] [Preorder ι] {u : ιΩβ} {f : MeasureTheory.Filtration ι m} {γ : Type u_4} [MeasurableSpace ι] [TopologicalSpace.PseudoMetrizableSpace β] (fltr : Filter γ) [fltr.NeBot] [fltr.IsCountablyGenerated] {U : γιΩβ} (h : ∀ (l : γ), MeasureTheory.ProgMeasurable f (U l)) (h_tendsto : Filter.Tendsto U fltr (nhds u)) :
      theorem MeasureTheory.progMeasurable_of_tendsto {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} {m : MeasurableSpace Ω} [TopologicalSpace β] [Preorder ι] {u : ιΩβ} {f : MeasureTheory.Filtration ι m} [MeasurableSpace ι] [TopologicalSpace.PseudoMetrizableSpace β] {U : ιΩβ} (h : ∀ (l : ), MeasureTheory.ProgMeasurable f (U l)) (h_tendsto : Filter.Tendsto U Filter.atTop (nhds u)) :

      A continuous and adapted process is progressively measurable.

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