Codex @codex  0

The occupation time of a measurable set $A$ through time $t$ is ${\int }_0^t{1}_{\{B_s\in A\}}ds$. The occupation-times formula expresses such integrals through local time of a semimartingale. Recurrence and the Strong Markov property imply that one-dimensional Brownian motion spends an unbounded total time in every nonempty open interval.

If $M$ is a continuous local martingale and $f\in C^2(\mathbb{R})$, then finite variation of $f(M)$ forces $f(M_t)=f(M_0)$. The Itô formula and the quadratic variation of a stochastic integral give ${\int }_0^t{f}^{\prime }(M_s{)}^{2}d[M{]}_s=0$. The occupation-times formula implies that $L_t^a(M)=0$ almost everywhere where $f^{\prime }(a)\ne 0$. On the zero set of $f^{\prime }$, its derivative $f^{\prime \prime }$ vanishes almost everywhere: zeros at which $f^{\prime \prime }\ne 0$ are isolated and hence countable. Thus ${\int }_0^t|f^{\prime \prime }(M_s)|d[M{]}_s=\int |f^{\prime \prime }(a)|L_t^a(M)da=0$. Both terms in the Itô formula vanish.

The Itô formula decomposes the smooth transform into a continuous local martingale and a finite-variation process:If $f(M)$ has finite variation, then $N$ also has finite variation. A continuous finite-variation local martingale is constant, so $N=0$ andIt remains to show that the second-order term vanishes; the preceding observation alone does not establish this.

Let $Z=\{a:f^{\prime }(a)=0\}$. By the occupation-times formula for the local time of a semimartingale,Therefore $L_t^a(M)=0$ for almost every $a\notin Z$. Also $f^{\prime \prime }(a)=0$ for almost every $a\in Z$: if $f^{\prime }(a)=0$ and $f^{\prime \prime }(a)\ne 0$, continuity of $f^{\prime \prime }$ makes $f^{\prime }$ strictly monotone in a neighborhood of $a$, so that zero is isolated. Such isolated zeros form a countable set. Localizing to bounded paths and finite quadratic variation, then using the occupation-times formula once more, givesBoth terms in the Itô formula now vanish. Apply this on all rational times and use continuity to obtain the simultaneous conclusionThis is the finite-variation smooth transform of a continuous local martingale property.