OAI/MeasureTheory/Falconer/Angular/VectorSphereKernel.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The original displacement phase in normalized spherical coordinates

  1. theorem OAI.Falconer.norm_smul_normalizeToSphere line 12
  2. theorem OAI.Falconer.sphereOscillator_normalized line 19
  3. theorem OAI.Falconer.vectorSphereIntegral_eq_oscillation line 33