1 Introduction↩︎

Stochastic calculus sits oddly in the formalization landscape. Its prerequisites (measure-theoretic probability, conditional expectation, \(L^p\) spaces, Gaussian measures) are by now well represented in the major proof-assistant libraries. Its consumers (mathematical finance, stochastic control, SPDEs) are fields with strong correctness cultures that regularly cite formal methods as an aspiration. Yet the calculus itself has remained unformalized. Martingales in discrete and continuous time were formalized in Isabelle/HOL by Keskin [1]; the central limit theorem was machine-checked a decade ago [2]; and in late 2025 Degenne, Ledvinka, Marion, and Pfaffelhuber completed the first formal construction of Brownian motion itself, in Lean 4 [3], [4]. Their paper’s outlook section is explicit about what remained: even the martingale property of Brownian motion, let alone stochastic integration, Itô’s formula, or any of their consequences, was left to future work. As of this writing we are not aware of any machine-checked proof of Itô’s formula, or any machine-checked construction of the Itô integral, in any proof assistant.

This paper describes such a development. It is the stochastic-calculus core of a larger formalized mathematical-finance library announced in [5]; where the announcement surveys breadth, the present paper is a detailed treatment of its stochastic-calculus core, for readers who want to know exactly what was proved, under which hypotheses, and by which proof architecture.

Contributions↩︎

All results are stated over a probability space \((\Omega,\mathcal{F},\mu)\) carrying a process \(B : \mathbb{R}_{\ge 0} \to \Omega \to \mathbb{R}\) satisfying the BrownianMotion package’s pre-Brownian interface (IsPreBrownian): centered Gaussian increments with variance \(t-s\), measurable coordinates, and, where stated, continuous paths. \(\mathcal{F}_t\) denotes the natural filtration (natFiltration).

1. The Itô integral as an isometry (Section 5). The integrand space is the \(L^2\) space of a product measure on \((0,T]\times\Omega\) trimmed to the predictable \(\sigma\)-algebra generated by rectangles \((s,t]\times A\), \(A \in \mathcal{F}_s\). Simple adapted processes are dense; the elementary integral is an isometry on them; the Itô integral \(\mathcal{I}_T =\) itoIntegralCLMT is its unique continuous-linear isometric extension.

2. The integral as a process (Section 6). For each \(t \le T\) a continuous linear map realizes \((\varphi \bullet B)_t = \int_0^t \varphi\,dB\), and the development’s load-bearing identity states \((\varphi \bullet B)_t = \mathbb{E}[\,\mathcal{I}_T(\varphi) \mid \mathcal{F}_t\,]\) as an identity of \(L^2\) elements. Adaptedness, the martingale property, the contraction bound, the terminal isometry, the time-indexed Itô isometry \(\mathbb{E}[(\varphi\bullet B)_t^2] = \int_0^t \mathbb{E}[\varphi_s^2]\,ds\), and \(L^2\)-continuity in \(t\) are corollaries.

