1.1 · Book p. 3 · PDF p. 15

A Primer on Stochastic Calculus

Introduces Brownian motion, stochastic integrals, Itô calculus, and the solution concept used to state Langevin dynamics as an SDE. Reading note on hidden prerequisites: Chewi often invokes standard calculation rules without numbering every supporting theorem. In this section the derivations implicitly require the usual conditions on the filtration; progressive measurability and its restriction/adaptedness consequences; measurability of stopped processes and first-hitting times of continuous adapted energy paths; Tonelli/Fubini on the probability-time product measure; nullity of singleton time endpoints so \((0,t)\), \([0,t]\), and related representatives agree in \(L^2\); the elementary Itô isometry \(\mathbb E[(\sum_i H_i\,\Delta B_i)^2]=\mathbb E[\int H_t^2\,dt]\); \(L^2\) completion and uniqueness of representatives; Doob's \(L^2\) maximal inequality plus Borel–Cantelli for a continuous version; continuity and monotonicity of \(A_t=\int_0^{t\wedge T}\eta_s^2\,ds\); the identity between energy-threshold stopping and stopping at \(\tau_n=\inf\{t:A_t\ge n\}\); finite expected energy after stopping; and consistency of stopped Itô integrals on overlapping horizons. ASTIS treats these as explicit implicit-lemma obligations rather than silently folding them into a calculation rule.

Open this section in the canonical August 9 source ↗

Theorem 1.1.8

Every progressive process with finite probability-time L2 energy has an Ito integral that is an adapted continuous martingale, is characterized at each deterministic time by the restricted terminal L2 completion, and satisfies the Ito isometry.

\[I_t(\eta)=\int_0^t \eta_s\,dB_s,\qquad \mathbb E[I_t(\eta)^2]=\mathbb E\!\left[\int_0^t \eta_s^2\,ds\right]\]

For a progressive square-integrable integrand \(\eta\), elementary adapted stochastic integrals extend by \(L^2\) completion to a continuous martingale \(I\). At every \(t\in[0,T]\), \(I_t\) is the completed integral of \(\eta\) restricted to \((0,t)\), and any other continuous adapted version with these fixed-time representatives is indistinguishable from \(I\).

Foundation references · what Chewi leaves implicit

Provenance. Chewi is still the theorem/definition source. The references below are supplementary explanations for standard stochastic-analysis infrastructure; they neither alter the source statement nor replace ASTIS Lean proof obligations.

Details ASTIS makes explicit

Construct the integral first for elementary adapted processes and prove the exact finite-sum Itô isometry.
Use density and the isometry to extend the terminal stochastic integral by L2 completion; show independence of the approximating sequence.
A terminal L2 random variable is not yet a continuous stochastic process. Doob L2 control plus a summable subsequence/Borel--Cantelli argument supplies one adapted continuous version.
Fixed-time L2 identification and continuous-version uniqueness are what later permit a single common full-measure pathwise equality, avoiding an uncountable intersection of null sets.

Classical references and their role

Karatzas--Shreve, Brownian Motion and Stochastic Calculus — Primary rigorous source for elementary stochastic integrals, Itô isometry, L2 extension, martingale structure, and continuous versions.
Protter, Stochastic Integration and Differential Equations — Process-level stochastic-integration and stopping/localization framework used to design reusable interfaces beyond a single finite horizon.
Revuz--Yor, Continuous Martingales and Brownian Motion — Continuous-martingale reference for maximal inequalities, modifications, and indistinguishability-style reasoning.
Shreve, Stochastic Calculus for Finance II — Pedagogical companion for the elementary-integrand construction and why the Itô isometry is the correct completion norm.

Why is this valid?

The filtration usual conditions, progressive measurability, global product-space L2 integrability, Brownian motion relative to that filtration, almost-everywhere path continuity, fixed-time L2 representatives, and indistinguishability criterion are all explicit.

Source assumptions

a complete right-continuous filtered probability space
a Brownian motion relative to the filtration
a progressive globally square-integrable integrand

Formal assumptions

SatisfiesUsualConditions filtration mu
IsBrownianMotionWithFiltration B filtration mu
ProgressiveL2Integrand filtration mu T
positive finite construction horizon

View Lean formalization

compiled · faithful paraphrase

ASTIS constructs causal lagged-dyadic approximants, refines their grids, completes the terminal integral in L2, proves elementary martingale and Doob bounds, obtains a uniformly convergent continuous version by Borel-Cantelli, and identifies its value at every time through right-dyadic stopping.

`AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.ItoIntegralProcess.chewi_theorem_1_1_8`

compiled Samplinglib leaf · AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/ItoIntegralProcess.lean:1196

theorem chewi_theorem_1_1_8
    (eta : ProgressiveL2Integrand filtration mu T) (hT : 0 < T)
    (hB : IsBrownianMotionWithFiltration B filtration mu)
    (hUsual : SatisfiesUsualConditions filtration mu) :
    ∃ I : ℝ≥0 → Omega → ℝ,
      StronglyAdapted filtration I ∧
      Martingale I filtration mu ∧
      (∀ᵐ omega ∂mu, ContinuousOn (fun t => I t omega) (Icc (0 : ℝ≥0) T)) ∧
      (∀ t ≤ T, I t =ᵐ[mu]
        fun omega => itoIntegralTerminal (eta.restrictAt t) hT hB omega) ∧
      (∀ t ≤ T, ∫ omega, (I t omega) ^ 2 ∂mu =
        ∫ z, (processFunction (eta.restrictAt t).process z) ^ 2
          ∂(ElementaryItoIntegral.processTimeMeasure mu T)) ∧
      (∀ J : ℝ≥0 → Omega → ℝ,
        StronglyAdapted filtration J →
        (∀ᵐ omega ∂mu,
          ContinuousOn (fun t => J t omega) (Icc (0 : ℝ≥0) T)) →
        (∀ t ≤ T, J t =ᵐ[mu]
          fun omega => itoIntegralTerminal (eta.restrictAt t) hT hB omega) →
        ∀ᵐ omega ∂mu, ∀ t ∈ Icc (0 : ℝ≥0) T, J t omega = I t omega) := by
  exact ⟨itoIntegralProcess eta hT hB hUsual,
    itoIntegralProcess_stronglyAdapted eta hT hB hUsual,
    itoIntegralProcess_martingale eta hT hB hUsual,
    itoIntegralProcess_continuous_ae eta hT hB hUsual,
    fun _ ht => itoIntegralProcess_at_eq_terminal eta hT hB hUsual ht,
    fun _ ht => chewi_display_1_1_9 eta hT hB hUsual ht,
    fun J hJadapted hJcontinuous hJterminal =>
      itoIntegralProcess_unique eta hT hB hUsual J hJadapted hJcontinuous hJterminal⟩

end ItoIntegralProcess
end StochasticProcesses
end TechnicalLemmas
end AutoSamplingTheory

Imports

AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.ContinuousDoobL2
AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.DyadicElementaryStopping
AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.ItoTerminalCompletion
Mathlib.MeasureTheory.Constructions.Polish.StronglyMeasurable
Mathlib.MeasureTheory.Function.ConvergenceInMeasure
Mathlib.MeasureTheory.Function.LpSpace.Complete
Mathlib.MeasureTheory.OuterMeasure.BorelCantelli

Local dependencies

IsBrownianMotionWithFiltrationchewi_display_1_1_9itoIntegralProcess_martingaleProgressiveL2IntegrandSatisfiesUsualConditions

Downstream consumers

display (1.1.9)
localized Ito integration
Ito formula and SDE arguments

Displayed identity (1.1.9)

At every deterministic time, the second moment of the Ito integral equals the probability-time L2 energy accumulated by the integrand up to that time.

\[\mathbb E[I_t(\eta)^2]=\mathbb E\!\left[\int_0^t \eta_s^2\,ds\right]\]

For \(t\in[0,T]\), the second moment \(\mathbb E[I_t(\eta)^2]\) equals \(\mathbb E[\int_0^t\eta_s^2\,ds]\). ASTIS represents the right side by restricting \(\eta\) to \((0,t)\); changing an endpoint does not change the integral because singleton times are null.

Why is this valid?

The theorem exposes the deterministic-time bound t <= T, the exact strict restriction representative, the fixed probability-time product measure, and the almost-everywhere identification needed to replace the process by its L2 class.

Source assumptions

a complete right-continuous filtered probability space
a Brownian motion relative to the filtration
a progressive globally square-integrable integrand
a deterministic time in the construction horizon

Formal assumptions

SatisfiesUsualConditions filtration mu
IsBrownianMotionWithFiltration B filtration mu
ProgressiveL2Integrand filtration mu T
t <= T

View Lean formalization

compiled · faithful paraphrase

The fixed-time process is first identified almost everywhere with the L2 terminal completion of the restricted integrand. The terminal norm isometry and the product-space norm formula then give the displayed equality.

`AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.ItoIntegralProcess.chewi_display_1_1_9`

compiled Samplinglib leaf · AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/ItoIntegralProcess.lean:1183

theorem chewi_display_1_1_9
    (eta : ProgressiveL2Integrand filtration mu T) (hT : 0 < T)
    (hB : IsBrownianMotionWithFiltration B filtration mu)
    (hUsual : SatisfiesUsualConditions filtration mu)
    {t : ℝ≥0} (htT : t ≤ T) :
    ∫ omega, (itoIntegralProcess eta hT hB hUsual t omega) ^ 2 ∂mu =
      ∫ z, (processFunction (eta.restrictAt t).process z) ^ 2
        ∂(ElementaryItoIntegral.processTimeMeasure mu T) :=
  itoIntegralProcess_isometry_restrictAt eta hT hB hUsual htT

