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.
Radial second moment of multidimensional Brownian motion
Example
Assume the Axiom of Choice. Let be finite, let be a standard -dimensional Brownian motion, and give it its uncompleted natural filtration
Then
and the real process
is an all-pairs continuous-time martingale: for every ,
Facts & Assumptions
Given: AC, a finite integer , and a standard -dimensional Brownian motion .
A standard -dimensional Brownian motion starts at zero almost surely, has mutually independent vector increments with law on every finite increasing grid, and equivalently has independent standard scalar Brownian coordinate processes. -dimensional Brownian motion
The uncompleted natural filtration is generated by observations up to time ; an all-pairs martingale is adapted, integrable at each time, and satisfies the displayed conditional identity for every . Continuous-time filtrations and all-pairs martingales
Disjoint groups of independent sigma-algebras remain independent, and measurable functions applied separately to independent random elements remain independent. Disjoint groups of an independent sigma-algebra family remain independent Measurable coordinatewise functions preserve independence
A pi-system contained in a lambda-system generates a sigma-algebra still contained in that lambda-system; probability is finitely additive and continuous on increasing event sequences. Dynkin's pi-lambda theorem Basic identities for a probability measure
The squared Euclidean norm is the finite sum of coordinate squares. The Euclidean norm is continuous, finite algebra preserves continuity, and continuous maps have Borel preimages. The Euclidean inner product on The finite and reverse triangle inequalities for a norm; and for every norm on satisfies and is Lipschitz, hence continuous, for Sums, products, absolute values, finite maxima and minima, and quotients of continuous real-valued maps on a topological space are continuous where defined A continuous map has Borel preimages of Borel sets
A scalar variable has mean zero and variance, hence second moment, , including . Characteristic function of a normal law
A variable measurable for the conditioning sigma-algebra conditions to itself; an integrable variable independent of that sigma-algebra conditions to its mean. Conditional expectation is linear, and a finite known factor may be taken out when the products are integrable. Ordinary integration is linear on arbitrary measure spaces. Conditioning a known variable and an independent variable Basic algebra and order properties of conditional expectation Taking out what is known The Lebesgue integral is linear on
Products of square-integrable real variables are integrable by Cauchy--Schwarz. Cauchy-Schwarz for random variables
AC is used through the Brownian, normal-law, and conditional-expectation suppliers. The Axiom of Choice
Verification
Write . By [F1], each has law , so [F6] gives . The coordinate-square sum in [F5] and finite linearity in [F7] therefore give Thus and are integrable. The map is continuous, hence Borel by [F5]; since is an observation generating , both and are -measurable. Consequently is adapted. At , the same calculation gives expectation zero although is only an almost-sure identity.
Fix and put . Let consist of and all finite intersections It is a pi-system and its generated sigma-algebra is by [F2]. Given one such cylinder, sort its distinct positive observation times and adjoin . On the probability-one event , every displayed past observation is a finite cumulative sum of the vector increments ending no later than . Those increments and are disjoint groups of the mutually independent increment family in [F1]; [F3] makes their grouped vectors, and then the past observation tuple and , independent. Replacing the tuple by its almost-surely equal cumulative-sum expression changes the cylinder event by a null set, so for every Borel and every , Empty cylinders give . If , every finite past tuple is almost surely the constant zero tuple, and the same null-set argument gives the identity.
Fix a Borel and let be the events satisfying the factorization in step 1.2. The class contains ; finite differences of nested members follow by subtracting the two finite probability identities, and increasing countable unions follow from probability continuity in [F4]. Thus is a lambda-system containing . By [F4], it contains . Since was arbitrary, is independent of . For , identically and the same independence conclusion is immediate.
Let . By [F1], the coordinates of have laws ; [F6] and [F7] give Indeed each scalar coordinate and the squared norm are Borel functions of the independent vector from step 2.1, and the squared norm is integrable by [F5]--[F7]. Also and are square-integrable by [F1] and [F6], so [F8] makes their product integrable. Because is -measurable, taking out what is known yields The formulas also hold when , where pointwise.
The pathwise Euclidean identity and conditional linearity now give Subtracting the deterministic proves With the adaptation and integrability from step 1.1, this is exactly the all-pairs martingale definition in [F2].
Steps 1.1--4.1 prove both displayed claims. The case is Durrett's scalar square martingale; is excluded. Time zero, , , and are all covered, and no completed or right-continuously augmented filtration has been substituted for the stated natural filtration. There is no biconditional. AC is used only through [F1], [F6], and [F7]; the finite grid, pi-lambda promotion, and coordinate sum make no additional choices.
Source notes
Durrett, Section 7.5, Theorem 7.5.4 and its proof, printed p. 376, proves is a martingale by expanding across the future centered increment and conditioning on the Brownian past. The proof above supplies the finite -coordinate extension and proves from the increment definition and a pi-lambda argument that the future vector increment is independent of the uncompleted natural filtration.
Depends on
- $d$-dimensional Brownian motion
- Continuous-time filtrations and all-pairs martingales
- The Euclidean inner product $\langle x,y\rangle = \sum_{k<n} x_k y_k$ on $\mathbb{R}^n$
- The finite and reverse triangle inequalities for a norm; and for $n \ge 1$ every norm $N$ on $\mathbb{R}^n$ satisfies $N(x) \le C\lVert x\rVert_1$ and is Lipschitz, hence continuous, for $d_2$
- Sums, products, absolute values, finite maxima and minima, and quotients of continuous real-valued maps on a topological space are continuous where defined
- A continuous map has Borel preimages of Borel sets
- Disjoint groups of an independent sigma-algebra family remain independent
- Measurable coordinatewise functions preserve independence
- Dynkin's pi-lambda theorem
- Basic identities for a probability measure
- Conditioning a known variable and an independent variable
- Taking out what is known
- Basic algebra and order properties of conditional expectation
- The Lebesgue integral is linear on $L^1(\mu)$
- Cauchy-Schwarz for random variables
- Characteristic function of a normal law
- The Axiom of Choice
Used by
Nothing in the library uses this result yet.
Dependency tree · two levels
110 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, Section 7.5 (standard reference, not scraped)