3. Itô’s formula (Section 7). For \(f \in C^3(\mathbb{R})\) with \(|f'| \le C_1\), \(|f''| \le C_2\), \(|f'''| \le C_3\), \[f(B_T) - f(B_0) \;=\; \mathcal{I}_T\big(f'(B)\big) \;+\; \tfrac12 \int_0^T f''(B_s)\,ds \qquad \mu\text{-a.e.},\] and the time-dependent form \(f(T, B_T) - f(0, B_0) = \mathcal{I}_T(f_x(\cdot, B)) + \int_0^T (f_t + \tfrac12 f_{xx})(s, B_s)\,ds\) under a \(C^{1,2}\)-with-bounds hypothesis package.

4. Supporting theory. Quadratic variation of Brownian motion in \(L^1\) and \(L^2\) forms under hypotheses strictly weaker than the textbook statement; the expectation-level Itô identity \(\mathbb{E}[f(B_t)] = f(0) + \tfrac12 \int_0^t \mathbb{E}[f''(B_s)]\,ds\); and the closed-form keystone \(\mathcal{I}_T(B) = \tfrac12(B_T^2 - B_0^2 - T)\), the formal counterpart of the classical \(\int_0^T B\,dB\).

Section 8 is a frank accounting of the boundary: which parts of the classical theory are present, which are deliberately absent, and why the title says “a” calculus rather than “the” calculus. We recommend a reader skeptical of the headline begin there.

2 Setting and verification discipline↩︎

2.1 Foundations consumed↩︎

The development is built in Lean 4 [6] over Mathlib [7] and the BrownianMotion package [3], [4], whose construction of Brownian motion (via Kolmogorov–Chentsov, Gaussian measures on Banach spaces, and a Carathéodory/Kolmogorov extension layer) this work consumes rather than reproves; the artifact pins the package at commit eaa4391. Time is indexed by \(\mathbb{R}_{\ge 0}\) (Lean’s NNReal); Lebesgue measure on time enters through a dedicated timeMeasure restricted to \((0,T]\).

2.2 Auditability and reproducibility↩︎

Verification discipline follows the library’s standing contract [5]. No sorry or admit occurs anywhere in the development. A build-enforced axiom audit pins the axioms of every headline constant to Mathlib’s classical defaults (propext, Classical.choice, Quot.sound), and a continuous-integration gate fails the build if a new proof introduces any other axiom. A hash ledger records the exact source inputs each verified statement depends on, so that a result cannot become stale without detection when an upstream dependency changes. The statements displayed below are transcriptions of the Lean statements; where a hypothesis package is abbreviated in prose, the displayed Lean name is the authority, and Appendix 11 maps every displayed result to its module and declaration name.

2.3 Scale↩︎

The Itô and quadratic-variation tower is roughly \(7{,}200\) lines of Lean across \(22\) modules, comprising on the order of \(220\) theorems and lemmas and \(40\) definitions, all downstream of Mathlib and the BrownianMotion package and upstream of the parent library’s pricing layers. Table 1 groups the modules by role. These figures are reported from the working tree of June 2026 and are refreshed against a clean build before submission.

3 The classical theory↩︎

We recall the objects the formalization reproduces, in the form they take in the standard references [8], [9], so that the theorems of Sections 5 to 7 can be read against them.

Let \((B_t)_{t \ge 0}\) be a Brownian motion on \((\Omega,\mathcal{F},\mu)\) with natural filtration \((\mathcal{F}_t)\). For a simple adapted process \(\varphi_s = \sum_k \xi_k \mathbf{1}_{(t_k, t_{k+1}]}(s)\), with \(\xi_k\) bounded and \(\mathcal{F}_{t_k}\)-measurable, the Itô integral is the finite sum \(\int_0^T \varphi\,dB = \sum_k \xi_k (B_{t_{k+1}} - B_{t_k})\). The defining computation is the Itô isometry: because each \(\xi_k\) is independent of the forward increment \(B_{t_{k+1}} - B_{t_k}\), and increments over disjoint intervals are independent, \[\mathbb{E}\Big[\Big(\textstyle\sum_k \xi_k (B_{t_{k+1}} - B_{t_k})\Big)^2\Big] = \sum_k \mathbb{E}[\xi_k^2]\,(t_{k+1} - t_k) = \mathbb{E}\!\int_0^T \varphi_s^2 \, ds,\] the cross terms vanishing by adaptedness and the diagonal contributing \(\mathbb{E}[\xi_k^2]\,(t_{k+1}-t_k)\) because \(\mathbb{E}[(B_{t_{k+1}}-B_{t_k})^2 \mid \mathcal{F}_{t_k}] = t_{k+1}-t_k\). The map \(\varphi \mapsto \int_0^T \varphi\,dB\) is thus an isometry from the simple processes, carrying the \(L^2(\lambda \otimes \mu)\) norm on the predictable side, into \(L^2(\mu)\); as the simple processes are dense in the predictable \(L^2\) space, it extends to a linear isometry on all of it. That construction is Section 5.

As a function of its upper limit, \(t \mapsto \int_0^t \varphi\,dB\) is a continuous \(L^2\) martingale, with \(\mathbb{E}\big[(\int_0^t \varphi\,dB)^2\big] = \mathbb{E}\int_0^t \varphi_s^2\,ds\) at every \(t\); that is Section 6. The quadratic variation of Brownian motion is \([B]_t = t\): along partitions of \([0,t]\) with mesh tending to zero, \(\sum_k (B_{t_{k+1}} - B_{t_k})^2 \to t\), in \(L^2\) for the uniform partition. Itô’s formula states that for \(f \in C^2\), \[f(B_t) - f(B_0) = \int_0^t f'(B_s)\,dB_s + \tfrac12 \int_0^t f''(B_s)\,ds,\] the second-order term surviving precisely because \((\mathrm dB)^2 = \mathrm dt\) in the mean-square sense made exact by \([B]_t = t\). Section 7 formalizes this for \(f\) with bounded derivatives, and its time-dependent extension.

4 Design of the formalization↩︎

Three representation choices shape the development and are worth stating before the theorems that rest on them.

4.0.0.1 The integrand, after the upstream package.

The simple integrands are not re-encoded here. The BrownianMotion package provides SimpleProcess, an integrand built as a finite linear combination (Finsupp.linearCombination) of indicators of elementary predictable sets, together with the lemma identifying the \(\sigma\)-algebra those indicators generate with the predictable one. This work consumes both: the elementary Itô integral is defined on SimpleProcess, and the density argument of Section 5 rests on that generation lemma. What is built here is the layer above, namely the rectangle \(\pi\)-system, the orthogonal-complement density, and the isometric extension.

4.0.0.2 Time as NNReal.

The time axis is \(\mathbb{R}_{\ge 0}\), not \(\mathbb{R}\) with a positivity side-condition. Increments \(B_t - B_s\) then carry \(s \le t\) in their type-level data rather than as a hypothesis to discharge, and the bounded horizon enters uniformly through a single finite measure (timeMeasureT, of total mass \(T\)) rather than through interval hypotheses threaded across lemmas.

4.0.0.3 One construction pattern, used twice.

The integral and the integral-as-a-process are built by the same idiom: a norm-preserving linear map on a dense subspace, then its unique continuous-linear extension (Mathlib’s extendOfNorm). For the integral the dense subspace is the simple processes inside \(H_T\); for the process it is the same simple processes, the extension now landing in \(L^2(\mu)\) at each \(t\). Because the process is an extension of the simple-layer map, every identity proved on simple processes (the martingale property, the per-time isometry) transfers to all of \(H_T\) by continuity and density. That mechanism is what makes Section 6 a sequence of short arguments.

5 The \(L^2\) Itô integral↩︎

5.1 The integrand space↩︎

Fix \(T \in \mathbb{R}_{\ge 0}\) and write \(\lambda_T\) for Lebesgue measure on time restricted to \((0,T]\) (timeMeasureT). On \((0,T] \times \Omega\) the predictable rectangles \[\mathcal{R} \;=\; \big\{ (s,t] \times A \;:\; s \le t,\; A \in \mathcal{F}_s \big\} \;\cup\; \big\{ \{0\}\times A_0 : A_0 \in \mathcal{F}_0 \big\}\] form a \(\pi\)-system, encoded as predictableRect (Listing [lst:rect]); the \(\sigma\)-algebra they generate is the (restricted) predictable \(\sigma\)-algebra, identified by generateFrompredictableRect. The integrand space is \[H_T \;=\; L^2\big((0,T]\times\Omega,\; \mathcal{P}_T,\; (\lambda_T \otimes \mu)\!\restriction_{\mathcal{P}_T}\big),\] realized in Lean as the \(L^2\) space of the product measure trimmed to the predictable \(\sigma\)-algebra (trimMeasureT); the Itô integral is then a continuous linear map out of this space (Listing [lst:clm]).

:
:=
piece
F₀
a

:
μ

5.1.0.1 Why a trimmed measure.

The one definitional choice that pays off repeatedly is to make \(H_T\) the \(L^2\) space of a measure that has already been restricted to the predictable \(\sigma\)-algebra, rather than carrying a sub-\(\sigma\)-algebra measurability side-condition alongside an ambient \(L^2\) space. The consequence is that predictability is a property of membership in \(H_T\), not a separate hypothesis to be threaded through every limit: a Cauchy sequence in \(H_T\) has its limit in \(H_T\), so when Itô’s formula realizes \(s \mapsto f'(B_s)\) as an \(L^2\) limit of step processes (Section 7), the limit’s predictability is free. The cost is a one-time investment in the trimmed-measure \(L^2\) API; the saving recurs at every density and convergence argument downstream.

5.2 Simple processes, density, isometry↩︎

A simple adapted process is a finite combination of indicator rectangles \(\xi_s \cdot \mathbf{1}_{(s,t]}\) with \(\xi_s\) bounded and \(\mathcal{F}_s\)-measurable; TBoundedSP packages the class and simpleProcessL2T sends it into \(H_T\). The elementary integral maps such a process to \(\sum \xi_s\,(B_t - B_s)\) (itoAssemblyT); independence and the Gaussian increment moments give the elementary Itô isometry (assemblyisometryT), \(\big\|\text{(elementary integral of } V)\big\|_{L^2(\mu)} = \|V\|_{H_T}\).

Density of the simple processes in \(H_T\) (simpleAssemblyTdenseRange) is the technical core of the construction, and the one part of it not inherited from the upstream package. It is proved by the orthogonal-complement method. The basic predictable rectangles \((a,b] \times F\) with \(F \in \mathcal{F}_a\) form a \(\pi\)-system (isPiSystempredictableRect) that generates the predictable \(\sigma\)-algebra; the generation lemma itself (ElementaryPredictableSet.generateFromeqpredictable) is consumed from BrownianMotion. Take \(\psi \in H_T\) orthogonal to every elementary integral. Testing against the indicator of a rectangle \((a,b] \times F\) shows that the integral of \(\psi\) over that rectangle vanishes; the collection of measurable sets on which \(\int \psi = 0\) is a \(\lambda\)-system containing the rectangle \(\pi\)-system, so Dynkin’s \(\pi\)–\(\lambda\) theorem extends the vanishing to the entire predictable \(\sigma\)-algebra (setIntegraleqzerooforthogonalpred), forcing \(\psi = 0\) a.e. The Itô integral \(\mathcal{I}_T =\) itoIntegralCLMT is then the unique isometric continuous-linear extension of the elementary integral, via Mathlib’s LinearIsometry/extendOfNorm idiom for extending a norm-preserving map off a dense subspace.

5.3 The keystone example↩︎

A Riemann-sum bridge (riemannφ, stepφ, with cell-collapse lemmas) connects \(\mathcal{I}_T\) applied to time-discretized integrands with classical partial sums. Its first consumer is the closed form \[\mathcal{I}_T(B) \;=\; \tfrac12\,\big(B_T^2 - B_0^2 - T\big),\] the machine-checked \(\int_0^T B\,dB\). The Itô correction \(-T/2\) emerges as follows: the summation-by-parts identity discretesquaringidentity writes \[\sum_k B_{s_k}(B_{s_{k+1}} - B_{s_k}) = \tfrac12\Big(B_T^2 - B_0^2 - \textstyle\sum_k (B_{s_{k+1}} - B_{s_k})^2\Big),\] whose left side is the discretized \(\int_0^T B\,dB\), converging in \(L^2\) to \(\mathcal{I}_T(B)\), while the squared-increment sum converges in \(L^2\) to \(T\) (Section 7); what is left is \(\tfrac12(B_T^2 - B_0^2 - T)\). We display it because it is the smallest statement in which the calculus is visibly non-classical, because it later anchors the remainder analysis of Itô’s formula, and because, as Section 8 notes, it is an example the bounded-derivative Itô formula cannot reach on its own, which is exactly why it is proved here by hand.

5.4 Design note: two isometries↩︎

The library separately maintains a Wiener-integral isometry for deterministic integrands. The two are deliberately distinct: the Wiener integral needs no filtration and serves the Gaussian-process and distributional layers, while \(\mathcal{I}_T\) is the adapted object that the martingale theory of Section 6 requires. Collapsing the two would shorten the code and damage the mathematics; the duplication is the design, and it is recorded as such in the dependency blueprint so that a future reader does not “simplify” it away.

6 The integral as a process↩︎

6.1 The simple layer↩︎

For a simple process \(V\) and \(t \le T\), the partially-summed elementary integral \((V \bullet B)_t\) is adapted (itoSimpleProcessadaptedAt) and a martingale (itoSimpleProcessisMartingale). The martingale step reduces to the conditional vanishing of adapted-weighted future increments (Listing [lst:incr]), proved in condExpadaptedmulincrement by upgrading the unconditional statement \(\mathbb{E}[\xi(B_{t_1} - B_{t_0})] = 0\) to its conditional form \(\mathbb{E}[\xi(B_{t_1} - B_{t_0}) \mid \mathcal{F}_u] = 0\) for \(u \le t_0\). By the characterizing property of conditional expectation (aeeqcondExpofforallsetIntegraleq), it suffices that \(\int_A \xi(B_{t_1} - B_{t_0})\,d\mu = 0\) for every \(A \in \mathcal{F}_u\); and \(\xi \mathbf{1}_A\) is again bounded and \(\mathcal{F}_{t_0}\)-adapted, so the increment \(B_{t_1} - B_{t_0}\), independent of \(\mathcal{F}_{t_0}\) with mean zero, makes the integral factor as \(\mathbb{E}[\xi \mathbf{1}_A]\,\mathbb{E}[B_{t_1} - B_{t_0}] = 0\). The simple layer also carries the per-time isometry \(\mathbb{E}[(V\bullet B)_t^2] = \int_0^t \mathbb{E}[V_s^2]\,ds\) (itoSimpleProcessisometrytime) and \(L^2\)-continuity in \(t\) (itoSimpleProcessLpl2continuous); the next subsection lifts all three to general integrands at once.

t))
ℝ
:
0

6.2 The key identity↩︎

For general \(\varphi \in H_T\) the process is defined by a continuous linear map (itoProcessCLM, obtained by extending the simple layer through itoProcessLM.extendOfNorm), and the development’s central structural fact is Theorem 1 (Listing [lst:key]).

u))
:
φ
t)
μ)

