OAI/Geometry/RCD/Sobolev/BoundedGlobalBochner.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Global 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_bochner line 17