11.bib · Book p. 280 · PDF p. 292
Bibliographical Notes
The bibliographical notes identify the papers and books behind this chapter's arguments and indicate where stronger or more technical versions can be found.
Open this section in the canonical August 9 source ↗Place in the proof route
The chapter uses this material in the route toward Small Fisher information provides a meaningful stationarity certificate for non-log-concave targets. The declaration-level source map is intentionally left inside the formalization layer until exact theorem anchors have been audited.
Why is this valid?
Chapter-level validity conditions
- Relative Fisher information needs an absolutely continuous law and a chosen score representative.
- Entropy dissipation must be justified for the actual process and function domain, not only calculated formally.
- Randomized-time output requires measurability of the time-indexed law and Fisher-information integrand.
- Finite-time discretization and score-error bounds must specify the law under which every squared error is integrated.
- Small Fisher information is a stationarity certificate, not automatically small total variation or rapid multimodal mixing.
View Lean formalization
No declaration-level mapping has been accepted for this section. This is a route status, not a failed Lean declaration.