OAI/Geometry/RCD/Sobolev/SobolevPositivePower.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Positive integer powers of bounded Sobolev functions

Only positive powers are constructed, so no integrable constant function is required when the ambient measure is infinite.

  1. theorem OAI.RegularPointCoordinates.exists_sobolev_positive_power line 18