OAI/MeasureTheory/Falconer/Estimates/ScalarPathCenters.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Real coordinates of the scalar dyadic tree used in the initial regularization. These are the existing geometric descendants.

  1. def OAI.Falconer.scalarPathCenter line 11
  2. theorem OAI.Falconer.scalar_space_dist line 14
  3. theorem OAI.Falconer.scalarPathCenter_separated line 18
  4. theorem OAI.Falconer.scalarPathCenter_injOn line 24
  5. theorem OAI.Falconer.scalarPathCenter_same_parent line 32
  6. theorem OAI.Falconer.Regularization.scalar_prefix_children_length line 41
  7. theorem OAI.Falconer.Regularization.scalar_prefix_children_parent line 50