Samplinglib
Lean gate not recorded for this source state main · 0e31a3cda412
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 ↗
Formal topologyOpen this section in the underlying Lean graph↗
Theorem 1.1.8
book 6 / PDF 18 · faithful paraphrase

Statement

\[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]\]

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.

Lean statement · chewi_theorem_1_1_8

Compare this exact declaration with the source statement and explicit hypotheses on this card. A formal premise is not proved merely because Lean accepts a conditional theorem.

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.

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)

Exact module and namespace context

Proof / derivation

Source-faithful equation route; notation is normalized but the argument is not replaced by an ASTIS proof.

1
\[\eta^{(n)}\in\mathcal E,\qquad \|\eta^{(n)}-\eta\|_{L^2(\mathbb P\otimes dt)}\longrightarrow0\]
2
\[\|I_T(\eta^{(n)})-I_T(\eta^{(m)})\|_{L^2(\mathbb P)}^2=\|\eta^{(n)}-\eta^{(m)}\|_{L^2(\mathbb P\otimes dt)}^2\longrightarrow0\]
3
\[I_T(\eta):=L^2(\mathbb P)\!\!-\!\lim_{n\to\infty}I_T(\eta^{(n)})\]
4
\[\|I_T(\eta^{(n)})-I_T(\widetilde\eta^{(n)})\|_2=\|\eta^{(n)}-\widetilde\eta^{(n)}\|_2\longrightarrow0\]
5
\[I_T(a\eta+b\xi)=aI_T(\eta)+bI_T(\xi)\]
6
\[\|I_T(\eta)\|_{L^2(\mathbb P)}^2=\|\eta\|_{L^2(\mathbb P\otimes dt)}^2=\mathbb E\!\left[\int_0^T|\eta_t|^2\,dt\right]\]
7
\[I_t(\eta):=I_T(\eta\mathbf1_{(0,t]}),\qquad 0\le s\le t\le T\Longrightarrow\mathbb E[I_t(\eta)\mid\mathcal F_s]=I_s(\eta)\]

Assumptions and implicit prerequisites

Source-level assumptions

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

Conditions made explicit by ASTIS

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

ASTIS rigorous LaTeX formalization

The source argument is restated here as a strict ASTIS LaTeX packet before the Lean correspondence.

\[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]\]
1
\[\eta^{(n)}\in\mathcal E,\qquad \|\eta^{(n)}-\eta\|_{L^2(\mathbb P\otimes dt)}\longrightarrow0\]
2
\[\|I_T(\eta^{(n)})-I_T(\eta^{(m)})\|_{L^2(\mathbb P)}^2=\|\eta^{(n)}-\eta^{(m)}\|_{L^2(\mathbb P\otimes dt)}^2\longrightarrow0\]
3
\[I_T(\eta):=L^2(\mathbb P)\!\!-\!\lim_{n\to\infty}I_T(\eta^{(n)})\]
4
\[\|I_T(\eta^{(n)})-I_T(\widetilde\eta^{(n)})\|_2=\|\eta^{(n)}-\widetilde\eta^{(n)}\|_2\longrightarrow0\]
5
\[I_T(a\eta+b\xi)=aI_T(\eta)+bI_T(\xi)\]
6
\[\|I_T(\eta)\|_{L^2(\mathbb P)}^2=\|\eta\|_{L^2(\mathbb P\otimes dt)}^2=\mathbb E\!\left[\int_0^T|\eta_t|^2\,dt\right]\]
7
\[I_t(\eta):=I_T(\eta\mathbf1_{(0,t]}),\qquad 0\le s\le t\le T\Longrightarrow\mathbb E[I_t(\eta)\mid\mathcal F_s]=I_s(\eta)\]
Lean proof · chewi_theorem_1_1_8

This is the complete declaration source underlying this mathematical step. Follow the named parent results, distinguishing the hypotheses supplied to the theorem from conclusions actually derived. Source correspondence and compilation are separate statuses.

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.

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

Exact module and namespace context

Source mapping and supporting declarations

Final declaration

Underlying proof leaves

  • progressiveL2_elementary_dense
  • itoIntegralTerminal_norm
  • itoIntegralProcess_martingale
  • itoIntegralProcess_continuous_ae
  • itoIntegralProcess_at_eq_terminal
  • itoIntegralProcess_unique
  • chewi_theorem_1_1_8
Chewi source ↗
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

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)
book 6 / PDF 18 · faithful paraphrase

Statement

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

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.

Lean statement · chewi_display_1_1_9

Compare this exact declaration with the source statement and explicit hypotheses on this card. A formal premise is not proved merely because Lean accepts a conditional theorem.

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.

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)

Exact module and namespace context

Proof / derivation

Source-faithful equation route; notation is normalized but the argument is not replaced by an ASTIS proof.

1
\[I_t(\eta)=I_T(\eta\mathbf1_{(0,t]})\]
2
\[\mathbb E[I_t(\eta)^2]=\|I_T(\eta\mathbf1_{(0,t]})\|_2^2=\|\eta\mathbf1_{(0,t]}\|_2^2\]
3
\[\boxed{\;\mathbb E[I_t(\eta)^2]=\mathbb E\!\left[\int_0^t|\eta_s|^2\,ds\right]\;}\]

Assumptions and implicit prerequisites

Source-level 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

Conditions made explicit by ASTIS

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

ASTIS rigorous LaTeX formalization

The source argument is restated here as a strict ASTIS LaTeX packet before the Lean correspondence.

\[\mathbb E[I_t(\eta)^2]=\mathbb E\!\left[\int_0^t \eta_s^2\,ds\right]\]
1
\[I_t(\eta)=I_T(\eta\mathbf1_{(0,t]})\]
2
\[\mathbb E[I_t(\eta)^2]=\|I_T(\eta\mathbf1_{(0,t]})\|_2^2=\|\eta\mathbf1_{(0,t]}\|_2^2\]
3
\[\boxed{\;\mathbb E[I_t(\eta)^2]=\mathbb E\!\left[\int_0^t|\eta_s|^2\,ds\right]\;}\]
Lean proof · chewi_display_1_1_9

This is the complete declaration source underlying this mathematical step. Follow the named parent results, distinguishing the hypotheses supplied to the theorem from conclusions actually derived. Source correspondence and compilation are separate statuses.

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.

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. -/

Exact module and namespace context

Source mapping and supporting declarations

Final declaration

Underlying proof leaves

  • chewi_display_1_1_9
Chewi source ↗
Why is this valid?

The theorem exposes the deterministic-time bound \(t\le 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\le 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)
book 5 / PDF 17 · faithful paraphrase

Statement

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

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

Lean statement · chewi_display_1_1_5

Compare this exact declaration with the source statement and explicit hypotheses on this card. A formal premise is not proved merely because Lean accepts a conditional theorem.

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.

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 ∂μ

Exact module and namespace context

Proof / derivation

Source-faithful equation route; notation is normalized but the argument is not replaced by an ASTIS proof.

1
\[I_T(\eta)=\sum_{i=0}^{m-1}H_i\,\Delta B_i,\qquad \Delta B_i:=B_{t_{i+1}\wedge T}-B_{t_i\wedge T}\]
2
\[\mathbb E[I_T(\eta)^2]=\sum_i\mathbb E[H_i^2(\Delta B_i)^2]+2\sum_{i<j}\mathbb E[H_iH_j\Delta B_i\Delta B_j]\]
3
\[i<j\quad\Longrightarrow\quad \mathbb E[H_iH_j\Delta B_i\Delta B_j]=0\]
4
\[\mathbb E[I_T(\eta)^2]=\sum_i\mathbb E[H_i^2(\Delta B_i)^2]\]

Assumptions and implicit prerequisites

Source-level assumptions

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

