OAI/MeasureTheory/Falconer/Fourier/AllDimensionalSpatialFourierSeparation.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Exact separated spatial factors in every dimension. Fourier inversion is applied on Space d, with an integrable coefficient and endpoint phases of norm one.

  1. def OAI.Falconer.spatialFourierCoeff line 12
  2. def OAI.Falconer.spatialFourierCost line 15
  3. def OAI.Falconer.spatialFourierPhase line 18
  4. theorem OAI.Falconer.spatialFourierCost_nonneg line 21
  5. theorem OAI.Falconer.spatialFourierPhase_continuous line 25
  6. theorem OAI.Falconer.spatialFourierPhase_norm line 30
  7. theorem OAI.Falconer.spatialFourierPhase_sub line 34
  8. theorem OAI.Falconer.spatialFourierCoeff_integrable line 43
  9. theorem OAI.Falconer.spatialFourierSeparation_integrable line 47
  10. theorem OAI.Falconer.spatialFourierSeparation line 63
  11. theorem OAI.Falconer.spatialInverseDistance_separation line 79