Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedaudited 2026-09-22
How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

  • Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
  • AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
  • AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

One-dimensional Ito formula

Statement

Assume the Axiom of Choice and the standing hypothesis (H) of Elementary predictable Brownian integrands. Let Xt=X0+∫0tbs ds+∫0tσs dBs be a real continuous Brownian Ito process Continuous Brownian Ito processes, under its usual-filtration conditions, and let f∈C1,2([0,∞)×R), meaning that f, its first time derivative ∂tf and its first two space derivatives ∂xf,∂x2f exist and are continuous on [0,∞)×R. Then, up to indistinguishability, for every t≥0 f(t,Xt)=f(0,X0)+∫0t(∂tf+b ∂xf+12σ2∂x2f)(s,Xs) ds+∫0tσs ∂xf(s,Xs) dBs, For the displayed integrands use the following representative convention. Intersect the measurable full events of continuity of X, validity of its decomposition, and local integrability of its coefficients at integer horizons. Its complement is an F0-measurable null event by the usual conditions. Replace X,X0,b,σ by zero there. This preserves the decomposition up to indistinguishability and all coefficient classes, and makes X continuous everywhere and its coefficient path integrals locally finite everywhere. All integrands below refer to these representatives. The stochastic integral is the localized Ito integral of the predictable locally square-integrable process σs∂xf(s,Xs) Localized Ito integral and the Lebesgue integral is the pathwise integral of the progressively measurable process s↦(∂tf+b∂xf+12σ2∂x2f)(s,Xs), which is pathwise integrable and finite almost surely for every t. In differential notation, df(t,Xt)=(∂tf+b∂xf+12σ2∂x2f)(t,Xt) dt+σt∂xf(t,Xt) dBt.

Facts & Assumptions

Given: AC, (H), a real continuous Brownian Ito process X=X0+A+M with At=∫0tbs ds and M=∫σ dB, a function f∈C1,2([0,∞)×R), a finite horizon T>0, and an arbitrary deterministic partition sequence (πn) of [0,T] with mesh δn→0. The stopping time ρc is defined as in [F7] below.

[F1]

Paths, measurability and local boundedness. After the statement's F0-null-event normalization, X is adapted with everywhere continuous paths, hence predictable, and on each finite time interval a continuous path is bounded. Every continuous function of (s,Xs) is predictable; its product with the predictable coefficient σ is predictable, while its product with the progressively measurable drift b is progressively measurable. Continuous Brownian Ito processes Adapted continuous processes are progressively measurable Progressively measurable and predictable processes

[F2]

Localized-integral interfaces. For a predictable G with finite energy: E(∫0TG dB)2=E∫0TG2ds, the integral over a subinterval is the integral of the restriction, the stopping identity holds, the elementary sums converge to the integral, and the Doob maximal bound Esup⁡t≤T(∫0tG dB)2≤4E∫0TG2ds holds. A locally square-integrable predictable G has a localized integral whose stopped pieces are the finite-energy integrals of G1(0,ρ]; and if c is bounded and Fu-measurable then the localized integral of cG over an interval inside (u,∞) equals c times that of G, because the finite-energy case follows from the elementary case and the L2 isometry and the general case by stopping and uniqueness. Localized Ito integral Stopping an Ito integral Ito isometry and linearity in predictable L2 Doob maximal bound for the Ito integral The Ito integral process has a continuous martingale version Ito integral for square-integrable predictable processes Locally square-integrable predictable Brownian integrands

[F3]

Quadratic variation and covariation of the class. [X]t=∫0tσs2 ds and, more generally, ∑jΔjXΔjY→[X,Y]=∫ξη ds uniformly in probability for class processes; in particular with ΔjX=Xtj+1−Xtj the step-convention sums QnX(t)=∑j: tj+1≤t(ΔjX)2 and QnM(t)=∑j: tj+1≤t(ΔjM)2 each satisfy sup⁡t≤T∣QnX(t)−∫0tσs2ds∣→0 and sup⁡t≤T∣QnM(t)−∫0tσs2ds∣→0 in probability for every deterministic vanishing-mesh sequence and both conventions. Quadratic covariation of Brownian Ito processes Quadratic covariation of Brownian Ito processes Quadratic variation along a partition sequence

