OAI/NumberTheory/DirichletL/Hecke/ThetaSeries.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SevenEighths.HeckeTheta.periodicCoeff_zero line 12
2. theorem OAI.SevenEighths.HeckeTheta.norm_periodicCoeff_le line 16
3. theorem OAI.SevenEighths.HeckeTheta.normForm_coordinates_eq_zero line 21
4. theorem OAI.SevenEighths.HeckeTheta.theta_sub_zero_hasSum line 26
5. theorem OAI.SevenEighths.HeckeTheta.completed_hasSum line 41
6. theorem OAI.SevenEighths.HeckeTheta.latticeL_hasSum line 55