OAI/MeasureTheory/Falconer/Angular/SphereProduct.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Actual products of two spherical oscillations

The leading expression keeps both signs at each stationary pole. Its product therefore contains the four radial phases used in the comparable far reduction. The error uses only norm bounds, never derivatives of a stationary remainder.

  1. def OAI.Falconer.stationarySphereApprox line 17
  2. theorem OAI.Falconer.sphere_stationary_expansion_unscaled line 23
  3. theorem OAI.Falconer.sphereOscillation_norm_le_of_bound line 60
  4. theorem OAI.Falconer.norm_complex_pair_approx line 67
  5. theorem OAI.Falconer.sphere_product_stationary_expansion line 88