[F4]

Taylor expansion with a third-order remainder. Let f∈C3 on an open set containing the closed segment from a=(t0,x0) to a+h=(t0+h1,x0+h2). Then f(a+h)=f(a)+∂tf(a)h1+∂xf(a)h2+12(∂tt2f(a)h12+2∂t∂xf(a)h1h2+∂xx2f(a)h22)+R with ∣R∣≤M3∣h∣3, where M3 bounds the third partial derivatives on a ball containing the segment: apply the one-variable Taylor formula with remainder bound to u↦f(a+uh) on [0,1]. Second-order Taylor expansion f(a+h)=f(a)+∇f(a)⋅h+12hTHf(a)h+o(∥h∥2) Multivariable Taylor formula with o(∥h∥k) remainder The multivariable Taylor polynomial in multi-index notation Taylor polynomials and their remainders A uniform derivative bound gives a uniform Taylor remainder bound

[F5]

Staircase comparison and the weighted pullback of quadratic variation. (a) If D∈F0, G is continuous adapted and bounded on D×[0,T], G(n) is its left-endpoint staircase on πn, and ∫0TH2ds≤c on D, then the integrals of 1DG(n)H converge to that of 1DGH in L2(P). Indeed the isometry bounds the squared distance by E[1Dsup⁡s∣Gs(n)−Gs∣2∫0TH2ds], which tends to zero by dominated convergence. (b) If w is continuous adapted with ∣w∣≤K and M=∫σ dB is a finite-energy integral, then ∑jw(tj)ΔjM2→∫0Twsσs2 ds in probability; this terminal-time weighted pullback is proved in steps 1.4--2.1 below. Ito isometry and linearity in predictable L2 Quadratic covariation of Brownian Ito processes Ito integral of an elementary predictable process

[F6]

Bounded Riemann integrals. If Z is continuous on [0,T] and h pathwise Lebesgue-integrable, then ∑jZtj∫tjtj+1hs ds→∫0TZshs ds along vanishing meshes, the error being at most max⁡jsup⁡Ij∣Z−Ztj∣∫0T∣h∣. A continuous function on the compact set [0,T] and a continuous function on a compact cylinder are uniformly continuous, so maximal oscillations on the mesh intervals vanish. Heine-Cantor in R: a continuous real function on a compact subset of R is uniformly continuous Continuity of f:A→R at a point of A and on A: the ε-δ condition, its agreement with lim⁡x→cf(x)=f(c) at a limit point, and continuity at an isolated point

[F7]

Localization of the class and of the coefficients. For c>0 put Dc:={∣X0∣≤c}∈F0 and ρc:=inf⁡{t:max⁡(∣Xt∣,∫0t∣b∣,∫0tσ2)≥c}∧T. Then ρc is a stopping time: for t<T, the event {ρc≤t} is the event that the running supremum of the continuous adapted process max⁡(∣X∣,∫∣b∣,∫σ2) on [0,t] is at least c. This supremum is the supremum over rational times together with t, hence is Ft-measurable; for t≥T the stopping event is the whole space. The process Xˉ(c):=1DcXρc is a continuous Brownian Ito process with initial value 1DcX0 and coefficients 1Dcb1[0,ρc], 1Dcσ1[0,ρc]. It is bounded by c, its drift variation and diffusion energy on [0,T] are at most c, and on Dc∩{ρc≥T} it and all its integrals coincide with those of X. These events increase to a probability-one event as c→∞, because X is continuous and ∫∣b∣,∫σ2 are finite and continuous in the upper limit almost surely. Continuous Brownian Ito processes Localized Ito integral Stopping an Ito integral Continuous-time stopping times and stopped sigma-algebras Heine-Cantor in R: a continuous real function on a compact subset of R is uniformly continuous