/-- Process-level existence theorem behind Chewi Theorem 1.1.8.  It packages
the constructed adapted continuous martingale, its terminal completion, and
the terminal Ito isometry; no stochastic-integral contract is assumed. -/

Imports

AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.ContinuousDoobL2
AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.DyadicElementaryStopping
AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.ItoTerminalCompletion
Mathlib.MeasureTheory.Constructions.Polish.StronglyMeasurable
Mathlib.MeasureTheory.Function.ConvergenceInMeasure
Mathlib.MeasureTheory.Function.LpSpace.Complete
Mathlib.MeasureTheory.OuterMeasure.BorelCantelli

Local dependencies

IsBrownianMotionWithFiltrationProgressiveL2IntegrandSatisfiesUsualConditions

Downstream consumers

localized stochastic integration
Ito formula energy estimates
SDE stability bounds

Displayed identity (1.1.5)

The expected square of an elementary stochastic integral expands to the sum of its diagonal increment terms because distinct adapted Brownian increments are orthogonal.

\[\mathbb E\!\left[\left(\sum_i H_i\Delta B_i\right)^2\right]=\sum_i \mathbb E[(H_i\Delta B_i)^2]\]

Write \(I_T(\eta)=\sum_i H_i\Delta B_i\). Expanding the square produces diagonal and cross terms; adaptedness and Brownian increment orthogonality make every cross term vanish in expectation.

Why is this valid?

The filtration, left-endpoint measurability, Brownian future-increment independence, centered increment law, and product integrability are explicit.

Source assumptions

an elementary adapted process
a Brownian motion relative to the filtration
a finite terminal time

Formal assumptions

ElementaryAdaptedProcess
IsBrownianMotionWithFiltration
MemLp two for weighted increments

View Lean formalization

compiled · faithful paraphrase

ASTIS proves the expectation identity after deriving L2 integrability and cross-term orthogonality from filtration-relative Brownian independence.

`AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.ElementaryItoIsometry.chewi_display_1_1_5`

compiled Samplinglib leaf · AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/ElementaryItoIsometry.lean:211

theorem chewi_display_1_1_5
    {Ω : Type*} {m : MeasurableSpace Ω}
    {B : ℝ≥0 → Ω → ℝ} {filtration : Filtration ℝ≥0 m} {μ : Measure Ω}
    {n : ℕ} (eta : ElementaryAdaptedProcess filtration n)
    (hB : IsBrownianMotionWithFiltration B filtration μ) (T : ℝ≥0) :
    ∫ omega, elementaryItoIntegral eta B T omega ^ 2 ∂μ =
      ∑ i, ∫ omega, weightedIncrement eta B T i omega ^ 2 ∂μ := by
  let _ : IsProbabilityMeasure μ := hB.isProbabilityMeasure
  let W : Fin n → Ω → ℝ := fun i => weightedIncrement eta B T i
  have hW : ∀ i, MemLp (W i) 2 μ := fun i => weightedIncrement_memLp_two eta hB T i
  have hpair : ∀ i j, Integrable (fun omega => W i omega * W j omega) μ := by
    intro i j
    change Integrable (W i * W j) μ
    exact (hW i).integrable_mul (hW j)
  calc
    ∫ omega, elementaryItoIntegral eta B T omega ^ 2 ∂μ =
        ∫ omega, ∑ i, ∑ j, W i omega * W j omega ∂μ := by
          apply integral_congr_ae
          filter_upwards [] with omega
          rw [elementaryItoIntegral_eq_sum_weightedIncrement]
          simp only [W, Finset.sum_mul_sum, pow_two]
    _ = ∑ i, ∑ j, ∫ omega, W i omega * W j omega ∂μ := by
      rw [integral_finsetSum]
      · apply Finset.sum_congr rfl
        intro i _
        rw [integral_finsetSum]
        intro j _
        exact hpair i j
      · intro i _
        exact integrable_finsetSum _ fun j _ => hpair i j
    _ = ∑ i, ∫ omega, W i omega ^ 2 ∂μ := by
      apply Finset.sum_congr rfl
      intro i _
      rw [Finset.sum_eq_single i]
      · simp [pow_two]
      · intro j _ hji
        exact integral_weightedIncrement_mul_eq_zero eta hB T hji.symm
      · simp
    _ = ∑ i, ∫ omega, weightedIncrement eta B T i omega ^ 2 ∂μ := rfl

/-- The probabilistic part of Chewi display (1.1.6): each diagonal term is
the coefficient's second moment times the clipped time-step length. -/

Imports

AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.BrownianMotion
AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.ElementaryItoIntegral
Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp

Local dependencies

IsBrownianMotionWithFiltrationintegral_weightedIncrement_mul_eq_zero

Downstream consumers

display (1.1.6)
Theorem 1.1.8
display (1.1.9)

Displayed identity (1.1.6)

The second moment of the elementary Ito integral equals the expected time integral of the squared elementary integrand.

\[\mathbb E\!\left[\left(\int_0^T \eta_s\,dB_s\right)^2\right]=\mathbb E\!\left[\int_0^T \eta_s^2\,ds\right]\]

The diagonal expansion is \(\sum_i\mathbb E[H_i^2]\,((t_{i+1}\wedge T)-(t_i\wedge T))\), exactly the probability-time \(L^2\) energy of \(\eta\) on \([0,T]\).

Why is this valid?

Coefficient integrability, clipped interval mass, time-cell disjointness, joint measurability, Tonelli, and the ENNReal energy representation are explicit.

Source assumptions

an elementary adapted process
a Brownian motion relative to the filtration
a finite terminal time

Formal assumptions

IsBrownianMotionWithFiltration
TimeMeasure.upTo
processTimeMeasure
processL2Energy

View Lean formalization

compiled · faithful paraphrase

ASTIS connects Brownian increment second moments to an exact evaluation of processL2Energy under the stopped nonnegative-time Lebesgue measure.

`AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.ElementaryItoIsometry.chewi_display_1_1_6`

compiled Samplinglib leaf · AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/ElementaryItoIsometry.lean:426

theorem chewi_display_1_1_6
    {Ω : Type*} {m : MeasurableSpace Ω}
    {B : ℝ≥0 → Ω → ℝ} {filtration : Filtration ℝ≥0 m} {μ : Measure Ω}
    {n : ℕ} (eta : ElementaryAdaptedProcess filtration n)
    (hB : IsBrownianMotionWithFiltration B filtration μ) (T : ℝ≥0) :
    ENNReal.ofReal (∫ omega, elementaryItoIntegral eta B T omega ^ 2 ∂μ) =
      processL2Energy eta.value μ T := by
  let _ : IsProbabilityMeasure μ := hB.isProbabilityMeasure
  rw [elementaryItoIntegral_sq_eq_sum eta hB T]
  rw [processL2Energy_value eta μ T]

end ElementaryItoIsometry
end StochasticProcesses
end TechnicalLemmas
end AutoSamplingTheory

Imports

AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.BrownianMotion
AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.ElementaryItoIntegral
Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp

Local dependencies

IsBrownianMotionWithFiltrationprocessL2Energy_value

Downstream consumers

Theorem 1.1.8
display (1.1.9)
general Ito integral by L2 completion

Displayed identity (1.1.10)

Localization permits progressive integrands whose squared time integral is finite almost surely, without requiring its expectation to be finite.

\[\int_0^T \eta_s(\omega)^2\,ds<\infty\quad\text{for a.e. }\omega\]

For almost every sample path \(\omega\), the quadratic energy \(\int_0^T\eta_s(\omega)^2\,ds\) is finite. This is weaker than assuming finite expected energy.

Why is this valid?

The finite time measure, nonnegative path energy, strict comparison with infinity, and probability almost-everywhere quantifier are explicit.

Source assumptions

a real stochastic integrand
a finite terminal time
a probability measure

Formal assumptions

TimeMeasure.upTo T
ENNReal lintegral
Filter.Eventually under mu

View Lean formalization

compiled · faithful paraphrase

The condition is ENNReal-valued and pathwise almost everywhere, so it is visibly weaker than finite expected process energy.

`AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.ElementaryItoIntegral.chewi_display_1_1_10`

compiled Samplinglib leaf · AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/ElementaryItoIntegral.lean:115

theorem chewi_display_1_1_10
    {Omega : Type*} [MeasurableSpace Omega]
    (eta : ℝ≥0 → Omega → ℝ) (mu : Measure Omega) (T : ℝ≥0) :
    IsLocallySquareIntegrableOn eta mu T ↔
      ∀ᵐ omega ∂mu,
        (∫⁻ t, ENNReal.ofReal ((eta t omega) ^ 2) ∂(TimeMeasure.upTo T)) < ∞ :=
  Iff.rfl

end ElementaryItoIntegral
end StochasticProcesses
end TechnicalLemmas
end AutoSamplingTheory

Imports

Mathlib.MeasureTheory.Measure.Prod
Mathlib.Probability.Process.Adapted
AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.TimeMeasure

Local dependencies

No Registry dependency inferred.

Downstream consumers

Proposition 1.1.13
display (1.1.14)
Proposition 1.1.16

Displayed identity (1.1.7)

The squared L2 norm of an integrand on the product probability-time space is the expectation of its squared time integral, and admissible integrands have finite value.

