OAI/MeasureTheory/Falconer/Geometry/SimilarityGeometry.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Common similarities for original pairs

Only a common orthogonal map and a positive dilation are used. The direction map is exactly orthogonal, so the original radial cap constants are unchanged.

  1. def OAI.Falconer.pairHomeomorph line 16
  2. theorem OAI.Falconer.pairHomeomorph_apply line 19
  3. def OAI.Falconer.scaledIsometry line 22
  4. theorem OAI.Falconer.scaledIsometry_apply line 26
  5. theorem OAI.Falconer.scaledIsometry_dist line 29
  6. theorem OAI.Falconer.scaledIsometry_normalize_sub line 34
  7. theorem OAI.Falconer.scaledIsometry_radial line 40
  8. theorem OAI.Falconer.scaledIsometry_ball_preimage line 45
  9. theorem OAI.Falconer.HasBorelProductPartition.homeomorph line 60
  10. theorem OAI.Falconer.scaledIsometry_distanceSet line 84
  11. theorem OAI.Falconer.positive_distance_of_scaledIsometry line 94