Vector Itô Process at Initial Time

This states that a vector Itô process equals its initial value almost everywhere at time zero.

Let $P$ be a probability measure, let $W$ be a multidimensional Brownian motion, and let $\mathcal F$ be a filtration with the required Brownian-coordinate properties. Let $H$ and $b$ be measurable and progressively measurable coefficient and drift families, and assume that each coefficient has finite squared energy on every interval $[0,T]$ with $T>0$. For an initial state $X_0:\Omega\to\mathbb R^n$,

The equality is an almost-everywhere equality of functions $\Omega\to(\mathbb R^n)$, with coordinates indexed by Fin n. This provides the initial-time property used by vector Itô version constructions.

Original Lean declaration header

Within namespace LevyStochCalc.Brownian.Ito. Shown in its original module context. Proof omitted.

theorem vectorItoProcess_ae_eq_zero (W : Multidim.MultidimBrownianMotion P d)
    (ℱ : Filtration ℝ ‹MeasurableSpace Ω›)
    (hcoord : ∀ k : Fin d, IsBrownianFiltration (W.W k) ℱ)
    {H : Fin n → Fin d → Ω → ℝ → ℝ}
    (hHm : ∀ p k, Measurable (Function.uncurry (H p k)))
    (hHp : ∀ p k, Probability.ProgressivelyMeasurable ℱ (H p k))
    (hHs : ∀ (p : Fin n) (k : Fin d) (T : ℝ), 0 < T → ∫⁻ ω, ∫⁻ s in Set.Icc (0 : ℝ) T,
      (‖H p k ω s‖₊ : ℝ≥0∞) ^ 2 ∂volume ∂P < ⊤)
    (X₀ : Ω → Fin n → ℝ) (b : Fin n → Ω → ℝ → ℝ) :
    vectorItoProcess W ℱ hcoord H hHm hHp hHs X₀ b 0 =ᵐ[P] X₀

Module navigation

Module: LevyStochCalc/Ito/VectorItoVersionLimit.

Definition modules: LevyStochCalc/Brownian/Filtered, LevyStochCalc/Brownian/Multidim, LevyStochCalc/Probability/Progressive, LevyStochCalc/Brownian/VectorItoProcess.

Previous: exists_seq_clampMesh_window_lt · Next: exists_isVectorItoVersion_of_unbounded.

Source excerpt, lines 157–166 · Frozen source 408915f.