[F8]

Cutoff and mollification on a cylinder. Reflection across t=0 by g(t,x):=f(t,x) for t≥0 and g(t,x):=2f(0,x)−f(−t,x) for t<0 extends f to a C1,2 function on a negative-time collar and agrees with f on the nonnegative half-space. Choose compact cylinders K⊆int⁡K′ inside a bounded open set on which g is defined. The cutoff lemma gives a continuous compactly supported cutoff equal to 1 on K′; convolution with a sufficiently small compactly supported mollifier gives χ∈Cc∞ equal to 1 on K and supported in that open set. Then gε:=(χg)∗ρε is smooth and compactly supported, and on the inner cylinder the functions gε,∂tgε,∂xgε,∂xx2gε converge uniformly to f,∂tf,∂xf,∂xx2f. To justify the derivative convergence, write the convolution as ∫ρ(z)(χg)(y−εz)dz. Difference quotients and the fundamental theorem in each variable move each available derivative (∂t, ∂x, ∂xx) onto χg, dominated on the fixed compact support by the corresponding continuous derivative bound times ∣ρ(z)∣. On the inner cylinder χ=1 on a neighbourhood; uniform continuity of each derivative bounds its convolution error by its modulus on shifts of size at most εR times ∫∣ρ∣, where R bounds the mollifier support. This tends to zero. The spaces Cc(Rn) and Cc∞(Rn) The mollifier family generated by a unit-mass smooth bump Convolution with a mollifier is smooth, and derivatives pass under the integral sign A compact set inside a bounded open set admits an explicit compactly supported continuous cutoff Cc∞(Rn) is dense in Lp(Rn) for 1≤p<∞

[F9]

Convergence tools and estimates. Cauchy--Schwarz for sums and expectations; dominated convergence for pathwise Lebesgue integrals; Fatou's lemma; and the fact that a sequence bounded by Rn with ERn→0 converges to 0 in probability. Cauchy-Schwarz for random variables Dominated convergence Fatou's lemma Convergence in probability

[F10]

AC bookkeeping. Choice is declared for the ambient conditional-expectation, completeness and density interfaces; all stopping levels, partitions and mollification scales used below are canonical functions of the given data. The Axiom of Choice

Proof

technique · direct
1.1F1F2F7given

Reduction to a bounded localized problem: fix c>0 and replace X by Xˉ(c)=1DcXρc as in [F7]. This is globally bounded by c, its drift variation and diffusion energy on [0,T] are at most c, and on Dc∩{ρc≥T} both sides of the desired formula agree with those for the original process. Thus the stochastic integrand has finite energy bounded by csup⁡∣∂xf∣2, and every continuous function of (s,Xˉs(c)) is bounded on [0,T]. It remains to prove the identity for this bounded process; localization is removed at the end. To simplify notation, call the bounded process and its coefficients again X,b,σ.

1.2F1F3given

Setup of the C3 case: assume first that f∈C3 on a neighbourhood of the cylinder [0,T]×[−c,c] with finite bounds M0,M1,M2,M3 for its partial derivatives of orders 0,1,2,3 there. For the partition πn write Δtj=tj+1−tj, ΔXj=Xtj+1−Xtj=ΔAj+ΔMj.

1.3F3given

Weighted pullback setup: for continuous adapted w with ∣w∣≤K put H=σ. In steps 1.4 and 2.1 we prove the weighted limit needed for the second-order term. Write Qn=QnM from [F3] throughout the remainder of the proof; then Qn(T) is bounded in probability and converges to ∫0TH2ds.

1.4F3F6given

