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.

Two-sided Brownian exit probability

Statement

Assume the Axiom of Choice. Let B be a standard Brownian motion Brownian motion, let a<x<b be reals, and let Px be the law of the shifted, everywhere-continuous process t↦x+B^t Brownian motion started at x, on canonical continuous path space with its compact-open Borel sigma-algebra. Here B^ is the normalized zero-start representative specified in that definition. For c∈R let Tc:=inf⁡{t≥0:Zt=c} be the hitting time of the level c for the coordinate process Z of the shifted law. Then Px(Tb<Ta)=x−ab−a.

Facts & Assumptions

Given: AC, a standard Brownian motion, reals a<x<b, and the shifted law Px. In the proof write B for its everywhere-continuous zero-start representative B^ and use that representative's own raw natural filtration and usual augmentation. No adaptation to a former raw filtration is claimed.

[F1]

For the shifted law Px, hitting times satisfy Px(Tc<∞)=P(Tc−x<∞) and Px(Tb<Ta)=P(Tb−x<Ta−x), because the shifted process is x+B. Brownian motion started at x

[F2]

One-dimensional Brownian motion hits every level almost surely: P(Tc<∞)=1 for every c. One-dimensional Brownian motion hits every point almost surely

[F3]

The hitting time of a closed set for the normalized everywhere-continuous B is a stopping time for its raw natural filtration and its usual augmentation. The maximum MN=sup⁡s≤NBs has the same law as ∣BN∣ for N>0. Hence EMN=E∣BN∣≤EBN2=N. The same argument applies to −B, which is Brownian by symmetry of its Gaussian increments. Since B0=0, sup⁡s≤N∣Bs∣≤sup⁡s≤NBs+sup⁡s≤N(−Bs), whose expectation is at most 2N. The suprema are measurable rational-time suprema by continuity; N=0 gives zero directly. Brownian closed-set hitting times are stopping times Law of the Brownian maximum Standard normal and normal laws Cauchy-Schwarz for random variables Brownian motion

[F4]

Strong Markov: for an a.s. finite stopping time τ of the usual augmentation, the increment process (Bτ+t−Bτ)t≥0 is a Brownian motion independent of Fτ. Strong Markov property of Brownian motion Continuous-time stopping times and stopped sigma-algebras Natural and usual augmented Brownian filtrations

[F6]

Dominated convergence and monotone convergence pass limits through integrals. Dominated convergence Monotone convergence for the integral

[F7]

AC supplies the conditional-expectation and strong-Markov interfaces. The Axiom of Choice Wiener measure on continuous path space

Proof

technique · direct
1.1F1F2F3given

By [F1] it suffices to prove the case a<0<b with the unshifted law: Px(Tb<Ta)=P(Tb−x<Ta−x) and (x−a)/(b−a)=(0−(a−x))/((b−x)−(a−x)), since (b−x)−(a−x)=b−a and a−x<0<b−x. So assume a=A<0<B=b and put T:=TA∧TB. Then T≤TA<∞ almost surely by [F2], and T is a stopping time of the usual augmentation because {A,B} is closed, by [F3]. For every u<T the path satisfies Bu∈(A,B), since leaving (A,B) would require hitting A or B by continuity.

1.2F3F4F5F6

By [F4] applied at the a.s. finite stopping time T, the process Wt=BT+t−BT on {T<∞} and Wt=0 otherwise is an everywhere-continuous zero-start Brownian motion independent of FT, using the supplier's measurable random-time convention. Consequently, for every FT-measurable random variable R with values in [0,N] one has E[WR ∣ FT]=0 almost surely. Indeed, if R is countably valued with values rj∈[0,N], then WR=∑jWrj1{R=rj} and for G∈FT one has ∫GWR dP=∑jP(G∩{R=rj}) EWrj=0, because G∩{R=rj}∈FT is independent of Wrj and EWrj=0; for general R the dyadic ceilings Rk:=min⁡(2−k⌈2kR⌉,N) decrease to R, so WRk→WR almost surely and ∣WRk∣≤S:=sup⁡[0,N]∣W∣, whose expectation is finite by [F3]; dominated convergence [F6] gives ∫GWR dP=lim⁡k∫GWRk dP=0 for every G∈FT, and [F5]'s uniqueness identifies E[WR∣FT]=0.

2.1F5step 1.2

Fix M>max⁡{∣A∣,∣B∣} and let R=M−T on {T≤M} and R=0 otherwise. This is an FT-measurable random variable with values in [0,M]: T is FT-measurable since {T≤r}∩{T≤u}={T≤min⁡(r,u)}∈Fu. No product 0⋅∞ is used. On {T≤M} one has BM−BT=WM−T=WR, and on {T>M} both BM−BT∧M and WR=W0 vanish; hence BM−BT∧M=WR. All terms are integrable: BM is Gaussian, WR is bounded in absolute value by its integrable finite-horizon supremum, and the identity gives integrability of BT∧M. Taking expectations and using step 1.2 with [F5]'s tower identity, E[BM−BT∧M]=0, so E[BT∧M]=E[BM]=0, the last equality because the law of BM is the centered N(0,M).

3.1F6step 1.1step 2.1

Let M→∞. Set BT=0 on the null event T=∞, as in the strong-Markov convention. The random variables BT∧M converge almost surely to BT because T<∞ almost surely and the paths are continuous, and they are bounded by max⁡{∣A∣,∣B∣}: for t<T the value Bt lies in (A,B) by step 1.1, and BT∈{A,B}. Dominated convergence [F6] therefore gives E[BT]=0.

4.1step 3.1

The events {TB<TA} and {TA<TB} are disjoint and their union is almost surely the whole space, because T<∞ almost surely and TA≠TB almost surely (the path cannot be at two distinct levels at one time). On the first event BT=B and on the second BT=A, so 0=E[BT]=B P(TB<TA)+A (1−P(TB<TA)); solving gives P(TB<TA)=−A/(B−A).

5.1step 1.1step 4.1

Undoing the shift with step 1.1, Px(Tb<Ta)=P(Tb−x<Ta−x)=−(a−x)(b−x)−(a−x)=x−ab−a, which is the assertion.

6.1F4F7givenstep 4.1∎

The endpoint cases are covered: the strict inequalities a<x<b keep Ta and Tb distinct from the starting level; the truncation parameter M is chosen larger than both endpoints and then sent to infinity in step 3.1; the case A=B is excluded because a<b; and TA=TB is the null event excluded in step 4.1. AC is used only through [F7] in the conditional-expectation and strong-Markov interfaces.

Source notes

Durrett, Theorem 7.5.3, proves the complementary lower-exit formula by bounded stopping and bounded convergence. Solving its endpoint expectation identity gives the stated upper-exit formula. The proof above instead verifies the centered martingale identity E[BT]=0 through the strong Markov restart at T, which keeps every step within the stopping-time and maximum machinery already established on this page.

Depends on

Used by

Dependency tree · two levels

92 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