OAI/MeasureTheory/Falconer/Radial/HyperplaneFourier.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The Fourier slice identity for the fixed hyperplane fiber.

  1. def OAI.Falconer.euclideanDensityMeasure line 11
  2. theorem OAI.Falconer.euclideanDensityMeasure_finite line 14
  3. theorem OAI.Falconer.hyperplaneProjection_inner line 22
  4. theorem OAI.Falconer.hyperplane_source_fourier_slice line 31
  5. theorem OAI.Falconer.euclidean_schwartz_density_fourier line 42
  6. theorem OAI.Falconer.hyperplaneSchwartzFiber_measure line 59
  7. theorem OAI.Falconer.hyperplaneSchwartzFiber_fourier line 70
  8. theorem OAI.Falconer.hyperplaneSchwartzFiber_energy line 79