Weighted pullback, elementary weights: let w=∑aλa1(ua,ua+1] be elementary with bounded Fua-measurable coefficients and fixed deterministic block points. For the cumulative sums Qn(v) on the original partition, [F3] gives uniform-in-v convergence in probability to ∫0vH2ds. The sum over those original intervals lying wholly in (ua,ua+1] is Qn(ua+1)−Qn(ua) up to the at most two boundary intervals. Their contribution is bounded by 2∥λa∥∞max⁡j∣ΔjM∣2, which tends to zero almost surely by continuity. Summing over the finitely many blocks gives ∑jw(tj)ΔjM2→∑aλa∫uaua+1H2ds=∫0TwH2ds in probability.

1.5F3F4F6

Remainder of the Taylor expansion: with hj=(tj+1−tj,Xtj+1−Xtj) the Taylor expansion [F4] gives, for each j, f(tj+1,Xtj+1)−f(tj,Xtj)=∂tfh1+∂xfh2+12(∂tt2fh12+2∂t∂xfh1h2+∂xx2fh22)+Rj with ∣Rj∣≤M3(∣h1∣+∣h2∣)3≤4M3(∣Δtj∣3+∣ΔXj∣3). Summing: ∑j∣Δtj∣3≤mesh⁡(πn)2T→0 and ∑j∣ΔXj∣3≤max⁡j∣ΔXj∣∑j∣ΔXj∣2≤max⁡j∣ΔXj∣(2∑jΔAj2+2Qn(T)), where max⁡j∣ΔXj∣→0 almost surely by continuity of the paths of A and M and Qn(T)−∫0Tσs2ds→0 in probability by [F3], so the sum of remainders tends to 0 in probability.

1.6F2F5F6given

First-order terms: ∑j∂tf(tj,Xtj)Δtj→∫0T∂tf(s,Xs)ds and ∑j∂xf(tj,Xtj)ΔAj→∫0T∂xf(s,Xs)bs ds both almost surely by the Riemann estimate [F6] applied with the continuous bounded weights ∂tf(⋅,X) and ∂xf(⋅,X); and the stochastic part satisfies ∑j∂xf(tj,Xtj)ΔjM=∫0Tg(n)σ dB for the left-endpoint staircase g(n) of s↦∂xf(s,Xs), which converges in L2(P) to ∫0T∂xf(s,Xs)σs dB by F5, now with D=Ω, and [F2].

2.1F5F6step 1.4

Weighted pullback, continuous weights: for continuous adapted w with ∣w∣≤K and its left-endpoint staircase w(m) on the deterministic grid of mesh 2−mT, uniform continuity of s↦ws gives sup⁡s∣ws(m)−ws∣→0 almost surely. Fix m first. Step 1.4 gives the asserted convergence with w(m) as n→∞. Put Rm=sup⁡s∣ws(m)−ws∣. The error in the sums is at most RmQn(T). For every L>0 its probability of exceeding ε is at most P(Rm>ε/L)+P(Qn(T)>L). First take L large using tightness from [F3], then m large; this bound needs no independence of the two factors. the error in the limiting integrals tends to zero as m→∞ by dominated convergence with integrable bound 2K∫0TH2ds. Taking these two limits successively proves F5.

3.1F3F6step 2.1

Second-order terms: by step 2.1 applied to w=∂xx2f(⋅,X), ∑j12∂xx2f(tj,Xtj)ΔjM2→12∫0T∂xx2f(s,Xs)σs2ds in probability. The mixed drift--martingale term satisfies ∣∑j∂xx2fΔjAΔjM∣≤M2(∑jΔjA2)1/2(∑jΔjM2)1/2≤M2(max⁡j∣ΔjA∣∫0T∣b∣)1/2Qn(T)1/2→0 in probability, because A is continuous and hence max⁡j∣ΔjA∣→0 by [F6] and Qn(T) is bounded in probability; and the two purely drift/time terms satisfy ∣∑j12∂xx2fΔjA2∣≤M22max⁡j∣ΔjA∣∫0T∣b∣→0 and ∣∑j∂t∂xfΔtjΔXj∣+∣∑j12∂tt2fΔtj2∣≤M2Tmax⁡j∣ΔXj∣+M22Tδn→0.

