The Occupation Density Formula and Its Proof

From Tanaka’s Formula to an Occupation Identity

Brownian local time records how occupation accumulates near each spatial level. The occupation density formula makes that description exact: time spent by Brownian motion in a set of levels can be recovered by integrating local time over those levels. The proof must justify integrating Tanaka’s formula with respect to the level, including the integrability of the local-time term.

Work on a filtered probability space $(\Omega,\mathcal{F},(\mathcal{F}_t)_{t\ge0},\mathbb{P})$ carrying a standard Brownian motion $B_t$ with $B_0=0$. Every stochastic integral below is an Itô integral. Its integrand is progressively measurable and belongs to $\mathcal{L}^2$ on the time interval in question: that is, $\mathbb{E}\int_0^T H_s^2\,ds<\infty$ for every finite $T$.

Use the local-time normalization from Tanaka’s formula: for each fixed $a\in\mathbb{R}$, $L_t^a$ is nonnegative and

|B_t-a|=|a|+\int_0^t \operatorname{sgn}(B_s-a)\,dB_s+L_t^a, \qquad \operatorname{sgn}(0)=0.

Here the stochastic integral is well-defined because its progressively measurable integrand is bounded by $1$, so its expected integrated square on $[0,T]$ is at most $T$. It is a square-integrable martingale: the Itô integral has conditional mean zero for its increments, by the corresponding property for simple adapted integrands and passage to the $L^2$ limit. Thus its expectation is zero. Tanaka’s formula is the result established in the earlier material on Tanaka’s formula; the argument here derives the occupation identity from it.

Theorem: For each fixed $t\ge0$, almost surely, for every nonnegative Borel function $f:\mathbb{R}\to[0,\infty]$, $$ \int_0^t f(B_s)\,ds=\int_{\mathbb{R}} f(a)L_t^a\,da. $$ The equality is an equality of extended nonnegative integrals. It also holds for signed Borel $f$ whenever $\int_0^t |f(B_s)|\,ds<\infty$; in that case both sides are absolutely integrable and equal.

Integrability Before Integrating Tanaka’s Formula

First establish that local time is integrable over bounded sets of levels. Taking expectations in Tanaka’s formula for a fixed $a$ gives

\mathbb{E}L_t^a=\mathbb{E}|B_t-a|-|a|.

Nonnegativity of $L_t^a$ shows that this difference is nonnegative. The inequality $\big||x-a|-|a|\big|\le |x|$, applied with $x=B_t$, gives the upper bound $\mathbb{E}L_t^a\le\mathbb{E}|B_t|<\infty$. Let $K$ be a compact set. The local-time field is taken in its jointly measurable version, as in its construction. Tonelli’s theorem then yields

\mathbb{E}\int_K L_t^a\,da =\int_K\mathbb{E}L_t^a\,da \le |K|\,\mathbb{E}|B_t|<\infty.

Consequently, $\int_K L_t^a\,da<\infty$ almost surely. In particular, if $f$ is bounded and compactly supported, then $\int_{\mathbb{R}}|f(a)|L_t^a\,da<\infty$ almost surely. Indeed, if its support is contained in $K$, its expected value is at most $\|f\|_\infty |K|\mathbb{E}|B_t|$. This step makes the subsequent integration of Tanaka’s formula legitimate, including when $f$ takes both signs.

Proof for Continuous Test Functions

We first prove the identity for continuous, compactly supported $f:\mathbb{R}\to\mathbb{R}$. Define

g(x)=\int_{\mathbb{R}} f(a)|x-a|\,da.

Since $f$ is continuous and compactly supported, differentiation under the integral gives $g'(x)=\int_{\mathbb{R}} f(a)\operatorname{sgn}(x-a)\,da$. The value of the sign at $a=x$ does not affect this Lebesgue integral. Differentiating once more gives $g''(x)=2f(x)$. Also $g'$ is bounded by $\int_{\mathbb{R}}|f(a)|\,da$, so the Itô integral with integrand $g'(B_s)$ belongs to $\mathcal{L}^2$ on every finite time interval.