\[\|\eta\|_{L^2(\mathbb P\otimes dt)}^2=\mathbb E\!\left[\int_0^T |\eta_t|^2\,dt\right]<\infty\]

Tonelli identifies the product integral of eta squared under P tensor m restricted to [0,T] with the iterated expectation and time integral.

Why is this valid?

The finite nonnegative-time measure, product measure, joint a.e. measurability, nonnegative integral, and separate finiteness condition are explicit.

Source assumptions

a probability measure
a finite terminal time
a jointly measurable squared process

Formal assumptions

TimeMeasure.upTo T
AEMeasurable squared process on processTimeMeasure
ENNReal lintegrals

View Lean formalization

compiled · faithful paraphrase

ASTIS uses ENNReal for the energy so the finiteness condition is visible and proves the product-to-iterated identity with Mathlib Tonelli.

`AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.ElementaryItoIntegral.chewi_display_1_1_7`

compiled Samplinglib leaf · AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/ElementaryItoIntegral.lean:94

theorem chewi_display_1_1_7
    {Omega : Type*} [MeasurableSpace Omega]
    (eta : ℝ≥0 → Omega → ℝ) (mu : Measure Omega) (T : ℝ≥0)
    (hη : AEMeasurable
      (fun z : Omega × ℝ≥0 => ENNReal.ofReal ((eta z.2 z.1) ^ 2))
      (processTimeMeasure mu T)) :
    processL2Energy eta mu T =
      ∫⁻ omega, ∫⁻ t, ENNReal.ofReal ((eta t omega) ^ 2)
        ∂(TimeMeasure.upTo T) ∂mu :=
  lintegral_prod _ hη

/-- Almost-sure local square integrability on `[0,T]`, the weaker condition
used when Chewi extends stochastic integration by localization. -/

Imports

Mathlib.MeasureTheory.Measure.Prod
Mathlib.Probability.Process.Adapted
AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.TimeMeasure

Local dependencies

No Registry dependency inferred.

Downstream consumers

Theorem 1.1.8
display (1.1.9)
Definition 1.1.12

Displayed identity (1.1.2)

An elementary adapted process is a finite sum of bounded left-endpoint measurable coefficients on half-open time intervals.

\[\eta_t=\sum_{k=0}^{m-1}H_k\,\mathbf 1_{(t_k,t_{k+1}]}(t),\qquad H_k\in L^\infty(\mathcal F_{t_k})\]

For a strict grid t_0 < ... < t_n, eta_t is the sum of H_i times the indicator of t in (t_i,t_{i+1}].

Why is this valid?

Finite indexing, strict endpoint order, left-endpoint strong measurability, boundedness, and the half-open interval convention are explicit.

Source assumptions

a filtered measurable sample space
a finite strict time grid
bounded left-endpoint measurable coefficients

Formal assumptions

Mathlib Filtration at NNReal time
StrictMono grid on Fin (n + 1)
StronglyMeasurable coefficients
pointwise coefficient bounds

View Lean formalization

compiled · faithful paraphrase

The Lean structure keeps the strict grid, filtration measurability, and coefficient bounds as data rather than erasing the source regularity.

`AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.ElementaryItoIntegral.chewi_display_1_1_2`

compiled Samplinglib leaf · AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/ElementaryItoIntegral.lean:45

theorem chewi_display_1_1_2
    {Omega : Type*} {m : MeasurableSpace Omega}
    {filtration : Filtration ℝ≥0 m} {n : ℕ}
    (eta : ElementaryAdaptedProcess filtration n) (t : ℝ≥0) (omega : Omega) :
    eta.value t omega =
      ∑ i, if eta.times i.castSucc < t ∧ t ≤ eta.times i.succ
        then eta.coeff i omega else 0 :=
  rfl

/-- The finite Brownian-increment sum used to define the Ito integral of an
elementary process at terminal time `T`. -/

Imports

Mathlib.MeasureTheory.Measure.Prod
Mathlib.Probability.Process.Adapted
AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.TimeMeasure

Local dependencies

No Registry dependency inferred.

Downstream consumers

display (1.1.3)
elementary Ito isometry

Displayed identity (1.1.3)

The Ito integral of an elementary process is defined by the finite sum of its adapted coefficients times Brownian increments stopped at the terminal time.

\[\int_0^T\eta_t\,dB_t:=\sum_{k=0}^{m-1}H_k\bigl(B_{t_{k+1}\wedge T}-B_{t_k\wedge T}\bigr)\]

I_[0,T](eta) is the sum of H_i times B_(t_(i+1) min T) minus B_(t_i min T).

Why is this valid?

The elementary-process contract supplies adapted bounded coefficients, and every Brownian increment is stopped by the same terminal time.

Source assumptions

an elementary adapted process
a scalar Brownian path
a nonnegative terminal time

Formal assumptions

the display (1.1.2) elementary-process structure
finite Fin-indexed summation
NNReal stopping by minimum

View Lean formalization

compiled · faithful paraphrase

This declaration is only the finite elementary integral; it does not claim the isometry, completion, or general stochastic integral.

`AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.ElementaryItoIntegral.chewi_display_1_1_3`

compiled Samplinglib leaf · AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/ElementaryItoIntegral.lean:67

theorem chewi_display_1_1_3
    {Omega : Type*} {m : MeasurableSpace Omega}
    {filtration : Filtration ℝ≥0 m} {n : ℕ}
    (eta : ElementaryAdaptedProcess filtration n)
    (B : ℝ≥0 → Omega → ℝ) (T : ℝ≥0) (omega : Omega) :
    elementaryItoIntegral eta B T omega =
      ∑ i, eta.coeff i omega *
        (B (min (eta.times i.succ) T) omega -
          B (min (eta.times i.castSucc) T) omega) :=
  rfl

/-- Product measure `P tensor m|[0,T]` used for the square-integrability
condition in Chewi display (1.1.7). -/

Imports

Mathlib.MeasureTheory.Measure.Prod
Mathlib.Probability.Process.Adapted
AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.TimeMeasure

Local dependencies

No Registry dependency inferred.

Downstream consumers

display (1.1.5)
display (1.1.6)
Theorem 1.1.8

Definition 1.1.1

Standard Brownian motion starts at zero, has independent centered Gaussian increments with covariance proportional to elapsed time, and has almost surely continuous paths.

\[B_0=0,\qquad B_t-B_s\sim\mathcal N(0,(t-s)I),\qquad 0\le s<t,\qquad t\mapsto B_t\text{ continuous a.s.}\]

For every s<t, B_t-B_s is centered Gaussian with covariance (t-s)I; increments over disjoint intervals are jointly independent.

Foundation references · what Chewi leaves implicit

Details ASTIS makes explicit

Separate the finite-dimensional distributions from almost-sure path continuity instead of treating ‘Brownian motion’ as one opaque primitive.
State the covariance/isotropy content of an N-dimensional standard Brownian increment through scalar projections or coordinates.
When a filtration is later fixed, add adaptation and future-increment independence from the past filtration; bare independent increments do not justify stochastic integration against an arbitrary enlarged filtration.

Classical references and their role

Karatzas--Shreve, Brownian Motion and Stochastic Calculus — Primary rigorous Brownian-motion and filtered-probability-space reference; used to separate law, path regularity, filtration, and stopping-time hypotheses.
Revuz--Yor, Continuous Martingales and Brownian Motion — Secondary reference for continuous-path Brownian and continuous-martingale viewpoints, especially later version and stopping arguments.
Shreve, Stochastic Calculus for Finance II — Pedagogical companion for first intuition about Brownian paths, increments, Gaussian scaling, and filtrations.

Why is this valid?

Zero start, finite-family independent increments, all projected Gaussian laws, and a.e. path continuity are separate conjuncts.

Source assumptions

a probability space
a finite-dimensional Euclidean state space

Formal assumptions

Borel measurable real Hilbert state space
HasLaw for every StrongDual projection
iIndepFun on disjoint intervals
a.e. Continuous paths

View Lean formalization

compiled · faithful paraphrase

ASTIS expresses the vector Gaussian law by every continuous-linear projection, matching Mathlib's coordinate-free Gaussian API.

`AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.BrownianMotion.IsStandardBrownianMotion`

compiled Samplinglib leaf · AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/BrownianMotion.lean:43

def IsStandardBrownianMotion
    (B : ℝ≥0 → Omega → E) (mu : Measure Omega) : Prop :=
  (∀ omega, B 0 omega = 0) ∧
    (∀ (n : ℕ) (s t : Fin n → ℝ≥0),
      (∀ i, s i ≤ t i) →
      Pairwise (fun i j => Disjoint (Ioc (s i) (t i)) (Ioc (s j) (t j))) →
      iIndepFun (fun i omega => B (t i) omega - B (s i) omega) mu) ∧
    (∀ s t : ℝ≥0, s < t → ∀ ell : StrongDual ℝ E,
      HasLaw
        (fun omega => ell (B t omega - B s omega))
        (gaussianReal 0 (projectedIncrementVariance s t ell)) mu) ∧
    ∀ᵐ omega ∂mu, Continuous (fun t => B t omega)

/-! ## Brownian motion relative to a filtration -/

/-- A real Brownian motion relative to a specified filtration.

The last field is the condition needed for stochastic integration: the
increment after `s` is independent of the whole past sigma-algebra `F_s`.
Bare independent increments do not imply this for an arbitrary enlarged
filtration. -/

Imports