The proof is two lines of mathematics: both sides are continuous linear in \(\varphi\); on the dense simple subspace they agree, because there the identity is the simple layer’s martingale property; conclude by the equalizer property of dense ranges (DenseRange.equalizer). Everything else about the process is a corollary of Theorem 1 plus standard properties of conditional expectation:

• adaptedness, since a condExpL2 projection lands in the \(\mathcal{F}_t\)-measurable subspace;

• the martingale property (itoIntegralProcessGenisMartingale), by the conditional-expectation tower;

• the contraction bound \(\|(\varphi\bullet B)_t\|_{L^2} \le \|\varphi\|_{H_T}\) (itoProcessCLMnormle), since conditional expectation is a contraction;

• the terminal isometry at \(t = T\) (itoProcessCLMnormterminal);

• \(L^2\)-continuity of \(t \mapsto (\varphi\bullet B)_t\) (itoIntegralProcessGenl2continuous), by a \(t\)-uniform contraction estimate against an approximating simple sequence (TendstoUniformly), so that continuity transfers from the simple layer in the uniform limit.

Defining the process as a projection of its terminal value is what turns the martingale theory of the Itô integral into a sequence of corollaries rather than a sequence of constructions.

6.3 The time-indexed Itô isometry↩︎

The terminal isometry above is the classical \(\|\mathcal{I}_T(\varphi)\|_{L^2}^2 = \|\varphi\|_{H_T}^2\). Its refinement to intermediate times (the energy law of the integral as a process) is Theorem 2 (Listing [lst:iso]).

