Pathwise Decomposition of a Finite-Range Stopped Integrand

This is the pathwise decomposition of the cut integrand used for finite-range optional stopping.

Let $\tau:\Omega\to\operatorname{WithTop}(\mathbb R)$, let $H:\Omega\times\mathbb R\to\mathbb R$, let $t\in\mathbb R$, and let $J$ be a finite set of real times. Assume:

1. every $c\in J$ satisfies $0\le c$;
2. every $c\in J$ satisfies $c<t$;
3. for every $\omega$, either $\tau(\omega)=c$ for some $c\in J$, or $t\le\tau(\omega)$.

Then the indicator-term representation indTerm of the stopped integrand Probability.stopped τ H on $(0,t]$ is pointwise

This neutral pathwise identity is the algebraic component of the finite-range optional-stopping theorem.

Original Lean declaration header

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

theorem stopped_eq_sub_sum (H : Ω → ℝ → ℝ) {t : ℝ} (J : Finset ℝ)
    (hJ0 : ∀ c ∈ J, 0 ≤ c) (hJt : ∀ c ∈ J, c < t)
    (hτJ : ∀ ω, (∃ c ∈ J, τ ω = ((c : ℝ) : WithTop ℝ)) ∨ ((t : ℝ) : WithTop ℝ) ≤ τ ω) :
    indTerm (Probability.stopped τ H) 0 t
      = fun ω s => indTerm H 0 t ω s - ∑ c ∈ J, cutTerm τ H c t ω s

Module navigation

Module: LevyStochCalc/Brownian/ItoOptionalStopping.

Definition modules: LevyStochCalc/Probability/StoppedProgressive.

Next: stochasticIntegralBrownian_stopped.

Source excerpt, lines 143–147 · Frozen source 408915f.