OAI/Geometry/RCD/Heat/BakryLedouxInput.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The integrated Bakry--Ledoux estimate for scalar Bochner inequalities

Erbar--Kuwada--Sturm, arXiv:1303.4382v2, Definition 4.6, equation (4.10), and Theorem 4.8. This is its bounded-weight integrated specialization on functions with an L² weak Laplacian. The Laplacian commutes with heat, so its term is written as heat applied to the actual weak source.

The finite-dimensional term is retained in the weak Bochner formula.

  1. def OAI.RegularPointCoordinates.IntegratedBakryLedoux line 22