1.bib · Book p. 40 · PDF p. 52
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 Itô's formula yields the formal Langevin generator. 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
- The weighted integration-by-parts identity first needs compactly supported test functions or a justified cutoff limit.
- Pointwise exhaustion of a cutoff does not imply convergence of its gradient term under an integral.
- A totalized Fréchet derivative equal to zero outside a support set does not assert differentiability there.
- The score-weighted source field must be integrable before dominated convergence can be applied.
- Formal symmetry, a closed generator on a stated domain, stationarity, and invariance are separate claims.
View Lean formalization
No declaration-level mapping has been accepted for this section. This is a route status, not a failed Lean declaration.