Finite-Range Optional Stopping Identity

This proves optional stopping for a stopping time whose values below the horizon form a finite set.

Let $(\Omega,\mathcal A,P)$ be a probability space, let $\tau:\Omega\to\operatorname{WithTop}(\mathbb R)$ be an $\mathcal F$-stopping time, and let $W$ and $\mathcal F$ form a Brownian motion and Brownian filtration. Let $H$ be jointly measurable and progressively measurable, with

$$\int_\Omega\int_{[0,T]}\|H(\omega,s)\|_+^2\,ds\,dP<\top$$

for every $T>0$. Fix $t>0$ and a finite set $J\subset\mathbb R$ such that every $c\in J$ satisfies $0\le c$ and $c<t$, and assume that for every $\omega$ either $\tau(\omega)=c$ for some $c\in J$ or $t\le\tau(\omega)$.

Then, $P$-almost everywhere,

$$I_t[\operatorname{stopped}(\tau,H)](\omega) = I_t[H](\omega) -\sum_{c\in J}\operatorname{hitInd}(\tau,c,\omega)\bigl(I_t[H](\omega)-I_c[H](\omega)\bigr).$$

The stopped integrand is equipped with the measurability, progressive-measurability, and finite-energy witnesses generated from the hypotheses.

This is the finite-range identity from which the general local property is obtained by approximation.

Original Lean declaration header

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

theorem stochasticIntegralBrownian_stopped
    (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) (J : Finset ℝ)
    (hJ0 : ∀ c ∈ J, 0 ≤ c) (hJt : ∀ c ∈ J, c < t)
    (hτJ : ∀ ω, (∃ c ∈ J, τ ω = ((c : ℝ) : WithTop ℝ)) ∨ ((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
      =ᵐ[P] fun ω => stochasticIntegralBrownian W ℱ hℱ H hm hp hq t ω
        - ∑ c ∈ J, hitInd τ c ω * (stochasticIntegralBrownian W ℱ hℱ H hm hp hq t ω
            - stochasticIntegralBrownian W ℱ hℱ H hm hp hq c ω)

Module navigation

Module: LevyStochCalc/Brownian/ItoOptionalStopping.

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

Selected supporting theorems: exists_stochasticIntegralBrownian_finsetSum, lintegral_energy_lt_top_of_bound, mul_stochasticIntegralBrownian_indIoc, progressivelyMeasurable_mul_indIoc, stochasticIntegralBrownian_indicator_Ioc.

Previous: stopped_eq_sub_sum.

Source excerpt, lines 240–255 · Frozen source 408915f.

import Definitions.Def_KLSModular_LevyStochCalc_Brownian_ItoOptionalStopping

/-
Copyright (c) 2026 Christian Garry. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Christian Garry
-/
-- Vendored from https://github.com/cgarryZA/LevyStochCalc at commit 984dbf0b790031eac05d56fe5a84b65e15e1e932 (upstream path LevyStochCalc/Brownian/ItoOptionalStopping.lean; Apache-2.0; provenance in formalization/vendor/vendor-lock.json of the KLS repository)
open MeasureTheory ProbabilityTheory
open scoped NNReal ENNReal
universe u
variable {Ω : Type u} [MeasurableSpace Ω] {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P]
variable (τ : Ω → WithTop ℝ)
variable (W : LevyStochCalc.Brownian.BrownianMotion P)
  (ℱ : MeasureTheory.Filtration ℝ ‹MeasurableSpace Ω›) (hℱ : LevyStochCalc.Brownian.IsBrownianFiltration W ℱ)
include hℱ

theorem LevyStochCalc.Brownian.Ito.stochasticIntegralBrownian_stopped_readable
    (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) (J : Finset ℝ)
    (hJ0 : ∀ c ∈ J, 0 ≤ c) (hJt : ∀ c ∈ J, c < t)
    (hτJ : ∀ ω, (∃ c ∈ J, τ ω = ((c : ℝ) : WithTop ℝ)) ∨ ((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
      =ᵐ[P] fun ω => stochasticIntegralBrownian W ℱ hℱ H hm hp hq t ω
        - ∑ c ∈ J, hitInd τ c ω * (stochasticIntegralBrownian W ℱ hℱ H hm hp hq t ω
            - stochasticIntegralBrownian W ℱ hℱ H hm hp hq c ω) := by sorry