OAI/Geometry/RCD/Sobolev/BoundedGlobalDimensionalBochner.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Global dimensional Bochner tests for bounded regular functions

Radial cutoff convergence removes the support restriction. The source is only required to belong to the actual Sobolev space.

  1. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.bounded_global_dimensional_bochner line 18