OAI/MeasureTheory/Falconer/Fourier/StationaryTransport.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Transport of the fixed-pole stationary expansion

A concrete orthogonal reflection takes the chart pole to any requested unit direction. Rotation invariance transports the actual spherical integral. Complex conjugation handles the opposite oscillatory sign. Neither transport uses an additional published input.

  1. def OAI.Falconer.stationaryPoleRotation line 19
  2. theorem OAI.Falconer.stationaryPoleRotation_pole line 23
  3. def OAI.Falconer.poleRotationFormula line 33

    Source documentation

    This formula gives smooth dependence on the requested pole whenever the pole is separated from the antipode of p.

    noncomputable def poleRotationFormula {n : ℕ} (p e x : Space n) : Space n :=
…

    Mentions: OAI.Falconer.Space

  4. theorem OAI.Falconer.stationaryPoleRotation_apply line 36
  5. theorem OAI.Falconer.poleRotationFormula_contDiffAt line 42
  6. theorem OAI.Falconer.stationaryPoleRotation_denominator line 53
  7. def OAI.Falconer.sphereOscillation line 59
  8. theorem OAI.Falconer.gnomonicChart_zero_pole line 64
  9. theorem OAI.Falconer.sphereOscillation_rotate line 78
  10. theorem OAI.Falconer.sphereOscillation_neg line 95