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 be the shifted planar Brownian law on canonical continuous path space Brownian motion started at x, and let be its coordinate process. For with and , let and let . Then
Facts & Assumptions
Given: AC, the continuous coordinate process under , in and .
Under , almost surely, the increments of over have law and are independent of the raw coordinate past, and each process is a standard one-dimensional Brownian motion. Every coordinate path is continuous. -dimensional Brownian motion Brownian motion started at x
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 for a known state and independent noise , . One-dimensional Brownian motion hits every point almost surely Conditioning a known state and independent noise Continuous-time stopping times and stopped sigma-algebras
is the law of a pair of independent standard normal coordinates, whose one-dimensional density is positive with and finite second moment. In particular follows from . Gaussian even moments for Brownian increments Multivariate normal law, including singular covariance Standard normal and normal laws
Compact integration by parts, the chain rule, the fundamental theorem of calculus for a differentiable primitive, dominated and monotone convergence, and Tonelli/Fubini for bounded or integrable product integrands. If are differentiable on with integrable, then The chain rule, in one line from Carathéodory: if is differentiable at and is differentiable at , then is differentiable at with The second fundamental theorem: if is differentiable on with and is integrable, then Dominated convergence Monotone convergence for the integral Tonelli's theorem for nonnegative measurable functions on a sigma-finite product Fubini's theorem for L^1 functions on a sigma-finite product If all partial derivatives exist on a neighbourhood and are continuous at a point, then the map is totally differentiable there with Jacobian derivative
Continuous real functions on compact intervals attain their extrema and take all intermediate values. The mean value theorem bounds difference quotients. Under AC, the Countable Choice Riemann-to-Lebesgue bridge identifies the compact calculus integrals in [F4] with Lebesgue integrals. Extreme value theorem: a continuous real function on a nonempty compact subset of attains a greatest and a least value Heine-Borel by bisection: every closed bounded interval is compact Intermediate value theorem, by bisection with a canonical left-half rule: a continuous function on takes every value between and The mean value theorem, as the case of Cauchy's: for continuous on with and differentiable on there is with A bounded Riemann integrable function on a closed bounded interval is Lebesgue measurable and has the same integral
Optional sampling for bounded discrete stopping times: for a martingale with and stopping times bounded by , ; a discrete martingale is defined by its adjacent conditional means, and the discrete stopped sigma-algebra is defined by the events . Martingale submartingale and supermartingale Optional sampling for bounded stopping times Continuous-time filtrations and all-pairs martingales
Conditional expectations are unique almost surely and are additive on bounded inputs. Conditional expectation as an ae class Conditional expectation is unique almost surely Basic algebra and order properties of conditional expectation Measurability of integration against a kernel Measure kernel and probability kernel
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
Put . Every path is continuous. For , compact attainment and rational approximation give The reverse inclusion follows since the continuous nonnegative distance of to the closed set then has minimum zero on . Similarly, for or , its circle hitting time has event 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 , the initial radius is strictly between the boundaries. Continuity and the intermediate value theorem give , the boundary value when , and for . These last claims are used only on that event.
Define for and extend it to a function on with on , on , and quintic Hermite splices on and that match value, first and second derivative at both joints: on use and on use , where satisfies at and , at . Each splice agrees with the neighbouring branches in value and in its first two derivatives at both endpoints, so the resulting is with bounded first and second derivatives, and is then a bounded function of , constant near and outside the disc of radius , with for ; its Laplacian at is continuous and bounded, and it vanishes on because there.
For the standard normal pair of [F3], every bounded function with bounded derivatives satisfies for and . Indeed, the law of 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 with the compact theorem of [F4] using and the bounded factor , where and the other Gaussian coordinate is fixed; the boundary terms vanish as 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 .
Let be the raw coordinate filtration. For every bounded Borel and one has almost surely: apply the conditioning lemma to the known state and independent noise .
The standard one-dimensional Brownian motion (zero-start almost surely) hits the level almost surely. At that time , so is no larger and is finite -almost surely.
Fix a bounded function with bounded first and second derivatives and put with the law of . Then is differentiable on with : differentiating the expectation is licensed by the mean value theorem in [F8] and dominated convergence on a neighborhood bounded away from , because is bounded and is integrable, and the resulting expression is by step 1.3.
Let and be as in step 2.2. Continuity of and bounded convergence imply that is continuous, including at zero. For , the fundamental theorem of calculus applied to the continuous integrand on gives by step 2.2; [F8] identifies this compact calculus integral with the Lebesgue integral. Letting , dominated convergence gives because is continuous and bounded, and the integrals converge by monotone convergence on the nonnegative and negative parts; hence for every .
Define . The map restricted to is -measurable: finite deterministic grid approximations to the continuous paths, using only coordinates at times at most , converge pointwise. Parameter integration therefore makes the drift integral -measurable. Thus is adapted, continuous on every path and integrable on each finite horizon, with . For and , Fubini on the bounded finite-time integrands and step 1.4 give By step 3.1 the inner integral is , while step 1.4 gives . Thus , and is a martingale.
Fix and let . For each put , define the discrete filtration and the discrete martingale , which satisfies by [F5] and step 4.1. The integer-valued ceiling is a stopping time for , since by step 1.1, and it is bounded by . Applying [F5] with and gives .
Expanding step 5.1 and letting , and by continuity. Dominated convergence on gives Since for , the integral vanishes, and .
Define by literal evaluation when and as otherwise. This is measurable by finite-grid approximation to and passage to the limit on . Letting , continuity and bounded convergence give . Moreover and almost surely, so on and on . The tie event can include paths with both times infinite, but it has -probability zero because almost surely; a finite tie is impossible when .
Therefore , and the two probabilities sum to one by step 7.1. Solving gives the stated formula.
The hypotheses are exactly those used: makes finite and the end annulus nondegenerate, the case is excluded, the degenerate case is excluded because the formula's denominator vanishes there, and the truncated times 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].
Source notes
Sousi, Section 6.7 and printed pp. 63--64, computes the annular exit probability from . 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 extension, a Gaussian integration-by-parts identity and discrete optional sampling at dyadic ceilings.
Depends on
- The mean value theorem, as the case $g(x) = x$ of Cauchy's: for $f$ continuous on $[a,b]$ with $a < b$ and differentiable on $(a,b)$ there is $c \in (a,b)$ with $f(b) - f(a) = f'(c)(b-a)$
- 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
- Heine-Borel by bisection: every closed bounded interval $[a,b]$ is compact
- 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)$
- Gaussian even moments for Brownian increments
- $d$-dimensional Brownian motion
- Brownian motion started at x
- Brownian motion
- Conditioning a known state and independent noise
- One-dimensional Brownian motion hits every point almost surely
- Continuous-time stopping times and stopped sigma-algebras
- Continuous-time filtrations and all-pairs martingales
- Martingale submartingale and supermartingale
- Optional sampling for bounded stopping times
- If $u,v$ are differentiable on $[a,b]$ with $u',v'$ integrable, then $\int_a^b u v' = u(b)v(b)-u(a)v(a) - \int_a^b u'v$
- The chain rule, in one line from Carathéodory: if $g$ is differentiable at $c$ and $f$ is differentiable at $g(c)$, then $f \circ g$ is differentiable at $c$ with $(f \circ g)'(c) = f'(g(c))\,g'(c)$
- If all partial derivatives exist on a neighbourhood and are continuous at a point, then the map is totally differentiable there with Jacobian derivative
- Dominated convergence
- Monotone convergence for the integral
- Tonelli's theorem for nonnegative measurable functions on a sigma-finite product
- Fubini's theorem for L^1 functions on a sigma-finite product
- The second fundamental theorem: if $G$ is differentiable on $[a,b]$ with $G' = f$ and $f$ is integrable, then $\int_a^b f = G(b)-G(a)$
- Measurability of integration against a kernel
- Measure kernel and probability kernel
- Multivariate normal law, including singular covariance
- Standard normal and normal laws
- Conditional expectation as an ae class
- Conditional expectation is unique almost surely
- Basic algebra and order properties of conditional expectation
- The Axiom of Choice
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
- Perla Sousi, Advanced Probability, Section 6.7 and printed pp. 63-64 (standard reference, not scraped)
- Rick Durrett, Probability: Theory and Examples, fifth edition, Theorem 9.1.1, Lemma 9.1.3 and formula (9.1.2) (standard reference, not scraped)