OAI/Geometry/RCD/Sobolev/BoundedLocalDimensionalBochner.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Dimensional local Bochner inequality for bounded regular functions

Compact localization retains the original function and its L² source. The source needs Sobolev regularity only for the displayed local mixed pairing. The actual Bakry--Ledoux estimate retains the squared-source term; no derivative of the cutoff source is used.

  1. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.bounded_local_dimensional_bochner line 27