OAI/MeasureTheory/Falconer/Shells/DistanceInverse.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Inverse stationary phase for the original Euclidean displacement

The direction and oscillation parameter are exactly z/‖z‖ and r*‖z‖. No projected distance is substituted for the original distance.

  1. def OAI.Falconer.displacementDirection line 16
  2. theorem OAI.Falconer.sphereOscillation_displacement line 19
  3. def OAI.Falconer.inverseDisplacementSum line 39
  4. theorem OAI.Falconer.inverseSphereSum_displacement line 45
  5. theorem OAI.Falconer.displacement_inverse_expansion line 53