OAI/MeasureTheory/Falconer/Angular/PublishedGnomonic.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The published surface-measure formula used for angular integration

Besau, Hack, Pivovarov, Schuster, Spherical centroid bodies, American Journal of Mathematics 145 (2023), 515–542, DOI 10.1353/ajm.2023.0012, Lemma 2.3(a), with the inverse chart of Lemma 2.2(a). The authors assume sphere dimension at least two.

Only the exact density of ordinary spherical Lebesgue measure under the gnomonic chart is assumed. This input contains no incidence or oscillatory estimate. The resulting integral formulas retain the actual sphere measure used in independentAngularEnergy.

  1. def OAI.Falconer.PublishedGnomonicSurface line 23
  2. theorem OAI.Falconer.gnomonic_integrable line 29
  3. theorem OAI.Falconer.gnomonic_sphere_integral line 45
  4. theorem OAI.Falconer.rotated_gnomonic_sphere_integral line 59