OAI/Geometry/RCD/Heat/BakryLedouxScalarBochner.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The Bakry--Ledoux estimate yields the exact compact scalar BE input

The positive-time estimate is passed through the actual heat approximation. Uniform Sobolev bounds of the energy density, the L² source limit, and bounded test pairings retain the dimensional term. This is the compact specialization of EKS, arXiv:1303.4382v2, Theorem 4.8.

  1. theorem OAI.RegularPointCoordinates.IntegratedBakryLedoux.compact_bochner_sobolev_test line 21
  2. theorem OAI.RegularPointCoordinates.IntegratedBakryLedoux.scalarBochner line 110