OAI/MeasureTheory/Falconer/Incidence/LocalCellIncidence.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The fine union inside a regular coarse cell retains the original pencil size in the elementary incidence bound. This is the local factor needed in the scale-combination argument.

  1. theorem OAI.Falconer.local_cell_variable_incidence line 12