OAI/MeasureTheory/Falconer/Shells/PositiveTests.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Full-cell projection estimates extracted from actual retained pairs

  1. theorem OAI.Falconer.DyadicCube.mem_ancestor line 15
  2. theorem OAI.Falconer.descriptorEndpointGood_reached line 21
  3. theorem OAI.Falconer.retained_projection_test line 34
  4. theorem OAI.Falconer.DyadicCube.pair_ne_of_separation line 72
  5. theorem OAI.Falconer.DyadicCube.pair_sphere_direction_dist line 88
  6. theorem OAI.Falconer.uniform_full_cell_tests_of_witness line 111