ExampleConstruction: Literature-sourcedVerification: AI-adaptedPipeline-generatedprecheck pending

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.

Finite VP noise leaves a terminal-prior mismatch

Example

Assume AC. Fix $T > 0$ and a continuous function $β : [0, T] \to (0, \infty)$ . Let $(Ω, F, (F_{t})_{t \geq 0}, P)$ be a complete filtered probability space with a right-continuous filtration, and let $W$ be an adapted standard one-dimensional Brownian motion such that, for every $0 \leq s < t$ , $W_{t} - W_{s}$ is independent of $F_{s}$ and has law $N (0, t - s)$ . Put $B (t) = \int_{0}^{t} β (r) d r$ , $X_{0} = 0$ , and

$X_{t} = e^{- B (t) / 2} \int_{0}^{t} e^{B (r) / 2} \sqrt{β (r)} d W_{r}, 0 \leq t \leq T .$

This solves the variance-preserving (VP) stochastic differential equation $d X_{t} = - \frac{1}{2} β (t) X_{t} d t + \sqrt{β (t)} d W_{t}$ . For $t > 0$ , its law $P_{t}$ has density and score

$p_{t} (x) = \frac{1}{\sqrt{2 π v_{t}}} e^{- x^{2} / (2 v_{t})}, s_{t} (x) = - \frac{x}{v_{t}}, v_{t} = 1 - e^{- B (t)} .$

Since $β$ is positive and continuous, $0 < B (T) < \infty$ and $0 < v_{T} < 1$ , so $P_{T} = N (0, v_{T}) \neq N (0, 1)$ . The predictor-corrector procedure defined above initializes from the actual terminal law $P_{T}$ ; replacing that draw by $N (0, 1)$ changes the initial law for this finite schedule. No convergence or solver-error claim follows from this comparison.

Example references

Song et al., Section 3.4

Särkkä and Solin, Sections 5.2 and 6.1

Raginsky, Sections 2.3 and 7.1

Facts & Assumptions

Given: AC, the filtered Brownian motion and schedule $β$ in the Example, and its explicit process $X$ .

[A1]

AC, the usual filtration conditions, and independent Brownian increments relative to the filtration are the hypotheses of the Brownian Itô and deterministic-integral interfaces used below. Continuous Brownian Ito processes The Axiom of Choice

[F1]

A process with pathwise integrable drift and a localized Brownian Itô integral is a continuous Brownian Itô process under the stated filtration conditions. Continuous Brownian Ito processes

[F2]

For a one-dimensional Brownian Itô process and a $C^{1, 2}$ function, Itô's formula adds the drift, diffusion, and half-variance second-derivative terms. One-dimensional Ito formula

[F3]

A deterministic square-integrable Itô integrand has a centered normal integral with variance equal to the integral of its square. Deterministic Ito integrals are Gaussian

[F4]

A scalar normal law is the affine image of the standard normal law, and for positive variance $v$ it has density $(2 π v)^{- 1 / 2} e^{- x^{2} / (2 v)}$ . Standard normal and normal laws A positive-variance normal law has its location-scale density

[F5]

At positive finite differentiable density points, the marginal score is the derivative of the log density. Marginal score function

[F6]

The law of a random element is its probability pushforward. Law or distribution of a random element

[F7]

The predictor-corrector procedure's initial draw has law $P_{T}$ . Predictor-corrector sampling for score SDEs

Verification

1.1A1F1F2givenalgebra

Write $K_{t} = \int_{0}^{t} e^{B (r) / 2} \sqrt{β (r)} d W_{r}$ , whose deterministic integrand is square-integrable because $B$ and $β$ are continuous on $[0, T]$ . Since $B^{'} (t) = β (t)$ , apply [F2] to $f (t, x) = e^{- B (t) / 2} x$ and the continuous Itô process $K_{t}$ . The product rule gives $d X_{t} = - \frac{1}{2} β (t) X_{t} d t + \sqrt{β (t)} d W_{t}$ and $X_{0} = 0$ .

1.2F3F4givenalgebra

By [F3], $K_{t}$ is centered normal with variance $\int_{0}^{t} e^{B (r)} β (r) d r$ . Differentiating $e^{B (r)}$ gives $\frac{d}{d r} e^{B (r)} = e^{B (r)} β (r)$ , so this variance is $e^{B (t)} - 1$ . Multiplication by $e^{- B (t) / 2}$ therefore gives $X_{t} \sim N (0, e^{- B (t)} (e^{B (t)} - 1)) = N (0, v_{t})$ . For $t > 0$ , positivity of $β$ implies $v_{t} > 0$ ; [F4] supplies its displayed density.

2.1F4F5givenstep 1.2algebra

Differentiating the density in step 1.2 gives $\partial_{x} \log p_{t} (x) = - x / v_{t}$ , so [F5] yields the score for every $t > 0$ . At $t = 0$ , $X_{0} = 0$ almost surely; its law assigns mass one to ${0}$ and therefore has no Lebesgue density, since every Lebesgue-density measure assigns zero mass to that singleton.

3.1F4F6F7step 1.2step 2.1givenalgebra∎

Continuity of $β$ on the compact interval makes $B (T)$ finite, and strict positivity gives $B (T) > 0$ . Hence $v_{T} = 1 - e^{- B (T)}$ lies strictly between zero and one. For any $v > 0$ , the density in [F4] and the substitution $x = \sqrt{v} z$ give $\int_{R} x^{2} \frac{e^{- x^{2} / (2 v)}}{\sqrt{2 π v}} d x = v \int_{R} z^{2} \frac{e^{- z^{2} / 2}}{\sqrt{2 π}} d z = v$ . Indeed integration by parts yields $\int z^{2} e^{- z^{2} / 2} d z = \int e^{- z^{2} / 2} d z$ over $R$ , because $z e^{- z^{2} / 2} \to 0$ at both ends, and the normalized standard-normal density integrates to one. Thus $E_{P_{T}} X^{2} = v_{T}$ by step 1.2, whereas $E_{N (0, 1)} Z^{2} = 1$ . If the laws were equal these finite second moments would be equal, a contradiction. Step 2.1 shows the exact positive-time score is available at $T$ , and [F7] prescribes initialization from $P_{T}$ ; replacing it by $N (0, 1)$ changes that initial law.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

72 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

Yang Song et al., Score-Based Generative Modeling through Stochastic Differential Equations, Section 3.4 (standard reference, not scraped)
Simo Särkkä and Arno Solin, Applied Stochastic Differential Equations, Sections 5.2 and 6.1 (standard reference, not scraped)
Maxim Raginsky, Stochastic Differential Equations: A Systems-Theoretic Approach, Sections 2.3 and 7.1 (standard reference, not scraped)