10.bib · Book p. 268 · PDF p. 280
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 Stochastic-gradient Langevin bounds separate oracle noise from discretization and mixing error. 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
- Stochastic-gradient unbiasedness and variance bounds are conditional statements with a specified filtration or kernel.
- Coordinate schedules, coordinate-dependent step sizes, and anisotropic norms must be measurable and retained in constants.
- Mirror maps need an open effective domain, invertible gradient map, and boundary/nonexplosion control for the transformed diffusion.
- Oracle error, discretization error, and continuous-time convergence remain separate terms.
View Lean formalization
No declaration-level mapping has been accepted for this section. This is a route status, not a failed Lean declaration.