OAI/MeasureTheory/Falconer/Estimates/RegularRefinementContradiction.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The regular-set alternative and the normalized scale comparison exclude a small fine union once the original configuration is refined.

  1. theorem OAI.Falconer.regular_refinement_contradiction line 12