10.3 · Book p. 257 · PDF p. 269
Mirror Langevin
Transfers Langevin ideas to non-Euclidean mirror geometry through a Legendre map and state-dependent diffusion.
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.