OAI/Geometry/RCD/Sobolev/WeakMaximal.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The local maximal estimate for the actual RCD measure

  1. def OAI.RegularPointCoordinates.fiveBallConstant line 14
  2. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.five_ball_doubling line 16
  3. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.local_weak_maximal line 34
  4. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.local_maximal_good_set line 45