OAI/MeasureTheory/Falconer/Fourier/FourierEnergy.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PlanarFalconer.rieszEnergyOn line 13
  2. def OAI.PlanarFalconer.gaussianQuadraticOn line 16
  3. def OAI.PlanarFalconer.sourceEnergyConstant line 19
  4. theorem OAI.PlanarFalconer.sourceEnergyConstant_pos line 23
  5. theorem OAI.PlanarFalconer.rieszEnergyOn_gaussian_mixture line 30
  6. theorem OAI.PlanarFalconer.source_fourier_energy_identity line 61
  7. theorem OAI.PlanarFalconer.rieszEnergyOn_plane line 105
  8. theorem OAI.PlanarFalconer.planar_fourier_energy_identity line 108
  9. theorem OAI.PlanarFalconer.line_fourier_energy_identity line 117
  10. theorem OAI.PlanarFalconer.finite_fourier_energy_of_ball_bound line 124