OAI/MeasureTheory/Falconer/Angular/SphereModel.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The actual Euclidean sphere and its surface measure

The surface measure is induced by polar coordinates of Euclidean Lebesgue measure.

  1. abbrev OAI.Falconer.Sphere line 17
  2. def OAI.Falconer.sphereMeasure line 19
  3. instance OAI.Falconer.sphereMeasure_finite line 22
  4. theorem OAI.Falconer.sphere_norm line 26