Alphabeta Math
LemmaStatement: 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.

Planar Brownian annular exit probability

Statement

Assume the Axiom of Choice. Let Px be the shifted planar Brownian law on canonical continuous path space Brownian motion started at x, and let Z be its coordinate process. For x,yR2 with xy and 0<ε<xy<R, let Sε:=inf{t0:Zty=ε},TR:=inf{t0:Zty=R}, and let H:=inf{t0:Zty(ε,R)}. Then Px(Sε<TR)=logRlogxylogRlogε.

Facts & Assumptions

Given: AC, the continuous coordinate process Z under Px, xy in R2 and 0<ε<xy<R.

[F1]

Under Px, Z0=x almost surely, the increments of Z over [s,t] have law N2(0,(ts)I2) and are independent of the raw coordinate past, and each process ZiZ0i is a standard one-dimensional Brownian motion. Every coordinate path is continuous. d-dimensional Brownian motion Brownian motion started at x

[F2]

One-dimensional Brownian motion hits every level almost surely. The stopping-time definition uses exact events; the required event identities are proved in step 1.1. The conditioning lemma gives E[h(X,Y)G]=H(X) for a known state X and independent noise Y, H(x)=h(x,y)μ(dy). One-dimensional Brownian motion hits every point almost surely Conditioning a known state and independent noise Continuous-time stopping times and stopped sigma-algebras

[F3]

N2(0,I2) is the law of a pair of independent standard normal coordinates, whose one-dimensional density φ is positive with φ=1 and finite second moment. In particular EGi< follows from u1+u2. Gaussian even moments for Brownian increments Multivariate normal law, including singular covariance Standard normal and normal laws

[F5]

Optional sampling for bounded discrete stopping times: for a martingale Y with E[Yk+1Gk]=Yk and stopping times 0στ bounded by N, E[Yτ]=E[Yσ]; a discrete martingale is defined by its adjacent conditional means, and the discrete stopped sigma-algebra is defined by the events {τk}. Martingale submartingale and supermartingale Optional sampling for bounded stopping times Continuous-time filtrations and all-pairs martingales

[F7]

Full AC supplies the Brownian and conditional-expectation interfaces and the inherited Countable Choice in the compact Riemann-to-Lebesgue bridge. The Axiom of Choice Brownian motion

Proof

technique · direct
1.1

Put as=Zsy. Every path is continuous. For t0, compact attainment and rational approximation give {Ht}=m1q(Q[0,t]){t}{aq<ε+1/m or aq>R1/m}. The reverse inclusion follows since the continuous nonnegative distance of as to the closed set (,ε][R,) then has minimum zero on [0,t]. Similarly, for c=ε or R, its circle hitting time has event m1q(Q[0,t]){t}{aqc<1/m}. These countable events are in the raw coordinate past, so all three times are stopping times and their comparisons are measurable. On the common probability-one event Z0=x, the initial radius is strictly between the boundaries. Continuity and the intermediate value theorem give H=SεTR, the boundary value ZHy{ε,R} when H<, and Zsy(ε,R) for s<H. These last claims are used only on that event.

F1F2F8given
1.2

Define ψ(r):=logr for r[ε,R] and extend it to a C2 function on [0,) with ψlogε on [0,ε/2], ψlogR on [2R,), and quintic Hermite splices on [ε/2,ε] and [R,2R] that match value, first and second derivative at both joints: on [ε/2,ε] use slogε+(logslogε)h(2s/ε1) and on [R,2R] use slogR+(logslogR)(1h(s/R1)), where h(θ)=6θ515θ4+10θ3 satisfies h=h=h=0 at θ=0 and h=1, h=h=0 at θ=1. Each splice agrees with the neighbouring branches in value and in its first two derivatives at both endpoints, so the resulting ψ is C2 with bounded first and second derivatives, and Φ(z):=ψ(zy) is then a bounded C2 function of zR2, constant near y and outside the disc of radius 2R, with Φ(z)=logzy for zy[ε,R]; its Laplacian ΔΦ(z)=ψ(r)+ψ(r)/r at r=zy>0 is continuous and bounded, and it vanishes on {εzyR} because Δlogzy=0 there.

F4algebra
1.3

For the standard normal pair G=(G1,G2) of [F3], every bounded C2 function f with bounded derivatives satisfies E[if(z+rG)Gi]=rE[i2f(z+rG)] for i=1,2 and r>0. Indeed, the law of G is the product of the two standard normal laws by [F3], so Fubini expresses the expectation as an iterated integral. Fix the other coordinate and integrate by parts in the chosen one-dimensional coordinate on [L,L] with the compact theorem of [F4] using φ=uφ and the bounded factor uif(z+r(uei+vej)), where ji and the other Gaussian coordinate v is fixed; the boundary terms vanish as L because φ decays rapidly and the derivative factor is bounded, and dominated convergence identifies the limit. On each finite interval the integrands are continuous, so [F8] identifies the compact integration-by-parts identity with its Lebesgue version. The bounds are independent of the fixed other coordinate; Fubini completes that coordinate integration. Summing the two coordinates gives E[f(z+rG)G]=rE[Δf(z+rG)].

F3F4F8
1.4

Let Gs:=σ(Zu:0us) be the raw coordinate filtration. For every bounded Borel g:R2R and 0st one has Ex[g(Zt)Gs]=Qtsg(Zs) almost surely: apply the conditioning lemma to the known state Zs and independent noise ZtZs.

