OAI/NumberTheory/DirichletL/Moments/Fourier.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SevenEighths.CenteredMomentFourier.frequencyReduction line 13
  2. theorem OAI.SevenEighths.CenteredMomentFourier.frequencyReduction_mk line 16
  3. theorem OAI.SevenEighths.CenteredMomentFourier.quotientTrace_scaled line 19
  4. def OAI.SevenEighths.CenteredMomentFourier.residueGauss line 32
  5. theorem OAI.SevenEighths.CenteredMomentFourier.residueGauss_supported_mk line 36
  6. theorem OAI.SevenEighths.CenteredMomentFourier.fourierSum_scaled line 45
  7. theorem OAI.SevenEighths.CenteredMomentFourier.actual_gauss_correlation line 52
  8. def OAI.SevenEighths.CenteredMomentFourier.normalizedResidueGauss line 67
  9. theorem OAI.SevenEighths.CenteredMomentFourier.normalized_gauss_correlation line 71