OAI/MeasureTheory/Falconer/Estimates/RegularRefinementBound.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A frozen regular refinement with a small fine union cannot have a large coarse union. This combines the actual local and coarse incidence estimates.

  1. theorem OAI.Falconer.regular_refinement_coarse_bound line 12