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.
Covariance of overlapping Brownian increments
Example
Assume the Axiom of Choice. If is a standard Brownian motion, , and , then
Thus the covariance is the length of the overlap of the time intervals and ; an intersection consisting of one endpoint has length zero.
Facts & Assumptions
Given: AC, a standard Brownian motion , and , .
Brownian motion is centered with ; its values are square-integrable normal random variables. Brownian motion, Brownian covariance is equivalent to independent stationary normal increments.
Covariance of square-integrable real random variables is defined by centered products and is symmetric and bilinear in finite linear combinations. Moments, variance, and covariance on a probability space, Covariance is symmetric and bilinear in finite linear combinations.
AC is inherited through the Brownian and normal-law interfaces. The Axiom of Choice.
Verification
Bilinearity and the Brownian covariance kernel give Every term is finite because the Brownian values are square-integrable.
Both sides of the claimed formula are unchanged when the ordered pairs and are exchanged, the left side by symmetry of covariance. It therefore suffices to assume . If , the four minima in step 1.1 are respectively , so the covariance is zero; also , so the stated overlap length is zero. This includes and all zero-length first intervals.
Still assuming , suppose . The four minima in step 1.1 are , so the covariance is . Here and , giving the same positive overlap length. This case includes and , but excludes , already handled in step 2.1.
Finally, if , the four minima in step 1.1 are , so the covariance is . Here and . The value is zero exactly when , so zero-length second intervals are included. These three cases exhaust ; pair symmetry handles .
Steps 2.1, 3.1, and 4.1 prove the formula for every allowed endpoint order, including coincident endpoints, , , and . There is no empty family or biconditional. AC is used only through [F1]; expanding four covariances and comparing endpoints uses no further choice.
Source notes
Durrett, Section 7.1, printed p. 355, derives for from independent increments. The four-term overlap calculation and its complete endpoint case split are given above.
Depends on
Used by
Nothing in the library uses this result yet.
Dependency tree · two levels
18 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.1 (standard reference, not scraped)