OAI/Geometry/RCD/Sobolev/InnerBallMeasuredTests.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Exact normalization by the smaller physical ball

  1. theorem OAI.RegularPointCoordinates.cancel_common_mass line 13
  2. theorem OAI.RegularPointCoordinates.inner_ball_measured_test_tendsto line 19