OAI/MeasureTheory/Falconer/Angular/AngularPair.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The two independent angular variables in one graph term

For fixed spatial points, the four-point phase separates into two sphere integrals. A nonstationary bound in either variable can thus be used without any angle separation or pointwise truncation of the amplitude.

  1. def OAI.Falconer.sphereOscillator line 16
  2. theorem OAI.Falconer.sphereOscillator_norm line 19
  3. theorem OAI.Falconer.angular_pair_factorization line 23
  4. theorem OAI.Falconer.angular_pair_bound line 38
  5. theorem OAI.Falconer.angular_pair_outer_bound line 53