Local time resolves an apparent paradox: Brownian motion spends zero Lebesgue time at any single level, yet its repeated visits have a nontrivial density in space. Tanaka's formula is Ito's formula for a convex function with a kink; the missing second derivative is a point mass, and its integral is local time.
Occupation measures
Definition. The occupation measure of Brownian motion up to time \(t\) is \[ \mu_t(A)=\int_0^t1_{\{B_s\in A\}}\,\mathrm{d} s. \] A local time is a density \(a\mapsto L_t^a\) satisfying \[ \mu_t(A)=\int_AL_t^a\,\mathrm{d} a, \] or equivalently \[ \int_0^tf(B_s)\,\mathrm{d} s = \int_{\mathbb R}f(a)L_t^a\,\mathrm{d} a \] for every nonnegative measurable \(f\).
Theorem. Brownian motion has a version of local time jointly continuous in \((t,a)\). For every \(a\), \[ L_t^a = \lim_{\varepsilon\downarrow0} \frac1{2\varepsilon} \int_0^t1_{\{|B_s-a|<\varepsilon\}}\,\mathrm{d} s \] in \(L^2\), and along suitable subsequences almost surely.
Proof outline. Define the approximate densities in the display. Their first and second moments can be written using the Brownian transition density and the joint density of \((B_r,B_s)\). Heat-kernel estimates make them Cauchy in \(L^2\) as \(\varepsilon\downarrow0\). Moment estimates for increments in both \(t\) and \(a\), followed by Kolmogorov-Chentsov, produce a jointly continuous version. Fubini and approximation of indicators establish the occupation-density identity.
Occupation density for semimartingales
Theorem. If \(X\) is a continuous semimartingale, there is local time \(L_t^a(X)\) such that \[ \int_0^tf(X_s)\,\mathrm{d}[X]_s = \int_{\mathbb R}f(a)L_t^a(X)\,\mathrm{d} a. \] Brownian motion is the special case \([B]_s=s\).
Local time is therefore density with respect to the clock that measures martingale roughness, not necessarily ordinary elapsed time.
Tanaka's formula
Theorem (Tanaka). For a continuous semimartingale \(X\), with \(\operatorname{sgn}(0)=0\), \[ |X_t-a| = |X_0-a| +\int_0^t\operatorname{sgn}(X_s-a)\,\mathrm{d}X_s +L_t^a(X). \] Equivalently, \[ (X_t-a)^+ = (X_0-a)^+ +\int_0^t1_{\{X_s>a\}}\,\mathrm{d}X_s +\frac12L_t^a(X). \]
Proof. Choose smooth convex \(f_\varepsilon\to|\cdot-a|\) with \(f_\varepsilon'\to\operatorname{sgn}(\cdot-a)\) and \(f_\varepsilon''(x)\,\mathrm{d} x\Rightarrow2\delta_a\). Ito's formula gives \[ f_\varepsilon(X_t) = f_\varepsilon(X_0) +\int_0^tf_\varepsilon'(X_s)\,\mathrm{d}X_s +\frac12\int_0^tf_\varepsilon''(X_s)\,\mathrm{d}[X]_s. \] Bounded convergence after localization handles the stochastic integral. The occupation-density formula rewrites the last term as \[ \frac12\int_{\mathbb R} f_\varepsilon''(y)L_t^y(X)\,\mathrm{d} y \to L_t^a(X) \] by continuity in \(y\). This proves the absolute-value formula; use \(x^+=(|x|+x)/2\) for the second.
Support and increase of local time
Proposition. For fixed \(a\), \(t\mapsto L_t^a(X)\) is continuous and increasing, and \[ \int_0^t1_{\{X_s\ne a\}}\,\mathrm{d}L_s^a(X)=0. \] Thus local time increases only while the process is at level \(a\).
Proof. The approximation by \((2\varepsilon)^{-1}1_{\{|X_s-a|<\varepsilon\}}\mathrm{d}[X]_s\) makes monotonicity in \(t\) clear. If \(|X_s-a|\ge\delta\) on a compact time set, the approximating integrands vanish there for \(\varepsilon<\delta\); pass to the limit and then cover \(\{X_s\ne a\}\) by the sets \(\{|X_s-a|\ge1/n\}\).
Reflection and Levy's identity
Theorem (Levy identity). For standard Brownian motion and \(S_t=\sup_{s\le t}B_s\), \[ (S_t-B_t,S_t)_{t\ge0} \stackrel d= (|B_t|,L_t^0)_{t\ge0}. \]
Proof outline. Tanaka writes \[ |B_t| = \int_0^t\operatorname{sgn}(B_s)\,\mathrm{d}B_s+L_t^0. \] The stochastic integral has bracket \(t\), hence is Brownian by Levy's characterization. The pair solves the Skorokhod reflection problem: add the minimal increasing process, supported where the reflected path is zero, to keep a Brownian path nonnegative. The unique solution is \(S_t-B_t\) with regulator \(S_t\), giving equality in law.
Corollary. \[ L_t^0\stackrel d=S_t\stackrel d=|B_t|. \] Local time at zero therefore has the half-normal distribution at each fixed time, although it is defined through infinitely many microscopic visits.