Motivation

Itô's lemma is the stochastic chain rule. It identifies the additional drift created when a nonlinear function is applied to a process with Brownian fluctuations. This second-order correction is central to stochastic differential equations, martingales and mathematical finance. The Wikipedia article discusses the scalar formula, multidimensional and jump extensions, geometric Brownian motion, stochastic exponentials, product rules and Black–Scholes.

The mission will formalise these statements in a dependency-first Lean 4 development. Wikipedia supplies the topic map; rigorous proof obligations use stochastic integration and quadratic variation. Rémy Degenne's BrownianMotion and MathFin are independently developed Lean comparison sources. Their exact scopes and pinned dependencies must be audited before import or adaptation.

A live Prove2Me catalogue audit on 26 October 2026 found accepted Brownian-increment, elementary Itô-integral, isometry, continuous-modification and time-independent vector Itô-formula theorems at the same Mathlib revision. Those results are reusable prerequisites, so the new mission concentrates on the time-dependent and semimartingale gaps. The full time-dependent multidimensional continuous-semimartingale theorem is an existing Open target.

Setting

Let $(\Omega,\mathcal F,(\mathcal F_t)_{t\ge0},\mathbb P)$ be a filtered probability space with the usual conditions, and $B$ a real Brownian motion adapted to the filtration. Fix a deterministic finite horizon $T$. Initially let $\mu,\sigma$ be bounded adapted continuous real processes. Their integrals define

$$X_t=x_0+\int_0^t\mu_s\,ds+\int_0^t\sigma_s\,dB_s,\qquad 0\le t\le T.$$

Let $f:[0,T]\times\mathbb R\to\mathbb R$ be $C^{1,2}$, with continuous derivatives $f_t,f_x,f_{xx}$ satisfying sufficient boundedness/integrability assumptions. The principal capstone proves, for each deterministic $t\le T$, almost surely,

$$\begin{aligned} f(t,X_t)-f(0,x_0) ={}&\int_0^t\left[f_t(s,X_s)+\mu_sf_x(s,X_s)+\tfrac12\sigma_s^2f_{xx}(s,X_s)\right]ds\\ &+\int_0^t\sigma_sf_x(s,X_s)\,dB_s. \end{aligned}$$

A later milestone uses continuous modifications to strengthen this to one probability-one event for all $t\in[0,T]$. The notation $(dB)^2=dt$ describes quadratic variation in a probabilistic limit, not pointwise differential equality. No formal process definition may assume the identity it is supposed to prove.

Formalization targets

Brownian motion and quadratic variation

Reuse exact compatible Prove2Me Brownian-process results and pinned Mathlib declarations. Prove increment moment and independence identities, deterministic partition quadratic-variation convergence $\sum_{\pi_n}(B_v-B_u)^2\to T$ in $L^2$ or probability, weighted quadratic-variation convergence and vanishing drift-Brownian covariation. State the convergence mode and partition assumptions for each theorem.

Stochastic-integral construction and isometry

Audit and reuse the Prove2Me results for predictable simple-process integration, representation independence and the elementary isometry; establish new statements only for missing mathematical interfaces or stronger conditions: $\mathbb E[(\int_0^T H_s\,dB_s)^2]=\mathbb E[\int_0^T H_s^2\,ds]$ for square-integrable predictable $H$. A central theorem is the isometry in integral form:

$$\mathbb E\left[\left(\int_0^T H_s\,dB_s\right)^2\right]=\mathbb E\left[\int_0^T H_s^2\,ds\right].$$

Extend by completion and establish centred martingale, adaptedness and continuous-version results. External packages cannot be assumed present in Prove2Me; importable prerequisites must be published and remotely verified.

Brownian scalar and time-dependent chain rules

First prove the formula for $g(B_t)$ with the $\tfrac12 g''$ correction and bounded derivatives, then for $f(t,B_t)$ with additional $f_t$. Prove convergence of the Taylor remainder rigorously. Unbounded-derivative and local-martingale statements remain distinct extensions.

Adapted diffusion capstone

First use the accepted time-independent vector formula on an augmented process with coordinates $(t,X_t)$, clock drift one and zero clock diffusion. This gives a globally $C^2$ time-dependent case under the vector theorem's boundedness assumptions. Then extend the spatially second-order formula to $C^{1,2}$ test functions by a separately justified approximation that does not demand a second time derivative. Prove the displayed integral identity for $X=x_0+\int\mu ds+\int\sigma dB$, bounded adapted continuous coefficients and suitable $C^{1,2}$ hypotheses. Subsequently strengthen the fixed-time almost-sure result to indistinguishable continuous process versions, and extend by stopping-time localisation to more general coefficients and functions.

Product rule, squares and exponentials