Mathlib.Probability.Distributions.Gaussian.Basic
Mathlib.Probability.BrownianMotion.Basic
Mathlib.Probability.ConditionalExpectation
Mathlib.Probability.Independence.Basic
Mathlib.Probability.Independence.Integration
Mathlib.Probability.Process.Adapted
Mathlib.MeasureTheory.Function.L2Space

Local dependencies

No Registry dependency inferred.

Downstream consumers

Ito integration
Ito processes
Langevin SDE

Definition 1.1.12

A localizing sequence is an increasing stopping-time sequence whose stopped integrands have finite L2 norm and which converges almost surely to the terminal time.

\[\tau_n\le\tau_{n+1},\qquad \tau_n\uparrow T\ \text{a.s.},\qquad \mathbb E\!\int_0^T|\eta_s|^2\mathbf 1_{\{s\le\tau_n\}}\,ds<\infty\]

Each stop makes the progressive integrand square-integrable on the finite time interval; monotone stops then exhaust that interval almost surely.

Foundation references · what Chewi leaves implicit

Details ASTIS makes explicit

A localizing sequence is not merely a sequence of random cutoffs: every cutoff must be a stopping time, the cutoffs must diverge almost surely, and the stopped object must satisfy the global integrability property needed downstream.
Chewi's energy localizers require a separate hitting-time proof, a stopped-energy bound, and convergence of the thresholds to infinity.
Endpoint conventions at a hitting time are harmless only after the singleton-time null-set lemma is made explicit.

Classical references and their role

Protter, Stochastic Integration and Differential Equations — Primary supplementary source for localization and stopped stochastic integrals as reusable process-level machinery.
Karatzas--Shreve, Brownian Motion and Stochastic Calculus — Rigorous stopping-time, local square-integrability, and stochastic-integral background.
Revuz--Yor, Continuous Martingales and Brownian Motion — Continuous local-martingale localization viewpoint and pathwise stopping arguments.

Why is this valid?

Progressive measurability, stopping-time measurability, monotonicity, finite expected time integral, and the almost-sure limit are separate conjuncts.

Source assumptions

a progressive process on a filtered probability space
a finite terminal time

Formal assumptions

Mathlib ProgMeasurable
Mathlib IsStoppingTime
nonnegative-time Lebesgue measure
a.e. filter limit

View Lean formalization

compiled · faithful paraphrase

ASTIS records the iterated nonnegative integral before finiteness, so no totalized real integral hides the L2 side condition.

`AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.Localization.IsLocalizingSequence`

compiled Samplinglib leaf · AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/Localization.lean:47

def IsLocalizingSequence
    {Omega : Type*} {m : MeasurableSpace Omega}
    (eta : ℝ≥0 → Omega → ℝ) (filtration : Filtration ℝ≥0 m)
    (mu : Measure Omega) (T : ℝ≥0)
    (tau : ℕ → Omega → WithTop ℝ≥0) : Prop :=
  IsStronglyProgressive filtration eta ∧
    (∀ n, IsStoppingTime filtration (tau n)) ∧
    Monotone tau ∧
    (∀ n,
      (∫⁻ omega, ∫⁻ t in Icc (0 : ℝ≥0) T,
        ENNReal.ofReal ((stoppedIntegrand eta (tau n) t omega) ^ 2) ∂nnrealLebesgue ∂mu) < ∞) ∧
    ∀ᵐ omega ∂mu, Tendsto (fun n => tau n omega) atTop (𝓝 (T : WithTop ℝ≥0))

/-- Chewi Definition 1.1.15: an adapted process is a local martingale when a
monotone sequence of stopping times tends to infinity almost surely and every
stopped, initially centered process is a martingale.

The limit is the *topological* neighborhood of `⊤` in `WithTop ℝ≥0`.  Using
the order filter `atTop` as the codomain would be too strong here because
`WithTop ℝ≥0` has a greatest element: that filter would force the stopping
times to be eventually equal to `⊤`, rather than allowing finite stopping
times to diverge to infinity as in Chewi's definition. -/

Imports

Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Mathlib.MeasureTheory.Measure.Comap
Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Mathlib.Probability.Martingale.Basic
Mathlib.Probability.Process.Stopping
AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.TimeMeasure

Local dependencies

No Registry dependency inferred.

Downstream consumers

localized Ito integral
local martingales

Definition 1.1.15

A local martingale is adapted and admits increasing stopping times tending almost surely to infinity for which every centered stopped process is a martingale.

\[M\in\mathcal M_{\mathrm{loc}}\iff\exists\,\tau_n\uparrow\infty\ \text{a.s. such that }M^{\tau_n}\in\mathcal M\ \text{for every }n\]

Localization replaces global integrability by ordinary martingale behavior before each stop.

Foundation references · what Chewi leaves implicit

Details ASTIS makes explicit

The local martingale is one global adapted process together with a localizing sequence; the localized martingales must therefore be coherent versions of the same process.
Deterministic-time almost-everywhere equality is too weak to glue stopped continuous martingales directly. A common full-measure event carrying all-time overlap is the safe process-level interface.
When a global process is glued from a countable localization ladder, continuity and adaptedness must be proved for the chosen glued version, including the null exceptional set.

Classical references and their role

Protter, Stochastic Integration and Differential Equations — Primary supplementary source for local martingales, stopping, localization, and stochastic-integration consistency.
Revuz--Yor, Continuous Martingales and Brownian Motion — Continuous local-martingale, modification, and pathwise-version reference.
Karatzas--Shreve, Brownian Motion and Stochastic Calculus — Rigorous filtered-space local-martingale background connecting the localization definition to Itô integrals and SDEs.

Why is this valid?

Adaptedness, stopping-time measurability, monotonicity, a.s. divergence, initial centering, and the martingale property are all required.

Source assumptions

a filtered probability space
a real adapted process

Formal assumptions

Mathlib Adapted
Mathlib stoppedProcess
Mathlib Martingale
a.e. atTop convergence

View Lean formalization

compiled · faithful paraphrase

ASTIS reuses Mathlib's stoppedProcess and Martingale predicates and leaves every quantifier visible.

`AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.Localization.IsLocalMartingale`

compiled Samplinglib leaf · AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/Localization.lean:69

def IsLocalMartingale
    {Omega : Type*} {m : MeasurableSpace Omega}
    (process : ℝ≥0 → Omega → ℝ) (filtration : Filtration ℝ≥0 m)
    (mu : Measure Omega) : Prop :=
  Adapted filtration process ∧
    ∃ tau : ℕ → Omega → WithTop ℝ≥0,
      (∀ n, IsStoppingTime filtration (tau n)) ∧
      Monotone tau ∧
      (∀ᵐ omega ∂mu, Tendsto (fun n => tau n omega) atTop (𝓝 (⊤ : WithTop ℝ≥0))) ∧
      ∀ n, Martingale
        (fun t omega => stoppedProcess process (tau n) t omega - process 0 omega)
        filtration mu

end

end Localization
end StochasticProcesses
end TechnicalLemmas
end AutoSamplingTheory

Imports

Mathlib.MeasureTheory.Integral.Lebesgue.Basic
Mathlib.MeasureTheory.Measure.Comap
Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Mathlib.Probability.Martingale.Basic
Mathlib.Probability.Process.Stopping
AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.TimeMeasure

Local dependencies

No Registry dependency inferred.

Downstream consumers

localized Ito integral theorem
Ito processes

Definition 1.1.4

A martingale is an adapted integrable process whose conditional expectation at an earlier time equals its earlier value.

\[0\le s\le t\quad\Longrightarrow\quad \mathbb E[M_t\mid\mathcal F_s]=M_s\]

For s <= t, \\(\mathbb E[M_t\mid\mathcal F_s]=M_s\\) almost everywhere, and M_t is measurable with respect to F_t. Mathlib's predicate derives integrability from the fixed-point conditional-expectation law.

Foundation references · what Chewi leaves implicit

Details ASTIS makes explicit

Adaptedness, integrability, and the conditional-expectation identity are separate obligations.
Conditional expectations are equivalence classes, so the martingale identity is an almost-everywhere statement at each pair of deterministic times.
Later pathwise statements require a continuous/right-continuous version argument rather than silently choosing representatives at every time.

Classical references and their role

Karatzas--Shreve, Brownian Motion and Stochastic Calculus — Primary rigorous martingale, filtration, conditional expectation, stopping, and regularization background.
Revuz--Yor, Continuous Martingales and Brownian Motion — Continuous-martingale and version/indistinguishability perspective used later when fixed-time identities must become process identities.
Shreve, Stochastic Calculus for Finance II — Reader-facing explanation of the information-flow meaning of a martingale.

Why is this valid?

The sample space has a measure and filtration, the process is strongly adapted, and the conditional-expectation equality is an almost-everywhere equality for every ordered pair of times.

Source assumptions

a filtered probability space
an adapted integrable real process

Formal assumptions

a Measure and Filtration indexed by NNReal
Mathlib StronglyAdapted process measurability
conditional expectation equality almost everywhere for s <= t

View Lean formalization

compiled · faithful paraphrase

ASTIS uses Mathlib's real-valued Martingale predicate at NNReal time so conditional expectation, stopped-process, and filtration lemmas remain available.

`AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.Martingale.IsChewiMartingale`

compiled Samplinglib leaf · AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/Martingale.lean:21

def IsChewiMartingale
    {Ω : Type*} {m : MeasurableSpace Ω}
    (process : ℝ≥0 → Ω → ℝ) (filtration : Filtration ℝ≥0 m)
    (μ : Measure Ω) : Prop :=
  MeasureTheory.Martingale process filtration μ

