OAI/NumberTheory/DirichletL/Moments/FirstLocalization.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SevenEighths.CenteredMomentFirstLocalization.weighted_fourier_summable line 17
  2. theorem OAI.SevenEighths.CenteredMomentFirstLocalization.retained_complex_norm line 29
  3. theorem OAI.SevenEighths.CenteredMomentFirstLocalization.discarded_complex_norm line 33
  4. theorem OAI.SevenEighths.CenteredMomentFirstLocalization.lattice_fourier_split line 37
  5. def OAI.SevenEighths.CenteredMomentFirstLocalization.canonicalRetainedTerm line 67
  6. def OAI.SevenEighths.CenteredMomentFirstLocalization.canonicalZeroTerm line 83
  7. def OAI.SevenEighths.CenteredMomentFirstLocalization.canonicalRetainedPair line 97
  8. def OAI.SevenEighths.CenteredMomentFirstLocalization.canonicalZeroPair line 101
  9. theorem OAI.SevenEighths.CenteredMomentFirstLocalization.reducedFirstSum_split line 105
  10. def OAI.SevenEighths.CenteredMomentFirstLocalization.retainedEnergy line 145
  11. def OAI.SevenEighths.CenteredMomentFirstLocalization.zeroEnergy line 152
  12. theorem OAI.SevenEighths.CenteredMomentFirstLocalization.finiteHeckeEnergy_localized line 159