OAI/NumberTheory/Ostmann/Quadratic/QuadraticFourierSeparation.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Exact logarithmic Fourier separation of a smooth pair weight

  1. theorem OAI.Ostmann.quadratic_schwartz_inversion line 14
  2. theorem OAI.Ostmann.quadratic_log_pair_integrable line 30
  3. theorem OAI.Ostmann.quadratic_finite_log_separation line 38
  4. def OAI.Ostmann.quadraticLogModulate line 77
  5. theorem OAI.Ostmann.quadraticLogModulate_norm line 80
  6. theorem OAI.Ostmann.quadraticSieveEnergy_logModulate line 84
  7. theorem OAI.Ostmann.quadraticDivisorMoment_logModulate line 90