OAI/MeasureTheory/Falconer/Estimates/RefinedPlanarClass.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Re-regularize an actual retained subset. The resulting class retains mass in every occupied block parent, with a single explicit global loss.

  1. theorem OAI.Falconer.Regularization.refine_planar_block_class line 11