/-- A constant real process is a martingale under a finite measure. -/

Imports

Mathlib.Probability.Martingale.Basic

Local dependencies

No Registry dependency inferred.

Downstream consumers

Ito integral construction
local martingales
martingale increment orthogonality

Definition 1.1.11

A stopping time is a random time whose occurrence by time t is measurable using the information available at time t.

\[\tau\text{ is a stopping time}\iff\{\tau\le t\}\in\mathcal F_t\quad\text{for every }t\ge0\]

For every nonnegative t, the event {omega | tau(omega) <= t} belongs to the filtration sigma-algebra F_t. Allowing tau = infinity represents paths that never stop.

Foundation references · what Chewi leaves implicit

Details ASTIS makes explicit

The stopping-time condition is measurability of every event {tau <= t} in the information available at time t.
Extended-valued stopping times and bounded finite-horizon stopping times should be distinguished explicitly.
Hitting times become stopping times only after the adaptedness/path-regularity hypotheses needed to make their level events measurable are proved.

Classical references and their role

Karatzas--Shreve, Brownian Motion and Stochastic Calculus — Primary rigorous stopping-time and filtered-space reference.
Revuz--Yor, Continuous Martingales and Brownian Motion — Continuous-process hitting-time and stopping technology used for canonical energy localizers.
Shreve, Stochastic Calculus for Finance II — Low-barrier intuition for why a stopping rule may only use present/past information.

Why is this valid?

The sample space carries an ambient measurable structure, the filtration is monotone and subordinate to it, and tau takes values in extended nonnegative time.

Source assumptions

a filtered measurable sample space
a nonnegative random time

Formal assumptions

a Mathlib Filtration indexed by NNReal
tau maps into WithTop NNReal
each event tau <= t is measurable in the filtration at t

View Lean formalization

compiled · faithful paraphrase

ASTIS uses Mathlib's native Filtration and IsStoppingTime predicate with nonnegative continuous time, preserving all later stopped-process APIs.

`AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.StoppingTime.IsChewiStoppingTime`

compiled Samplinglib leaf · AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/StoppingTime.lean:27

def IsChewiStoppingTime
    {Ω : Type*} {m : MeasurableSpace Ω}
    (filtration : Filtration ℝ≥0 m) (τ : Ω → WithTop ℝ≥0) : Prop :=
  MeasureTheory.IsStoppingTime filtration τ

/-- Constant nonnegative times satisfy the source stopping-time definition. -/

Imports

Mathlib.Probability.Process.Stopping

Local dependencies

No Registry dependency inferred.

Downstream consumers

localizing sequences
stopped stochastic integrals
local martingales

Proposition 1.1.13

The pathwise local-square-integrability condition admits an increasing canonical sequence of stopping times approaching the horizon such that each stopped integrand has finite global L2 energy.

\[\tau_n:=\inf\{t\le T:A_t=n+1\}\ \text{(fallback }T\text{)},\qquad \tau_n\uparrow T\]

Complete the null exceptional set, form the continuous accumulated-energy path, stop at equality level n+1, use continuity to rule out overshoot, characterize the threshold event to prove the stopping-time property, and use finite terminal energy to show the localizers exhaust the horizon.

Why is this valid?

Usual filtration conditions, completion of null sets, progressive measurability, pathwise energy continuity, stopping-time measurability, no overshoot, and the probability-space product-L2 consequence are explicit.

Source assumptions

a complete right-continuous filtered probability space
a progressive integrand whose squared time integral is finite almost surely on the finite horizon

Formal assumptions

SatisfiesUsualConditions filtration mu
IsProbabilityMeasure mu
LocalProgressiveL2Integrand filtration mu T

View Lean formalization

compiled · faithful paraphrase

ASTIS compiles exceptional-set completion, equality-level first hitting, the intermediate-value step, stopping-time measurability, exact stopped-energy control, monotonicity, and terminal exhaustion rather than treating localization as a black box.

`AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.CanonicalLocalizationTheorem.chewi_proposition_1_1_13`

compiled Samplinglib leaf · AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/CanonicalLocalizationTheorem.lean:48

theorem chewi_proposition_1_1_13
    [IsProbabilityMeasure mu]
    (hUsual : SatisfiesUsualConditions filtration mu)
    (eta : LocalProgressiveL2Integrand filtration mu T) :
    (∀ n, IsChewiStoppingTime filtration
      (fun omega =>
        (canonicalLocalizingTime hUsual eta n omega : WithTop ℝ≥0))) ∧
    (∀ omega, Monotone
      (fun n => canonicalLocalizingTime hUsual eta n omega)) ∧
    (∀ omega, Tendsto
      (fun n => canonicalLocalizingTime hUsual eta n omega)
      atTop (𝓝 T)) ∧
    (∀ n omega,
      ∫ s,
        ((canonicalStoppedProgressiveL2 hUsual eta n).process s omega) ^ 2
          ∂(TimeMeasure.upTo T) ≤ (n + 1 : ℝ)) := by
  refine ⟨?_, ?_, ?_, ?_⟩
  · exact fun n => canonicalLocalizingTime_isChewiStoppingTime hUsual eta n
  · exact fun omega => canonicalLocalizingTime_mono hUsual eta omega
  · exact fun omega => tendsto_canonicalLocalizingTime hUsual eta omega
  · intro n omega
    change ∫ s,
        (energyStoppedIntegrand hUsual eta (n + 1 : ℝ) s omega) ^ 2
          ∂(TimeMeasure.upTo T) ≤ (n + 1 : ℝ)
    exact integral_energyStoppedIntegrand_sq_le hUsual eta (by positivity) omega

end CanonicalLocalizationTheorem
end StochasticProcesses
end TechnicalLemmas
end AutoSamplingTheory

Imports

AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.CanonicalEnergyStoppingTime
AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.EnergyStoppedProgressiveL2

Local dependencies

tendsto_canonicalLocalizingTimecanonicalLocalizingTime_isChewiStoppingTimeintegral_energyStoppedIntegrand_sq_leSatisfiesUsualConditionsIsChewiStoppingTime

Downstream consumers

display (1.1.14)
Proposition 1.1.16

Displayed identity (1.1.14)

Each canonical energy truncation is globally square-integrable, so its Ito integral is an adapted continuous martingale with the deterministic-time restriction representation used in the localization proof.

\[\eta^{(n)}_s:=\eta_s\mathbf 1_{\{s\le\tau_n\}},\qquad \mathbb E\!\int_0^T|\eta^{(n)}_s|^2\,ds<\infty,\qquad M^{(n)}_t:=\int_0^t\eta^{(n)}_s\,dB_s\]

Proposition 1.1.13 turns the locally square-integrable integrand into a globally L2 stopped integrand. Applying the existing global Ito map gives a continuous martingale, and each deterministic-time value agrees almost surely with the terminal completed Ito integral of the stopped integrand restricted up to that time.

Why is this valid?

The stopped-integrand L2 bound, Brownian/filtration contract, positive horizon, continuous process representative, and distinction between deterministic restriction and random stopping are explicit.

Source assumptions

the canonical localizing sequence of Proposition 1.1.13
a Brownian motion relative to the filtration
a positive finite horizon

Formal assumptions

SatisfiesUsualConditions filtration mu
IsProbabilityMeasure mu
LocalProgressiveL2Integrand filtration mu T
0 < T
IsBrownianMotionWithFiltration B filtration mu

View Lean formalization

compiled · faithful paraphrase

ASTIS reuses the global Ito map from Theorem 1.1.8 and proves adaptedness, martingality, continuity, and deterministic-time restriction compatibility in one source-facing display theorem. Random-time stopping is deliberately discharged later in Proposition 1.1.16.

`AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.CanonicalStoppedItoIntegral.chewi_display_1_1_14`

compiled Samplinglib leaf · AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/CanonicalStoppedItoIntegral.lean:98

theorem chewi_display_1_1_14
    (hUsual : SatisfiesUsualConditions filtration mu)
    (eta : LocalProgressiveL2Integrand filtration mu T)
    (hT : 0 < T)
    (hB : IsBrownianMotionWithFiltration B filtration mu)
    (n : ℕ) :
    StronglyAdapted filtration
        (canonicalStoppedItoProcess hUsual eta hT hB n) ∧
      Martingale (canonicalStoppedItoProcess hUsual eta hT hB n)
        filtration mu ∧
      (∀ omega,
        ContinuousOn
          (fun t => canonicalStoppedItoProcess hUsual eta hT hB n t omega)
          (Icc (0 : ℝ≥0) T)) ∧
      (canonicalStoppedProgressiveL2 hUsual eta n).process =
        energyStoppedIntegrand hUsual eta (n + 1 : ℝ) ∧
      ∀ t : ℝ≥0, t ≤ T →
        canonicalStoppedItoProcess hUsual eta hT hB n t =ᵐ[mu]
          (fun omega =>
            ItoTerminalCompletion.itoIntegralTerminal
              ((canonicalStoppedProgressiveL2 hUsual eta n).restrictAt t)
              hT hB omega) := by
  refine ⟨canonicalStoppedItoProcess_stronglyAdapted hUsual eta hT hB n,
    canonicalStoppedItoProcess_martingale hUsual eta hT hB n,
    canonicalStoppedItoProcess_continuousOn hUsual eta hT hB n,
    canonicalStoppedProgressiveL2_process hUsual eta n, ?_⟩
  intro t htT
  exact canonicalStoppedItoProcess_at_eq_terminal hUsual eta hT hB n htT

