Almost-Everywhere Congruence Of Itô Integrals

This is an auxiliary locality theorem for the Brownian Itô integral. Let $W_j$ be a Brownian motion on a probability space $(\Omega,P)$ with Brownian filtration $\mathcal F$. Let $H_1,H_2:\Omega\times\mathbb R\to\mathbb R$ be jointly measurable and progressively measurable, and assume that for every $T>0$ their squared $\operatorname{ENNReal}$ norms are integrable over $\Omega\times[0,T]$:

If $t>0$ and $H_1(\omega,s)=H_2(\omega,s)$ for $P$-almost every $\omega$ and volume-almost every $s\in[0,t]$, then

The lemma records that the stochastic integral at time $t$ depends only on the integrand up to product-null equality on $[0,t]$.

Original Lean declaration header

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

theorem itoIntegral_congr_ae
    (Wj : LevyStochCalc.Brownian.BrownianMotion P)
    (ℱ : MeasureTheory.Filtration ℝ ‹MeasurableSpace Ω›)
    (hℱ : LevyStochCalc.Brownian.IsBrownianFiltration Wj ℱ)
    (H₁ H₂ : Ω → ℝ → ℝ)
    (hm₁ : Measurable (Function.uncurry H₁))
    (hp₁ : Probability.ProgressivelyMeasurable ℱ H₁)
    (hs₁ : ∀ T : ℝ, 0 < T →
      ∫⁻ ω, ∫⁻ s in Set.Icc (0 : ℝ) T, (‖H₁ ω s‖₊ : ℝ≥0∞) ^ 2 ∂volume ∂P < ⊤)
    (hm₂ : Measurable (Function.uncurry H₂))
    (hp₂ : Probability.ProgressivelyMeasurable ℱ H₂)
    (hs₂ : ∀ T : ℝ, 0 < T →
      ∫⁻ ω, ∫⁻ s in Set.Icc (0 : ℝ) T, (‖H₂ ω s‖₊ : ℝ≥0∞) ^ 2 ∂volume ∂P < ⊤)
    {t : ℝ} (ht : 0 < t)
    (h : ∀ᵐ ω ∂P, ∀ᵐ s ∂(volume.restrict (Set.Icc (0 : ℝ) t)), H₁ ω s = H₂ ω s) :
    ∀ᵐ ω ∂P, LevyStochCalc.Brownian.Ito.stochasticIntegral Wj ℱ hℱ H₁ hm₁ hp₁ hs₁ t ω
      = LevyStochCalc.Brownian.Ito.stochasticIntegral Wj ℱ hℱ H₂ hm₂ hp₂ hs₂ t ω

Module navigation

Module: LevyStochCalc/Ito/PicardLocality.

Definition modules: LevyStochCalc/Brownian/ItoL2CompletionApi, LevyStochCalc/Brownian/Filtered, LevyStochCalc/Brownian/Construction, LevyStochCalc/Probability/Progressive.

Next: compensatedIntegral_congr_ae.

Source excerpt, lines 90–106 · Frozen source 408915f.