OAI/NumberTheory/CubicGram/Periodization.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

Schwartz lattice periodization and coordinate Poisson summation.

  1. lemma OAI.CubicPoisson.schwartz_summable_lattice line 18
  2. lemma OAI.CubicPoisson.schwartz_locally_summable_lattice line 31
  3. def OAI.CubicPoisson.periodization line 85
  4. lemma OAI.CubicPoisson.periodization_apply line 88
  5. lemma OAI.CubicPoisson.periodization_add line 95
  6. abbrev OAI.CubicPoisson.stdLattice line 104
  7. def OAI.CubicPoisson.torusProjection line 107
  8. lemma OAI.CubicPoisson.torusProjection_openQuotient line 110
  9. lemma OAI.CubicPoisson.mem_stdLattice_iff line 113
  10. lemma OAI.CubicPoisson.torusProjection_eq_iff line 117
  11. def OAI.CubicPoisson.torusRepresentative line 126
  12. lemma OAI.CubicPoisson.torusProjection_representative line 130
  13. lemma OAI.CubicPoisson.periodization_eq_of_projection_eq line 135
  14. def OAI.CubicPoisson.torusPeriodization line 141
  15. lemma OAI.CubicPoisson.torusPeriodization_projection line 152
  16. lemma OAI.CubicPoisson.torusProjection_lattice_add line 156
  17. lemma OAI.CubicPoisson.stdFundamental_restrict line 162
  18. lemma OAI.CubicPoisson.mFourier_point_norm line 179
  19. lemma OAI.CubicPoisson.torusPeriodization_coefficient line 183
  20. def OAI.CubicPoisson.coordinateFourier line 233
  21. lemma OAI.CubicPoisson.coordinateFourier_apply line 240
  22. lemma OAI.CubicPoisson.mFourier_projection line 257
  23. lemma OAI.CubicPoisson.torusPeriodization_coefficient_fourier line 270
  24. lemma OAI.CubicPoisson.stdLattice_coordinates line 278
  25. lemma OAI.CubicPoisson.schwartz_summable_integerCoordinates line 284
  26. lemma OAI.CubicPoisson.torusPeriodization_summable_coefficients line 291
  27. lemma OAI.CubicPoisson.periodization_integerCoordinates line 300
  28. theorem OAI.CubicPoisson.poisson_coordinates line 309
  29. theorem OAI.CubicPoisson.poisson_coordinates_zero line 318