OAI/Geometry/RCD/Harmonic/RadialTimeCapacity.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Source-density control for arbitrary-time radial contraction

  1. theorem OAI.RegularPointCoordinates.timeSupportFactor_eq line 13
  2. theorem OAI.RegularPointCoordinates.timeSupportFactor_inv line 22
  3. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.exists_time_compression line 32