OAI/Geometry/RCD/Coordinates/BoundedRegularLocalization.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Compact regular localization retaining the full L² source

A bounded Lipschitz function with weak L² Laplacian is multiplied by an actual good cutoff. On its plateau both the function and source agree with the originals. No constant-source or source-gradient premise is used.

  1. theorem OAI.RegularPointCoordinates.bounded_regular_localization line 21