OAI/Geometry/RCD/Heat/BakryLedouxHeatBochner.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The finite-dimensional heat comparison gives weak Bochner on heat data

The extra term in EKS (4.14) is retained in the one-sided derivative. The test has only bounded Sobolev regularity; its heat pairing is right differentiable by the energy form, without a Laplacian of the test.

  1. theorem OAI.RegularPointCoordinates.IntegratedBakryLedoux.heat_bochner line 22