end CanonicalStoppedItoIntegral
end StochasticProcesses
end TechnicalLemmas
end AutoSamplingTheory

Imports

AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.CanonicalLocalizationTheorem
AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.ItoIntegralProcess

Local dependencies

IsBrownianMotionWithFiltrationSatisfiesUsualConditions

Downstream consumers

Proposition 1.1.16

Proposition 1.1.16

The Ito integral of a progressive locally square-integrable integrand has a continuous version that is a local martingale.

\[M_t=\int_0^t \eta_s\,dB_s,\qquad M_{t\wedge\tau_n}=\int_0^t \eta_s\mathbf 1_{\{s\le\tau_n\}}\,dB_s\]

Use canonical energy localizers to obtain globally L2 stopped integrands. Prove stochastic integration commutes with those random stops first on grid-valued stopping times, pass by dyadic approximation in L2 and along continuous paths, prove cross-horizon consistency, glue the finite-horizon processes pathwise, and use localizers tending to infinity almost surely.

Why is this valid?

Strict-versus-closed stopping differs only on a product-measure-zero stopping graph; finite-horizon Ito versions are proved compatible before gluing; and the localizers are proved monotone and tending to infinity almost surely.

Source assumptions

a complete right-continuous filtered probability space
a Brownian motion relative to the filtration
a progressive integrand with almost-sure locally finite squared energy

Formal assumptions

SatisfiesUsualConditions filtration mu
IsProbabilityMeasure mu
GlobalLocalProgressiveL2Integrand filtration mu
IsBrownianMotionWithFiltration B filtration mu

View Lean formalization

compiled · faithful paraphrase

ASTIS compiles the coefficient-level stopping identity, the entire elementary-Ito finite-sum identity, right-dyadic random-time convergence, stopped-integrand L2 contraction, stopping-graph nullity, horizon overlap, localized martingale coherence, and final pathwise gluing into the source-facing proposition.

`AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.ChewiProposition1_1_16.chewi_proposition_1_1_16`

compiled Samplinglib leaf · AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/ChewiProposition1_1_16.lean:51

theorem chewi_proposition_1_1_16
    [IsProbabilityMeasure mu]
    (hUsual : SatisfiesUsualConditions filtration mu)
    (eta : GlobalLocalProgressiveL2Integrand filtration mu)
    (hB : IsBrownianMotionWithFiltration B filtration mu) :
    StronglyAdapted filtration (globalItoProcess hUsual eta hB) ∧
      (∀ omega, Continuous (fun t => globalItoProcess hUsual eta hB t omega)) ∧
      Localization.IsLocalMartingale
        (globalItoProcess hUsual eta hB) filtration mu := by
  exact ⟨globalItoProcess_stronglyAdapted hUsual eta hB,
    globalItoProcess_continuous hUsual eta hB,
    globalItoProcess_isLocalMartingale hUsual eta hB⟩

/-- **Localized Itô representation for Proposition 1.1.16.**

For every canonical dyadic localizer `tau_k`, stopping the globally glued local
Itô process at `tau_k` recovers, almost surely and at every deterministic time
inside the matching horizon, the completed Itô process of the literal source
integrand `eta_s * 1_{s ≤ tau_k}`.  This is the formal certificate that the
process in `chewi_proposition_1_1_16` is Chewi's local stochastic integral, not
an unrelated local martingale with the same localization sequence. -/

Imports

AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.GlobalItoProcessGluing

Local dependencies

IsBrownianMotionWithFiltrationIsLocalMartingaleSatisfiesUsualConditions

Downstream consumers

Definition 1.1.17 (Ito process)
Ito formula and SDE localization

Chewi results with compiled ASTIS proofs

Source statements and formal expansions

Proposition 1.1.13

Canonical localization by accumulated energy

Chewi statement

\[A_t(\omega):=\int_0^t \eta_s(\omega)^2\,ds,\qquad \tau_n:=\inf\{t\in[0,T]:A_t\ge n+1\}\wedge T,\]

\[\tau_n\le \tau_{n+1},\qquad \tau_n\uparrow T\ \text{a.s.},\qquad \mathbb E\!\left[\int_0^T \eta_s^2\mathbf 1_{\{s\le\tau_n\}}\,ds\right]\le n+1.\]

Let eta be a progressive integrand on a finite horizon [0,T] whose pathwise quadratic energy is finite almost surely. Stop the path when accumulated energy reaches level n+1, using T if that level is never reached. These stopping times form a localizing sequence, and every corresponding stopped integrand is globally square-integrable.

Assumptions

a complete right-continuous filtered probability space
a progressive real integrand eta on [0,T]
pathwise finite quadratic energy on [0,T], almost surely

Chewi proof status

Chewi explicitly says that this proposition barely needs a proof and omits it. The expansion below is the ASTIS formal proof, not a reconstruction attributed to the book.

ASTIS formal expansion

Accumulated energy

\[A_t=\int_0^t\eta_s^2\,ds,\qquad 0\le s\le t\le T\Longrightarrow A_s\le A_t.\]

The energy process is adapted, continuous, and nondecreasing.

Stopping-time property

\[\{\tau_n\le t\}=\{A_t\ge n+1\}\in\mathcal F_t\qquad (t<T).\]

Continuity turns first passage into a fixed-time measurable event.

Stopped energy

\[\int_0^T\eta_s^2\mathbf 1_{\{s\le\tau_n\}}\,ds=A_{\tau_n}\le n+1.\]

Before the first hit, accumulated energy cannot exceed the threshold.

Global square integrability

\[\mathbb E\!\left[\int_0^T\eta_s^2\mathbf 1_{\{s\le\tau_n\}}\,ds\right]\le n+1<\infty.\]

Integrating the pathwise bound gives the global L2 estimate required by the Itô integral.

Exhaustion

\[A_T(\omega)<\infty\quad\Longrightarrow\quad \exists N(\omega)\ \forall n\ge N(\omega),\ \tau_n(\omega)=T.\]

If the terminal energy is finite, every sufficiently high level is never reached.

Lean correspondence

#	Mathematical step	Lean lemmas
1	Energy path regularity Make accumulated energy continuous and monotone.	`continuous_completedEnergy` `monotone_completedEnergy`
2	Stopping-time construction Characterize first hits and prove the canonical integer cutoffs are stopping times.	`canonicalEnergyLocalizer_le_iff` `canonicalLocalizingTime_isChewiStoppingTime`
3	Energy control and exhaustion Prove monotonicity, the n+1 energy bound, and convergence to T.	`canonicalLocalizingTime_mono` `completedEnergy_at_canonicalLocalizingTime_le` `tendsto_canonicalLocalizingTime`
4	Global L2 packaging Convert stopped pathwise energy into the exact L2 type consumed by the Ito integral.	`stoppedProgressiveL2`
5	Chewi Proposition 1.1.13 Assemble the stopping-time, monotonicity, exhaustion, and L2 obligations into the source theorem.	`chewi_proposition_1_1_13`

Focused test: Tests/CanonicalLocalizationTheorem.lean

Chewi, Proposition 1.1.13 ↗

Proposition 1.1.16

The local Ito integral is a continuous local martingale

Chewi statement

\[M_t:=\int_0^t \eta_s\,dB_s,\qquad M_{t\wedge\tau_n}=\int_0^t \eta_s\mathbf 1_{\{s\le\tau_n\}}\,dB_s,\]

\[0\le s\le t\quad\Longrightarrow\quad \mathbb E\!\left[M_{t\wedge\tau_n}\mid\mathcal F_s\right]=M_{s\wedge\tau_n},\]

\[\tau_n\uparrow\infty\ \text{a.s.}\quad\Longrightarrow\quad M\in\mathcal M_{\mathrm{loc}}\ \text{and }M\text{ has continuous paths.}\]

For a progressive integrand that is locally square-integrable, its Ito integral, defined by localization, is a continuous local martingale.

Assumptions

a complete right-continuous filtered probability space
Brownian motion relative to that filtration
a progressive integrand with finite quadratic energy on every finite horizon almost surely

Chewi proof status

Chewi defines the localized Itô integral through the stopped processes in (1.1.14) and says that the technical details are omitted. The expansion below records the ASTIS proof obligations.

ASTIS formal expansion

Localize into the L2 theory

\[\eta^{(n)}_s:=\eta_s\mathbf 1_{\{s\le\tau_n\}},\qquad \mathbb E\int_0^T|\eta^{(n)}_s|^2\,ds<\infty.\]

For each canonical localizer, the stopped integrand is a legal global-L2 integrand.

Apply the global Itô theorem

\[M^{(n)}_t:=\int_0^t\eta^{(n)}_s\,dB_s,\qquad \mathbb E[M^{(n)}_t\mid\mathcal F_s]=M^{(n)}_s\quad(s\le t).\]

Theorem 1.1.8 produces a continuous martingale on every localized window.

Random stopping commutes with Itô integration

\[\left(\int_0^{\cdot}\eta_s\,dB_s\right)_{t\wedge\tau}=\int_0^t\eta_s\mathbf 1_{\{s\le\tau\}}\,dB_s.\]

Grid-valued stopping is finite-sum algebra; dyadic approximation and the Itô isometry pass to bounded stopping times.

Endpoint convention

\[(dt\otimes d\mathbb P)\{(s,\omega):s=\tau(\omega)\}=0.\]

