OAI/MeasureTheory/Falconer/Estimates/EndpointCoarsening.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Coarsen actual endpoint centers by their original dyadic prefixes. The point fibers are exact, not geometric enlargements.

  1. theorem OAI.Falconer.planar_prefixChildren_filter line 11
  2. theorem OAI.Falconer.exists_quarterEndpoint_prefix_map line 22
  3. theorem OAI.Falconer.quarterEndpoint_prefix_image line 44
  4. theorem OAI.Falconer.quarterEndpoint_prefix_fiber line 59
  5. theorem OAI.Falconer.quarterEndpoint_prefix_local_fiber line 90
  6. theorem OAI.Falconer.quarterEndpoint_prefix_near line 105