HoleDefectCharge.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Charging a finite disjoint hole family to the actual RCD defect

Only relative Bishop--Gromov volume is used. The source balls and their large defect averages are explicit, so no coordinate-surjectivity result is hidden in this estimate.

theorem OAI.RegularPointCoordinates.NoncollapsedRCD.hole_defect_charge line 18