OAI/MeasureTheory/Falconer/Incidence/PlanarLeafInjection.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Inject the original separated point set into sufficiently small dyadic leaves, preserving the exact finite prefix counts.

  1. theorem OAI.Falconer.separated_planar_cube_card_le_one line 13
  2. theorem OAI.Falconer.exists_planar_leaf_injection line 28
  3. theorem OAI.Falconer.leaf_image_prefixFiber line 56
  4. theorem OAI.Falconer.leaf_image_prefixFiber_card line 68
  5. theorem OAI.Falconer.leaf_prefix_card_ball_bound line 75
  6. theorem OAI.Falconer.leaf_image_prefix_count_bound line 98