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.

A singular Brownian data law forces positive-time score truncation

Example

Assume AC, let $T > 0$ , and let $W = (W_{t})_{t \geq 0}$ be a standard one-dimensional Brownian motion. Set $X_{t} = W_{t}$ and let $P_{t}$ be the law of $X_{t}$ for $0 \leq t \leq T$ . Thus $P_{0} (A) = 1$ when a Borel set $A$ contains $0$ and $P_{0} (A) = 0$ otherwise. For every $t > 0$ , $P_{t}$ has density

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

The law $P_{0}$ has no Lebesgue density, so its marginal score is undefined at $t = 0$ . For every cutoff $0 < ϵ < T$ , the score is defined throughout $[ϵ, T]$ , and

$E ∣ W_{ϵ} ∣^{2} = ϵ, W_{ϵ} ⟶ 0 almost surely as ϵ ↓ 0, P_{ϵ} \Rightarrow P_{0} .$

Here $P_{ϵ} \Rightarrow P_{0}$ means that $\int f d P_{ϵ} \to \int f d P_{0}$ for every bounded continuous $f : R \to R$ . Consequently a score-based procedure requiring an exact marginal score can use this family only after choosing a positive cutoff; the limit at the singular data endpoint is a statement about the laws, not a score value at zero.

Example references

Särkkä and Solin, Section 5.2, Theorem 5.4 and proof

Raginsky, Section 2.3

Facts & Assumptions

Given: AC, $T > 0$ , and a standard one-dimensional Brownian motion $W$ .

[A1]

AC is assumed in the Brownian, normal-law, and deterministic score-sampling interfaces. The Axiom of Choice

[F1]

Brownian motion starts at zero almost surely, has a common full-measure event of continuous paths, and $W_{t} \sim N (0, t)$ . Brownian motion

[F2]

For $t > 0$ , the law $N (0, t)$ has density $(2 π t)^{- 1 / 2} e^{- x^{2} / (2 t)}$ . A positive-variance normal law has its location-scale density Standard normal and normal laws

[F3]

At a positive finite differentiable density, the marginal score is the spatial derivative of its logarithm. Marginal score function

[F4]

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

[F5]

Almost-everywhere convergence under an integrable bound implies convergence of integrals. Dominated convergence

[F6]

Weak convergence of Borel probability measures is convergence of integrals against every bounded continuous real-valued function. Weak convergence of borel probability measures

Verification

1.1A1F1F2F3F4givenalgebra

By [A1], [F1], and [F2], for each $t > 0$ the law of $W_{t}$ has the displayed Gaussian density. Differentiation gives $\partial_{x} \log p_{t} (x) = - x / t$ , so [F3] gives the stated score. At $t = 0$ , [F1] and [F4] give $P_{0} ({0}) = 1$ . Any measure with a Lebesgue density assigns mass $\int_{{0}} p (x) d x = 0$ to this singleton, so $P_{0}$ has no Lebesgue density.

1.2F2algebra

By [F2], changing variables $x = \sqrt{ϵ} z$ yields $E ∣ W_{ϵ} ∣^{2} = \int_{R} x^{2} \frac{e^{- x^{2} / (2 ϵ)}}{\sqrt{2 π ϵ}} d x = ϵ \int_{R} z^{2} \frac{e^{- z^{2} / 2}}{\sqrt{2 π}} d z = ϵ$ . For the last equality, integration by parts gives $\int z^{2} e^{- z^{2} / 2} d z = \int e^{- z^{2} / 2} d z$ over $R$ : the boundary term $- z e^{- z^{2} / 2}$ tends to $0$ at both ends, and the normalized standard-normal density integrates to $1$ . Hence the second moment tends to zero.

2.1F1F4F5F6step 1.1given∎

Fix any sequence $ϵ_{n} > 0$ with $ϵ_{n} \to 0$ . On the common continuity event from [F1], $W_{ϵ_{n}} \to W_{0} = 0$ , so for bounded continuous $f$ , $f (W_{ϵ_{n}}) \to f (0)$ almost surely and $∣ f (W_{ϵ_{n}}) ∣ \leq ∥ f ∥_{\infty}$ . Applying [F5] gives $\int f d P_{ϵ_{n}} = E f (W_{ϵ_{n}}) \to f (0) = \int f d P_{0}$ . Since this holds for every such sequence, the limit holds as $ϵ ↓ 0$ ; [F6] identifies it as $P_{ϵ} \Rightarrow P_{0}$ . The positive-time score conclusion in step 1.1 and the absence of a score at zero prove the stated truncation consequence.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

37 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

Simo Särkkä and Arno Solin, Applied Stochastic Differential Equations, Section 5.2, Theorem 5.4 and proof (standard reference, not scraped)
Maxim Raginsky, Stochastic Differential Equations: A Systems-Theoretic Approach, Section 2.3 (standard reference, not scraped)