Characterization of the stochastic integral.

This file contains an axiomatic characterization of the stochastic integral against a process Y : ι → Ω → ℝ. The integral is defined as a map from ι → Ω → ℝ to Ω → ℝ, meaning that we are evaluating the integral at some fixed, terminal time.

We ask for the following properties, which we expect any good stochastic integral I to have:

• The integral agrees with the Riemann-Stieltjes integral for elementary processes.
• Linearity for the integral and its domain.
• The integral and its domain respect indistinguishability.
• Dominated convergence: if a process X is integrable, then any pointwise limit of a sequence of integrable processes which is dominated by X should again be integrable.

The properties above are encoded in the predicate IsRiemannStieltjesExtension. However, this predicate does not ensure that the integral is canonical or unique. To get a true stochastic integral I, we additionally impose the following.

• Any extension of the Riemann-Stieltjes integral must agree with I on the intersection of their domains.

This additional condition is encoded in IsStochasticIntegral which extends IsRiemannStieltjesExtension.

Note that none of the definitions impose that the domain S should be maximal. As a consequence, it is possible to define stochastic integrals with different domains. However, any two such integrals will necessarily agree (almost surely) on the intersection of their domains.

@[reducible, inline]

abbrev ProbabilityTheory.Domain {Ω : Type u_1} {ι : Type u_2} : Type (max u_1 u_2)

A domain is a subset of stochastic processes.

Equations

• ProbabilityTheory.Domain = Set (ι → Ω → ℝ)

@[reducible, inline]

abbrev ProbabilityTheory.SIntegral {Ω : Type u_1} {ι : Type u_2} : Type (max u_1 u_2)

An SIntegral maps processes to random variables.

Equations

• ProbabilityTheory.SIntegral = ((ι → Ω → ℝ) → Ω → ℝ)

structure ProbabilityTheory.IsRiemannStieltjesExtension {Ω : Type u_1} {mΩ : MeasurableSpace Ω} (P : MeasureTheory.Measure Ω) {ι : Type u_2} [LinearOrder ι] [OrderBot ι] (Y : ι → Ω → ℝ) (𝓕 : MeasureTheory.Filtration ι mΩ) (I : SIntegral) (S : Domain) : Prop

An SIntegral I with domain S is an extension of the Riemann-Stieltjes integral if it agrees with Riemann-Stieltjes on elementary processes and respects linearity, indistinguishability, and dominated convergence.

• measurable (X : ι → Ω → ℝ) (h : X ∈ S) : MeasureTheory.AEStronglyMeasurable (I X) P

  The stochastic integral is measurable.

• elementary_ioc (i j : ι) (h : i ≤ j) (X : MeasureTheory.SimpleFunc Ω ℝ) : (fun (k : ι) (ω : Ω) => if k ∈ Set.Ioc i j then X ω else 0) ∈ S ∧ (I fun (k : ι) (ω : Ω) => if k ∈ Set.Ioc i j then X ω else 0) =ᵐ[P] ⇑X * (Y j - Y i)

  Elementary functions are in the domain and the value of the integral is the expected one.

• elementary_iic (i : ι) (X : MeasureTheory.SimpleFunc Ω ℝ) : (fun (j : ι) (ω : Ω) => if j ∈ Set.Iic i then X ω else 0) ∈ S ∧ (I fun (j : ι) (ω : Ω) => if j ∈ Set.Iic i then X ω else 0) =ᵐ[P] ⇑X * (Y i - Y ⊥)
• integral_add (X₁ X₂ : ι → Ω → ℝ) (h₁ : X₁ ∈ S) (h₂ : X₂ ∈ S) : X₁ + X₂ ∈ S ∧ I (X₁ + X₂) =ᵐ[P] I X₁ + I X₂

  The integral and the domain respect addition.

• integral_smul (X : ι → Ω → ℝ) (α : ℝ) (h : X ∈ S) : α • X ∈ S ∧ I (α • X) =ᵐ[P] α • I X

  The integral and the domain respect scalar multiplication.

• integral_indistinguishable (X₁ X₂ : ι → Ω → ℝ) (h₁ : X₁ ∈ S) (h₂ : X₁ ≡ᵐ[P] X₂) : X₂ ∈ S ∧ I X₁ =ᵐ[P] I X₂

  The integral and its domain respect indistinguishability.

