OAI/MeasureTheory/Falconer/Angular/SphereChartIntegral.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

One-coordinate formula for the actual sphere integral

The sole measure input is the published gnomonic density identity. The remaining coordinate split is an ordinary volume-preserving equivalence.

  1. theorem OAI.Falconer.gnomonic_sphere_iterated_integral line 16