OAI/MeasureTheory/Falconer/Angular/SphereRotations.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Rotation invariance of the actual sphere measure

The sphere measure used by the energy is defined from Euclidean volume. Its invariance follows directly by transporting its defining truncated cones through a linear isometry.

  1. def OAI.Falconer.sphereMap line 18
  2. theorem OAI.Falconer.continuous_sphereMap line 21
  3. def OAI.Falconer.sphereHomeomorph line 25
  4. theorem OAI.Falconer.sphereMap_cone_preimage line 33
  5. theorem OAI.Falconer.sphereMap_measurePreserving line 50
  6. theorem OAI.Falconer.sphere_integral_rotation line 59