OAI/MeasureTheory/Falconer/Angular/SmoothCapPartition.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

A finite smooth cap partition on the actual sphere

These are ambient smooth functions restricted to the sphere. The denominator is extended smoothly away from the sphere, where the covering lower bound need not hold. Quantitative derivative and overlap estimates are separate from this qualitative construction.

  1. def OAI.Falconer.capBump line 21
  2. theorem OAI.Falconer.smooth_cap_partition_on_net line 28
  3. theorem OAI.Falconer.finite_smooth_cap_partition line 77