BoundedStoppedItoMean: mathematical reading route

Read the statements and derivations in source order. Every result has its own optional Lean statement and proof. Source assumptions, library reuse and unproved boundaries are kept explicit.

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

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.

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.

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.