RegularFineGain.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Fine-scale growth for a regular point set. The frozen refinement and all its numerical budgets are obtained from the original configuration.