OAI/Geometry/RCD/Metric/ScaledEuclideanHoleBall.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A hole ball at an arbitrary physical target radius

The elementary enlargement step in De Philippis--Gigli (2018), Lemma 3.3, used for the image-volume estimate in Proposition 3.2.

  1. theorem OAI.RegularPointCoordinates.euclidean_hole_ball_at_radius line 17