4.1F2F3step 1.5step 1.6step 3.1

Assemble the C3 case at T: summing the exact expansion [step 1.5] over j, the left side telescopes to f(T,XT)−f(0,X0), while the right side is the sum of the terms controlled in steps 1.5, 1.6 and 3.1; passing to the limit along πn gives f(T,XT)−f(0,X0)=∫0T(∂tf+b∂xf+12σ2∂xx2f)(s,Xs)ds+∫0Tσs∂xf(s,Xs)dBs in probability, and uniqueness of limits in probability makes the difference of the two fixed random variables zero almost surely. For an arbitrary t∈[0,T] apply the same argument on [0,t] with the restricted, t-augmented partition sequence; both sides are continuous in t, so the identity holds for all t up to indistinguishability.

5.1F2F5F7F8F9step 4.1

Reduction to C1,2 by cutoff and mollification: let f∈C1,2 and take the reflected extension, smooth cutoff and mollifications gε of [F8]. On the nonnegative inner cylinder [0,T]×[−c,c], where the extension equals f, the functions gε and their derivatives ∂tgε,∂xgε,∂xx2gε converge uniformly to the corresponding derivatives of f. Applying step 4.1 to the smooth gε and passing to the limit, the drift term converges by dominated convergence with bound K′(1+∣bs∣+σs2), whose integral is at most K′(T+2c); the stochastic term converges in L2(P) by [F2], since its squared norm is bounded by the uniform squared derivative error times E∫0Tσs2ds≤c; and the left side converges uniformly on the inner cylinder. Hence the identity holds for f at T, and then for every t by the same continuity argument.

6.1F1F2F7step 5.1

Removal of the localization and conclusion: the identity for Xˉ(c) agrees with the desired identity on Dc∩{ρc≥T}. For each path with the normalized local bounds, every integer c larger than sup⁡t≤T∣Xt∣, ∫0T∣b∣ and ∫0Tσ2 has Dc true and ρc=T. Thus these events increase to a probability-one event by [F7], so the identity holds almost surely at every deterministic time, and by continuity of both sides up to indistinguishability. The stochastic integrand σ∂xf(⋅,X) is predictable and locally square-integrable by [F1] and [F2]. The Lebesgue integrand is progressively measurable and integrable almost surely on every finite horizon: after localization its continuous derivative factors are bounded, while ∣b∣ and σ2 are integrable. Thus the displayed statement follows.

7.1F2F3F10step 6.1∎

Boundary and consistency cases: for t=0 both sides equal f(0,X0); for f independent of x the formula reduces to f(t)=f(0)+∫0t∂tf(s)ds, the fundamental theorem for the deterministic continuous function ∂tf; for f(t,x)=x it reduces to the definition of X; for f(t,x)=x2 and X=B (so X0=0, b=0,σ=1) it gives Bt2=2∫0tBsdBs+t; if σ≡0 then X is pathwise absolutely continuous and the formula is the chain rule with the second-order term absent, consistent with the vanishing covariation of finite-variation parts; if X≡X0 is deterministic the formula is the fundamental theorem along the deterministic time variable; and if the diffusion coefficient is unbounded the localization of step 1.1 is what makes every integral finite, with no additional hypothesis. AC enters only through [F10], and all localization and mollification parameters are canonical.

Source notes

Van der Vaart states Theorem 5.79 for a continuous local martingale and a continuous finite-variation process; its proof discussion refers the direct Taylor argument to Chung and Williams and presents a polynomial proof of the more general Theorem 5.85. Lawler, Section 3.3, treats Brownian motion and smooth test functions. Neither attribution substitutes for the explicit local argument below. The C3-first route of steps 1.2 through 4.1 is written out in full because the sources present the argument only for their own bounded or stopped settings; the passage to C1,2 by reflection, cutoff and mollification in step 5.1 is the standard smoothing argument, included here so that the stated C1,2 hypothesis is proved rather than asserted.

Depends on

Used by

Dependency tree · two levels

136 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources