OAI/NumberTheory/DirichletL/GaussianTheta.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.SevenEighths.GaussianTheta.O line 12
  2. def OAI.SevenEighths.GaussianTheta.gaussian line 16
  3. def OAI.SevenEighths.GaussianTheta.coordinate line 19
  4. theorem OAI.SevenEighths.GaussianTheta.omega3_re line 21
  5. theorem OAI.SevenEighths.GaussianTheta.coordinate_norm_sq line 23
  6. theorem OAI.SevenEighths.GaussianTheta.exists_coordinate line 32
  7. theorem OAI.SevenEighths.GaussianTheta.coordinate_dual_phase line 38
  8. theorem OAI.SevenEighths.GaussianTheta.gaussian_coordinate_shift line 53
  9. theorem OAI.SevenEighths.GaussianTheta.gaussian_dual_coordinate line 68
  10. theorem OAI.SevenEighths.GaussianTheta.shifted_prefactor line 78
  11. theorem OAI.SevenEighths.GaussianTheta.shifted_lattice_poisson line 90
  12. theorem OAI.SevenEighths.GaussianTheta.gaussian_mul line 118
  13. theorem OAI.SevenEighths.GaussianTheta.gaussian_summable line 126
  14. theorem OAI.SevenEighths.GaussianTheta.paperE_norm line 130
  15. theorem OAI.SevenEighths.GaussianTheta.weighted_gaussian_summable line 134
  16. theorem OAI.SevenEighths.GaussianTheta.gaussian_coset_poisson line 147
  17. theorem OAI.SevenEighths.GaussianTheta.finite_gaussian_phase_sum line 168
  18. theorem OAI.SevenEighths.GaussianTheta.periodic_gaussian_poisson line 190
  19. theorem OAI.SevenEighths.GaussianTheta.primitive_gaussian_poisson line 218
  20. def OAI.SevenEighths.GaussianTheta.parameter line 233
  21. def OAI.SevenEighths.GaussianTheta.theta line 235
  22. theorem OAI.SevenEighths.GaussianTheta.parameter_pos line 239
  23. theorem OAI.SevenEighths.GaussianTheta.theta_summable line 245
  24. theorem OAI.SevenEighths.GaussianTheta.parameter_dual line 250
  25. theorem OAI.SevenEighths.GaussianTheta.parameter_prefactor line 259
  26. theorem OAI.SevenEighths.GaussianTheta.theta_functional_equation line 267
  27. def OAI.SevenEighths.GaussianTheta.constantTerm line 282
  28. theorem OAI.SevenEighths.GaussianTheta.constantTerm_eq line 285
  29. theorem OAI.SevenEighths.GaussianTheta.theta_zero_term line 303
  30. theorem OAI.SevenEighths.GaussianTheta.theta_inversion line 308
  31. theorem OAI.SevenEighths.GaussianTheta.theta_root_nonzero line 314
  32. theorem OAI.SevenEighths.GaussianTheta.embedding_unit_norm line 321
  33. theorem OAI.SevenEighths.GaussianTheta.theta_mul_global_unit line 328
  34. theorem OAI.SevenEighths.GaussianTheta.theta_eq_zero_of_global_unit line 344
  35. theorem OAI.SevenEighths.GaussianTheta.global_unit_invariant_of_theta_ne_zero line 350