1.ex · Book p. 41 · PDF p. 53
Exercises
The exercises test the chapter's definitions, proof calculations, edge cases, and extensions without changing the chapter's formalization status.
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.