For a continuous semimartingale ,
where is the local time of a semimartingale at zero.
Choose and , where is continuously differentiable, nondecreasing, equal to on and on . Then and . For with continuous adapted finite-variation , the Itô isometry and Doob L2 maximal inequality give local uniform convergence in probability of the martingale integrals. Dominated convergence against the total-variation measure gives pathwise uniform convergence of the drift integrals. The nondecreasing corrections therefore converge locally uniformly in probability to . A subsequence on one probability-one event shows that the limit is continuous and nondecreasing. Localization removes the deterministic bounds used in the argument.
For integer paths with increments in , the positive part obeys a telescoping identity with slope and a correction at the kink. For a martingale, the slope term is a martingale transform.
Let a simple symmetric random walk start from a deterministic integer , and put . Then is a martingale with . The visit count includes time if .
For every integer and step , the pathwise identity
holds with . Subtract the indicator function and sum over time to obtain
The sign function of the current state is a bounded predictable process for the next increment, so the sum is a martingale transform. Alternatively, averaging the two possible next absolute values shows directly that the conditional drift is . Bounds and verify integrability at each finite time.
This is an absolute-value version of the discrete Tanaka formula. The correction records the occasions when the random walk is at the corner of the absolute-value function; away from zero that function is locally linear along a single step.

Articles by others on the same topic (1)

Tanaka's formula is a result in stochastic calculus that provides a way to express the solution of a stochastic differential equation (SDE) in terms of the Itô integral and the quadratic variation of a continuous local martingale. The formula is particularly significant because it allows for the computation of expectations involving the stochastic processes that satisfy certain SDEs.