OAI/MeasureTheory/Falconer/Estimates/RotatedLaws.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Rotation transport of the original point and direction laws

  1. theorem OAI.Falconer.sphereMap_distance line 12
  2. theorem OAI.Falconer.sphereMap_symm_apply line 15
  3. theorem OAI.Falconer.sphereMap_apply_symm line 20
  4. theorem OAI.Falconer.sphereMap_ball_preimage line 25
  5. theorem OAI.Falconer.rotated_point_ball line 32
  6. theorem OAI.Falconer.rotated_direction_ball line 41
  7. theorem OAI.Falconer.rotated_direction_slab line 47
  8. theorem OAI.Falconer.rotated_perpendicular_norm line 59
  9. theorem OAI.Falconer.rotated_incidence line 67