OAI/Geometry/RCD/Sobolev/InteriorBoundedGradientRepresentative.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Bounded gradient representatives between two concentric balls

The cutoff gap, rather than the inner radius, controls the global Lipschitz extension. This allows every strict interior fraction.

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