2.2 · Book p. 50 · PDF p. 62
Proofs via Markov Semigroup Theory
Uses semigroup interpolation and dissipation identities to prove functional inequalities under curvature assumptions.
Open this section in the canonical August 9 source ↗Place in the proof route
The chapter uses this material in the route toward Markov-semigroup interpolation proves functional inequalities from curvature and dissipation. 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
- State whether Hessian inequalities hold everywhere, almost everywhere, or in a weak convex-analytic sense.
- Track normalization and absolute continuity whenever a potential is used to define a probability law.
- Keep localization inputs separate from the one-dimensional inequality they reduce to.
View Lean formalization
No declaration-level mapping has been accepted for this section. This is a route status, not a failed Lean declaration.