OAI/Geometry/RCD/Metric/EuclideanBallDensityLaw.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Compact ball densities and their translated probability laws

  1. theorem OAI.RegularPointCoordinates.euclideanBallDensity_nonneg line 14
  2. theorem OAI.RegularPointCoordinates.euclideanBallDensity_zero line 18
  3. theorem OAI.RegularPointCoordinates.euclideanBallDensity_mass_pos line 23
  4. def OAI.RegularPointCoordinates.euclideanBallDensityLaw line 28
  5. theorem OAI.RegularPointCoordinates.euclideanBallDensityLaw_support line 33
  6. theorem OAI.RegularPointCoordinates.euclideanBallDensity_translate line 43
  7. theorem OAI.RegularPointCoordinates.euclideanBallDensityLaw_translate line 51