`OAI/Geometry/RCD/Coordinates/NormalizedExponentialTilt.lean`

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Normalized positive Sobolev perturbations with controlled mass

theorem OAI.RegularPointCoordinates.SobolevSpace.exists_normalized_exp_tilt line 14