OAI/MeasureTheory/Falconer/Estimates/ScalarClosestScale.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Choosing the intermediate dyadic scale from the closest pair of a finite separated set. The entire set is separated at that scale, and two original points witness that the scale is not unnecessarily coarse.

  1. theorem OAI.Falconer.scalar_closest_pair line 11
  2. theorem OAI.Falconer.scalar_closest_dyadic_scale line 26
  3. theorem OAI.Falconer.scalar_dyadic_scale_indices line 42