Conditions made explicit by ASTIS

  • ElementaryAdaptedProcess
  • IsBrownianMotionWithFiltration
  • MemLp two for weighted increments

ASTIS rigorous LaTeX formalization

The source argument is restated here as a strict ASTIS LaTeX packet before the Lean correspondence.

\[\mathbb E\!\left[\left(\sum_i H_i\Delta B_i\right)^2\right]=\sum_i \mathbb E[(H_i\Delta B_i)^2]\]
1
\[I_T(\eta)=\sum_{i=0}^{m-1}H_i\,\Delta B_i,\qquad \Delta B_i:=B_{t_{i+1}\wedge T}-B_{t_i\wedge T}\]
2
\[\mathbb E[I_T(\eta)^2]=\sum_i\mathbb E[H_i^2(\Delta B_i)^2]+2\sum_{i<j}\mathbb E[H_iH_j\Delta B_i\Delta B_j]\]
3
\[i<j\quad\Longrightarrow\quad \mathbb E[H_iH_j\Delta B_i\Delta B_j]=0\]
4
\[\mathbb E[I_T(\eta)^2]=\sum_i\mathbb E[H_i^2(\Delta B_i)^2]\]
Lean proof · chewi_display_1_1_5

This is the complete declaration source underlying this mathematical step. Follow the named parent results, distinguishing the hypotheses supplied to the theorem from conclusions actually derived. Source correspondence and compilation are separate statuses.

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.

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. -/

Exact module and namespace context

Source mapping and supporting declarations

Final declaration

Underlying proof leaves

  • chewi_display_1_1_5
Chewi source ↗
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)
book 5 / PDF 17 · faithful paraphrase

Statement

\[\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 second moment of the elementary Ito integral equals the expected time integral of the squared elementary integrand.

Lean statement · chewi_display_1_1_6

Compare this exact declaration with the source statement and explicit hypotheses on this card. A formal premise is not proved merely because Lean accepts a conditional theorem.

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.

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

Exact module and namespace context

Proof / derivation

Source-faithful equation route; notation is normalized but the argument is not replaced by an ASTIS proof.

1
\[\mathbb E[H_i^2(\Delta B_i)^2]=\mathbb E[H_i^2]\,\bigl((t_{i+1}\wedge T)-(t_i\wedge T)\bigr)\]
2
\[\sum_i\mathbb E[H_i^2]\,\bigl((t_{i+1}\wedge T)-(t_i\wedge T)\bigr)=\mathbb E\!\left[\int_0^T|\eta_t|^2\,dt\right]\]
3
\[\boxed{\;\mathbb E\!\left[\left(\int_0^T\eta_t\,dB_t\right)^2\right]=\mathbb E\!\left[\int_0^T|\eta_t|^2\,dt\right]\;}\]

Assumptions and implicit prerequisites

Source-level assumptions

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

Conditions made explicit by ASTIS

  • IsBrownianMotionWithFiltration
  • TimeMeasure.upTo
  • processTimeMeasure
  • processL2Energy

ASTIS rigorous LaTeX formalization

The source argument is restated here as a strict ASTIS LaTeX packet before the Lean correspondence.

\[\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]\]
1
\[\mathbb E[H_i^2(\Delta B_i)^2]=\mathbb E[H_i^2]\,\bigl((t_{i+1}\wedge T)-(t_i\wedge T)\bigr)\]
2
\[\sum_i\mathbb E[H_i^2]\,\bigl((t_{i+1}\wedge T)-(t_i\wedge T)\bigr)=\mathbb E\!\left[\int_0^T|\eta_t|^2\,dt\right]\]
3
\[\boxed{\;\mathbb E\!\left[\left(\int_0^T\eta_t\,dB_t\right)^2\right]=\mathbb E\!\left[\int_0^T|\eta_t|^2\,dt\right]\;}\]
Lean proof · chewi_display_1_1_6

This is the complete declaration source underlying this mathematical step. Follow the named parent results, distinguishing the hypotheses supplied to the theorem from conclusions actually derived. Source correspondence and compilation are separate statuses.

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.

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

Exact module and namespace context

Source mapping and supporting declarations

Final declaration

Underlying proof leaves

  • chewi_display_1_1_6
Chewi source ↗
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)
book 6 / PDF 18 · faithful paraphrase

Statement

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

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

Lean statement · chewi_display_1_1_10

Compare this exact declaration with the source statement and explicit hypotheses on this card. A formal premise is not proved merely because Lean accepts a conditional theorem.

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.

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)) < ∞

Exact module and namespace context

Assumptions and implicit prerequisites

Source-level assumptions

  • a real stochastic integrand
  • a finite terminal time
  • a probability measure

Conditions made explicit by ASTIS

  • TimeMeasure.upTo T
  • ENNReal lintegral
  • Filter.Eventually under mu

ASTIS rigorous LaTeX formalization

This packet records the strict ASTIS statement. No additional proof is attributed to the source.

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

This is the complete declaration source underlying this mathematical step. Follow the named parent results, distinguishing the hypotheses supplied to the theorem from conclusions actually derived. Source correspondence and compilation are separate statuses.

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.

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

Exact module and namespace context

Source mapping and supporting declarations

Final declaration

Underlying proof leaves

  • chewi_display_1_1_10
Chewi source ↗
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)
book 5 / PDF 17 · faithful paraphrase

Statement

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

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.

Lean statement · chewi_display_1_1_7

Compare this exact declaration with the source statement and explicit hypotheses on this card. A formal premise is not proved merely because Lean accepts a conditional theorem.

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.

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

Exact module and namespace context

Assumptions and implicit prerequisites

Source-level assumptions

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

Conditions made explicit by ASTIS

  • TimeMeasure.upTo T
  • AEMeasurable squared process on processTimeMeasure
  • ENNReal lintegrals

ASTIS rigorous LaTeX formalization

This packet records the strict ASTIS statement. No additional proof is attributed to the source.

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

This is the complete declaration source underlying this mathematical step. Follow the named parent results, distinguishing the hypotheses supplied to the theorem from conclusions actually derived. Source correspondence and compilation are separate statuses.

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.

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. -/

Exact module and namespace context

Source mapping and supporting declarations

Final declaration

Underlying proof leaves

  • chewi_display_1_1_7
Chewi source ↗
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)
book 4 / PDF 16 · faithful paraphrase

Statement

\[\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})\]

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

Lean statement · chewi_display_1_1_2

Compare this exact declaration with the source statement and explicit hypotheses on this card. A formal premise is not proved merely because Lean accepts a conditional theorem.

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.

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

Exact module and namespace context

Assumptions and implicit prerequisites

Source-level assumptions

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

Conditions made explicit by ASTIS

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

ASTIS rigorous LaTeX formalization

This packet records the strict ASTIS statement. No additional proof is attributed to the source.

\[\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})\]
Lean proof · chewi_display_1_1_2

