LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6-luna)verified 2026-10-22 (gpt-6.1-sol)

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.

Conditional-score and Tweedie identities for Gaussian smoothing

Statement

Let $d \geq 1$ , let $σ > 0$ , and let $μ$ be a probability measure on the Borel subsets of $R^{d}$ . Write $φ_{σ} (v) = c_{σ, d} \exp (- ∥ v ∥^{2} / (2 σ^{2}))$ for the normalized Gaussian density with respect to Lebesgue measure $d x$ , define $P_{σ} (d u, d x) = μ (d u) φ_{σ} (x - u) d x$ , and set $p_{σ} (x) = \int φ_{σ} (x - u) μ (d u)$ . Define $Q_{σ} (x, d u) = φ_{σ} (x - u) μ (d u) / p_{σ} (x)$ and $m_{σ} (x) = \int u Q_{σ} (x, d u)$ ; under $P_{σ}$ , write $X_{0} (u, x) = u$ and $X_{σ} (u, x) = x$ for the coordinate random vectors, and set $Z = (X_{σ} - X_{0}) / σ$ , so $Z \sim N (0, I_{d})$ is independent of $X_{0}$ . For Borel maps $h, s : R^{d} \to R^{d}$ that are square-integrable with respect to $p_{σ} (x) d x$ , define $R (h) = \int ∥ h (x) - u ∥^{2} P_{σ} (d u, d x)$ and $J (s) = \int ∥ s (x) - (u - x) / σ^{2} ∥^{2} P_{σ} (d u, d x)$ . Then $p_{σ}$ is positive and continuously differentiable, $Q_{σ}$ is the conditional law of $X_{0}$ given $X_{σ} = x$ , and $\nabla \log p_{σ} (x) = (m_{σ} (x) - x) / σ^{2}$ for every $x \in R^{d}$ . If $\int ∥ u ∥^{2} μ (d u) < \infty$ , $m_{σ}$ uniquely minimizes $R$ up to $p_{σ}$ -almost-everywhere equality. The unique minimizer of $J$ is $\nabla \log p_{σ}$ , also up to $p_{σ}$ -almost-everywhere equality. Under the same Gaussian noising, suppose an observation variable $Y$ is conditionally independent of $Z$ given $X_{0}$ , and, for the fixed observation $y$ , $ℓ_{y} : R^{d} \to (0, \infty)$ is the bounded Borel conditional density of $Y$ at $y$ given $X_{0} = u$ , relative to a fixed sigma-finite observation measure, and assume $0 < Z_{y} = \int ℓ_{y} (u) μ (d u) < \infty$ . Let $μ_{y} (d u) = ℓ_{y} (u) μ (d u) / Z_{y}$ and $p_{σ} (x ∣ y) = \int φ_{σ} (x - u) μ_{y} (d u)$ . Then, for $r_{σ} (y ∣ x) = \int ℓ_{y} (u) Q_{σ} (x, d u)$ , the conditional score satisfies $\nabla_{x} \log p_{σ} (x ∣ y) = \nabla_{x} \log p_{σ} (x) + \nabla_{x} \log r_{σ} (y ∣ x)$ . No absolute-continuity or bounded-support assumption on $μ$ is required; $σ > 0$ supplies the full-support smoothing density.

Statement references

Daras et al., §2.2 and Appendix A.1–A.2

Song et al., §§3.3 and 5

Prince, Chapter 18, “Diffusion models”

Facts & Assumptions

Given: The probability measure, positive scale, normalized Gaussian density, joint law and likelihood assumptions in the Statement. The denoising risk uses the additional finite-second-moment hypothesis stated there.

[A1]

The Gaussian kernel has the normalized density displayed in the Statement and $σ > 0$ . Its first and second derivatives follow by coordinate differentiation; each is a polynomial times a Gaussian exponential and is bounded.

[A2]

The observation variable $Y$ is conditionally independent of $Z$ given $X_{0}$ . For the fixed observation $y$ , $ℓ_{y} : R^{d} \to (0, \infty)$ is the bounded Borel conditional density of $Y$ at $y$ given $X_{0} = u$ , relative to a fixed sigma-finite observation measure; its normalizer $Z_{y}$ is finite and positive.

[A3]

Denoising estimators and score predictors are Borel measurable and belong to the square-integrable classes named in the Statement.

[F1]

A probability kernel assigns a measure to each source point, has measurable evaluation functions, and has total mass one at every source point. Measure kernel and probability kernel

[F2]

For sigma-finite measure spaces, nonnegative product-measurable functions have measurable section integrals and the product integral equals either iterated integral. Tonelli's theorem for nonnegative measurable functions on a sigma-finite product

[F3]

A probability measure is a measure of total mass one. Probability measures and probability spaces

[F4]

The Borel sigma-algebra is generated by the open sets, and its members are the Borel subsets. The Borel sigma-algebra of a topological space

Proof

Given: The hypotheses and notation in the Statement.

1.1A1F3

For $v = x - u$ , $\partial_{i} φ_{σ} (v) = - v_{i} φ_{σ} (v) / σ^{2}$ and $\partial_{j} \partial_{i} φ_{σ} (v) = (v_{i} v_{j} / σ^{4} - δ_{i j} / σ^{2}) φ_{σ} (v)$ . Each second derivative is bounded, so for every coordinate direction the difference quotient of $φ_{σ} (x - u)$ converges to its derivative uniformly in $u$ : by the one-variable fundamental theorem of calculus, its error is at most $∣ h ∣ \sup_{v} ∣ \partial_{i i} φ_{σ} (v) ∣ / 2$ . Integrating this uniform bound against $μ$ proves $\partial_{i} p_{σ} (x) = \int \partial_{i} φ_{σ} (x - u) μ (d u)$ . The bounded Hessian also makes this derivative continuous in $x$ . Boundedness and [F3] give $p_{σ} (x) < \infty$ , while strict positivity of $φ_{σ}$ and total mass one give $p_{σ} (x) > 0$ .

