OAI/MeasureTheory/Falconer/Radial/SignedRadialKernel.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Radial decay with both actual stationary signs

The two Boolean indices are the outgoing and incoming terms of the full sphere expansion. The original amplitude remains the argument in all four cases; antipodal conjugation is internal to its signed coefficient.

  1. def OAI.Falconer.stationarySign line 16
  2. theorem OAI.Falconer.stationarySign_cases line 18
  3. def OAI.Falconer.signedRadialCoefficient line 22
  4. theorem OAI.Falconer.signed_radial_kernel line 30