Samplinglib mathematical lesson

A completed Ito process is integrable at a bounded stopping time

AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.BoundedStoppedItoMean.itoIntegralProcess_at_boundedStopping_integrable · theorem · Teaching coverage

Read this first

Mathematical statement

Let eta be progressive and square-integrable on a positive finite horizon T, and let tau be a nonnegative stopping time with tau at most T pointwise. The completed Ito process I(eta) evaluated at tau is integrable.

\[I_t=\int_0^t\eta_s\,dB_s,\qquad \tau\le T\Longrightarrow I_\tau\in L^1.\]

Lean statement · itoIntegralProcess_at_boundedStopping_integrable

The theorem returns literal Bochner integrability of omega ↦ itoIntegralProcess eta ... (tau omega) omega under the ambient measure, with an explicit finite-measure typeclass already entailed by the Brownian contract.

Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.

Download module (.lean)

theorem itoIntegralProcess_at_boundedStopping_integrable
    [IsFiniteMeasure mu]
    (eta : ProgressiveL2Integrand filtration mu T) (hT : 0 < T)
    (tau : Omega → ℝ≥0)
    (htau : IsChewiStoppingTime filtration
      (fun omega => (tau omega : WithTop ℝ≥0)))
    (htauT : ∀ omega, tau omega ≤ T)
    (hB : IsBrownianMotionWithFiltration B filtration mu)
    (hUsual : SatisfiesUsualConditions filtration mu) :
    Integrable
      (fun omega => itoIntegralProcess eta hT hB hUsual (tau omega) omega) mu

Exact module and namespace context

Proof roadmap

1Stop the integrand
Form the closed stopped integrand eta times the indicator of s≤tau. It remains progressive and L2 on the same horizon.
2Use terminal L2 integrability
The terminal representative of the completed Ito integral of the stopped integrand belongs to L2, hence to L1 on the finite measure space.
3Identify random evaluation
The completed bounded random-stopping theorem identifies that terminal representative almost everywhere with the original continuous Ito process evaluated at tau. Integrability transfers across almost-everywhere equality.

Full assumptions and notation

All objects and hypotheses

eta is a Samplinglib ProgressiveL2Integrand on a positive NNReal horizon T.
B is Brownian with respect to the filtration and measure; this contract implies that the measure is a probability measure.
The filtration satisfies Samplinglib's usual conditions.
tau is an NNReal-valued Chewi stopping time and tau(omega)≤T for every omega.
Lean requests an ambient finite-measure instance to elaborate the completed process; this is logically redundant because the Brownian contract supplies a probability measure.

Mathematical proof

1. Stop the integrand

Form the closed stopped integrand eta times the indicator of s≤tau. It remains progressive and L2 on the same horizon.

\[\eta^\tau_s=\eta_s\mathbf 1_{s\le\tau}.\]

Corresponding Lean step

Use ProgressiveL2Stopping.stop.

2. Use terminal L2 integrability

The terminal representative of the completed Ito integral of the stopped integrand belongs to L2, hence to L1 on the finite measure space.

\[\int_0^T\eta^\tau_s\,dB_s\in L^2\subseteq L^1.\]

Corresponding Lean step

Use ItoIntegralProcess.terminalRepresentative_integrable.

3. Identify random evaluation

The completed bounded random-stopping theorem identifies that terminal representative almost everywhere with the original continuous Ito process evaluated at tau. Integrability transfers across almost-everywhere equality.

\[\int_0^T\eta^\tau_s\,dB_s=I_\tau\quad\text{a.s.}\]

Corresponding Lean step

Use RandomStoppingGeneralIto.itoIntegralTerminal_stop_ae and Integrable.congr.

Lean verification

The exact proof begins folded immediately after the mathematical argument; the statement is folded beside the claim above.

Lean proof · itoIntegralProcess_at_boundedStopping_integrable

The proof transfers the existing L1 property of the stopped terminal representative through the library's completed random-stopping almost-everywhere identity.

Download module (.lean)

theorem itoIntegralProcess_at_boundedStopping_integrable
    [IsFiniteMeasure mu]
    (eta : ProgressiveL2Integrand filtration mu T) (hT : 0 < T)
    (tau : Omega → ℝ≥0)
    (htau : IsChewiStoppingTime filtration
      (fun omega => (tau omega : WithTop ℝ≥0)))
    (htauT : ∀ omega, tau omega ≤ T)
    (hB : IsBrownianMotionWithFiltration B filtration mu)
    (hUsual : SatisfiesUsualConditions filtration mu) :
    Integrable
      (fun omega => itoIntegralProcess eta hT hB hUsual (tau omega) omega) mu := by
  let _ : IsProbabilityMeasure mu := hB.isProbabilityMeasure
  let stoppedEta := stop eta (fun omega => (tau omega : WithTop ℝ≥0)) htau
  have hterminal :
      terminalRepresentative stoppedEta hT hB =ᵐ[mu]
        (fun omega => itoIntegralProcess eta hT hB hUsual (tau omega) omega) := by
    exact (itoIntegralTerminal_stop_ae eta hT tau htau htauT hB hUsual)
  exact (terminalRepresentative_integrable stoppedEta hT hB).congr hterminal

Exact module and namespace context

Scope and omitted-condition boundaries

The theorem requires a positive finite construction horizon and a pointwise bounded NNReal stopping time. It does not cover unbounded stopping, local-L2 integrands before localization, vector stochastic integrals, or any Ito formula.

Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

MeasureTheory.Integrable.congr

Mathematical sources

Samplinglib completed bounded random-stopping identity (historical source) — Almost-everywhere identification of the stopped terminal integral with random evaluation of the continuous completed Ito process.

Samplinglib prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.