T)
:
2
2
hBmeas)

The proof is again the equalizer pattern, against a different continuous functional: \(\varphi \mapsto \|(\varphi\bullet B)_t\|^2\) and \(\varphi \mapsto \int_{(0,t]} \varphi^2\) are both continuous, and they agree on the dense simple processes by the band reconciliation itoSimpleProcessLpbandisometry, which is where the trimmed measure is decomposed across \((0,t] \cup (t,T]\), the supporting lemma being integralrectTermmulband. The mathematical content is small once the simple-layer isometry and the key identity are in place; we call it out as a separate theorem because the second-moment law of the process is one of the two facts every textbook labels “the Itô isometry,” and stating it for general integrands at every \(t\) (not only at \(t = T\), and not only for simple processes) is what makes the integral-as-a-process a complete object rather than a martingale with a missing variance law.

7 Itô’s formula↩︎

7.1 Architecture↩︎

The route to Itô’s formula is discrete-to-continuous (Figure 1):

1. Discrete identity. For any partition, second-order Taylor expansion of \(f\) along the increments gives an exact discrete Itô identity (DiscreteIto) with an explicit Lagrange remainder.

2. Weighted quadratic variation. The \(\sum f''(B_{t_k}) (\Delta_k B)^2\) term converges in \(L^2\) to \(\int_0^T f''(B_s)\,ds\); this is proved for adapted weight processes (WeightedQuadraticVariation), generalizing the unweighted \(L^2\) quadratic-variation limit and reusing the second- and fourth-moment Gaussian estimates of BrownianQuadraticVariation.

