OAI/MeasureTheory/Falconer/Geometry/PlanarGridScales.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Compatible original, grid and analysis scales for a weakly separated pair of projection bases. All costs are polynomial in the inverse separation.

  1. theorem OAI.Falconer.planar_grid_scale_bounds line 9
  2. theorem OAI.Falconer.planar_analysis_dyadic line 50