Samplinglib mathematical lesson

A completed Ito process has mean zero at a bounded stopping time

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

Read this first

Mathematical statement

Under the same global L2, Brownian, usual-filtration, stopping-time, and pointwise horizon-bound assumptions, the integral of the completed Ito process evaluated at tau is zero.

\[\mathbb E\left[\int_0^\tau\eta_s\,dB_s\right]=0.\]

Lean statement · integral_itoIntegralProcess_at_boundedStopping_eq_zero

The conclusion is the literal Bochner integral equality for random-time evaluation of the constructed completed Ito process.

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 integral_itoIntegralProcess_at_boundedStopping_eq_zero
    [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) :
    ∫ omega, itoIntegralProcess eta hT hB hUsual (tau omega) omega ∂mu = 0

Exact module and namespace context

Proof roadmap

1Use the stopped-integrand martingale
The completed Ito process of the stopped integrand is a martingale and starts exactly at zero, including on the patched exceptional set.
2Compare deterministic times zero and T
The martingale set-integral identity on the whole sample space makes the expectation at T equal the expectation at zero, hence zero.
3Transfer to the bounded stopping time
The terminal representative agrees almost everywhere both with J_T and with the original completed process I evaluated at tau. Integral congruence transfers the zero expectation.

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, and the filtration satisfies the usual conditions.
tau is an NNReal-valued stopping time with tau(omega)≤T for every omega.
The theorem concerns the library's actual completed continuous Ito process, not an arbitrary process supplied together with a martingale premise.

Mathematical proof

1. Use the stopped-integrand martingale

The completed Ito process of the stopped integrand is a martingale and starts exactly at zero, including on the patched exceptional set.

\[J_t=\int_0^t\eta_s\mathbf 1_{s\le\tau}\,dB_s,\qquad J_0=0.\]

Corresponding Lean step

Use itoIntegralProcess_martingale and itoIntegralProcess_at_zero.

2. Compare deterministic times zero and T

The martingale set-integral identity on the whole sample space makes the expectation at T equal the expectation at zero, hence zero.

\[\mathbb E[J_T]=\mathbb E[J_0]=0.\]

Corresponding Lean step

Use Martingale.setIntegral_eq with the universal measurable set.

3. Transfer to the bounded stopping time

The terminal representative agrees almost everywhere both with J_T and with the original completed process I evaluated at tau. Integral congruence transfers the zero expectation.

\[J_T=\int_0^T\eta_s\mathbf 1_{s\le\tau}\,dB_s=I_\tau\quad\text{a.s.}\]

Corresponding Lean step

Use terminalRepresentative_ae_eq_actual, itoIntegralTerminal_stop_ae, and integral_congr_ae.

Lean verification

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

Lean proof · integral_itoIntegralProcess_at_boundedStopping_eq_zero

The proof applies deterministic-time preservation of martingale expectation to the stopped integrand and then rewrites the terminal value using the two existing almost-everywhere consistency theorems.

Download module (.lean)

theorem integral_itoIntegralProcess_at_boundedStopping_eq_zero
    [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) :
    ∫ omega, itoIntegralProcess eta hT hB hUsual (tau omega) omega ∂mu = 0 := by
  let _ : IsProbabilityMeasure mu := hB.isProbabilityMeasure
  let stoppedEta := stop eta (fun omega => (tau omega : WithTop ℝ≥0)) htau
  have hmartingale :
      Martingale (itoIntegralProcess stoppedEta hT hB hUsual) filtration mu :=
    itoIntegralProcess_martingale stoppedEta hT hB hUsual
  have hterminalMean :
      ∫ omega, terminalRepresentative stoppedEta hT hB omega ∂mu = 0 := by
    have hmean := hmartingale.setIntegral_eq (show (0 : ℝ≥0) ≤ T from bot_le)
      (MeasurableSet.univ : MeasurableSet[filtration 0] Set.univ)
    have hprocessMean :
        ∫ omega, itoIntegralProcess stoppedEta hT hB hUsual T omega ∂mu = 0 := by
      simpa only [Measure.restrict_univ, itoIntegralProcess_at_zero,
        Pi.zero_apply, integral_zero] using hmean.symm
    exact integral_congr_ae
      (terminalRepresentative_ae_eq_actual stoppedEta hT hB hUsual) |>.trans hprocessMean
  calc
    ∫ omega, itoIntegralProcess eta hT hB hUsual (tau omega) omega ∂mu =
        ∫ omega, terminalRepresentative stoppedEta hT hB omega ∂mu := by
          apply integral_congr_ae
          exact (itoIntegralTerminal_stop_ae eta hT tau htau htauT hB hUsual).symm
    _ = 0 := hterminalMean

end BoundedStoppedItoMean
end StochasticProcesses
end TechnicalLemmas
end AutoSamplingTheory

Exact module and namespace context

Scope and omitted-condition boundaries

This is not a general optional-sampling theorem and does not cover unbounded stopping times, local martingales without localization, vector stochastic integrals, quadratic variation, or Ito's formula.

Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

MeasureTheory.Martingale.setIntegral_eq
MeasureTheory.integral_congr_ae

Mathematical sources

Samplinglib completed bounded random-stopping identity (historical source) — The completed stochastic-integral consistency result used after the martingale mean calculation.
Mathlib martingale set-integral identity — Equality of martingale integrals at ordered deterministic times.

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