OAI/Geometry/RCD/Metric/InnerConstantMeasure.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Exact inner-ball normalization of a locally constant weak limit

  1. theorem OAI.RegularPointCoordinates.inner_constant_measure line 13
  2. theorem OAI.RegularPointCoordinates.inner_constant_sphere_null line 23
  3. theorem OAI.RegularPointCoordinates.cancel_inner_mass line 37
  4. theorem OAI.RegularPointCoordinates.inner_ball_constant_limit_test line 45