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.
Distribution of a one-sided Brownian hitting time
Statement
Assume the Axiom of Choice, let be a standard Brownian motion Brownian motion. Use the everywhere-continuous, zero-start representative of Law of the Brownian maximum: replace paths by zero outside a measurable probability-one event of continuity and zero start, retaining the notation . Let and , with . This is a measurable -valued hitting time for this representative; its distribution does not depend on the chosen full-measure event. With the standard normal distribution function Standard normal and normal laws Cumulative distribution function of a real random variable, and on the law of has the density Moreover , so is finite almost surely and there is no mass at infinity, and .
Facts & Assumptions
Given: AC, a standard Brownian motion in this everywhere-continuous zero-start representative, and .
For the representative in the statement, is a finite measurable random variable and for (Law of the Brownian maximum). The closed-set hitting-time lemma applies to an everywhere-continuous Brownian process with its own natural filtration (Brownian closed-set hitting times are stopping times). Brownian motion supplies a measurable full-measure continuity and zero-start event (Brownian motion).
Limits of the standard normal distribution function: , and is continuous, and for ; . Standard normal and normal laws Cumulative distribution function of a real random variable The standard normal density has total mass one
Substitution on compact intervals for the continuous integrand , and monotone convergence for the limits at the endpoints. Substitution: if is differentiable on with integrable and is continuous on an interval containing , then Monotone convergence for the integral. The compact integrals agree with their Lebesgue counterparts under Countable Choice. A bounded Riemann integrable function on a closed bounded interval is Lebesgue measurable and has the same integral
A probability measure on is determined by its distribution function; countable choice, which AC supplies, is used there. Probability laws correspond to distribution functions The Axiom of Countable Choice () The Axiom of Choice
Closed bounded real intervals are compact, a continuous function attains its maximum on a nonempty compact set, and the intermediate value theorem holds on real intervals (Heine-Borel by bisection: every closed bounded interval is compact, Extreme value theorem: a continuous real function on a nonempty compact subset of attains a greatest and a least value, Intermediate value theorem, by bisection with a canonical left-half rule: a continuous function on takes every value between and ). A nonnegative measurable density defines a measure by integration (The indefinite integral of a nonnegative measurable function is a measure).
Proof
Fix the measurable full-measure event specified in the statement. Replacing the original path by zero on preserves every finite-dimensional law and makes every path continuous with . Each coordinate remains measurable because is measurable. Two such choices agree on the intersection of their events, so the resulting measurable hitting times agree there and have the same distribution. By [F1] applied to the closed singleton , is a stopping time for the chosen process's own raw natural filtration, hence an extended nonnegative measurable random variable. No stopping-time claim for the original raw filtration is used.
Define for . For , the substitution on , whose derivative is continuous and is continuous, gives by oriented substitution, the compact Riemann/Lebesgue bridge, and the density-integral identity for increments of .
For , if , the first hit is attained by continuity (as in the closed-set hitting lemma), so . Conversely gives a time with by [F5]; since , the intermediate value theorem gives a hit by time . Hence as exact measurable events for this representative. Continuity at zero also gives on every path, since .
The normal CDF obeys , by its density bound, hence is continuous. Symmetry and total mass one give ; monotone convergence of density integrals gives as . Put for . The measurable events increase to , so [F3] and [F1] give . Thus , and step 2.1 yields . Taking integer and monotone convergence of the events gives .
Let in step 1.2 and let integers tend to infinity. The nonnegative integrals increase to , and , so . Letting integer now gives .
Extend by zero on . It is nonnegative Borel measurable, and [F5] and step 4.1 make its density measure a Borel probability measure on . To use [F4] with a real random variable, replace by the value on its measurable null event, obtaining . This leaves every finite-time distribution probability unchanged, and by step 2.1. The density measure and have CDF zero for nonpositive arguments, and the same CDF at every positive argument by step 4.1. Thus [F4] identifies the laws. In particular the original extended hitting time has density on , no atom there or at zero, and no mass at infinity.
The parameter and compact substitution bounds ensure every denominator is positive. At , step 2.1 gives . The infinity limit and total density mass were proved in steps 3.1 and 4.1. AC supplies the Countable Choice hypotheses of both the compact integration bridge and [F4], and the Brownian and hitting-time suppliers. The event equality uses the declared continuous representative throughout.
The proof combines the Brownian maximum law with an exact continuous-path hitting identity. It computes the density integral by compact substitution, the Riemann/Lebesgue bridge and monotone limits, then identifies probability laws through their CDFs on all real arguments.
Depends on
- Law of the Brownian maximum
- Brownian closed-set hitting times are stopping times
- Standard normal and normal laws
- Cumulative distribution function of a real random variable
- The standard normal density has total mass one
- Brownian motion
- 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'$
- Monotone convergence for the integral
- Probability laws correspond to distribution functions
- The Axiom of Countable Choice ($\mathrm{AC}_\omega$)
- The Axiom of Choice
- A bounded Riemann integrable function on a closed bounded interval is Lebesgue measurable and has the same integral
- Extreme value theorem: a continuous real function on a nonempty compact subset of $\mathbb{R}$ attains a greatest and a least value
- Intermediate value theorem, by bisection with a canonical left-half rule: a continuous function on $[a,b]$ takes every value between $f(a)$ and $f(b)$
- Heine-Borel by bisection: every closed bounded interval $[a,b]$ is compact
- The indefinite integral of a nonnegative measurable function is a measure
Used by
Dependency tree · two levels
111 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
- Rick Durrett, Probability: Theory and Examples, fifth edition, equation (7.4.6) after Example 7.4.2 (standard reference, not scraped)
- Gregory F. Lawler, Stochastic Calculus: An Introduction with Applications, Example 2.7.1 (standard reference, not scraped)