OAI/Geometry/RCD/Metric/AnnularDerivativeComparison.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Passing sharp annular volume comparison to radial derivatives

  1. theorem OAI.RegularPointCoordinates.derivative_density_le_of_annular_comparison line 12