OAI/MeasureTheory/Falconer/Angular/SphereStationaryAssembly.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Algebra and integration for the two stationary poles

These identities retain the original sphere measure and the original ambient amplitude. The antipodal contribution uses the same smooth pole patch as the outgoing contribution.

  1. def OAI.Falconer.antipodalConjugate line 16
  2. theorem OAI.Falconer.antipodalConjugate_contDiff line 19
  3. theorem OAI.Falconer.antipodalConjugate_derivative_norm line 23
  4. theorem OAI.Falconer.sphere_phase_norm line 32
  5. theorem OAI.Falconer.sphereOscillation_integrable line 38
  6. theorem OAI.Falconer.sphereOscillation_pole_partition line 49
  7. theorem OAI.Falconer.sphere_stationary_phase_norm line 76
  8. theorem OAI.Falconer.remove_outgoing_phase line 80
  9. theorem OAI.Falconer.stationary_offPole_scale line 90