OAI/MeasureTheory/Falconer/Incidence/GoodProfileIncidence.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The good-interval gain on the actual retained endpoint centers. Both profile errors and earlier retention costs enter the explicit weak budget.

  1. theorem OAI.Falconer.blockClass_retained_good_gain line 12