11.1 · Book p. 272 · PDF p. 284
Approximate First-Order Stationarity via Fisher Information
Uses relative Fisher information as an approximate first-order stationarity criterion for non-log-concave targets.
Open this section in the canonical August 9 source ↗Section 11.1
Relative Fisher information is used as a first-order stationarity measure for non-log-concave sampling, and entropy dissipation supplies an averaged finite-time bound.
Relative Fisher information measures the squared difference between the current score and the target score. Integrating entropy dissipation over time yields a bound for a randomized or averaged output even when global mixing is computationally inaccessible.
Why is this valid?
Define the relative score almost everywhere, prove Fisher-information measurability and finiteness where used, justify entropy dissipation on a stated domain, then add discretization and oracle errors.
Source assumptions
- absolutely continuous time marginals
- finite initial relative entropy
Formal assumptions
- chosen score representative
- finite Fisher-information terms
- justified entropy-dissipation identity
- measurable randomized output time
View Lean formalization
ASTIS exposes the density, score-representative, absolute-continuity, entropy-dissipation, and randomized-time interfaces separately.
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
- non-log-concave stationarity bounds
- algorithmic Fisher-information estimates