• integral_dct (X : ℕ → ι → Ω → ℝ) (X_dom X_lim : ι → Ω → ℝ) (h₁ : ∀ (n : ℕ), X n ∈ S) (h₂ : X_dom ∈ S) (h_dom : ∀ (n : ℕ) (i : ι) (ω : Ω), |X n i ω| ≤ |X_dom i ω|) (h_lim : ∀ (i : ι) (ω : Ω), Filter.Tendsto (fun (x : ℕ) => X x i ω) Filter.atTop (nhds (X_lim i ω))) : X_lim ∈ S ∧ MeasureTheory.TendstoInMeasure P (fun (n : ℕ) => I (X n)) Filter.atTop (I X_lim)

  The domain is closed under dominated convergence, and in this case the integral commutes with the limit.

structure ProbabilityTheory.IsStochasticIntegral {Ω : Type u_1} {mΩ : MeasurableSpace Ω} (P : MeasureTheory.Measure Ω) {ι : Type u_2} [LinearOrder ι] [OrderBot ι] (Y : ι → Ω → ℝ) (𝓕 : MeasureTheory.Filtration ι mΩ) (I : SIntegral) (S : Domain) extends ProbabilityTheory.IsRiemannStieltjesExtension P Y 𝓕 I S : Prop

An SIntegral I with domain S is a stochastic integral if it is an extension of the Riemann-Stieltjes integral and it agrees with any other extension on the intersection of their domains.

• measurable (X : ι → Ω → ℝ) (h : X ∈ S) : MeasureTheory.AEStronglyMeasurable (I X) P
• elementary_ioc (i j : ι) (h : i ≤ j) (X : MeasureTheory.SimpleFunc Ω ℝ) : (fun (k : ι) (ω : Ω) => if k ∈ Set.Ioc i j then X ω else 0) ∈ S ∧ (I fun (k : ι) (ω : Ω) => if k ∈ Set.Ioc i j then X ω else 0) =ᵐ[P] ⇑X * (Y j - Y i)
• elementary_iic (i : ι) (X : MeasureTheory.SimpleFunc Ω ℝ) : (fun (j : ι) (ω : Ω) => if j ∈ Set.Iic i then X ω else 0) ∈ S ∧ (I fun (j : ι) (ω : Ω) => if j ∈ Set.Iic i then X ω else 0) =ᵐ[P] ⇑X * (Y i - Y ⊥)
• integral_add (X₁ X₂ : ι → Ω → ℝ) (h₁ : X₁ ∈ S) (h₂ : X₂ ∈ S) : X₁ + X₂ ∈ S ∧ I (X₁ + X₂) =ᵐ[P] I X₁ + I X₂
• integral_smul (X : ι → Ω → ℝ) (α : ℝ) (h : X ∈ S) : α • X ∈ S ∧ I (α • X) =ᵐ[P] α • I X
• integral_indistinguishable (X₁ X₂ : ι → Ω → ℝ) (h₁ : X₁ ∈ S) (h₂ : X₁ ≡ᵐ[P] X₂) : X₂ ∈ S ∧ I X₁ =ᵐ[P] I X₂
• integral_dct (X : ℕ → ι → Ω → ℝ) (X_dom X_lim : ι → Ω → ℝ) (h₁ : ∀ (n : ℕ), X n ∈ S) (h₂ : X_dom ∈ S) (h_dom : ∀ (n : ℕ) (i : ι) (ω : Ω), |X n i ω| ≤ |X_dom i ω|) (h_lim : ∀ (i : ι) (ω : Ω), Filter.Tendsto (fun (x : ℕ) => X x i ω) Filter.atTop (nhds (X_lim i ω))) : X_lim ∈ S ∧ MeasureTheory.TendstoInMeasure P (fun (n : ℕ) => I (X n)) Filter.atTop (I X_lim)
• consistent (I' : SIntegral) (S' : Domain) (h : IsRiemannStieltjesExtension P Y 𝓕 I' S') (X : ι → Ω → ℝ) (hX : X ∈ S ∩ S') : I X =ᵐ[P] I' X