CoveredCoercivity.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Coercivity from uniformly large local zero sets

Separated nets cover the whole working ball. Enlarged energy balls have uniform overlap by the CD packing estimate, so their local inequalities sum to one global energy bound with the square of the net radius.

theorem OAI.RegularPointCoordinates.NoncollapsedRCD.covered_zero_set_coercivity line 22