OAI/Geometry/RCD/Metric/BallMassFubini.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Integrating the masses of translated Euclidean balls

  1. theorem OAI.RegularPointCoordinates.lintegral_closedBall_mass line 14