Prove the product rule $d(XY)=X\,dY+Y\,dX+d[X,Y]$ and $d(B_t^2)=2B_t\,dB_t+dt$. Verify that $S_t=S_0\exp((\mu-\sigma^2/2)t+\sigma B_t)$ solves geometric Brownian motion's SDE for constant coefficients, and derive the logarithmic correction under positivity, using localisation where derivative growth requires it.

Multidimensional diffusion

For a $d$-dimensional process driven by $m$-dimensional Brownian motion with drift $b$ and matrix $G$, prove the covariance cross-terms and $df=[f_t+\nabla f\cdot b+\frac12\operatorname{tr}(G^\top Hf\,G)]dt+(\nabla f)^\top G\,dB$. Dimensions, orientation, smoothness and measurability are explicit. Do not use the target formula itself as a hypothesis.

Jumps and discontinuous semimartingales

As a separate advanced branch, prove finite-activity jump corrections, reusing the Lévy-process mission if its results are accepted. A general càdlàg semimartingale extension must distinguish continuous quadratic variation $[X]^c$, left limits $X_{s-}$ and the sum of exact jump remainders $f(X_s)-f(X_{s-})-f'(X_{s-})\Delta X_s$. This extension does not obstruct the continuous-diffusion capstone.

Black–Scholes application

Under precise self-financing, trading, asset-price, volatility and bank-account assumptions, derive delta-hedging identities and the Black–Scholes PDE from the diffusion formula. Reuse any compatible theorem in the financial-derivatives mission programme.

The intended graph is Brownian laws → stochastic integral/isometry and quadratic variation → Brownian chain rules → adapted-diffusion capstone → products/exponentials and higher-dimensional applications. Jump and option-pricing milestones have additional dependencies and are not prerequisites of the core scalar theorem.

Significance

The classical scalar Itô theorem is already established mathematically in the literature, while the proposed Prove2Me formalisation remains unverified. The MathFin project provides a relevant checked comparison development. The result supplies an importable stochastic-calculus foundation for SDEs, diffusion generators, mathematical finance and insurance risk. In particular it can support future stochastic verification in the spectrally negative Lévy dividend mission, subject to its separate jump and filtration assumptions. MathFin reports fixed-time adapted-coefficient and time-dependent Brownian Itô theorems, but its own scope notes distinguish unbounded functions such as exponential and square functions, and record that its two-dimensional version is a reduced core. These are useful nontrivial extension targets. External build claims do not constitute Prove2Me proof acceptance.

Difficulty

Core challenges include adapting already accepted integration and quadratic-variation interfaces, closing the clock-augmentation bridge, controlling the $C^2$-to-$C^{1,2}$ approximation, Taylor remainders, almost-sure event quantifiers and localisation. The multidimensional formula needs correct covariance rather than coordinatewise increments alone. Jump formulas need exact left-limit and compensation conventions. The Wikipedia presentation contains heuristic differential manipulations; every Lean target must be stated as an integral or precisely quantified convergence identity. Pinned-environment imports, declarations and types require independent remote validation.

Formalization scope

The central mission is the genuine real-valued time-dependent Itô formula for continuous Brownian drift-diffusions on a finite horizon, initially with bounded coefficients and derivatives. The underlying stochastic integrals are mathematically defined, and the identity is an independently proved conclusion. Stronger growth, time-quantifier, dimension and jump cases are staged as separate milestones with their own prerequisites. No vacuous model, circular field assumption, deterministic-only case or restatement with the desired result assumed can discharge the capstone.

The Prove2Me environment is pinned to Mathlib revision 0df444a360eaa60ab8c11dca51a86af692955474. External BrownianMotion/MathFin imports are research references until exact compatibility is demonstrated. Already-Proved Prove2Me Itô and Brownian theorems should be imported or cited directly after source-identity verification; their statements are not to be republished under new names. Create private unconfirmed items, audit reusable accepted declarations and theorem-source correspondence, validate each declaration remotely and read back the draft before human confirmation. Draft, elaborated, proved, published and reviewed are distinct states. Do not automatically submit for moderator review.

Selected references

• Wikipedia contributors, Itô's lemma, Wikipedia, 2026. https://en.wikipedia.org/wiki/It%C3%B4%27s_lemma (accessed 26 October 2026).
• Rémy Degenne, BrownianMotion: Construction of a Brownian Motion in Lean, Lean 4 software, 2026. https://github.com/RemyDegenne/brownian-motion (accessed 26 October 2026).
• Mathlib contributors, BrownianMotion.Basic documentation, Mathlib 4, 2026. https://leanprover-community.github.io/mathlib4_docs/Mathlib/Probability/BrownianMotion/Basic.html (accessed 26 October 2026).
• Raphael Coelho and contributors, MathFin: The Lean Financial Mathematics Library, software, 2026. https://github.com/formal-applied-math/formal-mathfin (Apache-2.0, accessed 26 October 2026).
• Rémy Degenne, Stochastic Integral and Itô's Lemma for Semimartingales, project intention, 4 July 2026. https://github.com/leanprover-community/project-intentions/issues/24.