LemmaStatement: 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.

Endpoint law and restriction density of a scalar Brownian bridge

Statement

Assume AC, let $h > 0$ and $x, y \in R$ , and let $μ_{x, y}^{h}$ be the law on $C ([0, h])$ of the bridge in Scalar Brownian bridge from x to y. If $X_{s} = x + W_{s}$ is Brownian motion started at $x$ , then for every Borel path event $A \subseteq C ([0, h])$ and Borel set $D \subseteq R$ , $P {X \in A, X_{h} \in D} = \int_{D} p_{h} (y - x) μ_{x, y}^{h} (A) d y,$ where $p_{t} (z) = (2 π t)^{- 1 / 2} e^{- z^{2} / (2 t)}$ . In particular this specifies the endpoint-conditioned bridge law for every endpoint $y$ . For every $0 \leq t < h$ , the restriction of $μ_{x, y}^{h}$ to path events up to time $t$ has density $\frac{p_{h - t} (y - X_{t})}{p_{h} (y - x)}$ relative to Brownian motion $X$ started at $x$ on $[0, t]$ .

Facts & Assumptions

Given: AC; $h > 0$ ; endpoints $x, y \in R$ ; and the bridge process of Scalar Brownian bridge from x to y.

[F1]

Brownian motion has independent centered normal increments with variance equal to elapsed time, and its finite-dimensional vectors are Gaussian with covariance $\min (s, t)$ . Brownian motion

[F2]

Linear images of jointly Gaussian vectors are jointly Gaussian; uncorrelated Gaussian blocks are independent, as follows by factorization of their Gaussian characteristic function. Multivariate normal law, including singular covariance Characteristic function of a multivariate normal law Characteristic functions under affine maps and independent sums

[F3]

The Brownian transition density is $p_{t} (y - x)$ for $t > 0$ , and these densities satisfy the convolution identity $\int_{R} p_{s} (z - x) p_{t} (y - z) d z = p_{s + t} (y - x)$ . The Brownian kernels form a semigroup

[F4]

On $C ([0, h])$ with the uniform topology, the Borel sigma-algebra is generated by coordinate evaluations, and finite rational-coordinate cylinders form a generating pi-system. This follows from the cited result on $C ([0, \infty))$ by extending each path constantly after $h$ : that extension is a homeomorphism onto the closed subspace of paths constant after $h$ , and coordinates after $h$ equal the coordinate at $h$ . Continuity makes the rational coordinates in $[0, h]$ generate the endpoint coordinate as well. Borel sigma-algebra of continuous path space is generated by coordinates Dynkin's pi-lambda theorem

[A1]

AC is inherited from the Brownian and Gaussian interfaces; the explicit bridge process and the countable cylinder argument add no further choice. The Axiom of Choice

Proof

1.1F1F2F4givenalgebra

Write $β_{s} = W_{s} - (s / h) W_{h}$ . For any finite times $s_{1}, \dots, s_{k} \in [0, h]$ , [F1] makes $(β_{s_{1}}, \dots, β_{s_{k}}, W_{h})$ jointly Gaussian. Direct covariance calculation gives $Cov (β_{s_{i}}, W_{h}) = s_{i} - (s_{i} / h) h = 0$ and $Cov (β_{s}, β_{t}) = \min (s, t) - s t / h$ . Hence [F2] makes every finite vector of bridge residual coordinates independent of $W_{h}$ . The countable generating coordinates in [F4] then make the entire continuous residual path independent of $W_{h}$ . Therefore conditioning on $W_{h} = y - x$ gives exactly the explicit bridge process from the definition, for each $y$ .

2.1F1F3step 1.1algebra

If $t = 0$ , the restricted bridge path is the constant initial value $x$ and the density ratio is $p_{h} (y - x) / p_{h} (y - x) = 1$ . Now take $0 < t < h$ and fix $0 = s_{0} < s_{1} < \dots < s_{k} = t$ . By independent increments and [F3], the joint density of $X_{s_{1}}, \dots, X_{s_{k}}, X_{h}$ at $z_{1}, \dots, z_{k}, y$ is $p_{s_{1}} (z_{1} - x) \prod_{i = 2}^{k} p_{s_{i} - s_{i - 1}} (z_{i} - z_{i - 1}) p_{h - t} (y - z_{k}) .$ Dividing by the strictly positive endpoint density $p_{h} (y - x)$ gives the conditional bridge density for these coordinates. By step 1.1 this is the finite-dimensional law of the bridge in the definition. The same expression is the Brownian path density on $[0, t]$ multiplied by $p_{h - t} (y - X_{t}) / p_{h} (y - x)$ when the coordinate at time $t$ is included; integrating out that last coordinate uses the convolution identity [F3].

3.1F3F4step 2.1

Thus the restriction-density identity holds for every finite cylinder event on $[0, t]$ . The density is nonnegative and integrates to one by [F3]. The class of path events for which the identity holds is a lambda-system containing the generating cylinder pi-system of [F4]; Dynkin's pi-lambda theorem therefore extends the identity to all Borel path events on $[0, t]$ . This proves the restriction assertion.

4.1A1F1step 1.1step 3.1given∎

By step 1.1, the joint law of the residual bridge path and endpoint $W_{h}$ is the product of the bridge residual law and the $N (0, h)$ endpoint density. Applying the measurable map $(β, z) \mapsto (x + (s / h) z + β_{s})_{0 \leq s \leq h}$ and translating $z = y - x$ gives the stated full-path disintegration. The endpoint density is continuous and positive for every $y$ since $h > 0$ . The degenerate cases $t = 0$ and a one-coordinate cylinder follow from the same formulas; $t = h$ is excluded from the restriction statement. AC is used only through [A1].

Depends on

Used by

Scalar Brownian bridge barrier-crossing probability Theorem

Dependency tree · two levels

59 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

Dario Gasbarra, Tommi Sottinen, and Esko Valkeila, Gaussian Bridges, §1, equation (1.3), and §2.3, equation (2.6) (standard reference, not scraped)