OAI/MeasureTheory/Falconer/Estimates/SuffixScales.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The suffix scale hypotheses in the manuscript's separated geometry

  1. theorem OAI.Falconer.sqrt_dimension_le line 10
  2. theorem OAI.Falconer.dyadic_side_mono line 16
  3. theorem OAI.Falconer.dyadic_side_le_radius line 21
  4. theorem OAI.Falconer.suffix_linearization_scale line 28
  5. theorem OAI.Falconer.suffix_direction_small line 39
  6. theorem OAI.Falconer.suffix_direction_buffer line 52
  7. theorem OAI.Falconer.uniform_suffix_witness_width line 72
  8. theorem OAI.Falconer.DyadicCube.separated_pairs_lower line 84