Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedaudited 2026-09-22
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 B be a standard Brownian motion Brownian motion, choose its all-path continuous jointly measurable version B^, and for t>0 let At:=0t1{B^s>0}ds be the occupation time of the positive half-line up to time t. Then for every 0x1, P(Attx)=2πarcsinx, and At/t has the arcsine density f(x)=1πx(1x),0<x<1. 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 B with its all-path continuous jointly measurable version B^, t>0, and reals α,β>0.

[F1]

With V=α+β1{y>0} the function u(x)=0E[exp(0tV(x+B^r)dr)]dt satisfies u(0)=1/α(α+β), and its defining integral is an E-integral against the occupied time. Brownian step-potential resolvent at zero

[F2]

Every path of B^ is continuous and the evaluation is jointly measurable, so s1{B^s>0} is measurable and At=0t1{B^s>0}ds is a random variable with 0Att. 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

[F3]

Scaling: for c>0 the process rc1/2Bcr is again standard Brownian motion, so the occupation times satisfy At=dtA1. Brownian scaling

[F4]

Tonelli for nonnegative product-measurable integrands. Tonelli's theorem for nonnegative measurable functions on a sigma-finite product

[F6]

Stone-Weierstrass: the unital point-separating algebra of polynomials is uniformly dense in C([0,1],R). Real Stone–Weierstrass theorem for compact Hausdorff spaces

[F7]

Dominated convergence justifies interchanging limits with expectations and integrals under an integrable dominating function. Dominated convergence

[F8]

AC is the ambient assumption of the Brownian and resolvent interfaces. The Axiom of Choice

Proof

technique · direct
1.1

By [F2], At is a random variable with values in [0,t]; by [F3] applied with c=t one has At=dtA1, because the time change maps the set of positive times for B to the corresponding set for the scaled motion, and hence At/t has the law of A1.

givenF2F3
1.2

The probability measure μ on [0,1] with density π1x1/2(1x)1/2 satisfies 01(α+βx)1μ(dx)=1/α(α+β) for all α,β>0: substituting x=sin2θ turns the integral into 2π0π/2(α+βsin2θ)1dθ, then s=tanθ turns it into 2π0dt/(α+(α+β)t2), and finally w=t(α+β)/α and [F5] give 2π1α(α+β)π2.

givenF5
2.1

For α,β>0, 0eαtE[eβAt]dt=E[(α+βA1)1]: [step 1.1] gives E[eβAt]=E[eβtA1], so the left side is 0E[e(α+βA1)t]dt, and [F4] equals it to E[0e(α+βA1)tdt]=E[1/(α+βA1)], the integrand being nonnegative and α+βA1α>0.

step 1.1F4
3.1

For V=α+β1{y>0} and t>0 one has 0tV(B^r)dr=αt+βAt up to the single point r=0, which is Lebesgue-null; hence the function u of [F1] satisfies u(0)=0eαtE[eβAt]dt, and [F1] with [step 2.1] yields E[1/(α+βA1)]=1/α(α+β) for all α,β>0.

step 2.1F1F2
4.1

The law of A1 and μ have the same moments: fixing α=1 and expanding 1/(1+βx)=k0(βx)k for x[0,1] and 0<β<1, uniformly on the square, [F7] shows that E[1/(1+βA1)]=k(β)kE[A1k] and (1+βx)1μ(dx)=k(β)kxkμ(dx) for every such β; since [step 3.1] and [step 1.2] make the two sides equal for all β(0,1), subtracting the two power series gives k(β)k(E[A1k]xkμ(dx))=0 on an interval, so every coefficient vanishes and all moments agree.

step 3.1step 1.2F7
5.1

Consequently E[f(A1)]=fdμ for every continuous f:[0,1]R: given ε>0, [F6] supplies a polynomial p with fp<ε, and E[f(A1)]fdμ2ε+E[p(A1)]pdμ=2ε by [step 4.1]; taking continuous fn1[0,x] and applying [F7] to both sides gives P(A1x)=μ([0,x])=2πarcsinx for 0x1.

step 4.1F6F7
6.1

By [step 1.1], P(At/tx)=P(A1x)=2πarcsinx for every t>0 and 0x1, which is the displayed distribution function.

step 1.1step 5.1
7.1

Differentiating the distribution function on (0,1) gives ddx2πarcsinx=2π12x(1x)=1πx(1x); this density is integrable on (0,1) (substitute x=sin2θ), so it is the density of At/t and both endpoints carry zero mass.

step 6.1F5
8.1

The boundary cases are covered: x=0 gives P(A1=0)=0=2πarcsin0 and x=1 gives 1=2πarcsin1=2ππ2; the value θ=π/2 of the substitution is the endpoint of the principal branch of [F5]; the parameters satisfy α,β>0 in [step 3.1] and 0<β<1 in [step 4.1]; the occupation time is taken over the half-line {y>0} so the single instant s=0 is excluded by a null set; and AC enters only through [F8].

step 3.1step 4.1step 7.1F5F8given

Source notes

Yoshida, Proposition 6.8.4, obtains the occupation-time arcsine law from the Laplace transform E[1/(α+βA1)]=1/α(α+β) 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 [0,1] with that transform by moment matching and Stone-Weierstrass, and transfers the result from A1 to At by scaling.

Depends on

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