OAI/MeasureTheory/Falconer/Fourier/SignedStationary.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The two actual stationary signs and their radial scaling

The incoming coefficient is the conjugate coefficient of the antipodal amplitude. Both signs use the original amplitude derivative budget.

  1. def OAI.Falconer.signedStationaryCoefficient line 17
  2. theorem OAI.Falconer.signedStationaryCoefficient_bound line 22
  3. theorem OAI.Falconer.normalizedStationaryCoefficient_scale line 42
  4. theorem OAI.Falconer.signedStationaryCoefficient_scale line 50
  5. theorem OAI.Falconer.directStationarySum_normalized line 59
  6. theorem OAI.Falconer.stationarySphereApprox_signed line 67
  7. theorem OAI.Falconer.DescriptorJetSymbol.signed_stationary_support line 80