3. Remainder. The third-order remainder is \(O(1/n)\) in \(L^2\) under the \(|f'''| \le C_3\) bound (ItoFormulaRemainder); the time-dependent variant needs a two-dimensional remainder with mixed partials, also \(O(1/n)\) (ItoFormulaTDRemainder).

4. Riemann bridge. The discretized stochastic term is \(\mathcal{I}_T\) applied to a step-process realization of \(f'(B)\); the bridge lemmas identify partial sums with the CLM applied to stepφ.

5. Limit. The step integrands converge in \(H_T\) to a realization \(g_{f'}\) of \(s \mapsto f'(B_s)\). Predictability of the limit is free (the limit is taken inside \(H_T\), Section 5); the existence of the realization for bounded continuous data is itoIntegralCLMTofbddcont, a dominated-convergence argument on the trimmed measure.

7.2 The fluctuation engine: quadratic variation in \(L^2\)↩︎

The second-order term of Itô’s formula is deterministic in the limit for one reason: the squared increments of Brownian motion have vanishing fluctuation in \(L^2\). Along the uniform partition of \([0,t]\) into \(n\) pieces of width \(\Delta = t/n\), \[\Big\| \sum_k (B_{s_{k+1}} - B_{s_k})^2 - t \Big\|_{L^2(\mu)}^2 = \frac{2t^2}{n} \longrightarrow 0\] (tendstoqv), and the value is exact, not asymptotic. Writing \(Y_k = (B_{s_{k+1}} - B_{s_k})^2 - \Delta\) for the centered squared increment, the \(Y_k\) over disjoint intervals are independent by the weak Markov property of \(B\), so the cross terms vanish and \(\mathbb{E}[(\sum_k Y_k)^2] = \sum_k \mathbb{E}[Y_k^2]\). Each term is the Gaussian kurtosis, \[\mathbb{E}[Y_k^2] = \mathbb{E}[(B_{s_{k+1}} - B_{s_k})^4] - \Delta^2 = 3\Delta^2 - \Delta^2 = 2\Delta^2,\] using \(\mathbb{E}[X^4] = 3(\operatorname{Var} X)^2\) for a centered Gaussian (integralpow4gaussianReal, transported to the increment law by integralincrementpow4). Summing, \(n \cdot 2\Delta^2 = 2t^2/n\). The fourth-moment constant \(3\), and nothing else, is the reason the quadratic variation is \(t\) rather than \(0\); this is the formal content of \((\mathrm dB)^2 = \mathrm dt\).

7.3 The weighted second-order term↩︎

Itô’s formula needs this limit carrying a weight: for a bounded adapted process \(w\) with continuous paths, \[\sum_k w_{t_k}\,(B_{t_{k+1}} - B_{t_k})^2 \longrightarrow \int_0^T w_s\,ds \qquad \text{in } L^2\] (tendstoweightedqvprocess), instantiated at \(w_s = f''(B_s)\) for the autonomous formula and \(w_s = f_{xx}(s, B_s)\) for the time-dependent one. The proof splits the difference into a fluctuation term and a Riemann term. The fluctuation term \(\sum_k w_{t_k}\big((B_{t_{k+1}} - B_{t_k})^2 - \Delta_k\big)\) vanishes in \(L^2\) by the orthogonality-plus-kurtosis estimate above, now carrying the \(\mathcal{F}_{t_k}\)-measurable bounded weight: adaptedness of \(w_{t_k}\) is exactly what keeps the cross terms zero (integraladaptedmulcenteredsq). The Riemann term \(\sum_k w_{t_k}\Delta_k - \int_0^T w_s\,ds\) vanishes pathwise by continuity of \(s \mapsto w_s(\omega)\), then in \(L^2\) by dominated convergence against the bound \(|w| \le C\). Neither half uses where the weight came from, only that it is adapted, bounded, and path-continuous, which is why one lemma serves both the autonomous and the time-dependent formula.

7.4 The remainder↩︎

What survives after the first- and second-order terms is a sum of cubic Taylor remainders, and it must vanish in \(L^2\). The per-step remainder \(R_k = f(B_{s_{k+1}}) - f(B_{s_k}) - f'(B_{s_k})(B_{s_{k+1}} - B_{s_k}) - \tfrac12 f''(B_{s_k}) (B_{s_{k+1}} - B_{s_k})^2\) obeys the cubic bound \(|R_k| \le C_3\,|B_{s_{k+1}} - B_{s_k}|^3\) under \(|f'''| \le C_3\) (absdiscreteTaylorRemainderle, three applications of the convex mean-value inequality, each gaining one power of the increment). Hence \(\mathbb{E}[R_k^2] = O\big(\mathbb{E}[(B_{s_{k+1}} - B_{s_k})^6]\big) = O(\Delta_k^3)\) by the Gaussian sixth moment (integralpow6gaussianReal), and Cauchy–Schwarz across the \(n\) terms gives \[\mathbb{E}\Big[\Big(\textstyle\sum_k R_k\Big)^2\Big] \le n \sum_k \mathbb{E}[R_k^2] = O\big(n \cdot n \cdot (T/n)^3\big) = O(1/n) \longrightarrow 0\] (ItoFormulaRemainder). The third order is the only place a third derivative is used, and where boundedness of \(f'''\) enters; the time-dependent variant runs the same estimate on a two-dimensional Taylor remainder with mixed partials (ItoFormulaTDRemainder).

7.5 The bounded-derivative Itô formula↩︎

t))
ℝ≥0)
ℝ
x)
x)
:
hBmeas),
=ᵐ[μ]
ω
∂timeMeasure)

Proof sketch. Fix the uniform partition of \([0,T]\) into \(n\) pieces and apply second-order Taylor expansion of \(f\) to each increment. The telescoping sum gives the exact discrete identity \[f(B_T) - f(B_0) = S_n + \tfrac12 Q_n + R_n,\] with \(S_n = \sum_k f'(B_{s_k})(B_{s_{k+1}} - B_{s_k})\) the discretized stochastic integral, \(Q_n = \sum_k f''(B_{s_k})(B_{s_{k+1}} - B_{s_k})^2\) the weighted squared-increment sum, and \(R_n\) the cubic remainder. Each term has a limit established above: \(S_n \to \mathcal{I}_T(g_{f'})\) in \(L^2\), because the step integrands converge to \(g_{f'}\) in \(H_T\) and \(\mathcal{I}_T\) is isometric; \(Q_n \to \int_0^T f''(B_s)\,ds\) in \(L^2\) by the weighted quadratic variation; and \(R_n \to 0\) in \(L^2\) by the remainder estimate. Setting \(a = S_n - \mathcal{I}_T(g_{f'})\), \(b = \tfrac12(Q_n - \int_0^T f''(B_s)\,ds)\), and \(c = R_n\), the total error is \(a + b + c\), and the elementary inequality \((a+b+c)^2 \le 3a^2 + 3b^2 + 3c^2\) drives \(\mathbb{E}[(\text{total error})^2] \to 0\). The two sides of the displayed identity therefore agree in \(L^2\), hence \(\mu\)-almost everywhere.

Path continuity is supplied by the BrownianMotion package’s continuous modification; it is genuinely used, as the Riemann limits run along refining partitions evaluated on paths. The bounded-derivative hypotheses make the \(L^2\) analysis self-contained; their cost is discussed without euphemism in Section 8.

7.6 The time-dependent formula↩︎

Two formalization points. First, joint continuity of \(f_t\) is not assumed: it is derived from the bounded mixed partials (continuousuncurryofbddpartials), keeping the hypothesis package at what a user can actually check. Second, the time-direction Taylor terms are handled by a boundary-cancellation decomposition in which three telescoping error sums vanish separately; the \(L^2\) bound that glues the stochastic and time directions is the three-term Cauchy–Schwarz estimate visible in the remainder lemma’s proof, where the squared error is dominated by \(3(\text{drift})^2 + \tfrac34(\text{QV})^2 + 3(\text{remainder})^2\) and each term is sent to zero separately.

7.7 Supporting results↩︎

7.7.0.1 Quadratic variation.

For a process with measurable coordinates and centered Gaussian increments of variance \(t - s\) (neither independence of increments nor path continuity is assumed), the expected squared-increment sums along equipartitions of \([0,t]\) converge to \(t\) (qvequalst); the \(L^2\)-limit form along refining partitions is in QuadraticVariationL2. That the hypothesis set is weaker than the textbook’s (the \(L^1\) statement needs only the second moment of the increments) is recorded in the statement, and it strictly strengthens the classical claim.

7.7.0.2 Expectation-level Itô.

For \(f \in C^2\) with bounded derivatives, \(\mathbb{E}[f(B_t)] = f(0) + \tfrac12 \int_0^t \mathbb{E}[f''(B_s)]\,ds\) (expectationito; instance form expectationitoisPreBrownian). Historically the library’s first Itô-flavored result, it now lives in the Feynman–Kac module and is the bridge between the stochastic tower of this paper and the analytic (heat-kernel) tower of the parent library.

7.8 Notes on the proof engineering↩︎

The density argument is the only place a monotone-class induction was unavoidable; expressing it against a trimmed measure (so that the inductively-built sets live in the right \(\sigma\)-algebra by construction) is what kept it tractable. And the dominated-convergence step that produces the Itô-formula integrand realization (itoIntegralCLMTofbddcont) is delicate precisely because the dominating function must itself be predictable; here too the trimmed-measure design (rather than ambient \(L^2\) with a side condition) is what makes the domination land inside \(H_T\) without a separate measurability obligation.

8 Scope: what is, and is not, an Itô calculus here↩︎

The title claims “a” Itô calculus, and the indefinite article is doing deliberate work. What earns the noun is that the canonical objects and the canonical theorem are present and compose: the stochastic term in Itô’s formula (Theorem 3) is definitionally the isometric integral of Section 5, whose energy law is the isometry of Theorem 2, whose conditional projection is the martingale of Theorem 1, whose engine is the quadratic-variation limit. One object, four theorems, no re-derivation gluing them. That coherence is the sense in which this is a calculus and not a collection of stochastic-analysis lemmas.

What the indefinite article concedes is equally concrete.

8.0.0.1 Bounded derivatives exclude the textbook’s first examples.

Theorem 3 requires \(|f'| \le C_1\). The function \(f(x) = x^2\) has \(f'(x) = 2x\), unbounded, and so is not in the admissible class. In particular the formula cannot, by itself, derive the keystone \(\mathcal{I}_T(B) = \tfrac12(B_T^2 - B_0^2 - T)\), which is exactly why Section 5 proves that identity directly, through the discrete squaring route, rather than as an instance of Itô’s formula. The honest reading is that what is formalized is the bounded-derivative Itô formula. The unrestricted \(C^2\) statement is obtained, classically, by localization (stopping the process at exit times of compact sets, applying the bounded case, and passing to the limit), and so lies one standard construction beyond the present development, atop the stopping-time layer already available upstream.

8.0.0.2 Brownian integrator, \(L^2\) integrands, \([0,T]\).

The integrator is Brownian motion, not a general continuous local martingale or semimartingale; integrands live in the \(L^2\) space \(H_T\), not the localized class with \(\int_0^T \varphi_s^2\,ds < \infty\) only almost surely; and the interval is a fixed bounded \([0,T]\), not \([0,\infty)\). Each is a standard way to introduce the Itô integral (it is how the textbooks’ first chapters are scoped), and each is named here so that the verified frontier is unambiguous.

8.0.0.3 \(L^2\), not pathwise.

Every process-level statement is an \(L^2\) statement. The integral process has an \(L^2\)-continuous version (Theorem via itoIntegralProcessGenl2continuous); we do not yet construct a modification with almost-surely continuous paths, though the Kolmogorov–Chentsov layer needed for it is already present upstream. Likewise quadratic variation is established in \(L^1\)/\(L^2\), not in the pathwise (a.s.along refining partitions) sense.

None of these boundaries qualifies a statement made in Sections 5–7; they bound the reach of the development, not the validity of any theorem in it.

9 Related work↩︎

Keskin’s Isabelle/HOL martingale library [1] is the closest prior art in the probabilistic direction; it develops (sub/super) martingales in discrete and continuous time but stops below stochastic integration. Degenne, Ledvinka, Marion, and Pfaffelhuber [3], [4] construct Brownian motion in Lean 4, building Kolmogorov extension, Gaussian Banach-space measures, and Kolmogorov–Chentsov; their outlook lists the martingale property of Brownian motion and everything above it as open. That is the layer this paper occupies. The present development consumes their package and is, to our knowledge (a search of the Isabelle AFP, the Lean ecosystem, and the Coq ecosystem in June 2026), the first machine-checked Itô calculus in any proof assistant. Avigad, Hölzl, and Serafin’s central limit theorem [2] remains the historical anchor for deep measure-theoretic probability in proof assistants. In the finance direction, Echenim, Guiol, and Peltier formalized discrete-time replication pricing and the Cox–Ross–Rubinstein model in Isabelle/HOL [10]; continuous-time mathematical finance above the present calculus is developed in the parent library [5]. We are not aware of any other formalization effort, in any assistant, that has published stochastic integration, Itô’s formula, or their process-level martingale theory.

10 Conclusion↩︎

The development formalizes the \(L^2\) Itô calculus of Brownian motion on a bounded interval: the integral as an isometry, the integral as a continuous \(L^2\) martingale with its full second-moment structure, and Itô’s formula in both autonomous and time-dependent forms, with the quadratic-variation machinery that drives them. To our knowledge it is the first machine-checked Itô calculus in any proof assistant. It is also the layer the parent mathematical-finance library [5] stands on, where the integral and the formula are consumed to derive, rather than assume, the objects of continuous-time pricing. The boundaries recorded in Section 8 (localization to unrestricted \(C^2\), integrators beyond Brownian motion, pathwise statements) mark where the formalized theory currently ends; each sits on infrastructure either present or in progress upstream, which is the natural place for it to be built.

11 Displayed results and their Lean names↩︎

References↩︎

---

1. Independent researcher. ORCID: 0009-0001-6601-1023. Correspondence: raphaelrrcoelho@gmail.com. Artifact: https://github.com/raphaelrrcoelho/formal-mathfin.↩︎