ExampleConstruction: Literature-sourcedVerification: AI-adaptedPipeline-generatedprecheck pendingjudge pass (gpt-6-luna)

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.

Bounded-start Brownian reversal under Anderson's hypotheses

Example

Assume AC. Let $X_{0}$ have a compactly supported $C^{\infty}$ probability density $ρ$ on $R^{d}$ , let $W$ be standard $d$ -dimensional Brownian motion independent of $X_{0}$ , and use the usual augmentation of the filtration generated by $X_{0}$ and $W$ . Set $X_{t} = X_{0} + W_{t}$ on $[0, T]$ . For $t > 0$ its density is $p_{t} (x) = \int_{R^{d}} (2 π t)^{- d / 2} e^{- ∣ x - z ∣^{2} / (2 t)} ρ (z) d z .$ Assume that $p_{t}$ is the unique smooth forward-density solution on $[0, T]$ and, in addition, Anderson's unique smooth joint-density and conditional-density hypotheses for $(X_{t}, {\tilde{W}}_{t})$ , where ${\tilde{W}}_{0} = 0$ and, for $t > 0$ , $d {\tilde{W}}_{t} = d W_{t} + \nabla \log p_{t} (X_{t}) d t$ . Then on reverse times $0 \leq u < T$ , the reverse drift is $\nabla \log p_{T - u} (Y_{u})$ with unit diffusion covariance. The value of $\nabla \log p_{0}$ is not used in the time integral; the statement makes no score assertion at the data endpoint $u = T$ .

Example references

Gaussian-smoothed law and transition density: supplies the positive-time Gaussian convolution formula.

Anderson, Sections 3–4: states the bounded-start reversal theorem with the augmented-density uniqueness hypotheses retained here.

Facts & Assumptions

Given: AC, the initial law and Brownian motion in the Example, and Anderson's unique smooth joint and conditional density premises.

[A1]

Anderson's theorem requires bounded initial state independent of the forward Brownian process, a unique smooth forward density, unique smooth augmented joint density, and unique smooth conditional augmented density; strong SDE well-posedness alone does not supply these density hypotheses. Anderson's bounded-start reverse-time diffusion theorem

[F1]

In the additive Gaussian setup with $g \equiv 1$ , the positive-time marginal density is the displayed convolution, is positive, and solves $\partial_{t} p_{t} = \frac{1}{2} Δ p_{t}$ . Gaussian-smoothed data law and transition density Gaussian smoothing density and forward equation

Verification

1.1A1F1given

The compact support of $ρ$ makes $X_{0}$ almost surely bounded, and its independence from $W$ is part of the Example. The restart map is explicit: for $s \leq r \leq T$ , $X_{r} = X_{s} + (W_{r} - W_{s})$ . The SDE has $b = 0$ and $σ = I_{d}$ , so it is a globally Lipschitz strong SDE; the convolution and heat equation in [F1] give the stated positive-time marginal density. The separate augmented joint and conditional uniqueness requirements are explicitly assumed, exactly as listed in [A1].

2.1A1F1step 1.1∎

Apply Anderson's theorem with $t_{0} = 0$ , $b = 0$ , $a = I_{d}$ , $\nabla ⁣ \cdot a = 0$ , and $p_{t}$ from [F1]. Its reverse drift is $- b + \nabla ⁣ \cdot a + a \nabla \log p_{t} = \nabla \log p_{t}$ , and the reverse diffusion covariance is $I_{d}$ . Since $p_{t}$ is only used for $t > 0$ , this gives the stated equation for $u < T$ and asserts nothing about a score at $u = T$ .

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

27 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

B. D. O. Anderson, Reverse-time diffusion equation models, Sections 3–4 (standard reference, not scraped)