Documentation

Mathlib.Probability.Process.Filtration

Filtrations #

This file defines filtrations of a measurable space and σ-finite filtrations.

Main definitions #

Main results #

Tags #

filtration, stochastic process

structure MeasureTheory.Filtration {Ω : Type u_1} (ι : Type u_2) [Preorder ι] (m : MeasurableSpace Ω) :
Type (max u_1 u_2)

A Filtration on a measurable space Ω with σ-algebra m is a monotone sequence of sub-σ-algebras of m.

Instances For
    theorem MeasureTheory.Filtration.mono' {Ω : Type u_1} {ι : Type u_2} [Preorder ι] {m : MeasurableSpace Ω} (self : MeasureTheory.Filtration ι m) :
    Monotone self
    theorem MeasureTheory.Filtration.le' {Ω : Type u_1} {ι : Type u_2} [Preorder ι] {m : MeasurableSpace Ω} (self : MeasureTheory.Filtration ι m) (i : ι) :
    self i m
    Equations
    theorem MeasureTheory.Filtration.mono {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [Preorder ι] {i : ι} {j : ι} (f : MeasureTheory.Filtration ι m) (hij : i j) :
    f i f j
    theorem MeasureTheory.Filtration.le {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [Preorder ι] (f : MeasureTheory.Filtration ι m) (i : ι) :
    f i m
    theorem MeasureTheory.Filtration.ext_iff {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [Preorder ι] {f : MeasureTheory.Filtration ι m} {g : MeasureTheory.Filtration ι m} :
    f = g f = g
    theorem MeasureTheory.Filtration.ext {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [Preorder ι] {f : MeasureTheory.Filtration ι m} {g : MeasureTheory.Filtration ι m} (h : f = g) :
    f = g
    def MeasureTheory.Filtration.const {Ω : Type u_1} (ι : Type u_3) {m : MeasurableSpace Ω} [Preorder ι] (m' : MeasurableSpace Ω) (hm' : m' m) :

    The constant filtration which is equal to m for all i : ι.

    Equations
    Instances For
      @[simp]
      theorem MeasureTheory.Filtration.const_apply {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [Preorder ι] {m' : MeasurableSpace Ω} {hm' : m' m} (i : ι) :
      (MeasureTheory.Filtration.const ι m' hm') i = m'
      Equations
      instance MeasureTheory.Filtration.instLE {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [Preorder ι] :
      Equations
      Equations
      Equations
      Equations
      • MeasureTheory.Filtration.instSup = { sup := fun (f g : MeasureTheory.Filtration ι m) => { seq := fun (i : ι) => f i g i, mono' := , le' := } }
      theorem MeasureTheory.Filtration.coeFn_sup {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [Preorder ι] {f : MeasureTheory.Filtration ι m} {g : MeasureTheory.Filtration ι m} :
      (f g) = f g
      Equations
      • MeasureTheory.Filtration.instInf = { inf := fun (f g : MeasureTheory.Filtration ι m) => { seq := fun (i : ι) => f i g i, mono' := , le' := } }
      theorem MeasureTheory.Filtration.coeFn_inf {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [Preorder ι] {f : MeasureTheory.Filtration ι m} {g : MeasureTheory.Filtration ι m} :
      (f g) = f g
      Equations
      • One or more equations did not get rendered due to their size.
      theorem MeasureTheory.Filtration.sSup_def {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [Preorder ι] (s : Set (MeasureTheory.Filtration ι m)) (i : ι) :
      (sSup s) i = sSup ((fun (f : MeasureTheory.Filtration ι m) => f i) '' s)
      noncomputable instance MeasureTheory.Filtration.instInfSet {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [Preorder ι] :
      Equations
      • One or more equations did not get rendered due to their size.
      theorem MeasureTheory.Filtration.sInf_def {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [Preorder ι] (s : Set (MeasureTheory.Filtration ι m)) (i : ι) :
      (sInf s) i = if s.Nonempty then sInf ((fun (f : MeasureTheory.Filtration ι m) => f i) '' s) else m
      Equations
      theorem MeasureTheory.measurableSet_of_filtration {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [Preorder ι] {f : MeasureTheory.Filtration ι m} {s : Set Ω} {i : ι} (hs : MeasurableSet s) :

      A measure is σ-finite with respect to filtration if it is σ-finite with respect to all the sub-σ-algebra of the filtration.

      Instances

        Given an integrable function g, the conditional expectations of g with respect to a filtration is uniformly integrable.

        def MeasureTheory.filtrationOfSet {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [Preorder ι] {s : ιSet Ω} (hsm : ∀ (i : ι), MeasurableSet (s i)) :

        Given a sequence of measurable sets (sₙ), filtrationOfSet is the smallest filtration such that sₙ is measurable with respect to the n-th sub-σ-algebra in filtrationOfSet.

        Equations
        Instances For
          theorem MeasureTheory.measurableSet_filtrationOfSet {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [Preorder ι] {s : ιSet Ω} (hsm : ∀ (i : ι), MeasurableSet (s i)) (i : ι) {j : ι} (hj : j i) :
          theorem MeasureTheory.measurableSet_filtrationOfSet' {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [Preorder ι] {s : ιSet Ω} (hsm : ∀ (n : ι), MeasurableSet (s n)) (i : ι) :
          def MeasureTheory.Filtration.natural {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} {m : MeasurableSpace Ω} [TopologicalSpace β] [TopologicalSpace.MetrizableSpace β] [mβ : MeasurableSpace β] [BorelSpace β] [Preorder ι] (u : ιΩβ) (hum : ∀ (i : ι), MeasureTheory.StronglyMeasurable (u i)) :

          Given a sequence of functions, the natural filtration is the smallest sequence of σ-algebras such that that sequence of functions is measurable with respect to the filtration.

          Equations
          Instances For
            theorem MeasureTheory.Filtration.filtrationOfSet_eq_natural {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} {m : MeasurableSpace Ω} [TopologicalSpace β] [TopologicalSpace.MetrizableSpace β] [mβ : MeasurableSpace β] [BorelSpace β] [Preorder ι] [MulZeroOneClass β] [Nontrivial β] {s : ιSet Ω} (hsm : ∀ (i : ι), MeasurableSet (s i)) :
            MeasureTheory.filtrationOfSet hsm = MeasureTheory.Filtration.natural (fun (i : ι) => (s i).indicator fun (x : Ω) => 1)
            noncomputable def MeasureTheory.Filtration.limitProcess {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [Preorder ι] {E : Type u_4} [Zero E] [TopologicalSpace E] (f : ιΩE) (ℱ : MeasureTheory.Filtration ι m) (μ : MeasureTheory.Measure Ω) :
            ΩE

            Given a process f and a filtration , if f converges to some g almost everywhere and g is ⨆ n, ℱ n-measurable, then limitProcess f ℱ μ chooses said g, else it returns 0.

            This definition is used to phrase the a.e. martingale convergence theorem Submartingale.ae_tendsto_limitProcess where an L¹-bounded submartingale f adapted to converges to limitProcess f ℱ μ μ-almost everywhere.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              @[deprecated MeasureTheory.Filtration.memℒp_limitProcess_of_eLpNorm_bdd]
              theorem MeasureTheory.Filtration.memℒp_limitProcess_of_snorm_bdd {Ω : Type u_1} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {R : NNReal} {p : ENNReal} {F : Type u_5} [NormedAddCommGroup F] {ℱ : MeasureTheory.Filtration m} {f : ΩF} (hfm : ∀ (n : ), MeasureTheory.AEStronglyMeasurable (f n) μ) (hbdd : ∀ (n : ), MeasureTheory.eLpNorm (f n) p μ R) :

              Alias of MeasureTheory.Filtration.memℒp_limitProcess_of_eLpNorm_bdd.