3.5 · Book p. 110 · PDF p. 122
Schrödinger Bridge
Formulates Schrödinger bridge problems as entropic path-space interpolation and connects them to stochastic control.
Open this section in the canonical August 9 source ↗Place in the proof route
The chapter uses this material in the route toward Brownian quadratic variation produces the correction in Itô calculus. 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
- Quadratic-variation limits require an explicit convergence mode and partition scheme.
- A stochastic exponential needs measurability and integrability conditions before it defines a change of law.
- Finite-dimensional cylinder identities are not automatically path-space Girsanov theorems.
View Lean formalization
No declaration-level mapping has been accepted for this section. This is a route status, not a failed Lean declaration.