TheoremStatement: AI-adaptedProof: AI-adaptedPipeline-generated

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.

Exact increment laws in the dyadic Brownian bridge tree

Statement

Assume AC. Fix $m \geq 1$ , $h > 0$ , and a finite tree depth $r \geq 0$ . Take a root increment $D_{\emptyset} \sim N_{m} (0, h I_{m})$ . At each internal node $v$ of length $ℓ_{v} = h / 2^{∣ v ∣}$ , use the split in Dyadic Brownian bridge increment tree with a fresh $Z_{v} \sim N_{m} (0, (ℓ_{v} / 4) I_{m})$ independent of the root and of all other innovations. Then the $2^{r}$ increments at depth $r$ are mutually independent and each has law $N_{m} (0, (h / 2^{r}) I_{m})$ . At every internal node its increment is exactly the sum of its two children. The independence claim is unconditional; conditional on a fixed parent, the two children have covariance $- (ℓ_{v} / 4) I_{m}$ and are not independent.

Facts & Assumptions

Given: AC, a finite integer $m \geq 1$ , a duration $h > 0$ , finite depth $r$ , and the root increment and fresh independent innovations in the Statement.

[F1]

At a node of length $ℓ$ with parent $D$ , draw independent $Z \sim N_{m} (0, (ℓ / 4) I_{m})$ and set the children to $D / 2 + Z$ and $D / 2 - Z$ ; each split uses a fresh innovation. Dyadic Brownian bridge increment tree

[F2]

A multivariate normal law has its specified mean and covariance and is realizable as an affine image of independent standard normals. Gaussian characteristic functions multiply under independent sums, and a joint Gaussian with block-diagonal covariance has a factored characteristic function. Multivariate normal law, including singular covariance Characteristic function of a multivariate normal law Characteristic functions under affine maps and independent sums

[A1]

AC is inherited from the multivariate-normal and Brownian interfaces; the covariance and induction arguments below make no additional selection. The Axiom of Choice

Proof

1.1F1F2givenalgebra

Let $D \sim N_{m} (0, ℓ I_{m})$ and let $Z \sim N_{m} (0, (ℓ / 4) I_{m})$ be independent. Put $L = D / 2 + Z$ and $R = D / 2 - Z$ . The vector $(L, R)$ is a linear image of the independent jointly Gaussian pair $(D, Z)$ , so it is jointly Gaussian. Its means are zero, and direct covariance expansion gives $Cov (L) = Cov (R) = \frac{1}{4} ℓ I_{m} + \frac{1}{4} ℓ I_{m} = \frac{ℓ}{2} I_{m},$ $Cov (L, R) = \frac{1}{4} ℓ I_{m} - \frac{1}{4} ℓ I_{m} = 0.$ Also $L + R = D$ identically.

2.1F2step 1.1algebra

The joint Gaussian characteristic function of $(L, R)$ from [F2] has zero cross-covariance blocks by step 1.1, so it factors into the product of the characteristic functions of $N_{m} (0, (ℓ / 2) I_{m})$ in the two blocks. Uniqueness of the multivariate normal law in [F2] therefore gives independent children with those marginal laws. If one conditions on $D$ , the common $D / 2$ term is fixed and the remaining terms are $Z$ and $- Z$ , so their conditional cross-covariance is $- Cov (Z) = - (ℓ / 4) I_{m}$ .

3.1F1F2step 2.1givenconstruct

At depth $0$ the assertion is the root law. Suppose the increments at depth $k$ are mutually independent with law $N_{m} (0, (h / 2^{k}) I_{m})$ . The fresh innovations at depth $k$ are mutually independent and independent of the entire parent family by the input construction. Therefore the pairs consisting of each parent and its own innovation are mutually independent across the depth- $k$ nodes. For each such pair, step 2.1 gives the unconditional joint law of its two children: they are independent $N_{m} (0, (h / 2^{k + 1}) I_{m})$ vectors. Since child pairs from distinct parents are measurable functions of disjoint independent parent-innovation pairs, those pairs are mutually independent as well. Hence all depth- $(k + 1)$ increments are mutually independent with the claimed law.

4.1A1F1step 1.1step 3.1given∎

Finite induction from step 3.1 proves the assertion for every fixed $r$ . The case $r = 0$ is the root law; every interval has positive length by $h > 0$ , so zero-length nodes are excluded. Sum consistency holds at each node by step 1.1. The result concerns each fixed finite tree, not a claim that an endpoint-selected random traversal is predictable. AC enters only through [A1].

Depends on

Used by

Dependency tree · two levels

20 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

Mike Giles, Monte Carlo Methods, Module 4: Monte Carlo path simulation, Brownian bridge, pp. 27–30 (standard reference, not scraped)