11.3 · Book p. 276 · PDF p. 288
Applications of Fisher Information Bounds
Applies Fisher-information guarantees to concrete nonconvex sampling and statistical tasks.
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.