Proof. Integrate Tanaka’s formula over $a$, multiplying by $f(a)$. The absolute-value terms are integrable because $f$ has compact support, and the local-time term is absolutely integrable almost surely by the preceding estimate. The stochastic terms can be interchanged using the stochastic Fubini theorem. Its integrability condition holds here: for every $a$, the integrand $\operatorname{sgn}(B_s-a)$ has expected integrated square at most $t$, and $\int_{\mathbb{R}} |f(a)|\sqrt{t}\,da<\infty$. The resulting integrand $\int f(a)\operatorname{sgn}(B_s-a)\,da=g'(B_s)$ is progressively measurable and bounded, hence is in $\mathcal{L}^2$. Tanaka’s formula holds for each fixed $a$; joint measurability and Fubini’s theorem allow its use for almost every pair $(\omega,a)$, which is sufficient for this integration. We obtain $$ g(B_t)-g(0)=\int_0^t g'(B_s)\,dB_s+\int_{\mathbb{R}}f(a)L_t^a\,da. $$ Apply Itô’s formula to $g(B_t)$. Its derivatives are $g'$ and $g''=2f$, and its quadratic-variation correction is $\tfrac12g''(B_s)\,ds=f(B_s)\,ds$, since $dB_s\,dB_s=ds$. Thus $$ g(B_t)-g(0)=\int_0^t g'(B_s)\,dB_s+\int_0^t f(B_s)\,ds. $$ Comparing the two equalities and cancelling their common Itô integral proves $\int_0^t f(B_s)\,ds=\int_{\mathbb{R}}f(a)L_t^a\,da$. $\square$

Extending the Identity to Borel Functions

To obtain a statement for all Borel functions on one event of probability one, it is useful to identify measures rather than intersect uncountably many probability-one events. For fixed $t$, define the occupation measure $\mu_t$ by $\mu_t(A)=\int_0^t\mathbf{1}_A(B_s)\,ds$ for Borel $A$. It is a finite measure of total mass $t$. Define $\nu_t(A)=\int_A L_t^a\,da$; the local integrability estimate shows that $\nu_t$ is almost surely finite on compact sets, so it is a locally finite Borel measure.

Proof. For each continuous compactly supported $f$, the preceding argument gives $\int f\,d\mu_t=\int f\,d\nu_t$ almost surely. Choose a countable family of continuous compactly supported functions that is uniformly dense, on each compact interval, among continuous functions supported in a slightly larger compact interval. Such a family can be formed from piecewise linear functions with rational breakpoints and rational values. Intersecting the probability-one events for this countable family still gives an event of probability one. On that event, local finiteness allows uniform approximation on each compact set: the error in either integral is bounded by the uniform approximation error times the measure of that compact set. Hence the integrals agree for every continuous compactly supported function. Locally finite Borel measures on $\mathbb{R}$ that agree on all such functions are equal, so $\mu_t=\nu_t$. Integrating any nonnegative Borel $f$ against these equal measures proves the asserted extended-integral identity. For signed $f$, apply the nonnegative result to its positive and negative parts; if $\int |f|\,d\mu_t<\infty$, then $\int |f|\,d\nu_t<\infty$ as well, and subtraction is valid. $\square$

The theorem is stated for each fixed $t$. This proof does not assert that the same probability-one event works simultaneously for every real $t$; such a simultaneous version requires additional path-regularity arguments.

Worked Interval and Weighted Occupation Identities

Worked Example: Time in an Interval

Let $u<v$ be real numbers and $t\ge0$. Apply the formula to $f(a)=\mathbf{1}_{[u,v]}(a)$. The left side is the amount of time that $B_s$ lies in the closed interval, and the right side is the local-time mass of that interval:

\int_0^t \mathbf{1}_{[u,v]}(B_s)\,ds =\int_u^v L_t^a\,da.

The open interval $(u,v)$ gives the same result. Indeed, the difference between the two time integrals is bounded by the time spent at the two endpoint levels. The occupation identity applied to either singleton gives $\int_0^t\mathbf{1}_{\{u\}}(B_s)\,ds=\int_{\{u\}}L_t^a\,da=0$, since a singleton has Lebesgue measure zero; the same holds for $v$. Thus endpoint inclusion does not change the occupation time. The strictness in the interval test is immaterial in this instance, not an assumed convention.

