OAI/Geometry/RCD/Metric/LocalDensityOrder.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Compact Lipschitz tests detect the sign of a local integrable density

  1. theorem OAI.RegularPointCoordinates.local_density_nonneg_of_tests line 16
  2. theorem OAI.RegularPointCoordinates.local_density_nonneg_of_tests_integrableOn line 36