OAI/MeasureTheory/Falconer/Angular/NormalizedCaps.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The normalized cap partition and its uniform derivative bounds

The normalization uses the same fixed smooth reciprocal for all radii. On the sphere the covering bound makes it the exact reciprocal of the positive bump sum.

  1. def OAI.Falconer.normalizedCap line 17
  2. theorem OAI.Falconer.normalizedCap_contDiff line 21
  3. theorem OAI.Falconer.normalizedCap_properties line 25
  4. theorem OAI.Falconer.normalizedCap_chart_derivatives line 57