OAI/NumberTheory/DirichletL/EisensteinTheta.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SevenEighths.EisensteinTheta.normForm line 13
  2. def OAI.SevenEighths.EisensteinTheta.shearEquiv line 15
  3. def OAI.SevenEighths.EisensteinTheta.parityEquiv line 21
  4. def OAI.SevenEighths.EisensteinTheta.xShift line 24

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

  5. def OAI.SevenEighths.EisensteinTheta.yShift line 25

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

  6. theorem OAI.SevenEighths.EisensteinTheta.normForm_parity line 27
  7. def OAI.SevenEighths.EisensteinTheta.cosetTheta line 35
  8. def OAI.SevenEighths.EisensteinTheta.parityPair line 39

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

  9. theorem OAI.SevenEighths.EisensteinTheta.cosetTheta_hasSum line 43
  10. theorem OAI.SevenEighths.EisensteinTheta.cosetTheta_eq_parity_sum line 78
  11. theorem OAI.SevenEighths.EisensteinTheta.parityPair_k line 82
  12. def OAI.SevenEighths.EisensteinTheta.cosetConstant line 85
  13. theorem OAI.SevenEighths.EisensteinTheta.parityPair_f₀ line 88
  14. theorem OAI.SevenEighths.EisensteinTheta.cosetConstant_eq line 93
  15. def OAI.SevenEighths.EisensteinTheta.completedCoset line 135
  16. theorem OAI.SevenEighths.EisensteinTheta.completedCoset_differentiableAt line 138