Strict and closed stopping differ only on the stopping graph, which is product-measure null.

Coherence

\[k\le \ell\quad\Longrightarrow\quad M^{(\ell)}_{t\wedge\tau_k}=M^{(k)}_t\qquad\text{a.s. for all }t.\]

Localized martingales agree on every common stopping window.

Glue and localize

\[M^{\tau_k}=M^{(k)}\in\mathcal M_c,\qquad \tau_k\uparrow\infty\ \text{a.s.}\]

Coherence defines one continuous process whose stopped versions are genuine martingales.

Conclusion

\[M_t=\int_0^t\eta_s\,dB_s\in\mathcal M_{\mathrm{loc}}\cap C([0,\infty)).\]

This is exactly the definition of a continuous local martingale.

Lean correspondence

#	Mathematical step	Lean lemmas
1	Finite stopping algebra Establish the exact random-stop identity before any limiting argument.	`elementaryItoIntegral_stop_gridValued`
2	Random-stop completion Pass from dyadic right approximations to arbitrary bounded stopping times at process level.	`itoIntegralProcess_stop_eq_stoppedProcess_pathwise_ae`
3	Cross-horizon L2 overlap Identify the smaller stopped integrand with the zero-extended restriction of the larger-horizon one.	`stop_globalStopped_toLp_eq_extendByZero`
4	Localized martingales Build continuous martingales on each canonical stop and prove their pathwise overlap.	`globalStoppedItoProcess_martingale` `globalStoppedItoProcess_overlap_pathwise_ae`
5	Global gluing Choose one adapted continuous global version and certify local-martingale structure.	`globalItoProcess_continuous` `globalItoProcess_isLocalMartingale`
6	Chewi Proposition 1.1.16 Expose the source theorem, stopped-integral representation, and canonical localizers.	`chewi_proposition_1_1_16` `chewi_proposition_1_1_16_stopped_integral_representation` `chewi_proposition_1_1_16_localizers`

Focused test: Tests/ChewiProposition1_1_16.lean

Chewi, Proposition 1.1.16 ↗

ASTIS makes the calculation rules explicit

Implicit prerequisite theorems and proofs

Provenance rule. These are not additional claims attributed to Chewi. They are the measure-theoretic, stochastic-process, and functional-analytic facts that the textbook calculation uses without promoting each one to a numbered standalone result. ASTIS states their assumptions and proofs explicitly, records the classical sources that explain the omitted infrastructure, and keeps Lean details optional.

9/9 prerequisite cards currently have compiled Lean support. A frontier card remains mathematically documented without being promoted to a compiled source result.

ASTIS implicit prerequisite · not a standalone Chewi result

Tonelli/Fubini bridge for stochastic-process energy

Why the textbook calculation needs this. Used whenever the calculation route identifies a product-space L2 norm with an expectation of a time integral.

\[\text{If } f\ge 0 \text{ is measurable on } \Omega\times[0,T],\quad \int_{\Omega\times[0,T]} f\,d(\mathbb P\otimes dt)=\int_\Omega\!\left(\int_0^T f(\omega,t)\,dt\right)d\mathbb P(\omega).\]

compiled Lean support

Full theorem and mathematical proof

Assumptions

a sigma-finite time measure on [0,T]
a probability measure on the sample space
joint measurability of the nonnegative integrand

Proof

Apply Tonelli's theorem to the nonnegative measurable function f. No prior integrability assumption is needed because both sides are ENNReal-valued. If either side is finite, Tonelli identifies the other with the same finite value. For f(omega,t)=|eta_t(omega)|^2 this is exactly the bridge between the product-space L2 energy and the expected pathwise energy.

Where Chewi uses it implicitly

display (1.1.7)
Theorem 1.1.8
Definition 1.1.12
Proposition 1.1.13

Foundation references

These sources explain the omitted background; they do not replace the Chewi source statement or the ASTIS proof obligation.

Karatzas--Shreve, Brownian Motion and Stochastic Calculus — Rigorous stochastic-integration context for the product-space L2 energy and Ito isometry; ASTIS states the underlying Tonelli step explicitly rather than attributing it to a Chewi result.
Shreve, Stochastic Calculus for Finance II — Reader-facing explanation of why square-integrable stochastic integrands are measured through expected time-integrated energy.

View Lean formalization

This is ASTIS supplemental infrastructure. Its Lean status does not alter the completion status of a Chewi source item. Each compiled link below resolves through the generated source catalog: Registry theorem card, reviewed declaration card, or exact module anchor.

chewi_display_1_1_7open exact Lean declaration →

ASTIS implicit prerequisite · not a standalone Chewi result

Singleton time endpoints are null

Why the textbook calculation needs this. Justifies changing [0,t], (0,t], [0,t), or strict stopping conventions inside L2 and stochastic integrals.

\[dt(\{s\})=0\quad\text{for every }s\ge 0,\qquad \int_{[0,T]} f\,dt=\int_{(0,T]} f\,dt\quad\text{whenever either side is defined in the usual a.e. sense}.\]

compiled Lean support

Full theorem and mathematical proof

Assumptions

Lebesgue measure on nonnegative time
measurability of the integrand

Proof

Lebesgue measure is atomless, so every singleton has measure zero. Two measurable functions or indicators that differ only at finitely many endpoints are therefore equal almost everywhere. Lebesgue integrals, Lp classes, and the L2 completion used for the Ito integral identify such representatives.

Where Chewi uses it implicitly

display (1.1.6)
display (1.1.9)
Proposition 1.1.13
stopped-integrand compatibility

Foundation references

These sources explain the omitted background; they do not replace the Chewi source statement or the ASTIS proof obligation.

Karatzas--Shreve, Brownian Motion and Stochastic Calculus — The stochastic-integral construction is formulated modulo almost-everywhere equality, which is the conceptual reason deterministic endpoint conventions do not change the L2 integral.
Protter, Stochastic Integration and Differential Equations — General stochastic-integration framework in which integrands are identified through the relevant almost-everywhere/process equivalences; ASTIS isolates the singleton-time lemma needed here.

View Lean formalization

upTo_singletonopen exact Lean declaration →ae_mem_Ioc_zero_upToopen exact Lean declaration →

ASTIS implicit prerequisite · not a standalone Chewi result

Progressive measurability survives adapted stopping thresholds

Why the textbook calculation needs this. The stopped integrand must still lie in the measurable domain of the stochastic integral.

\[\eta^{(c)}_t(\omega):=\eta_t(\omega)\mathbf 1_{\{A_t(\omega)<c\}}\quad\text{is progressive whenever }\eta\text{ and }A\text{ are progressive}.\]

compiled Lean support

Full theorem and mathematical proof

Assumptions

eta is progressive
A is a real-valued progressive process
c is deterministic

Proof

For every terminal time u, the restriction of (t,omega) -> A_t(omega) to [0,u] x Omega is measurable with respect to B([0,u]) tensor F_u. Hence the sublevel set {A<c} is measurable in the same product sigma-algebra. Multiplying eta by its indicator, equivalently using a measurable if-then-else with zero, preserves strong/progressive measurability.

Where Chewi uses it implicitly

Proposition 1.1.13
display (1.1.14)

Foundation references

These sources explain the omitted background; they do not replace the Chewi source statement or the ASTIS proof obligation.

Karatzas--Shreve, Brownian Motion and Stochastic Calculus — Filtered probability spaces, adapted/progressive processes, stopping times, and the measurability conditions needed before stochastic integration.
Protter, Stochastic Integration and Differential Equations — Process-level stochastic-integration preliminaries and stopping/localization conventions that motivate treating stopped integrands as first-class measurable processes.

View Lean formalization

energyStoppedIntegrand_stronglyProgressiveopen exact Lean declaration →

ASTIS implicit prerequisite · not a standalone Chewi result

First hitting time of an adapted continuous energy path is a stopping time

Why the textbook calculation needs this. Chewi's canonical energy thresholds must satisfy the stopping-time clause of a localizing sequence.

\[A_t:=\int_0^{t\wedge T}|\eta_s|^2ds,\qquad \tau_c:=\inf\{t\in[0,T]:A_t=c\}\ \text{(with }T\text{ if the level is never hit)}.\quad \{\tau_c\le t\}\in\mathcal F_t.\]

compiled Lean support

Full theorem and mathematical proof

Assumptions

A is adapted
every path t -> A_t is continuous and nondecreasing
c >= 0

Proof

For t<T, continuity and monotonicity imply tau_c <= t if and only if c <= A_t: if the level has been reached, monotonicity gives A_t >= c; conversely, if A_t >= c, the intermediate value theorem between A_0=0 and A_t produces a level-c time no later than t. Since A_t is F_t-measurable, {c<=A_t} is F_t-measurable. For t>=T the event is the whole space because tau_c<=T.

Where Chewi uses it implicitly

Definition 1.1.12
Proposition 1.1.13

Foundation references

These sources explain the omitted background; they do not replace the Chewi source statement or the ASTIS proof obligation.

Karatzas--Shreve, Brownian Motion and Stochastic Calculus — Stopping-time and hitting-time technology for adapted continuous processes; ASTIS specializes it to the monotone accumulated-energy path used by Chewi.
Revuz--Yor, Continuous Martingales and Brownian Motion — Continuous-process stopping-time background and deeper pathwise stopping technology used as a secondary reference when version/hitting arguments become delicate.

View Lean formalization

