OAI/MeasureTheory/Falconer/Geometry/ScalarNonporousCover.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The binary alternative compared directly with a covering bound for the original repeated sumset. This avoids multiplying a regularization loss by the number of summands in a Pluennecke estimate.

  1. theorem OAI.Falconer.scalar_nsmul_subset line 11
  2. theorem OAI.Falconer.Regularization.scalar_nonporous_cover_bound line 19
  3. theorem OAI.Falconer.Regularization.scalar_porous_count_of_sumset line 37