2.1A1F1F2F4step 1.1

Tonelli and normalization give $P_{σ} (R^{d} \times R^{d}) = \int μ (d u) \int φ_{σ} (x - u) d x = 1$ , so $P_{σ}$ is a probability law. The change of variables $x = u + σ z$ gives the joint law $μ (d u) φ_{1} (z) d z$ of $(X_{0}, Z)$ , proving the stated Gaussian law and independence. For each Borel $A \subseteq R^{d}$ , the numerator $x \mapsto \int_{A} φ_{σ} (x - u) μ (d u)$ is continuous because the first derivative of $φ_{σ}$ is bounded. Dividing by the positive continuous $p_{σ}$ makes $Q_{σ} (x, A)$ Borel; for fixed $x$ , $Q_{σ} (x, \cdot)$ is a probability measure by its defining ratio. Thus $Q_{σ}$ is a probability kernel by [F1]. Tonelli gives $P_{σ} (A \times B) = \int_{B} p_{σ} (x) Q_{σ} (x, A) d x$ for Borel $A, B$ , so it is the conditional law of the clean coordinate given $x$ . The numerator defining $m_{σ} (x)$ is finite because $∥ u ∥ φ_{σ} (x - u)$ is bounded as a function of $u$ . For each coordinate, the integrand $u_{i} φ_{σ} (x - u)$ is continuous in $x$ and uniformly bounded in $u$ when $x$ ranges over a compact set, so dominated convergence makes its integral continuous. Since $p_{σ}$ is positive and continuous, $m_{σ}$ is Borel.

3.1A1A2step 1.1step 2.1algebra

Substituting the first derivative from step 1.1 gives $\nabla p_{σ} (x) = \int (u - x) φ_{σ} (x - u) μ (d u) / σ^{2}$ . Dividing by $p_{σ} (x) > 0$ yields $\nabla \log p_{σ} (x) = (m_{σ} (x) - x) / σ^{2}$ . Applying the same Gaussian-convolution calculation to the posterior probability $μ_{y}$ shows that $p_{σ} (x ∣ y)$ is positive and continuously differentiable. The definitions give $Z_{y} p_{σ} (x ∣ y) = \int φ_{σ} (x - u) ℓ_{y} (u) μ (d u) = p_{σ} (x) r_{σ} (y ∣ x)$ . Taking logarithms and differentiating in $x$ , with $Z_{y}$ independent of $x$ , gives the conditional-score decomposition.

3.2A3F2step 2.1algebra

By step 2.1, $R (h) = \int p_{σ} (x) \int ∥ h (x) - u ∥^{2} Q_{σ} (x, d u) d x$ , with the iterated-integral identity justified by [F2]. Nonnegativity of $\int ∥ u - m_{σ} (x) ∥^{2} Q_{σ} (x, d u)$ gives $∥ m_{σ} (x) ∥^{2} \leq \int ∥ u ∥^{2} Q_{σ} (x, d u)$ ; integrating and using [F2] proves $m_{σ} \in L^{2} (p_{σ})$ under the finite-second-moment hypothesis. Expanding about $m_{σ} (x)$ makes the cross term vanish because $\int u Q_{σ} (x, d u) = m_{σ} (x)$ , so $R (h) = R (m_{σ}) + \int ∥ h (x) - m_{σ} (x) ∥^{2} p_{σ} (x) d x$ . The last term is nonnegative and vanishes exactly for the same $p_{σ}$ -almost-everywhere class.

4.1A3F2step 3.1step 3.2algebra∎

The conditional mean of $(u - x) / σ^{2}$ under $Q_{σ} (x, d u)$ is $(m_{σ} (x) - x) / σ^{2} = \nabla \log p_{σ} (x)$ by step 3.1. The noise target has finite second moment because $\int ∥ v ∥^{2} φ_{σ} (v) d v < \infty$ ; the conditional-mean square bound then puts $\nabla \log p_{σ}$ in $L^{2} (p_{σ})$ . Expanding the squared score risk around that conditional mean gives $J (s) = J (\nabla \log p_{σ}) + \int ∥ s (x) - \nabla \log p_{σ} (x) ∥^{2} p_{σ} (x) d x$ , so the unique score-risk minimizer is the stated score. Under the finite-second-moment hypothesis of step 3.2, $x$ and $m_{σ} (x)$ are in $L^{2} (p_{σ})$ ; then $s \mapsto h (x) = x + σ^{2} s (x)$ is a bijection between the two predictor classes and $R (h) = σ^{4} J (s)$ , proving the claimed denoiser/score minimizer equivalence.

Depends on

Used by

Measurement-guided reverse-kernel reconstruction Algorithm
Diffusion prior and measurement scores Definition
Diffusion inverse solver families and their target laws Example
Posterior-mean plug-in measurement scores need not be exact Proposition

Dependency tree · two levels

16 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

Giannis Daras et al., A Survey on Diffusion Models for Inverse Problems (2024), arXiv:2410.00083 (standard reference, not scraped)
Yang Song et al., Score-Based Generative Modeling through Stochastic Differential Equations (2021), arXiv:2011.13456 (standard reference, not scraped)
Simon J. D. Prince, Understanding Deep Learning, Chapter 18: Diffusion Models (2026), pp. 363–387; full course notes (standard reference, not scraped)