OAI/NumberTheory/CubicGauss/GaussianPoisson.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

Poisson summation for shifted Gaussian functions on the hexagonal lattice.

  1. def OAI.CubicFirstMoment.HeckeTheta.hexQ line 14
  2. lemma OAI.CubicFirstMoment.HeckeTheta.hexQ_lower line 16
  3. lemma OAI.CubicFirstMoment.HeckeTheta.completed_square line 20
  4. def OAI.CubicFirstMoment.HeckeTheta.EisensteinGaussianPoissonStatement line 26
  5. lemma OAI.CubicFirstMoment.HeckeTheta.summable_cexp_quadratic line 36
  6. lemma OAI.CubicFirstMoment.HeckeTheta.first_poisson_exponent line 44
  7. lemma OAI.CubicFirstMoment.HeckeTheta.shifted_gaussian_exponent line 55
  8. lemma OAI.CubicFirstMoment.HeckeTheta.shifted_gaussian_dual_exponent line 60
  9. lemma OAI.CubicFirstMoment.HeckeTheta.shifted_gaussian_poisson line 70
  10. lemma OAI.CubicFirstMoment.HeckeTheta.shifted_gaussian_summable line 95
  11. lemma OAI.CubicFirstMoment.HeckeTheta.norm_real_phase line 105
  12. def OAI.CubicFirstMoment.HeckeTheta.middle line 109
  13. lemma OAI.CubicFirstMoment.HeckeTheta.middle_phase_norm line 114
  14. lemma OAI.CubicFirstMoment.HeckeTheta.middle_summable line 120
  15. lemma OAI.CubicFirstMoment.HeckeTheta.eisenstein_first_exponent line 131
  16. lemma OAI.CubicFirstMoment.HeckeTheta.first_poisson_step line 139
  17. lemma OAI.CubicFirstMoment.HeckeTheta.second_poisson_exponent line 170
  18. lemma OAI.CubicFirstMoment.HeckeTheta.second_poisson_step line 176
  19. lemma OAI.CubicFirstMoment.HeckeTheta.poisson_normalization line 213
  20. theorem OAI.CubicFirstMoment.HeckeTheta.eisenstein_gaussian_poisson line 232
  21. lemma OAI.CubicFirstMoment.HeckeTheta.hex_gaussian_summable line 239