OAI/MeasureTheory/Falconer/Graphs/DyadicGraph.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Retained graph on the actual dyadic cells

The grid degree estimate is transported to arbitrary finite collections of equal-depth descendants. Their original cube centers define every test. The final Schur bound can therefore be applied directly to the endpoint transforms restricted to those cells.

  1. def OAI.Falconer.retainedDyadicEdge line 18
  2. theorem OAI.Falconer.retainedDyadicEdge_symm line 25
  3. theorem OAI.Falconer.retainedDyadicEdge_iff_grid line 33
  4. theorem OAI.Falconer.dyadic_candidate_grid_bound line 45
  5. theorem OAI.Falconer.retainedDyadic_degree line 66
  6. theorem OAI.Falconer.retainedDyadic_schur line 107