OAI/MeasureTheory/Falconer/Fourier/GaussianRepresentation.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PlanarFalconer.inverse_power_gaussian_integral line 11
  2. theorem OAI.PlanarFalconer.source_inverse_power_gaussian_integral line 33
  3. theorem OAI.PlanarFalconer.gaussian_mixture_integrable line 38
  4. theorem OAI.PlanarFalconer.source_riesz_kernel_gaussian_mixture line 46
  5. def OAI.PlanarFalconer.gaussianQuadratic line 61
  6. theorem OAI.PlanarFalconer.rieszEnergy_eq_prod line 64
  7. theorem OAI.PlanarFalconer.gaussianQuadratic_le_mass_sq line 69
  8. theorem OAI.PlanarFalconer.rieszEnergy_gaussian_mixture line 81