OAI/Geometry/RCD/Coordinates/UniformPlanPullback.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Uniform continuity of Sobolev pullbacks along short compressed plans

The modulus depends on the function and compression bound, so it applies to a family of different radial plans as their lengths tend to zero.

  1. theorem OAI.RegularPointCoordinates.uniform_short_plan_pullback line 20