OAI/NumberTheory/CubicGram/PeriodicPoisson.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

Periodic lattice Poisson summation and exact trace frequencies.

  1. def OAI.CubicFirstMoment.traceFourierSchwartz line 21
  2. lemma OAI.CubicFirstMoment.traceFourierSchwartz_apply line 25
  3. lemma OAI.CubicFirstMoment.schwartz_summable_eisenstein line 39
  4. lemma OAI.CubicFirstMoment.schwartz_summable_eisenstein_coset line 47
  5. lemma OAI.CubicFirstMoment.traceFourier_summable_eisenstein line 56
  6. lemma OAI.CubicFirstMoment.traceFourier_phase_summable line 62
  7. def OAI.CubicFirstMoment.residueCosetMap line 74
  8. lemma OAI.CubicFirstMoment.residueCosetMap_mk line 77
  9. lemma OAI.CubicFirstMoment.residueCosetMap_bijective line 85
  10. lemma OAI.CubicFirstMoment.periodic_schwartz_summable line 109
  11. theorem OAI.CubicFirstMoment.poisson_eisenstein_periodic line 121
  12. def OAI.CubicFirstMoment.lambdaE line 175
  13. lemma OAI.CubicFirstMoment.lambdaE_coe line 177
  14. lemma OAI.CubicFirstMoment.lambdaE_sq line 179
  15. lemma OAI.CubicFirstMoment.three_lambda_cube line 183
  16. lemma OAI.CubicFirstMoment.primary_coprime_lambda line 187
  17. lemma OAI.CubicFirstMoment.tracePair_div_lambda_integral line 193
  18. lemma OAI.CubicFirstMoment.fourierChar_int line 205
  19. lemma OAI.CubicFirstMoment.tracePhase_div_lambda_one line 212
  20. lemma OAI.CubicFirstMoment.additivePhase_fourierChar line 217
  21. lemma OAI.CubicFirstMoment.tracePhase_congr line 232