F1F2given
2.1

The standard one-dimensional Brownian motion Z(1)x1 (zero-start almost surely) hits the level y1+Rx1 almost surely. At that time ZtyZt(1)y1=R, so H is no larger and is finite Px-almost surely.

F1F2step 1.1
2.2

Fix a bounded C2 function f with bounded first and second derivatives and put Qrf(z):=E[f(z+rG)]=f(z+u)μr(du) with μr the law of rG. Then rQrf(z) is differentiable on (0,) with ddrQrf(z)=12QrΔf(z): differentiating the expectation is licensed by the mean value theorem in [F8] and dominated convergence on a neighborhood bounded away from r=0, because f is bounded and G is integrable, and the resulting expression E[f(z+rG)G/(2r)] is 12E[Δf(z+rG)] by step 1.3.

F4F8step 1.3
3.1

Let f and Q be as in step 2.2. Continuity of Δf and bounded convergence imply that rQrΔf(z) is continuous, including at zero. For 0<δ<h, the fundamental theorem of calculus applied to the continuous integrand r12QrΔf(z) on [δ,h] gives 12δhQrΔf(z)dr=Qhf(z)Qδf(z) by step 2.2; [F8] identifies this compact calculus integral with the Lebesgue integral. Letting δ0, dominated convergence gives Qδf(z)f(z) because f is continuous and bounded, and the integrals converge by monotone convergence on the nonnegative and negative parts; hence Qhf(z)f(z)=120hQrΔf(z)dr for every h>0.

F4F8step 2.2
4.1

Define Mt:=Φ(Zt)Φ(Z0)120tΔΦ(Zr)dr. The map (r,ω)Zr(ω) restricted to [0,t] is B([0,t])Gt-measurable: finite deterministic grid approximations to the continuous paths, using only coordinates at times at most t, converge pointwise. Parameter integration therefore makes the drift integral Gt-measurable. Thus M is adapted, continuous on every path and integrable on each finite horizon, with Mt2Φ+(t/2)ΔΦ. For st and AGs, Fubini on the bounded finite-time integrands and step 1.4 give AstΔΦ(Zr)drdPx=A0tsQuΔΦ(Zs)dudPx. By step 3.1 the inner integral is 2(QtsΦ(Zs)Φ(Zs)), while step 1.4 gives AΦ(Zt)dPx=AQtsΦ(Zs)dPx. Thus A(MtMs)dPx=0, and M is a martingale.

F4F6step 1.2step 3.1step 1.4
5.1

Fix n1 and let Hn:=Hn. For each m1 put δ:=2m, define the discrete filtration Dk:=Gkδ and the discrete martingale Yk:=Mkδ, which satisfies E[Yk+1Dk]=Yk by [F5] and step 4.1. The integer-valued ceiling ρm:=2mHn is a stopping time for (Dk), since {ρmk}={Hnkδ}Gkδ=Dk by step 1.1, and it is bounded by 2mn. Applying [F5] with σ=0 and τ=ρm gives E[Mρmδ]=0.

F5step 1.1step 4.1
6.1

Expanding step 5.1 and letting m, ρmδHn and ZρmδZHn by continuity. Dominated convergence on [0,n+1] gives Ex[Φ(ZHn)]=Φ(x)+12Ex0HnΔΦ(Zr)dr. Since Zry(ε,R) for r<H, the integral vanishes, and Ex[Φ(ZHn)]=logxy.

F4step 1.1step 5.1
7.1

Define ZH by literal evaluation when H< and as y otherwise. This is measurable by finite-grid approximation to ZHn and passage to the limit on {H<}. Letting n, continuity and bounded convergence give Ex[Φ(ZH)]=logxy. Moreover H=SεTR and ZHy{ε,R} almost surely, so Φ(ZH)=logε on {Sε<TR} and logR on {TR<Sε}. The tie event can include paths with both times infinite, but it has Px-probability zero because H< almost surely; a finite tie is impossible when ε<R.

step 1.1step 2.1step 6.1
8.1

Therefore logxy=logεPx(Sε<TR)+logRPx(TR<Sε), and the two probabilities sum to one by step 7.1. Solving gives the stated formula.

step 1.2step 7.1
9.1

The hypotheses are exactly those used: 0<ε<xy<R makes log finite and the end annulus nondegenerate, the case x=y is excluded, the degenerate case ε=R is excluded because the formula's denominator vanishes there, and the truncated times Hn are bounded so that the discrete optional sampling theorem applies. AC covers [F7] and the Countable Choice bridge in [F8], and no countable or dependent choice beyond AC is spent: the integration by parts, the fundamental theorem of calculus and the optional sampling theorem used here are the compact and discrete statements cited in [F4]-[F5].

F4F5F7givenstep 8.1

Source notes

Sousi, Section 6.7 and printed pp. 63--64, computes the annular exit probability from logzy. Durrett, Theorem 9.1.1, Lemma 9.1.3 and formula (9.1.2), gives the same harmonic-martingale calculation and planar formula. The proof above makes the harmonic martingale rigorous with an explicitly spliced bounded C2 extension, a Gaussian integration-by-parts identity and discrete optional sampling at dyadic ceilings.

Depends on

Used by

Dependency tree · two levels

173 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