Stochastic Processes

DefinitionMartingale#

A family of functions f : ι → Ω → E is a martingale with respect to a filtration ℱ if f is strongly adapted with respect to ℱ and for all i ≤ j, μ[f j | ℱ i] =ᵐ[μ] f i.

MeasureTheory.Martingale.{u_1, u_2, u_3} {Ω : Type u_1} {E : Type u_2} {ι : Type u_3} [Preorder ι]
  {m0 : MeasurableSpace Ω} [NormedAddCommGroup E] [NormedSpace ℝ E] (f : ι → Ω → E)
  (ℱ : MeasureTheory.Filtration ι m0) (μ : MeasureTheory.Measure Ω) : Prop
Sources
MathlibMeasureTheory.Martingale
Uses 1
Statement usesConditional expectation

TheoremOptional stopping theorem#

The optional stopping theorem (fair game theorem): a strongly adapted integrable process f is a submartingale if and only if for all bounded stopping times τ and π such that τ ≤ π, the stopped value of f at τ has expectation smaller than its stopped value at π.

MeasureTheory.submartingale_iff_expected_stoppedValue_mono.{u_1} {Ω : Type u_1}
  {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {𝒢 : MeasureTheory.Filtration ℕ m0}
  {f : ℕ → Ω → ℝ} [MeasureTheory.SigmaFiniteFiltration μ 𝒢]
  (hadp : MeasureTheory.StronglyAdapted 𝒢 f) (hint : ∀ (i : ℕ), MeasureTheory.Integrable (f i) μ) :
  MeasureTheory.Submartingale f 𝒢 μ ↔
    ∀ (τ π : Ω → WithTop ℕ),
      MeasureTheory.IsStoppingTime 𝒢 τ →
        MeasureTheory.IsStoppingTime 𝒢 π →
          τ ≤ π →
            (∃ N, ∀ (x : Ω), π x ≤ ↑N) →
              ∫ (x : Ω), MeasureTheory.stoppedValue f τ x ∂μ ≤
                ∫ (x : Ω), MeasureTheory.stoppedValue f π x ∂μ
Sources
MathlibMeasureTheory.submartingale_iff_expected_stoppedValue_mono
Uses 3
Statement usesBochner integral · Conditional expectation · Stopping time

DefinitionStopping time#

A stopping time with respect to some filtration f is a function τ such that for all i, the preimage of {j | j ≤ i} along τ is measurable with respect to f i.

Intuitively, the stopping time τ describes some stopping rule such that at time i, we may determine it with the information we have at time i.

MeasureTheory.IsStoppingTime.{u_1, u_3} {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω}
  [Preorder ι] (f : MeasureTheory.Filtration ι m) (τ : Ω → WithTop ι) : Prop
Sources
MathlibMeasureTheory.IsStoppingTime
Uses 1 · Used by 1
Statement usesEvents
Used byOptional stopping theorem

DefinitionHitting time#

Hitting time: given a stochastic process u and a set s, hittingBtwn u s n m is the first time u is in s after time n and before time m (if u does not hit s after time n and before m then the hitting time is simply m).

The hitting time is a stopping time if the process is strongly adapted and discrete.

MeasureTheory.hittingBtwn.{u_1, u_2, u_3} {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} [Preorder ι]
  [InfSet ι] (u : ι → Ω → β) (s : Set β) (n m : ι) : Ω → ι
Sources
MathlibMeasureTheory.hittingBtwn
Uses 1
Statement usesSet

StructureGaussian processes#

A stochastic process is a Gaussian process if all its finite dimensional distributions are Gaussian.

ProbabilityTheory.IsGaussianProcess.{u_1, u_2, u_3} {Ω : Type u_1} {E : Type u_2} {T : Type u_3}
  {mΩ : MeasurableSpace Ω} [MeasurableSpace E] [TopologicalSpace E] [AddCommMonoid E]
  [_root_.Module ℝ E] (X : T → Ω → E) (P : MeasureTheory.Measure Ω := by volume_tac) : Prop
Sources
MathlibProbabilityTheory.IsGaussianProcess
Uses 2
Statement usesGaussian measures · Product of sigma-algebras

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.