OAI/Geometry/RCD/Sobolev/BoundedLocalBochner.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

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. No derivative of the cutoff source is used.

  1. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.bounded_local_bochner line 24