8.4 · Book p. 221 · PDF p. 233
Convergence under Log-Concavity
Extends proximal convergence beyond strong convexity to the log-concave setting.
Open this section in the canonical August 9 source ↗Place in the proof route
The chapter uses this material in the route toward The augmentation preserves the desired target as a marginal. 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
- Both conditional distributions require finite, measurable normalizing constants.
- Marginal preservation follows from Tonelli/Fubini only after nonnegativity and measurability are established.
- An oracle specification must state whether samples are exact or approximate.
View Lean formalization
No declaration-level mapping has been accepted for this section. This is a route status, not a failed Lean declaration.