Local Time and Tanaka's Formula

Ito's lemma tells you how a smooth function of Brownian motion evolves, but it needs the function to be twice differentiable — no kinks allowed. The absolute-value function $|x|$ has exactly one kink, at zero, and it turns out that is precisely where the interesting behavior of a random path lives: how much time does the path spend hovering right at a given level?

That question has a precise answer called local time, written $L_t^a$: informally, the amount of time a path spends in an infinitesimally thin band around level $a$, up to time $t$, rescaled so it stays a finite, meaningful number rather than zero (a single instant has zero width) or infinite. A path that crosses level zero constantly, the way Brownian motion does, has local time at zero that grows steadily over time even though the path is at exactly zero for a set of moments with zero total length in the ordinary sense.

Tanaka's formula is what lets you apply an Ito-lemma-style expansion to $|B_t|$ despite the kink at zero:

$$|B_t| = |B_0| + \int_0^t \text{sign}(B_s)\, dB_s + L_t^0$$

In words: the absolute value of Brownian motion equals its starting value, plus an ordinary stochastic integral that tracks the sign of the path, plus a correction term — the local time at zero — that accounts for all the moments the path spent exactly at the kink. Where Ito's lemma for a smooth function has only a $\frac{1}{2}f''$ correction from curvature, Tanaka's formula shows that a kink contributes its own correction: local time at that exact point, rather than a curvature term that would not be well-defined there.

This shows up practically in barrier-option pricing and in results about reflected or absorbed processes, where "how much time does the path spend at the boundary" is exactly the quantity local time was built to measure.