Initial Value of a Vector Itô Version

This vendored statement from LevyStochCalc asserts that a vector Itô version starts at its prescribed initial value.

Let $(\Omega,P)$ be a measurable probability space. Let $W$ be a $d$-dimensional Brownian motion under $P$, let $\mathcal F'$ be a filtration, and assume that every coordinate Brownian motion of $W$ is Brownian with respect to $\mathcal F'$. Let $H$, $X_0$, $b$, and $X$ satisfy the measurability, progressive measurability, local square-integrability, and vector-Itô-version hypotheses appearing in IsVectorItoVersion.

Then the process value at time zero equals the initial function almost everywhere:

The equality is an a.e. equality of functions $\Omega\to\operatorname{Fin}(n)\to\mathbb R$. This metadata describes the theorem from the vendored upstream repository at commit 984dbf0b790031eac05d56fe5a84b65e15e1e932.

Original Lean declaration header

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

theorem version_ae_eq_zero
    {H : Fin n → Fin d → Ω → ℝ → ℝ}
    {hm : ∀ p k, Measurable (Function.uncurry (H p k))}
    {hpg : ∀ p k, Probability.ProgressivelyMeasurable ℱ' (H p k)}
    {hq : ∀ (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 → Ω → ℝ → ℝ} {X : ℝ → Ω → Fin n → ℝ}
    (hX : IsVectorItoVersion W ℱ' hcoord H hm hpg hq X₀ b X) :
    X 0 =ᵐ[P] X₀

Module navigation

Module: LevyStochCalc/Ito/ItoFormulaUnboundedClamp.

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

Previous: ae_tendsto_version_clamp_at.

Source excerpt, lines 520–528 · Frozen source 408915f.