OAI/Geometry/RCD/Heat/NonpositiveBakryLedoux.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Bakry--Ledoux from the actual dimensional heat evolution

For nonpositive curvature, the exponential two-time estimate gives the bounded-weight form with coefficient c(t)=1. This is sufficient for the scalar Bochner limit in EKS, Definition 4.6 and Theorem 4.8.

  1. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.bakryLedoux_nonpositive line 20