OAI/NumberTheory/DirichletL/Hecke/Theta.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SevenEighths.HeckeTheta.locallyIntegrableOn_sum line 13

    Also declared: ComparatorChallenges/HeckeSevenEighths.lean:155 (same declaration text).

  2. def OAI.SevenEighths.HeckeTheta.finitePair line 19

    Also declared: ComparatorChallenges/HeckeSevenEighths.lean:161 (same declaration text).

  3. def OAI.SevenEighths.HeckeTheta.regroup line 52
  4. def OAI.SevenEighths.HeckeTheta.residueEquiv line 58
  5. def OAI.SevenEighths.HeckeTheta.periodicCoeff line 61
  6. def OAI.SevenEighths.HeckeTheta.theta line 64
  7. def OAI.SevenEighths.HeckeTheta.pair line 68

    Also declared: ComparatorChallenges/HeckeSevenEighths.lean:194 (same declaration text).

  8. theorem OAI.SevenEighths.HeckeTheta.pair_k line 73
  9. theorem OAI.SevenEighths.HeckeTheta.theta_hasSum line 76
  10. theorem OAI.SevenEighths.HeckeTheta.theta_eq_pair line 112
  11. theorem OAI.SevenEighths.HeckeTheta.pair_fā‚€ line 116
  12. def OAI.SevenEighths.HeckeTheta.dualScalar line 134
  13. theorem OAI.SevenEighths.HeckeTheta.pair_gā‚€ line 138
  14. theorem OAI.SevenEighths.HeckeTheta.pair_gā‚€_eq_zero line 150
  15. def OAI.SevenEighths.HeckeTheta.completed line 153

    Also declared: ComparatorChallenges/HeckeSevenEighths.lean:199 (same declaration text).

  16. theorem OAI.SevenEighths.HeckeTheta.completed_differentiableAt line 155
  17. theorem OAI.SevenEighths.HeckeTheta.pair_hasMellin line 159
  18. def OAI.SevenEighths.HeckeTheta.latticeL line 164

    Also declared: ComparatorChallenges/HeckeSevenEighths.lean:201 (same declaration text).

  19. theorem OAI.SevenEighths.HeckeTheta.completed_differentiableAt_of_mean_zero line 167
  20. theorem OAI.SevenEighths.HeckeTheta.latticeL_differentiableAt line 172
  21. def OAI.SevenEighths.HeckeTheta.regularizedCompleted line 183
  22. theorem OAI.SevenEighths.HeckeTheta.regularizedCompleted_differentiableAt line 186
  23. theorem OAI.SevenEighths.HeckeTheta.regularizedCompleted_eq line 193
  24. def OAI.SevenEighths.HeckeTheta.regularizedLatticeL line 203
  25. theorem OAI.SevenEighths.HeckeTheta.regularizedLatticeL_differentiableAt line 206
  26. theorem OAI.SevenEighths.HeckeTheta.regularizedLatticeL_eq line 214
  27. theorem OAI.SevenEighths.HeckeTheta.completed_functional_equation line 221