Worked Example: Two Disjoint Intervals

Suppose $u<v<w<z$. The half-open intervals $[u,v)$ and $[w,z)$ are disjoint, so their indicator functions add to the indicator of their union. Applying the formula and splitting the level integral gives

\int_0^t\mathbf{1}_{[u,v)\,\cup\,[w,z)}(B_s)\,ds =\int_u^v L_t^a\,da+\int_w^z L_t^a\,da.

To check the endpoint convention, replacing either half-open interval by its closed version can only add time spent at its right endpoint. Each such level has zero occupation time by the singleton calculation in the previous example. The local-time integrals over the endpoints themselves are also zero. Thus the formula agrees with the direct decomposition into the two disjoint time-occupation sets.

Worked Example: A Weighted Occupation Time

Consider the signed weight $f(a)=a\mathbf{1}_{[-1,1]}(a)$. It is bounded and compactly supported, so both sides are integrable. The formula gives

\int_0^t B_s\mathbf{1}_{[-1,1]}(B_s)\,ds =\int_{-1}^{1}aL_t^a\,da =\int_0^1 aL_t^a\,da-\int_{-1}^0(-a)L_t^a\,da.

The last equality separates positive and negative levels: on $[-1,0]$, $a=-(-a)$, which accounts for the minus sign. As a check on the sign, if the weight is replaced by $-a\mathbf{1}_{[-1,1]}(a)$, both sides are multiplied by $-1$. This example also illustrates why the signed version requires absolute integrability before the positive and negative contributions are subtracted.

Worked Example: Total Occupation and a Single Level

Take $f(a)=1$ on all of $\mathbb{R}$. The measure identity applies even though this function is not compactly supported. Since $B_s\in\mathbb{R}$ for every $s$, its time integral is $\int_0^t 1\,ds=t$. Therefore

\int_{\mathbb{R}} L_t^a\,da=t.

Now take $f(a)=\mathbf{1}_{\{c\}}(a)$ for any fixed $c\in\mathbb{R}$. The level integral is zero because $\{c\}$ has Lebesgue measure zero, so $\int_0^t\mathbf{1}_{\{c\}}(B_s)\,ds=0$. The membership test is equality $B_s=c$; the conclusion is that this event occupies zero Lebesgue time almost surely, not that Brownian motion never visits $c$.

Why the Formula Matters—and a Common Pitfall

The formula converts a time integral along a random path into an ordinary integral over spatial levels. Its interval case is particularly useful: it translates a question about how long the path lies in a region into the local-time profile across that region. The measure formulation also clarifies the scope of the identity. Nonnegative Borel functions are allowed with infinite values on either side; for signed functions, absolute integrability is what makes subtraction legitimate.

Common pitfall: integrating before checking integrability. A tempting but incomplete argument is to multiply Tanaka’s formula by a signed $f(a)$ and integrate immediately. That has not yet shown that $\int |f(a)|L_t^a\,da$ is finite, so the local-time term may not be defined as a finite signed integral. The correction is to take expectations in Tanaka’s formula first, obtain $\mathbb{E}L_t^a\le\mathbb{E}|B_t|$, and use Tonelli on the compact support of $f$. This proves the required almost-sure local integrability before any signed integration is performed.

A related distinction is that $L_t^a$ is a density with respect to the level variable $a$, not the amount of time spent exactly at level $a$. The latter is zero for each fixed $a$; positive occupation over an interval is obtained by integrating the density across that interval.

Check Your Understanding

Use the measure identity and the local-time normalization stated above.

Write the occupation-time identity for the half-open interval $[u,v)$, where $u<v$, and explain why including $v$ does not change it.
Why is it necessary to establish local integrability of $L_t^a$ before integrating Tanaka’s formula against a signed compactly supported function?
For a Borel set $A$, express the time Brownian motion spends in $A$ using local time.
What does the occupation formula imply about the time Brownian motion spends at one fixed level $c$? Does it imply that the path never visits $c$?
Use $f(a)=1$ to state the total mass of the local-time profile over all levels.