OAI/Geometry/RCD/Sobolev/ScalarBochnerConstruction.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Scalar dimensional Bochner for nonpositive curvature

The estimate is derived from FullCD through the actual heat evolution, with no Bakry--Ledoux or second-order input remaining.

  1. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.scalarBochner_nonpositive line 17