Locality of the Itô Integral at an Unreached Stopping Time

This proves the local property of the Itô integral.

Let $(\Omega,\mathcal A,P)$ be a probability space, let $\tau$ be an $\mathcal F$-stopping time, and let $W$ be a Brownian motion with Brownian filtration $\mathcal F$. Let $H$ be jointly measurable and progressively measurable, and assume that for every $T>0$ its ENNReal energy is finite:

For every $t>0$, for $P$-almost every $\omega$ such that $t\le\tau(\omega)$, the integral of the stopped integrand agrees with the original integral:

The conclusion is conditional on the event that the stopping time has not been reached by time $t$; the equality is not asserted outside that event.

Formalization Note. The stopping-time values and the comparison with $t$ use WithTop ℝ; all finite-energy conditions are strict inequalities below $\top$ in ENNReal.

Original Lean declaration header

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

theorem stochasticIntegralBrownian_stopped_eq_of_le
    (hτ : MeasureTheory.IsStoppingTime ℱ τ)
    {H : Ω → ℝ → ℝ} (hm : Measurable (Function.uncurry H))
    (hp : Probability.ProgressivelyMeasurable ℱ H)
    (hq : ∀ T, 0 < T → ∫⁻ ω, ∫⁻ s in Set.Icc (0 : ℝ) T,
      (‖H ω s‖₊ : ℝ≥0∞) ^ 2 ∂volume ∂P < ⊤)
    {t : ℝ} (ht : 0 < t) :
    ∀ᵐ ω ∂P, ((t : ℝ) : WithTop ℝ) ≤ τ ω →
      stochasticIntegralBrownian W ℱ hℱ (Probability.stopped τ H)
          (Probability.measurable_uncurry_stopped hτ hm)
          (Probability.ProgressivelyMeasurable.stopped hτ hp)
          (energy_lt_top_of_abs_le (fun ω s => Probability.abs_stopped_le τ H ω s) hq) t ω
        = stochasticIntegralBrownian W ℱ hℱ H hm hp hq t ω

Module navigation

Module: LevyStochCalc/Brownian/ItoLocality.

Definition modules: LevyStochCalc/Brownian/ItoL2CompletionMaster, LevyStochCalc/Brownian/Filtered, LevyStochCalc/Probability/StoppedProgressive, LevyStochCalc/Brownian/Construction, LevyStochCalc/Probability/Progressive, LevyStochCalc/Brownian/ItoOptionalStopping.

Supporting theorems: eventually_gridStop_lt, gridStopAux_le_iff, stochasticIntegralBrownian_stopped.

Previous: eventually_gridStop_lt · Next: stochasticIntegralBrownian_congr_of_pos.

Source excerpt, lines 294–306 · Frozen source 408915f.