canonicalEnergyLocalizer_le_iffopen exact Lean declaration →canonicalLocalizingTime_isStoppingTimeopen exact Lean declaration →

ASTIS implicit prerequisite · not a standalone Chewi result

Extension of the elementary Ito map by L2 completion

Why the textbook calculation needs this. The textbook calculation rule passes from elementary adapted processes to arbitrary progressive L2 integrands.

\[I_T:\mathcal E\to L^2(\Omega),\quad I_T(\eta)=\sum_i H_i(B_{t_{i+1}}-B_{t_i}),\qquad \|I_T(\eta)\|_{L^2(\Omega)}=\|\eta\|_{L^2(\Omega\times[0,T])}.\quad I_T\text{ extends uniquely and linearly to }\overline{\mathcal E}^{L^2}.\]

compiled Lean support

Full theorem and mathematical proof

Assumptions

elementary adapted processes are dense in the progressive L2 domain
the elementary Ito isometry
L2(Omega) is complete

Proof

The elementary Ito isometry makes I_T an isometry on the dense elementary subspace. For any L2-Cauchy approximating sequence eta^n, the sequence I_T(eta^n) is Cauchy in L2(Omega), hence converges. Isometry shows that the limit does not depend on the chosen approximation. Passing addition and scalar multiplication through limits gives linearity, and the norm identity survives by continuity.

Where Chewi uses it implicitly

Theorem 1.1.8
display (1.1.9)
display (1.1.14)

Foundation references

These sources explain the omitted background; they do not replace the Chewi source statement or the ASTIS proof obligation.

Karatzas--Shreve, Brownian Motion and Stochastic Calculus — Primary rigorous reference for constructing the stochastic integral from elementary processes by isometry and L2 completion.
Shreve, Stochastic Calculus for Finance II — Pedagogical companion for the elementary-integrand construction, Ito isometry, and extension to general square-integrable integrands.

View Lean formalization

itoIntegralTerminalopen exact Lean declaration →itoIntegralTerminal_normopen exact Lean declaration →

ASTIS implicit prerequisite · not a standalone Chewi result

Doob L2 maximal inequality for continuous martingales

Why the textbook calculation needs this. Controls the entire stochastic-integral path from terminal L2 differences and upgrades terminal convergence to uniform path convergence along a subsequence.

\[\mathbb E\left[\sup_{0\le t\le T}|M_t|^2\right]\le 4\,\mathbb E|M_T|^2\qquad\text{for a square-integrable martingale }M.\]

compiled Lean support

Full theorem and mathematical proof

Assumptions

M is an adapted square-integrable martingale
a continuous or right-continuous version on [0,T]

Proof

Apply Doob's maximal inequality with exponent p=2. In the standard proof, the submartingale |M_t| is controlled by its terminal L2 norm using the weak maximal inequality, layer-cake integration, and Cauchy-Schwarz, yielding the sharp factor (p/(p-1))^p=4 at p=2.

Where Chewi uses it implicitly

Theorem 1.1.8 continuous version
stability of Ito-process approximants

Foundation references

These sources explain the omitted background; they do not replace the Chewi source statement or the ASTIS proof obligation.

Karatzas--Shreve, Brownian Motion and Stochastic Calculus — Primary martingale/maximal-inequality background used to control the stochastic-integral approximating processes.
Revuz--Yor, Continuous Martingales and Brownian Motion — Secondary reference for continuous-martingale inequalities and the path-space viewpoint used by the continuous-version construction.

View Lean formalization

doobL2_continuousopen exact Lean declaration →

ASTIS implicit prerequisite · not a standalone Chewi result

Borel-Cantelli construction of a uniformly convergent continuous version

Why the textbook calculation needs this. A fixed-time L2 completion alone does not produce one process with continuous sample paths at all times.

\[\sum_k\mathbb P\!\left(\sup_{t\le T}|M^{k+1}_t-M^k_t|>2^{-k}\right)<\infty\quad\Longrightarrow\quad M^k\text{ is uniformly Cauchy on }[0,T]\text{ a.s.}\]

compiled Lean support

Full theorem and mathematical proof

Assumptions

continuous approximating processes
summable maximal-deviation probabilities

Proof

By the first Borel-Cantelli lemma, with probability one only finitely many bad maximal-deviation events occur. On every remaining sample path, the tail increments are bounded by a summable geometric series, so M^k is uniformly Cauchy on [0,T]. The uniform limit exists and is continuous because a uniform limit of continuous functions is continuous. Fixed-time L2 convergence identifies this pathwise limit with the completed Ito integral representatives.

Where Chewi uses it implicitly

Theorem 1.1.8 adapted continuous process construction

Foundation references

These sources explain the omitted background; they do not replace the Chewi source statement or the ASTIS proof obligation.

Karatzas--Shreve, Brownian Motion and Stochastic Calculus — Rigorous stochastic-integral construction and continuous-modification arguments that motivate the subsequence/maximal-inequality route formalized by ASTIS.
Revuz--Yor, Continuous Martingales and Brownian Motion — Continuous-martingale path regularity and version/indistinguishability background used to interpret the resulting continuous stochastic-integral process.

View Lean formalization

itoIntegralProcess_continuous_aeopen exact Lean declaration →

ASTIS implicit prerequisite · not a standalone Chewi result

Energy stopping converts local square integrability into global L2

Why the textbook calculation needs this. This is the quantitative heart of Proposition 1.1.13: stopping at level n makes the expected stochastic-integral energy finite.

\[A_t=\int_0^{t\wedge T}|\eta_s|^2ds,\quad \tau_n=\inf\{t:A_t=n+1\}\wedge T,\qquad \int_0^T |\eta_t|^2\mathbf 1_{\{t<\tau_n\}}dt=A_{\tau_n}\le n+1.\]

compiled Lean support

Full theorem and mathematical proof

Assumptions

pathwise finite square energy almost surely
continuous nondecreasing accumulated energy
the exceptional nonintegrable paths are completed or stopped immediately

Proof

Before tau_n the accumulated energy is strictly below n+1; after tau_n the stopped integrand is zero. Since a single hitting-time endpoint has zero Lebesgue measure, integrating the stopped square gives exactly the prefix energy A_{tau_n}. If the level is reached, continuity gives A_{tau_n}=n+1; if it is not reached, tau_n=T and A_T<n+1. Hence the pathwise energy is at most n+1. Taking expectation under a probability measure preserves the same finite bound.

Where Chewi uses it implicitly

Proposition 1.1.13
display (1.1.14)

Foundation references

These sources explain the omitted background; they do not replace the Chewi source statement or the ASTIS proof obligation.

Karatzas--Shreve, Brownian Motion and Stochastic Calculus — Localization and stochastic-integrability background: stopping at an accumulated-energy threshold converts a locally square-integrable integrand into an L2-integrable one on the finite horizon.
Protter, Stochastic Integration and Differential Equations — General localization viewpoint for stochastic integrals and local martingales; ASTIS makes Chewi's particular energy-localizer estimate quantitative and explicit.

View Lean formalization

integral_energyStoppedIntegrand_sq_leopen exact Lean declaration →stoppedProgressiveL2open exact Lean declaration →

ASTIS implicit prerequisite · not a standalone Chewi result

Consistency of stopped Ito integrals

Why the textbook calculation needs this. Proposition 1.1.16 must patch the L2 Ito integrals of the localized integrands into one local martingale without contradictory values on overlaps.

\[m\le n\quad\Longrightarrow\quad \int_0^{t\wedge\tau_m}\eta_s\,dB_s = \left(\int_0^{\cdot\wedge\tau_n}\eta_s\,dB_s\right)_{t\wedge\tau_m}\quad\text{a.s.}\]

compiled Lean support

Full theorem and mathematical proof

Assumptions

tau_m <= tau_n
both stopped integrands are in global progressive L2
the Ito map is unique in L2 and compatible with deterministic-time restriction

Proof

Up to tau_m, both localized integrands agree with eta; after tau_m, the m-localized integrand is zero. Therefore restricting the n-localized integrand again at tau_m gives the same L2 integrand as the m-localized one, modulo the null hitting-time endpoint. Equality in product L2 is first transferred to equality of the completed Ito processes on one common full-measure event using continuous-version uniqueness. The bounded random-stopping theorem then identifies the Ito process of the stopped integrand with the stopped continuous Ito process simultaneously for every time on the horizon. Combining these facts yields coherent localized martingales without intersecting uncountably many deterministic-time null sets.

Where Chewi uses it implicitly

Proposition 1.1.16
definition of the localized Ito integral

Foundation references

These sources explain the omitted background; they do not replace the Chewi source statement or the ASTIS proof obligation.

Karatzas--Shreve, Brownian Motion and Stochastic Calculus — Primary rigorous background for stochastic-integral uniqueness, stopped stochastic integrals, continuous versions, and local martingales.
Protter, Stochastic Integration and Differential Equations — Primary supplementary reference for process-level stopping/localization and stochastic-integral consistency; ASTIS formalizes the exact finite-horizon L2 and pathwise version needed by Chewi.
Revuz--Yor, Continuous Martingales and Brownian Motion — Secondary reference for continuous local-martingale versions and indistinguishability-style pathwise reasoning.

View Lean formalization

itoIntegralProcess_congr_toLp_pathwise_aeopen exact Lean declaration →itoIntegralProcess_stop_eq_stoppedProcess_pathwise_aeopen exact Lean declaration →globalStoppedItoProcess_overlap_pathwise_aeopen exact Lean declaration →