12.1 · Book p. 283 · PDF p. 295
Introduction
Introduces forward noising and reverse-time SDEs, identifying the marginal score in the reverse drift.
Open this section in the canonical August 9 source ↗Section 12.1
The reverse-time drift uses the score of the forward marginal, and approximation errors become drift errors.
A forward diffusion transports data toward a tractable reference law. Under suitable marginal regularity, the reverse SDE contains the time-dependent score \(\nabla\log\pi_t\); replacing that score and discretizing time create distinct error terms.
Why is this valid?
Choose a density representative, establish spatial and temporal regularity, state the time-reversal theorem, and only then analyze learned-score and discretization errors.
Source assumptions
- regular time marginals
- available score approximation
Formal assumptions
- score representative
- time-reversal regularity
- law under which score error is controlled
View Lean formalization
ASTIS exposes Fisher-information roots but does not yet claim a reverse-time SDE theorem.
AutoSamplingTheory.lsiKlFiSqrtDensityFisherChainIntegralHandoffScalar
theorem lsiKlFiSqrtDensityFisherChainIntegralHandoffScalar
{α ι : Type*} [MeasurableSpace α] [Fintype ι] (mu : Measure α)
{r : α → Real} {dirichlet fisher : Real} {dr dSqrt dLog : ι → α → Real}
(hdirichlet : dirichlet = ∫ x, (∑ i, dSqrt i x ^ 2) ∂mu)
(hfisher : fisher = ∫ x, (r x * ∑ i, dLog i x ^ 2) ∂mu)
(hr : ∀ᵐ x ∂mu, 0 < r x)
(hdSqrt : ∀ᵐ x ∂mu,
∀ i, dSqrt i x = (1 / (2 * Real.sqrt (r x))) * dr i x)
(hdLog : ∀ᵐ x ∂mu, ∀ i, dLog i x = dr i x / r x) :
dirichlet = (1 / 4) * fisher := by
rw [hdirichlet, hfisher]
rw [← integral_const_mul]
exact lsiKlFiSqrtDensityFisherChainIntegralFiniteSum mu hr hdSqrt hdLog
/-- Scalar rearrangement behind the one-sided use of the cited DV formula.
This is not a proof of Donsker--Varadhan. It starts after a cited or
eventually formalized entropy-duality theorem has supplied the variational
upper bound for an admissible test.
-/Imports
- Mathlib.Data.Real.Basic
- Mathlib.Algebra.Order.Archimedean.Real.Basic
- Mathlib.Analysis.Real.Sqrt
- Mathlib.Analysis.Calculus.ParametricIntegral
- Mathlib.Analysis.SpecialFunctions.Log.Basic
- Mathlib.InformationTheory.KullbackLeibler.Basic
- Mathlib.MeasureTheory.Measure.LogLikelihoodRatio
- Mathlib.MeasureTheory.Measure.Tilted
- Mathlib.Probability.Kernel.Condexp
- Mathlib.Probability.Moments.IntegrableExpMul
- AutoSamplingTheory.Core
Local dependencies
No Registry dependency inferred.
Downstream consumers
- diffusion generative models