OAI/Geometry/RCD/Transport/DiagonalHopfRecoverySlope.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

One smoothing sequence with asymptotically sharp local slope bounds

  1. theorem OAI.RegularPointCoordinates.diagonal_hopf_recovery_slope line 14