OAI/NumberTheory/CubicGauss/HeckeFunctions.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

Hecke theta functional equations, rapid decay and completed Mellin series.

  1. def OAI.CubicFirstMoment.HeckeTheta.heckeGauss line 18
  2. lemma OAI.CubicFirstMoment.HeckeTheta.residueFourier_primitive line 21
  3. lemma OAI.CubicFirstMoment.HeckeTheta.heckeGauss_norm line 32
  4. theorem OAI.CubicFirstMoment.HeckeTheta.primitive_theta_reciprocity line 44
  5. def OAI.CubicFirstMoment.HeckeTheta.heckeRootNumber line 68
  6. lemma OAI.CubicFirstMoment.HeckeTheta.heckeRootNumber_norm line 71
  7. def OAI.CubicFirstMoment.HeckeTheta.heckeScale line 80
  8. def OAI.CubicFirstMoment.HeckeTheta.heckeTheta line 82
  9. lemma OAI.CubicFirstMoment.HeckeTheta.heckeScale_pos line 85
  10. lemma OAI.CubicFirstMoment.HeckeTheta.heckeScale_eq line 89
  11. theorem OAI.CubicFirstMoment.HeckeTheta.heckeTheta_functional_equation line 96
  12. lemma OAI.CubicFirstMoment.HeckeTheta.gaussian_norm line 127
  13. lemma OAI.CubicFirstMoment.HeckeTheta.norm_one_le line 134
  14. lemma OAI.CubicFirstMoment.HeckeTheta.weighted_gaussian_continuous line 138
  15. lemma OAI.CubicFirstMoment.HeckeTheta.weighted_theta_exponential_bound line 156
  16. lemma OAI.CubicFirstMoment.HeckeTheta.weighted_theta_rapid_decay line 190
  17. lemma OAI.CubicFirstMoment.HeckeTheta.heckeTheta_continuous line 202
  18. lemma OAI.CubicFirstMoment.HeckeTheta.heckeTheta_rapid_decay line 208
  19. def OAI.CubicFirstMoment.HeckeTheta.heckeThetaFEPair line 215
  20. lemma OAI.CubicFirstMoment.HeckeTheta.mulChar_zero_of_nonprincipal line 242
  21. lemma OAI.CubicFirstMoment.HeckeTheta.heckeThetaFEPair_strong line 253
  22. def OAI.CubicFirstMoment.HeckeTheta.completedHeckeMellin line 262
  23. theorem OAI.CubicFirstMoment.HeckeTheta.completedHeckeMellin_entire line 267
  24. theorem OAI.CubicFirstMoment.HeckeTheta.completedHeckeMellin_functional_equation line 277
  25. lemma OAI.CubicFirstMoment.HeckeTheta.shifted_int_rpow_summable line 290
  26. lemma OAI.CubicFirstMoment.HeckeTheta.norm_coords_product_bound line 309
  27. lemma OAI.CubicFirstMoment.HeckeTheta.lattice_norm_rpow_summable line 321
  28. instance OAI.CubicFirstMoment.HeckeTheta.(instance at line 347) line 347
  29. lemma OAI.CubicFirstMoment.HeckeTheta.weighted_norm_rpow_summable line 349
  30. def OAI.CubicFirstMoment.HeckeTheta.elementHeckeSeries line 366
  31. lemma OAI.CubicFirstMoment.HeckeTheta.elementHeckeSeries_summable line 369
  32. lemma OAI.CubicFirstMoment.HeckeTheta.heckeTheta_mellin_hasSum line 376
  33. theorem OAI.CubicFirstMoment.HeckeTheta.completedHeckeMellin_eq_series line 406
  34. theorem OAI.CubicFirstMoment.HeckeTheta.completedHeckeMellin_eq_exact_completion line 427