4.3 · Book p. 131 · PDF p. 143
Proof via Convex Optimization
Reads sampling as optimization over probability measures and relates the Euler update to splitting in Wasserstein geometry.
Open this section in the canonical August 9 source ↗Place in the proof route
The chapter uses this material in the route toward Wasserstein coupling yields contraction plus a one-step discretization bias. 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 coupled processes must be constructed on one filtered probability space.
- Path-space laws and filtration-adapted drift differences must be explicit.
- Optimization analogies do not replace stochastic existence or integrability assumptions.
View Lean formalization
No declaration-level mapping has been accepted for this section. This is a route status, not a failed Lean declaration.