Alphabeta Math
ExampleConstruction: Literature-sourcedVerification: 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.

A Brownian hitting time has infinite mean

Example

Assume the Axiom of Choice and let B be a standard Brownian motion Brownian motion. Use the everywhere-continuous, zero-start representative fixed in Distribution of a one-sided Brownian hitting time: replace the path by zero outside a measurable probability-one event of continuity and zero start, retaining the notation B. Let a>0 and τa=inf⁡{t≥0:Bt=a}, with inf⁡∅=+∞. Then τa is a measurable extended random variable and τa<∞ almost surely, while E[τa]=∫0∞t g(t) dt=+∞,g(t)=a(2πt3)1/2e−a2/(2t). Thus almost-sure finiteness does not imply integrability for this random time.

Facts & Assumptions

Given: AC, a standard Brownian motion B in the stated everywhere-continuous zero-start representative, and a>0.

[F1]

For the representative fixed in the statement, τa is measurable and finite almost surely, and on t>0 its law has the displayed density g. One-dimensional Brownian motion hits every point almost surely Distribution of a one-sided Brownian hitting time

[F2]

For a nonnegative random variable with a density, the expectation is the integral of t against that density; integration against a density is integration of the product with the density. Expectation of a nonnegative or integrable random variable Integrating against a density agrees with integrating the product

[F3]

Monotone convergence applies to nonnegative integrands. Monotone convergence for the integral

[F4]

AC is the standing hypothesis under which the Brownian and hitting-time interfaces in [F1] are supplied; this expectation calculation makes no additional selection. The Axiom of Choice

Verification

technique · direct
1.1F1F2given

Since τa≥0 and its law has density g by [F1], [F2] gives E[τa]=∫0∞t g(t) dt=a(2π)−1/2∫0∞t−1/2e−a2/(2t) dt, the last integrand being nonnegative.

2.1algebra

For t≥a2 the exponent satisfies a2/(2t)≤1/2, so e−a2/(2t)≥e−1/2; hence the integrand in step 1.1 is bounded below on [a2,∞) by a(2π)−1/2e−1/2 t−1/2.

3.1F3step 1.1step 2.1

For every integer j≥0, on Ij=[2ja2,2j+1a2] one has t−1/2≥(2j+1a2)−1/2, so ∫Ijt−1/2dt≥a2(j−1)/2. These lower bounds do not tend to zero and their partial sums diverge. Monotone convergence over the increasing finite unions of the Ij, together with step 2.1, therefore gives ∫0∞t−1/2e−a2/(2t)dt=+∞ and hence E[τa]=+∞.

4.1F1F4givenstep 3.1∎

The comparison with finite almost-sure values is the point of the example: [F1] gives τa<∞ almost surely, so the random variable is finite-valued almost surely while its expectation is infinite; the divergence comes from the polynomial tail t−1/2 of the first-moment integrand and not from any exceptional path. The cases a=0 (where τ0=0) and a<0 are excluded by the hypothesis a>0. AC is used only through [F4].

Source notes

Lawler, Section 2.7, evaluates the first-passage density and records the divergent first moment; Durrett, equation (7.4.6), gives the same density. The example avoids any integration-by-parts argument and bounds the first-moment integrand directly.

Depends on

Used by

Dependency tree · two levels

45 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