OAI/MeasureTheory/Falconer/Angular/RetainedSmallSphere.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The smaller sphere remains an exact integral

No derivatives of the smaller amplitude are used. Its original value is retained through Fubini, and only its absolute bound is used afterward.

  1. theorem OAI.Falconer.single_profile_sum line 15
  2. theorem OAI.Falconer.stationary_profile_regular line 40
  3. theorem OAI.Falconer.radial_sphere_swap line 65
  4. theorem OAI.Falconer.single_sphere_retained_bound line 111