This is the complete declaration source underlying this mathematical step. Follow the named parent results, distinguishing the hypotheses supplied to the theorem from conclusions actually derived. Source correspondence and compilation are separate statuses.

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.

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`. -/

Exact module and namespace context

Source mapping and supporting declarations

Final declaration

Underlying proof leaves

  • chewi_display_1_1_2
Chewi source ↗
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)
book 5 / PDF 17 · faithful paraphrase

Statement

\[\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)\]

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.

Lean statement · chewi_display_1_1_3

Compare this exact declaration with the source statement and explicit hypotheses on this card. A formal premise is not proved merely because Lean accepts a conditional theorem.

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.

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)

Exact module and namespace context

Assumptions and implicit prerequisites

Source-level assumptions

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

Conditions made explicit by ASTIS

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

ASTIS rigorous LaTeX formalization

This packet records the strict ASTIS statement. No additional proof is attributed to the source.

\[\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)\]
Lean proof · chewi_display_1_1_3

This is the complete declaration source underlying this mathematical step. Follow the named parent results, distinguishing the hypotheses supplied to the theorem from conclusions actually derived. Source correspondence and compilation are separate statuses.

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.

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). -/

Exact module and namespace context

Source mapping and supporting declarations

Final declaration

Underlying proof leaves

  • chewi_display_1_1_3
Chewi source ↗
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
book 4 / PDF 16 · faithful paraphrase

Statement

\[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.}\]

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

Lean statement · IsStandardBrownianMotion

Compare this exact declaration with the source statement and explicit hypotheses on this card. A formal premise is not proved merely because Lean accepts a conditional theorem.

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.

def IsStandardBrownianMotion
    (B : ℝ≥0 → Omega → E) (mu : Measure Omega) : Prop

Exact module and namespace context

Assumptions and implicit prerequisites

Source-level assumptions

  • a probability space
  • a finite-dimensional Euclidean state space

Conditions made explicit by ASTIS

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

ASTIS rigorous LaTeX formalization

This packet records the strict ASTIS statement. No additional proof is attributed to the source.

\[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.}\]
Lean construction · IsStandardBrownianMotion

This is the complete declaration source underlying this mathematical step. Follow the named parent results, distinguishing the hypotheses supplied to the theorem from conclusions actually derived. Source correspondence and compilation are separate statuses.

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.

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. -/

Exact module and namespace context

Source mapping and supporting declarations

Final declaration

Underlying proof leaves

  • IsStandardBrownianMotion
Chewi source ↗
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

  • 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

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
book 6 / PDF 18 · faithful paraphrase

Statement

\[\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\]

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.

Lean statement · IsLocalizingSequence

Compare this exact declaration with the source statement and explicit hypotheses on this card. A formal premise is not proved merely because Lean accepts a conditional theorem.

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.

def IsLocalizingSequence
    {Omega : Type*} {m : MeasurableSpace Omega}
    (eta : ℝ≥0 → Omega → ℝ) (filtration : Filtration ℝ≥0 m)
    (mu : Measure Omega) (T : ℝ≥0)
    (tau : ℕ → Omega → WithTop ℝ≥0) : Prop

Exact module and namespace context

Assumptions and implicit prerequisites

Source-level assumptions

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

Conditions made explicit by ASTIS

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

ASTIS rigorous LaTeX formalization

This packet records the strict ASTIS statement. No additional proof is attributed to the source.

\[\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\]
Lean construction · IsLocalizingSequence

This is the complete declaration source underlying this mathematical step. Follow the named parent results, distinguishing the hypotheses supplied to the theorem from conclusions actually derived. Source correspondence and compilation are separate statuses.

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.

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. -/

Exact module and namespace context

Source mapping and supporting declarations

Final declaration

Underlying proof leaves

  • IsLocalizingSequence
Chewi source ↗
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

  • 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

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
book 7 / PDF 19 · faithful paraphrase

Statement

\[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\]

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

Lean statement · IsLocalMartingale

Compare this exact declaration with the source statement and explicit hypotheses on this card. A formal premise is not proved merely because Lean accepts a conditional theorem.

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.

def IsLocalMartingale
    {Omega : Type*} {m : MeasurableSpace Omega}
    (process : ℝ≥0 → Omega → ℝ) (filtration : Filtration ℝ≥0 m)
    (mu : Measure Omega) : Prop

Exact module and namespace context

Assumptions and implicit prerequisites

Source-level assumptions

  • a filtered probability space
  • a real adapted process

Conditions made explicit by ASTIS

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

ASTIS rigorous LaTeX formalization

This packet records the strict ASTIS statement. No additional proof is attributed to the source.

\[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\]
Lean construction · IsLocalMartingale

This is the complete declaration source underlying this mathematical step. Follow the named parent results, distinguishing the hypotheses supplied to the theorem from conclusions actually derived. Source correspondence and compilation are separate statuses.

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.

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

Exact module and namespace context

Source mapping and supporting declarations

Final declaration

Underlying proof leaves

  • IsLocalMartingale
Chewi source ↗
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

  • 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

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
book 5 / PDF 17 · faithful paraphrase

Statement

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

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

Lean statement · IsChewiMartingale

Compare this exact declaration with the source statement and explicit hypotheses on this card. A formal premise is not proved merely because Lean accepts a conditional theorem.

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.

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

Exact module and namespace context

Assumptions and implicit prerequisites

Source-level assumptions

  • a filtered probability space
  • an adapted integrable real process

Conditions made explicit by ASTIS

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

ASTIS rigorous LaTeX formalization

This packet records the strict ASTIS statement. No additional proof is attributed to the source.

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

This is the complete declaration source underlying this mathematical step. Follow the named parent results, distinguishing the hypotheses supplied to the theorem from conclusions actually derived. Source correspondence and compilation are separate statuses.

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.

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. -/

Exact module and namespace context

Source mapping and supporting declarations

Final declaration

Underlying proof leaves

  • IsChewiMartingale
Chewi source ↗
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

  • 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

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\le 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
book 6 / PDF 18 · faithful paraphrase

Statement

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

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

Lean statement · IsChewiStoppingTime

Compare this exact declaration with the source statement and explicit hypotheses on this card. A formal premise is not proved merely because Lean accepts a conditional theorem.

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.

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

Exact module and namespace context

Assumptions and implicit prerequisites

Source-level assumptions

  • a filtered measurable sample space
  • a nonnegative random time

Conditions made explicit by ASTIS

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

ASTIS rigorous LaTeX formalization

This packet records the strict ASTIS statement. No additional proof is attributed to the source.

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

This is the complete declaration source underlying this mathematical step. Follow the named parent results, distinguishing the hypotheses supplied to the theorem from conclusions actually derived. Source correspondence and compilation are separate statuses.

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.

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

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

Exact module and namespace context

Source mapping and supporting declarations

Final declaration

Underlying proof leaves

  • IsChewiStoppingTime
Chewi source ↗
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

  • The stopping-time condition is measurability of every event \(\{\tau\le 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

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\le 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
book 7 / PDF 19 · faithful paraphrase

Statement

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

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.

Lean statement · chewi_proposition_1_1_13

Compare this exact declaration with the source statement and explicit hypotheses on this card. A formal premise is not proved merely because Lean accepts a conditional theorem.

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.

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 : ℝ))

Exact module and namespace context

Proof / derivation status

No source-proof supplement is currently audited for this result. ASTIS does not present a reconstructed argument as if it were Chewi's proof.

Assumptions and implicit prerequisites

Source-level assumptions

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

Conditions made explicit by ASTIS

  • SatisfiesUsualConditions filtration mu
  • IsProbabilityMeasure mu
  • LocalProgressiveL2Integrand filtration mu T

ASTIS rigorous LaTeX formalization

This packet records the strict ASTIS statement. No additional proof is attributed to the source.

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

This is the complete declaration source underlying this mathematical step. Follow the named parent results, distinguishing the hypotheses supplied to the theorem from conclusions actually derived. Source correspondence and compilation are separate statuses.

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.

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

Exact module and namespace context

Source mapping and supporting declarations

Final declaration

Underlying proof leaves

  • chewi_proposition_1_1_13
Chewi source ↗
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)
book 7 / PDF 19 · faithful paraphrase

Statement

\[\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\]

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.

Lean statement · chewi_display_1_1_14

Compare this exact declaration with the source statement and explicit hypotheses on this card. A formal premise is not proved merely because Lean accepts a conditional theorem.

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.

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)

Exact module and namespace context

Assumptions and implicit prerequisites

Source-level assumptions

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

Conditions made explicit by ASTIS

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

ASTIS rigorous LaTeX formalization

This packet records the strict ASTIS statement. No additional proof is attributed to the source.

\[\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\]
Lean proof · chewi_display_1_1_14

This is the complete declaration source underlying this mathematical step. Follow the named parent results, distinguishing the hypotheses supplied to the theorem from conclusions actually derived. Source correspondence and compilation are separate statuses.

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.

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

Exact module and namespace context

Source mapping and supporting declarations

Final declaration

Underlying proof leaves

  • chewi_display_1_1_14
Chewi source ↗
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
book 7 / PDF 19 · faithful paraphrase

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\]

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

Lean statement · chewi_proposition_1_1_16

Compare this exact declaration with the source statement and explicit hypotheses on this card. A formal premise is not proved merely because Lean accepts a conditional theorem.

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.

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

Exact module and namespace context

Proof / derivation status

No source-proof supplement is currently audited for this result. ASTIS does not present a reconstructed argument as if it were Chewi's proof.

Assumptions and implicit prerequisites

Source-level 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

Conditions made explicit by ASTIS

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

ASTIS rigorous LaTeX formalization

This packet records the strict ASTIS statement. No additional proof is attributed to the source.

\[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\]
Lean proof · chewi_proposition_1_1_16

This is the complete declaration source underlying this mathematical step. Follow the named parent results, distinguishing the hypotheses supplied to the theorem from conclusions actually derived. Source correspondence and compilation are separate statuses.

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.

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. -/

Exact module and namespace context

Source mapping and supporting declarations

Final declaration

Underlying proof leaves

  • chewi_proposition_1_1_16
Chewi source ↗
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

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

Proof / derivation 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
1

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.

2

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.

3

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.

4

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.

5

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 stepLean lemmas
1Energy path regularity
Make accumulated energy continuous and monotone.		continuous_completedEnergy
monotone_completedEnergy
2Stopping-time construction
Characterize first hits and prove the canonical integer cutoffs are stopping times.		canonicalEnergyLocalizer_le_iff
canonicalLocalizingTime_isChewiStoppingTime
3Energy control and exhaustion
Prove monotonicity, the n+1 energy bound, and convergence to T.		canonicalLocalizingTime_mono
completedEnergy_at_canonicalLocalizingTime_le
tendsto_canonicalLocalizingTime
4Global L2 packaging
Convert stopped pathwise energy into the exact L2 type consumed by the Ito integral.		stoppedProgressiveL2
5Chewi 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

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

Proof / derivation 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
1

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.

2

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.

3

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.

4

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.

5

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.

6

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.

7

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 stepLean lemmas
1Finite stopping algebra
Establish the exact random-stop identity before any limiting argument.		elementaryItoIntegral_stop_gridValued
2Random-stop completion
Pass from dyadic right approximations to arbitrary bounded stopping times at process level.		itoIntegralProcess_stop_eq_stoppedProcess_pathwise_ae
3Cross-horizon L2 overlap
Identify the smaller stopped integrand with the zero-extended restriction of the larger-horizon one.		stop_globalStopped_toLp_eq_extendByZero
4Localized martingales
Build continuous martingales on each canonical stop and prove their pathwise overlap.		globalStoppedItoProcess_martingale
globalStoppedItoProcess_overlap_pathwise_ae
5Global gluing
Choose one adapted continuous global version and certify local-martingale structure.		globalItoProcess_continuous
globalItoProcess_isLocalMartingale
6Chewi 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 source result

Tonelli/Fubini bridge for stochastic-process energy

Why it is needed. Used whenever the calculation route identifies a product-space \(L^2\) 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).\]

Assumptions

  • a sigma-finite time measure on \([0,T]\)
  • a probability measure on the sample space
  • joint measurability of the nonnegative integrand
Lean statement · chewi_display_1_1_7

The background statement above and this exact formal declaration have distinct scopes. A mapped Lean result may be a specialization; compare its actual hypotheses instead of promoting the whole background theorem from this link.

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.

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

Exact module and namespace context

Mathematical proof

Apply Tonelli's theorem to the nonnegative measurable integrand. Nonnegativity removes the need for a prior integrability hypothesis, and the displayed identity is the resulting iterated-integral equality.

Lean proof · chewi_display_1_1_7

Follow the actual proof calls for the mapped ASTIS result. The displayed mathematical background explains their use; compilation of this declaration does not certify a broader unmapped statement.

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.

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. -/

Exact module and namespace context

Source mapping and supporting declarations
ASTIS implicit prerequisite · not a standalone source result

Singleton time endpoints are null

Why it is needed. Justifies changing [0,t], (0,t], [0,t), or strict stopping conventions inside \(L^2\) 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}.\]

Assumptions

  • Lebesgue measure on nonnegative time
  • measurability of the integrand
Lean statement · upTo_singleton

The background statement above and this exact formal declaration have distinct scopes. A mapped Lean result may be a specialization; compare its actual hypotheses instead of promoting the whole background theorem from this link.

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.

@[simp] theorem upTo_singleton (T t : ℝ≥0) : upTo T {t} = 0

Exact module and namespace context

Lean statement · ae_mem_Ioc_zero_upTo

The background statement above and this exact formal declaration have distinct scopes. A mapped Lean result may be a specialization; compare its actual hypotheses instead of promoting the whole background theorem from this link.

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.

theorem ae_mem_Ioc_zero_upTo (T : ℝ≥0) :
    ∀ᵐ t ∂upTo T, t ∈ Ioc 0 T

Exact module and namespace context

Mathematical proof

Lebesgue measure is atomless, so changing a measurable representative at finitely many time points preserves its almost-everywhere class. The Lebesgue integral, the relevant Lp class, and the completed Itô integral therefore do not depend on those endpoint choices.

Lean proof · upTo_singleton

Follow the actual proof calls for the mapped ASTIS result. The displayed mathematical background explains their use; compilation of this declaration does not certify a broader unmapped statement.

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.

@[simp] theorem upTo_singleton (T t : ℝ≥0) : upTo T {t} = 0 := by
  calc
    upTo T {t} =
        (volume.restrict (Icc 0 (T : ℝ)))
          (NNReal.toReal '' ({t} : Set ℝ≥0)) := by
      unfold upTo
      exact Measure.comap_apply NNReal.toReal NNReal.coe_injective
        (fun _ hs => (MeasurableEmbedding.subtype_coe
          (measurableSet_Ici : MeasurableSet (Ici (0 : ℝ)))).measurableSet_image' hs)
        _ (measurableSet_singleton t)
    _ = 0 := by simp

/-- The mass of `(a, b]` under time measure stopped at `T` is the length of
the clipped interval. -/

Exact module and namespace context

Lean proof · ae_mem_Ioc_zero_upTo

Follow the actual proof calls for the mapped ASTIS result. The displayed mathematical background explains their use; compilation of this declaration does not certify a broader unmapped statement.

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.

theorem ae_mem_Ioc_zero_upTo (T : ℝ≥0) :
    ∀ᵐ t ∂upTo T, t ∈ Ioc 0 T := by
  apply (ae_mem_iff_measure_eq measurableSet_Ioc.nullMeasurableSet).2
  rw [upTo_Ioc T 0 T (by simp), upTo_univ]
  simp

/-- Restricting stopped time to `(0,T]` leaves the measure unchanged. -/

Exact module and namespace context

Source mapping and supporting declarations
ASTIS implicit prerequisite · not a standalone source result

Progressive measurability survives adapted stopping thresholds

Why it is needed. 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}.\]

Assumptions

  • eta is progressive
  • A is a real-valued progressive process
  • c is deterministic
Lean statement · energyStoppedIntegrand_stronglyProgressive

The background statement above and this exact formal declaration have distinct scopes. A mapped Lean result may be a specialization; compare its actual hypotheses instead of promoting the whole background theorem from this link.

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.

theorem energyStoppedIntegrand_stronglyProgressive
    (hUsual : SatisfiesUsualConditions filtration mu)
    (eta : LocalProgressiveL2Integrand filtration mu T)
    (level : ℝ) :
    IsStronglyProgressive filtration
      (energyStoppedIntegrand hUsual eta level)

Exact module and namespace context

Mathematical proof

On every finite horizon, progressiveness makes the threshold event measurable in the corresponding time-filtration product sigma-algebra. Multiplication by its indicator, equivalently a measurable piecewise definition with zero, preserves progressive measurability.

Lean proof · energyStoppedIntegrand_stronglyProgressive

Follow the actual proof calls for the mapped ASTIS result. The displayed mathematical background explains their use; compilation of this declaration does not certify a broader unmapped statement.

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.

theorem energyStoppedIntegrand_stronglyProgressive
    (hUsual : SatisfiesUsualConditions filtration mu)
    (eta : LocalProgressiveL2Integrand filtration mu T)
    (level : ℝ) :
    IsStronglyProgressive filtration
      (energyStoppedIntegrand hUsual eta level) := by
  intro terminal
  have henergy := completedEnergy_stronglyProgressive hUsual eta terminal
  have hset : @MeasurableSet (Set.Iic terminal × Omega)
      (Subtype.instMeasurableSpace.prod (filtration terminal))
      {p | completedEnergy hUsual eta p.1 p.2 < level} :=
    measurableSet_Iio.preimage henergy.measurable
  exact StronglyMeasurable.ite hset
    (completedIntegrand_stronglyProgressive hUsual eta terminal)
    stronglyMeasurable_const

/-- Before terminal time, being below the energy level is equivalent to being
strictly before the canonical equality-level localizer. -/

Exact module and namespace context

Source mapping and supporting declarations
ASTIS implicit prerequisite · not a standalone source result

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

Why it is needed. 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.\]

Assumptions

  • A is adapted
  • every path \(t\mapsto A_t\) is continuous and nondecreasing
  • \(c\ge 0\)
Lean statement · canonicalEnergyLocalizer_le_iff

The background statement above and this exact formal declaration have distinct scopes. A mapped Lean result may be a specialization; compare its actual hypotheses instead of promoting the whole background theorem from this link.

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.

theorem canonicalEnergyLocalizer_le_iff
    (hUsual : SatisfiesUsualConditions filtration mu)
    (eta : LocalProgressiveL2Integrand filtration mu T)
    {level : ℝ} (hlevel : 0 ≤ level) (omega : Omega) (t : ℝ≥0) :
    canonicalEnergyLocalizer hUsual eta level omega ≤ t ↔
      T ≤ t ∨ level ≤ completedEnergy hUsual eta t omega

Exact module and namespace context

Lean statement · canonicalLocalizingTime_isStoppingTime

The background statement above and this exact formal declaration have distinct scopes. A mapped Lean result may be a specialization; compare its actual hypotheses instead of promoting the whole background theorem from this link.

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.

theorem canonicalLocalizingTime_isStoppingTime
    (hUsual : SatisfiesUsualConditions filtration mu)
    (eta : LocalProgressiveL2Integrand filtration mu T)
    (n : ℕ) :
    IsStoppingTime filtration
      (fun omega => (canonicalLocalizingTime hUsual eta n omega : WithTop ℝ≥0))

Exact module and namespace context

Mathematical proof

Continuity and monotonicity identify the first-passage event by a fixed-time level event. Adaptedness makes that fixed-time event measurable in the filtration, which is exactly the stopping-time requirement.

Lean proof · canonicalEnergyLocalizer_le_iff

Follow the actual proof calls for the mapped ASTIS result. The displayed mathematical background explains their use; compilation of this declaration does not certify a broader unmapped statement.

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.

theorem canonicalEnergyLocalizer_le_iff
    (hUsual : SatisfiesUsualConditions filtration mu)
    (eta : LocalProgressiveL2Integrand filtration mu T)
    {level : ℝ} (hlevel : 0 ≤ level) (omega : Omega) (t : ℝ≥0) :
    canonicalEnergyLocalizer hUsual eta level omega ≤ t ↔
      T ≤ t ∨ level ≤ completedEnergy hUsual eta t omega := by
  classical
  constructor
  · intro hstop
    by_cases hTt : T ≤ t
    · exact Or.inl hTt
    · right
      have hne : (energyLevelSet hUsual eta level omega).Nonempty := by
        by_contra hempty
        have hterminal : canonicalEnergyLocalizer hUsual eta level omega = T := by
          rw [canonicalEnergyLocalizer, dif_neg hempty]
        exact hTt (hterminal ▸ hstop)
      have hmem := canonicalEnergyLocalizer_mem hUsual eta level omega hne
      have hmono := monotone_completedEnergy hUsual eta omega hstop
      calc
        level = completedEnergy hUsual eta
            (canonicalEnergyLocalizer hUsual eta level omega) omega := hmem.2.symm
        _ ≤ completedEnergy hUsual eta t omega := hmono
  · rintro (hTt | hcross)
    · exact (canonicalEnergyLocalizer_le_terminal hUsual eta level omega).trans hTt
    · by_cases htT : t ≤ T
      · rcases exists_level_time_of_le hUsual eta hlevel htT hcross with
          ⟨s, hs, hvalue⟩
        have hmem : s ∈ energyLevelSet hUsual eta level omega :=
          ⟨⟨hs.1, hs.2.trans htT⟩, hvalue⟩
        exact (canonicalEnergyLocalizer_le_of_mem hUsual eta level omega hmem).trans hs.2
      · exact (canonicalEnergyLocalizer_le_terminal hUsual eta level omega).trans
          (lt_of_not_ge htT).le

/-- Canonical-localizer events are measurable at the observation time. -/

Exact module and namespace context

Lean proof · canonicalLocalizingTime_isStoppingTime

Follow the actual proof calls for the mapped ASTIS result. The displayed mathematical background explains their use; compilation of this declaration does not certify a broader unmapped statement.

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.

theorem canonicalLocalizingTime_isStoppingTime
    (hUsual : SatisfiesUsualConditions filtration mu)
    (eta : LocalProgressiveL2Integrand filtration mu T)
    (n : ℕ) :
    IsStoppingTime filtration
      (fun omega => (canonicalLocalizingTime hUsual eta n omega : WithTop ℝ≥0)) :=
  canonicalLocalizingTime_isChewiStoppingTime hUsual eta n

end CanonicalEnergyStoppingTime
end StochasticProcesses
end TechnicalLemmas
end AutoSamplingTheory

Exact module and namespace context

Source mapping and supporting declarations
ASTIS implicit prerequisite · not a standalone source result

Extension of the elementary Ito map by L2 completion

Why it is needed. The textbook calculation rule passes from elementary adapted processes to arbitrary progressive \(L^2\) 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}.\]

Assumptions

  • elementary adapted processes are dense in the progressive \(L^2\) domain
  • the elementary Ito isometry
  • \(L^2\)(Omega) is complete
Lean statement · itoIntegralTerminal

The background statement above and this exact formal declaration have distinct scopes. A mapped Lean result may be a specialization; compare its actual hypotheses instead of promoting the whole background theorem from this link.

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.

noncomputable def itoIntegralTerminal
    (eta : ProgressiveL2Integrand filtration mu T) (hT : 0 < T)
    (hB : IsBrownianMotionWithFiltration B filtration mu) : Lp ℝ 2 mu

Exact module and namespace context

Lean statement · itoIntegralTerminal_norm

The background statement above and this exact formal declaration have distinct scopes. A mapped Lean result may be a specialization; compare its actual hypotheses instead of promoting the whole background theorem from this link.

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.

theorem itoIntegralTerminal_norm
    (eta : ProgressiveL2Integrand filtration mu T) (hT : 0 < T)
    (hB : IsBrownianMotionWithFiltration B filtration mu) :
    ‖itoIntegralTerminal eta hT hB‖ = ‖integrandToLp eta hB‖

Exact module and namespace context

Mathematical proof

The elementary Itô isometry sends every Cauchy approximating sequence to a Cauchy sequence in the terminal \(L^2\) space. Completeness gives a limit, the isometry makes it independent of the approximation, and linearity passes through the limit.

Lean construction · itoIntegralTerminal

Follow the actual proof calls for the mapped ASTIS result. The displayed mathematical background explains their use; compilation of this declaration does not certify a broader unmapped statement.

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.

noncomputable def itoIntegralTerminal
    (eta : ProgressiveL2Integrand filtration mu T) (hT : 0 < T)
    (hB : IsBrownianMotionWithFiltration B filtration mu) : Lp ℝ 2 mu :=
  atTop.limUnder (terminalApprox eta hT hB)

Exact module and namespace context

Lean proof · itoIntegralTerminal_norm

Follow the actual proof calls for the mapped ASTIS result. The displayed mathematical background explains their use; compilation of this declaration does not certify a broader unmapped statement.

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.

theorem itoIntegralTerminal_norm
    (eta : ProgressiveL2Integrand filtration mu T) (hT : 0 < T)
    (hB : IsBrownianMotionWithFiltration B filtration mu) :
    ‖itoIntegralTerminal eta hT hB‖ = ‖integrandToLp eta hB‖ := by
  let _ : IsProbabilityMeasure mu := hB.isProbabilityMeasure
  have hterminal := (tendsto_terminalApprox eta hT hB).norm
  have hprocess := (tendsto_processApprox eta hT hB).norm
  have heq : (fun n ↦ ‖terminalApprox eta hT hB n‖) =
      fun n ↦ ‖processApprox eta hT hB n‖ := by
    funext n
    exact norm_terminalToLp_eq_processToLp
      (canonicalElementaryApprox eta hT n) hB
  rw [heq] at hterminal
  exact tendsto_nhds_unique hterminal hprocess

/-- Same-grid sum after refining both operands to their least common dyadic
level. -/

Exact module and namespace context

Source mapping and supporting declarations
ASTIS implicit prerequisite · not a standalone source result

Doob L2 maximal inequality for continuous martingales

Why it is needed. Controls the entire stochastic-integral path from terminal \(L^2\) 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.\]

Assumptions

  • M is an adapted square-integrable martingale
  • a continuous or right-continuous version on \([0,T]\)
Lean statement · doobL2_continuous

The background statement above and this exact formal declaration have distinct scopes. A mapped Lean result may be a specialization; compare its actual hypotheses instead of promoting the whole background theorem from this link.

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.

theorem doobL2_continuous
    [IsFiniteMeasure mu] {filtration : Filtration ℝ≥0 m}
    {M : ℝ≥0 → Omega → ℝ} (hM : Martingale M filtration mu)
    {T : ℝ≥0} (hT : 0 < T)
    (hcont : ∀ᵐ omega ∂mu, ContinuousOn (fun t => M t omega) (Icc 0 T))
    (a : ℝ) :
    ENNReal.ofReal a ^ (2 : ℝ) * mu (continuousExceedEvent M T a) ≤
      4 * eLpNorm (M T) 2 mu ^ (2 : ℝ)

Exact module and namespace context

Mathematical proof

Apply Doob's maximal inequality with exponent two to the absolute value of the martingale. The standard exponent-two constant is four, giving the displayed bound for the whole path from the terminal second moment.

Lean proof · doobL2_continuous

Follow the actual proof calls for the mapped ASTIS result. The displayed mathematical background explains their use; compilation of this declaration does not certify a broader unmapped statement.

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.

theorem doobL2_continuous
    [IsFiniteMeasure mu] {filtration : Filtration ℝ≥0 m}
    {M : ℝ≥0 → Omega → ℝ} (hM : Martingale M filtration mu)
    {T : ℝ≥0} (hT : 0 < T)
    (hcont : ∀ᵐ omega ∂mu, ContinuousOn (fun t => M t omega) (Icc 0 T))
    (a : ℝ) :
    ENNReal.ofReal a ^ (2 : ℝ) * mu (continuousExceedEvent M T a) ≤
      4 * eLpNorm (M T) 2 mu ^ (2 : ℝ) := by
  have hsubset : continuousExceedEvent M T a ≤ᵐ[mu]
      dyadicMaxEventAll M T a := by
    filter_upwards [hcont] with omega hcontinuous homega
    obtain ⟨t, ht, hexceed⟩ := homega
    exact continuousOn_mem_dyadicMaxEventAll hT hcontinuous ht hexceed
  calc
    ENNReal.ofReal a ^ (2 : ℝ) * mu (continuousExceedEvent M T a) ≤
        ENNReal.ofReal a ^ (2 : ℝ) * mu (dyadicMaxEventAll M T a) :=
      mul_le_mul_of_nonneg_left (MeasureTheory.measure_mono_ae hsubset) bot_le
    _ ≤ 4 * eLpNorm (M T) 2 mu ^ (2 : ℝ) :=
      pow_mul_measure_dyadicMaxEventAll_le hM T a

end ContinuousDoobL2
end StochasticProcesses
end TechnicalLemmas
end AutoSamplingTheory

Exact module and namespace context

Source mapping and supporting declarations
ASTIS implicit prerequisite · not a standalone source result

Borel-Cantelli construction of a uniformly convergent continuous version

Why it is needed. A fixed-time \(L^2\) 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.}\]

Assumptions

  • continuous approximating processes
  • summable maximal-deviation probabilities
Lean statement · itoIntegralProcess_continuous_ae

The background statement above and this exact formal declaration have distinct scopes. A mapped Lean result may be a specialization; compare its actual hypotheses instead of promoting the whole background theorem from this link.

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.

theorem itoIntegralProcess_continuous_ae
    (eta : ProgressiveL2Integrand filtration mu T) (hT : 0 < T)
    (hB : IsBrownianMotionWithFiltration B filtration mu)
    (hUsual : SatisfiesUsualConditions filtration mu) :
    ∀ᵐ omega ∂mu,
      ContinuousOn (fun t => itoIntegralProcess eta hT hB hUsual t omega)
        (Icc (0 : ℝ≥0) T)

Exact module and namespace context

Mathematical proof

Summability of the maximal-deviation events implies by the first Borel-Cantelli lemma that only finitely many occur almost surely. The remaining tail is uniformly Cauchy, and the uniform limit of continuous paths is continuous.

Lean proof · itoIntegralProcess_continuous_ae

Follow the actual proof calls for the mapped ASTIS result. The displayed mathematical background explains their use; compilation of this declaration does not certify a broader unmapped statement.

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.

theorem itoIntegralProcess_continuous_ae
    (eta : ProgressiveL2Integrand filtration mu T) (hT : 0 < T)
    (hB : IsBrownianMotionWithFiltration B filtration mu)
    (hUsual : SatisfiesUsualConditions filtration mu) :
    ∀ᵐ omega ∂mu,
      ContinuousOn (fun t => itoIntegralProcess eta hT hB hUsual t omega)
        (Icc (0 : ℝ≥0) T) :=
  Filter.Eventually.of_forall (itoIntegralProcess_continuousOn eta hT hB hUsual)

Exact module and namespace context

Source mapping and supporting declarations
ASTIS implicit prerequisite · not a standalone source result

Energy stopping converts local square integrability into global L2

Why it is needed. 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.\]

Assumptions

  • pathwise finite square energy almost surely
  • continuous nondecreasing accumulated energy
  • the exceptional nonintegrable paths are completed or stopped immediately
Lean statement · integral_energyStoppedIntegrand_sq_le

The background statement above and this exact formal declaration have distinct scopes. A mapped Lean result may be a specialization; compare its actual hypotheses instead of promoting the whole background theorem from this link.

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.

theorem integral_energyStoppedIntegrand_sq_le
    (hUsual : SatisfiesUsualConditions filtration mu)
    (eta : LocalProgressiveL2Integrand filtration mu T)
    {level : ℝ} (hlevel : 0 ≤ level) (omega : Omega) :
    ∫ s, (energyStoppedIntegrand hUsual eta level s omega) ^ 2
        ∂(TimeMeasure.upTo T) ≤ level

Exact module and namespace context

Lean statement · stoppedProgressiveL2

The background statement above and this exact formal declaration have distinct scopes. A mapped Lean result may be a specialization; compare its actual hypotheses instead of promoting the whole background theorem from this link.

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.

noncomputable def stoppedProgressiveL2
    [IsProbabilityMeasure mu]
    (hUsual : SatisfiesUsualConditions filtration mu)
    (eta : LocalProgressiveL2Integrand filtration mu T)
    {level : ℝ} (hlevel : 0 ≤ level) :
    ProgressiveL2Integrand filtration mu T

Exact module and namespace context

Mathematical proof

Before the first hit, accumulated energy stays below the threshold; at the hit, continuity prevents overshoot. The resulting pathwise bound becomes a global \(L^2\) bound after integration under the probability measure.

Lean proof · integral_energyStoppedIntegrand_sq_le

Follow the actual proof calls for the mapped ASTIS result. The displayed mathematical background explains their use; compilation of this declaration does not certify a broader unmapped statement.

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.

theorem integral_energyStoppedIntegrand_sq_le
    (hUsual : SatisfiesUsualConditions filtration mu)
    (eta : LocalProgressiveL2Integrand filtration mu T)
    {level : ℝ} (hlevel : 0 ≤ level) (omega : Omega) :
    ∫ s, (energyStoppedIntegrand hUsual eta level s omega) ^ 2
        ∂(TimeMeasure.upTo T) ≤ level := by
  rw [integral_energyStoppedIntegrand_sq hUsual eta hlevel omega]
  exact completedEnergy_at_canonical_le hUsual eta hlevel omega

end EnergyStoppedIntegrand
end StochasticProcesses
end TechnicalLemmas
end AutoSamplingTheory

Exact module and namespace context

Lean construction · stoppedProgressiveL2

Follow the actual proof calls for the mapped ASTIS result. The displayed mathematical background explains their use; compilation of this declaration does not certify a broader unmapped statement.

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.

noncomputable def stoppedProgressiveL2
    [IsProbabilityMeasure mu]
    (hUsual : SatisfiesUsualConditions filtration mu)
    (eta : LocalProgressiveL2Integrand filtration mu T)
    {level : ℝ} (hlevel : 0 ≤ level) :
    ProgressiveL2Integrand filtration mu T where
  process := energyStoppedIntegrand hUsual eta level
  progressive := energyStoppedIntegrand_stronglyProgressive hUsual eta level
  memLp := (memLp_two_iff_integrable_sq
      (processFunction_aestronglyMeasurable hUsual eta level)).2
    (processFunction_sq_integrable hUsual eta hlevel)

Exact module and namespace context

Source mapping and supporting declarations
ASTIS implicit prerequisite · not a standalone source result

Consistency of stopped Ito integrals

Why it is needed. Proposition 1.1.16 must patch the \(L^2\) 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.}\]

Assumptions

  • \(\tau_m\le\tau_n\)
  • both stopped integrands are in global progressive \(L^2\)
  • the Ito map is unique in \(L^2\) and compatible with deterministic-time restriction
Lean statement · itoIntegralProcess_congr_toLp_pathwise_ae

The background statement above and this exact formal declaration have distinct scopes. A mapped Lean result may be a specialization; compare its actual hypotheses instead of promoting the whole background theorem from this link.

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.

theorem itoIntegralProcess_congr_toLp_pathwise_ae [IsFiniteMeasure mu]
    (eta xi : ProgressiveL2Integrand filtration mu T)
    (hT : 0 < T)
    (hB : IsBrownianMotionWithFiltration B filtration mu)
    (hUsual : SatisfiesUsualConditions filtration mu)
    (hEq : eta.toLp = xi.toLp) :
    ∀ᵐ omega ∂mu, ∀ t ∈ Icc (0 : ℝ≥0) T,
      itoIntegralProcess eta hT hB hUsual t omega =
        itoIntegralProcess xi hT hB hUsual t omega

Exact module and namespace context

Lean statement · itoIntegralProcess_stop_eq_stoppedProcess_pathwise_ae

The background statement above and this exact formal declaration have distinct scopes. A mapped Lean result may be a specialization; compare its actual hypotheses instead of promoting the whole background theorem from this link.

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.

theorem itoIntegralProcess_stop_eq_stoppedProcess_pathwise_ae
    [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 ∂mu, ∀ t ∈ Icc (0 : ℝ≥0) T,
      itoIntegralProcess
          (stop eta (fun omega => (tau omega : WithTop ℝ≥0)) htau)
          hT hB hUsual t omega =
        stoppedProcess (itoIntegralProcess eta hT hB hUsual)
          (fun omega => (tau omega : WithTop ℝ≥0)) t omega

Exact module and namespace context

Lean statement · globalStoppedItoProcess_overlap_pathwise_ae

The background statement above and this exact formal declaration have distinct scopes. A mapped Lean result may be a specialization; compare its actual hypotheses instead of promoting the whole background theorem from this link.

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.

theorem globalStoppedItoProcess_overlap_pathwise_ae
    [IsProbabilityMeasure mu]
    (hUsual : SatisfiesUsualConditions filtration mu)
    (eta : GlobalLocalProgressiveL2Integrand filtration mu)
    (hB : IsBrownianMotionWithFiltration B filtration mu)
    {k ell : ℕ} (hkell : k ≤ ell) :
    ∀ᵐ omega ∂mu, ∀ t ∈ Icc (0 : ℝ≥0) (dyadicHorizon k),
      globalStoppedItoProcess hUsual eta hB k t omega =
        stoppedProcess (globalStoppedItoProcess hUsual eta hB ell)
          (fun w =>
            (dyadicGlobalLocalizingTime hUsual eta k w : WithTop ℝ≥0))
          t omega

Exact module and namespace context

Mathematical proof

Stop the larger localized integrand once more at the smaller localizer. The two stopped integrands agree in product-space \(L^2\), and the Itô isometry transfers that equality to the corresponding stochastic integrals.

Lean proof · itoIntegralProcess_congr_toLp_pathwise_ae

Follow the actual proof calls for the mapped ASTIS result. The displayed mathematical background explains their use; compilation of this declaration does not certify a broader unmapped statement.

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.

theorem itoIntegralProcess_congr_toLp_pathwise_ae [IsFiniteMeasure mu]
    (eta xi : ProgressiveL2Integrand filtration mu T)
    (hT : 0 < T)
    (hB : IsBrownianMotionWithFiltration B filtration mu)
    (hUsual : SatisfiesUsualConditions filtration mu)
    (hEq : eta.toLp = xi.toLp) :
    ∀ᵐ omega ∂mu, ∀ t ∈ Icc (0 : ℝ≥0) T,
      itoIntegralProcess eta hT hB hUsual t omega =
        itoIntegralProcess xi hT hB hUsual t omega := by
  let J : ℝ≥0 → Omega → ℝ := itoIntegralProcess eta hT hB hUsual
  have hJadapted : StronglyAdapted filtration J := by
    simpa only [J] using
      itoIntegralProcess_stronglyAdapted eta hT hB hUsual
  have hJcontinuous : ∀ᵐ omega ∂mu,
      ContinuousOn (fun t => J t omega) (Icc (0 : ℝ≥0) T) := by
    filter_upwards [] with omega
    simpa only [J] using
      itoIntegralProcess_continuousOn eta hT hB hUsual omega
  have hJterminal : ∀ t ≤ T,
      J t =ᵐ[mu] fun omega =>
        itoIntegralTerminal (xi.restrictAt t) hT hB omega := by
    intro t ht
    have heta := itoIntegralProcess_at_eq_terminal eta hT hB hUsual ht
    have hrestrict : (eta.restrictAt t).toLp = (xi.restrictAt t).toLp :=
      restrictAt_toLp_eq_of_toLp_eq eta xi hEq t
    have hterminal :
        itoIntegralTerminal (eta.restrictAt t) hT hB =
          itoIntegralTerminal (xi.restrictAt t) hT hB := by
      apply itoIntegralTerminal_congr_toLp
      simpa only [integrandToLp] using hrestrict
    rw [hterminal] at heta
    simpa only [J] using heta
  simpa only [J] using
    itoIntegralProcess_unique xi hT hB hUsual
      J hJadapted hJcontinuous hJterminal

end ItoIntegralProcessCongruence
end StochasticProcesses
end TechnicalLemmas
end AutoSamplingTheory

Exact module and namespace context

Lean proof · itoIntegralProcess_stop_eq_stoppedProcess_pathwise_ae

Follow the actual proof calls for the mapped ASTIS result. The displayed mathematical background explains their use; compilation of this declaration does not certify a broader unmapped statement.

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.

theorem itoIntegralProcess_stop_eq_stoppedProcess_pathwise_ae
    [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 ∂mu, ∀ t ∈ Icc (0 : ℝ≥0) T,
      itoIntegralProcess
          (stop eta (fun omega => (tau omega : WithTop ℝ≥0)) htau)
          hT hB hUsual t omega =
        stoppedProcess (itoIntegralProcess eta hT hB hUsual)
          (fun omega => (tau omega : WithTop ℝ≥0)) t omega := by
  let stoppedEta := stop eta (fun omega => (tau omega : WithTop ℝ≥0)) htau
  let J : ℝ≥0 → Omega → ℝ :=
    stoppedProcess (itoIntegralProcess eta hT hB hUsual)
      (fun omega => (tau omega : WithTop ℝ≥0))
  have hBaseAdapted : StronglyAdapted filtration
      (itoIntegralProcess eta hT hB hUsual) :=
    itoIntegralProcess_stronglyAdapted eta hT hB hUsual
  have hBaseContinuous : ∀ omega,
      Continuous (fun t => itoIntegralProcess eta hT hB hUsual t omega) :=
    itoIntegralProcess_continuous eta hT hB hUsual
  have hJadapted : StronglyAdapted filtration J := by
    simpa only [J] using hBaseAdapted.stoppedProcess hBaseContinuous htau
  have hJcontinuous : ∀ᵐ omega ∂mu,
      ContinuousOn (fun t => J t omega) (Icc (0 : ℝ≥0) T) := by
    filter_upwards [] with omega
    have hmin : Continuous (fun t : ℝ≥0 => min t (tau omega)) :=
      continuous_id.min continuous_const
    have hcomp := (hBaseContinuous omega).comp hmin
    apply hcomp.continuousOn.congr
    intro t _
    change
      J t omega =
        itoIntegralProcess eta hT hB hUsual (min t (tau omega)) omega
    simpa only [J] using
      stoppedProcess_coe_apply
        (itoIntegralProcess eta hT hB hUsual) tau t omega
  have hJterminal : ∀ t ≤ T,
      J t =ᵐ[mu] fun omega =>
        itoIntegralTerminal (stoppedEta.restrictAt t) hT hB omega := by
    intro t ht
    have hstop :=
      itoIntegralProcess_stop_eq_stoppedProcess_ae
        eta hT tau htau htauT hB hUsual ht
    have hterminal :=
      itoIntegralProcess_at_eq_terminal stoppedEta hT hB hUsual ht
    exact hstop.symm.trans hterminal
  have huniq :=
    itoIntegralProcess_unique stoppedEta hT hB hUsual
      J hJadapted hJcontinuous hJterminal
  filter_upwards [huniq] with omega homega
  intro t ht
  simpa only [stoppedEta, J] using (homega t ht).symm

end RandomStoppingProcessConsistency
end StochasticProcesses
end TechnicalLemmas
end AutoSamplingTheory

Exact module and namespace context

Lean proof · globalStoppedItoProcess_overlap_pathwise_ae

Follow the actual proof calls for the mapped ASTIS result. The displayed mathematical background explains their use; compilation of this declaration does not certify a broader unmapped statement.

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.

theorem globalStoppedItoProcess_overlap_pathwise_ae
    [IsProbabilityMeasure mu]
    (hUsual : SatisfiesUsualConditions filtration mu)
    (eta : GlobalLocalProgressiveL2Integrand filtration mu)
    (hB : IsBrownianMotionWithFiltration B filtration mu)
    {k ell : ℕ} (hkell : k ≤ ell) :
    ∀ᵐ omega ∂mu, ∀ t ∈ Icc (0 : ℝ≥0) (dyadicHorizon k),
      globalStoppedItoProcess hUsual eta hB k t omega =
        stoppedProcess (globalStoppedItoProcess hUsual eta hB ell)
          (fun w =>
            (dyadicGlobalLocalizingTime hUsual eta k w : WithTop ℝ≥0))
          t omega := by
  let low := globalStoppedProgressiveL2 hUsual eta k
  let high := globalStoppedProgressiveL2 hUsual eta ell
  let tau : Omega → ℝ≥0 := dyadicGlobalLocalizingTime hUsual eta k
  let stoppedHigh := stop high
    (fun w => (tau w : WithTop ℝ≥0))
    (dyadicGlobalLocalizingTime_isChewiStoppingTime hUsual eta k)
  let extendedLow := extendByZero low
    (DyadicHorizonExtension.dyadicHorizon_mono hkell)
  have htauHigh : ∀ omega, tau omega ≤ dyadicHorizon ell := by
    intro omega
    exact (dyadicGlobalLocalizingTime_le_horizon hUsual eta k omega).trans
      (DyadicHorizonExtension.dyadicHorizon_mono hkell)
  have hLp : stoppedHigh.toLp = extendedLow.toLp := by
    simpa only [low, high, tau, stoppedHigh, extendedLow] using
      stop_globalStopped_toLp_eq_extendByZero hUsual eta hkell
  have hcongr := itoIntegralProcess_congr_toLp_pathwise_ae
    stoppedHigh extendedLow (dyadicHorizon_pos ell) hB hUsual hLp
  have hstop := itoIntegralProcess_stop_eq_stoppedProcess_pathwise_ae
    high (dyadicHorizon_pos ell) tau
    (dyadicGlobalLocalizingTime_isChewiStoppingTime hUsual eta k)
    htauHigh hB hUsual
  have hhorizon := itoIntegralProcess_extendByZero_pathwise_ae
    hkell low hB hUsual
  filter_upwards [hcongr, hstop, hhorizon] with omega hcongrOmega hstopOmega hhorizonOmega
  intro t ht
  have htHigh : t ∈ Icc (0 : ℝ≥0) (dyadicHorizon ell) :=
    ⟨ht.1, ht.2.trans (DyadicHorizonExtension.dyadicHorizon_mono hkell)⟩
  have hc := hcongrOmega t htHigh
  have hs := hstopOmega t htHigh
  have hh := hhorizonOmega t ht
  change
    itoIntegralProcess low (dyadicHorizon_pos k) hB hUsual t omega =
      stoppedProcess
        (itoIntegralProcess high (dyadicHorizon_pos ell) hB hUsual)
        (fun w => (tau w : WithTop ℝ≥0)) t omega
  exact hh.symm.trans (hc.symm.trans hs)

/-- Before the lower localizer has fired, all later localized martingales agree
with the lower one.  This is the eventual pathwise stability used in global
gluing. -/

Exact module and namespace context

Source mapping and supporting declarations