OAI/MeasureTheory/Falconer/Angular/SphereCapBound.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The actual spherical surface measure has its dimensional cap bound

  1. theorem OAI.Falconer.sphere_cap_bound line 13
  2. def OAI.Falconer.surfaceMeasure line 31
  3. instance OAI.Falconer.surfaceMeasure_finite line 34
  4. theorem OAI.Falconer.surfaceMeasure_ball_bound line 38