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.
Brownian reflection principle
Statement
Assume the Axiom of Choice, let be a standard Brownian motion Brownian motion. All path operations below use a fixed everywhere-continuous, zero-start representative: choose a measurable probability-one event on which the paths are continuous and , and replace by the zero path off this event, as in Wiener measure on continuous path space. Retain the notation for this representative and use its own raw natural filtration and usual augmentation. This preserves every finite-dimensional law; all maxima and hitting times below refer to this representative, without transferring stopping times between the raw filtrations of different versions. Let and , and put Then:
- The path reflected at has Wiener law: for each the process and its reflection for , for , have the same law on the cylinder sigma-algebra of .
- For every , and in particular .
Facts & Assumptions
Given: AC, a standard Brownian motion with every path continuous and everywhere, real , and .
is a stopping time for the raw natural filtration and hence for the usual augmentation, which is right-continuous; and if and only if . The combination is a stopping time bounded by . Brownian closed-set hitting times are stopping times Continuous-time stopping times and stopped sigma-algebras Natural and usual augmented Brownian filtrations
Strong Markov: for an a.s. finite stopping time of the usual augmentation, the shifted increment process is independent of with the finite-dimensional marginals of Wiener measure; moreover for bounded Borel path functionals . Strong Markov property of Brownian motion
Wiener measure is the unique Borel probability on continuous path space whose coordinates are centered Gaussian with covariance ; hence the map preserves Wiener measure, because it preserves every finite-dimensional centered Gaussian law with that covariance. Uniqueness of Wiener measure Wiener measure on continuous path space
For each the law of has the strictly positive density , so for every . The Brownian kernels form a semigroup
By definition, the cylinder sigma-algebra is generated by finite-coordinate cylinder sets, which form a pi-system; a lambda-system containing that pi-system contains the generated sigma-algebra, and conditional laws agree almost surely when their defining conditional expectations agree. Dynkin's pi-lambda theorem Conditional expectation as an ae class
If is -measurable and is an independent random element with law , then for bounded product-measurable , . The Borel sigma-algebra of continuous path space is generated by coordinates; thus coordinate measurability and cylinder independence imply path-space measurability and independence for an everywhere-continuous random path. Conditioning a known state and independent noise Borel sigma-algebra of continuous path space is generated by coordinates
AC supplies the conditional-expectation and strong-Markov interfaces. The Axiom of Choice Strong Markov property of Brownian motion
Proof
By [F1] the time is a stopping time of the usual augmentation and is a stopping time bounded by the deterministic time , hence a.s. finite; on the event one has and by continuity, while on one has . Also by continuity of the path.
The law of any finite-dimensional marginal of is unchanged by the substitution , and the cylinder pi-system determines a law on ; hence the law of is invariant under negation, and the same holds for every process whose finite-dimensional marginals are those of Brownian motion, by [F5] and [F3].
Define for and for . Every coordinate is measurable by the stopping-time tests. The path is continuous: if , then , and if it is unchanged. For finitely many , put . This is -measurable: is measurable there by its test events, and [F2]'s stopped-value measurability at , followed by the stopped-sigma-algebra inclusion for , gives the other coordinates. Since paths are everywhere continuous and these times finite, the version convention in [F2] gives the literal values. The path is everywhere continuous, has Wiener law and is independent of by [F2], [F7] and coordinate generation. Random evaluation is measurable: replace its time by the ceiling on the dyadic mesh, use the countable coordinate formula, then pass to the pointwise limit by continuity. Hence the vectors and are product-measurable functions of . These formulas also hold when because . For every bounded Borel test of this vector, [F7] and invariance of Wiener measure under from step 1.2 give equal conditional expectations. Thus the finite-dimensional laws agree, and [F5] gives equality on the entire cylinder sigma-algebra.
On the event , the reflected path coincides with on , so ; moreover there. Hence as events. These are cylinder-measurable events on the continuous-path representatives: use the rational-distance formula of [F1] for the hit event and the terminal coordinate for the inequality. Thus by step 2.1 the probability equals . Since implies , the event is contained in , so the last probability is . Together with from step 1.1, this is the first identity of assertion 2.
Taking in step 3.1 gives . Since and differs from by the null event by [F4], adding to both sides gives , the second identity of assertion 2. Assertion 1 is step 2.1.
The endpoint and degenerate cases are covered: the statement requires and ; the value is used in step 4.1 and is the boundary case of the constraint ; the case is step 3.1 unchanged; the case contributes to neither event in the first probability identity, by the containment in step 3.1; the case with equality is the null event excluded by [F4]. AC is used through [F6] for the strong Markov and conditional-expectation interfaces.
Source notes
Lawler, Proposition 2.7.2, derives the maximum formula from post-hit symmetry and absence of a terminal atom. Here the full reflected-path law is proved by conditioning on the bounded time tau_a wedge T, so the proof needs no prior almost-sure finiteness of tau_a. The measurable continuous-path representative is fixed before forming its filtration and hitting times.
Depends on
- Brownian closed-set hitting times are stopping times
- Strong Markov property of Brownian motion
- Natural and usual augmented Brownian filtrations
- Continuous-time stopping times and stopped sigma-algebras
- Brownian motion
- Wiener measure on continuous path space
- The Brownian kernels form a semigroup
- Uniqueness of Wiener measure
- Dynkin's pi-lambda theorem
- Conditional expectation as an ae class
- The Axiom of Choice
- Conditioning a known state and independent noise
- Borel sigma-algebra of continuous path space is generated by coordinates
Used by
- Law of the Brownian maximum Corollary
Dependency tree · two levels
83 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
- Gregory F. Lawler, Stochastic Calculus: An Introduction with Applications, Proposition 2.7.2 (standard reference, not scraped)
- Rick Durrett, Probability: Theory and Examples, fifth edition, Example 7.4.2 and equation (7.4.4) (standard reference, not scraped)