OAI/MeasureTheory/Falconer/Geometry/DyadicPacking.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PlanarFalconer.dyadicPaths line 11
  2. theorem OAI.PlanarFalconer.mem_dyadicPaths line 16
  3. theorem OAI.PlanarFalconer.DyadicSquare.descendant_side line 25
  4. theorem OAI.PlanarFalconer.DyadicSquare.descendants_disjoint line 33
  5. theorem OAI.PlanarFalconer.DyadicSquare.mem_descendant_at_depth line 52
  6. def OAI.PlanarFalconer.DyadicSquare.box line 69
  7. def OAI.PlanarFalconer.pairToPlane line 72
  8. theorem OAI.PlanarFalconer.pairToPlane_mem line 74
  9. theorem OAI.PlanarFalconer.DyadicSquare.box_measurable line 81
  10. theorem OAI.PlanarFalconer.DyadicSquare.box_area line 84
  11. theorem OAI.PlanarFalconer.DyadicSquare.boxes_disjoint line 88
  12. theorem OAI.PlanarFalconer.plane_coordinate_dist_le line 96
  13. theorem OAI.PlanarFalconer.box_subset_of_meets_ball line 100
  14. def OAI.PlanarFalconer.cellsMeeting line 117
  15. theorem OAI.PlanarFalconer.dyadic_ball_card_le line 123
  16. theorem OAI.PlanarFalconer.dyadic_ball_measure_le line 170