OAI/MeasureTheory/Falconer/Estimates/UniformScaleCombination.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The scale-product construction for original cell configurations. Coarse pencils and every local pencil are constructed, with explicit logarithmic losses.

  1. theorem OAI.Falconer.uniform_scale_combination line 12