How statement and proof provenance work
The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.
- Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
- AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
- AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.
These labels describe origin, not correctness: citations and verification chips remain separate evidence.
Brownian positive occupation time has the arcsine law
Statement
Let be a standard Brownian motion Brownian motion, choose its all-path continuous jointly measurable version , and for let be the occupation time of the positive half-line up to time . Then for every , and has the arcsine density Thus the occupation-time proportion of Brownian motion has the same distribution as the last-zero proportion of the theorem The last Brownian zero has the arcsine law, although the two random variables are of a different nature.
Facts & Assumptions
Given: AC, a standard Brownian motion with its all-path continuous jointly measurable version , , and reals .
With the function satisfies , and its defining integral is an -integral against the occupied time. Brownian step-potential resolvent at zero
Every path of is continuous and the evaluation is jointly measurable, so is measurable and is a random variable with . Any two such jointly measurable indistinguishable versions give the same occupation time almost surely by Tonelli. Brownian motion has a jointly measurable continuous version Tonelli's theorem for nonnegative measurable functions on a sigma-finite product
Scaling: for the process is again standard Brownian motion, so the occupation times satisfy . Brownian scaling
Tonelli for nonnegative product-measurable integrands. Tonelli's theorem for nonnegative measurable functions on a sigma-finite product
Substitution and the principal inverse tangent: and is the inverse bijection of . Substitution: if is differentiable on with integrable and is continuous on an interval containing , then Principal arctangent: derivative, integral, power series, and the Gregory–Leibniz series The principal inverse tangent
Stone-Weierstrass: the unital point-separating algebra of polynomials is uniformly dense in . Real Stone–Weierstrass theorem for compact Hausdorff spaces
Dominated convergence justifies interchanging limits with expectations and integrals under an integrable dominating function. Dominated convergence
AC is the ambient assumption of the Brownian and resolvent interfaces. The Axiom of Choice
Proof
By [F2], is a random variable with values in ; by [F3] applied with one has , because the time change maps the set of positive times for to the corresponding set for the scaled motion, and hence has the law of .
The probability measure on with density satisfies for all : substituting turns the integral into , then turns it into , and finally and [F5] give .
For , : [step 1.1] gives , so the left side is , and [F4] equals it to , the integrand being nonnegative and .
For and one has up to the single point , which is Lebesgue-null; hence the function of [F1] satisfies , and [F1] with [step 2.1] yields for all .
The law of and have the same moments: fixing and expanding for and , uniformly on the square, [F7] shows that and for every such ; since [step 3.1] and [step 1.2] make the two sides equal for all , subtracting the two power series gives on an interval, so every coefficient vanishes and all moments agree.
Consequently for every continuous : given , [F6] supplies a polynomial with , and by [step 4.1]; taking continuous and applying [F7] to both sides gives for .
By [step 1.1], for every and , which is the displayed distribution function.
Differentiating the distribution function on gives ; this density is integrable on (substitute ), so it is the density of and both endpoints carry zero mass.
The boundary cases are covered: gives and gives ; the value of the substitution is the endpoint of the principal branch of [F5]; the parameters satisfy in [step 3.1] and in [step 4.1]; the occupation time is taken over the half-line so the single instant is excluded by a null set; and AC enters only through [F8].
Source notes
Yoshida, Proposition 6.8.4, obtains the occupation-time arcsine law from the Laplace transform produced by the step-potential resolvent of Lemmas 6.8.1-6.8.3. The proof above proves the same transform identity directly from the resolvent lemma of this page, identifies the arcsine law as the unique probability measure on with that transform by moment matching and Stone-Weierstrass, and transfers the result from to by scaling.
Depends on
- Brownian step-potential resolvent at zero
- Brownian motion has a jointly measurable continuous version
- Brownian scaling
- Tonelli's theorem for nonnegative measurable functions on a sigma-finite product
- Substitution: if $\varphi$ is differentiable on $[c,d]$ with $\varphi'$ integrable and $f$ is continuous on an interval containing $\varphi([c,d])$, then $\int_{\varphi(c)}^{\varphi(d)} f = \int_c^d (f\circ\varphi)\,\varphi'$
- Principal arctangent: derivative, integral, power series, and the Gregory–Leibniz series
- The principal inverse tangent $\arctan:\mathbb R\to(-\pi/2,\pi/2)$
- Real Stone–Weierstrass theorem for compact Hausdorff spaces
- Dominated convergence
- The Axiom of Choice
- Brownian motion
- The last Brownian zero has the arcsine law
Used by
Nothing in the library uses this result yet.
Dependency tree · two levels
87 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.
Sources
- Nobuo Yoshida, Probability Theory, Proposition 6.8.4, printed pp. 216-217 (standard reference, not scraped)