OAI/NumberTheory/DirichletL/Eisenstein/RationalTranslations.lean

GitHub source file

47 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CubicEisenstein.rationalComplex line 84
  2. lemma OAI.CubicEisenstein.rationalUnipotent_nat line 86
  3. lemma OAI.CubicEisenstein.rationalComplex_S_sq_row line 91
  4. lemma OAI.CubicEisenstein.hyperbolicEisenstein_S_sq line 106
  5. lemma OAI.CubicEisenstein.hyperbolicEisenstein_T_pow line 117
  6. lemma OAI.CubicEisenstein.hyperbolicEisenstein_S_even line 121
  7. lemma OAI.CubicEisenstein.hyperbolicEisenstein_bruhat line 127
  8. theorem OAI.CubicEisenstein.sourceEisenstein_four_cusps line 138
  9. def OAI.CubicEisenstein.translatedCuspCompact line 160
  10. lemma OAI.CubicEisenstein.translatedCuspCompact_isCompact line 163
  11. def OAI.CubicEisenstein.translatedCuspFourier line 166
  12. lemma OAI.CubicEisenstein.translatedCuspFourier_integral line 169
  13. lemma OAI.CubicEisenstein.translatedCuspFourier_restrict line 181
  14. def OAI.CubicEisenstein.translatedCuspFamily line 198
  15. lemma OAI.CubicEisenstein.translatedCuspFamily_meromorphicAt line 202
  16. lemma OAI.CubicEisenstein.translatedCuspFamily_analyticAt_nonreal line 208
  17. lemma OAI.CubicEisenstein.translatedCuspFamily_residue_limit line 216
  18. lemma OAI.CubicEisenstein.translatedCuspFamily_actual_integral line 226
  19. theorem OAI.CubicEisenstein.translatedCuspFamily_initial line 244
  20. def OAI.CubicEisenstein.oppositeSource line 272
  21. lemma OAI.CubicEisenstein.oppositeSource_matrix line 274
  22. lemma OAI.CubicEisenstein.hyperbolicEisenstein_opposite_upper line 281
  23. theorem OAI.CubicEisenstein.opposite_cusp_fourier_average line 287
  24. lemma OAI.CubicEisenstein.translatedCuspFamily_opposite_initial line 322
  25. def OAI.CubicEisenstein.continuedUnramifiedGauss line 331
  26. def OAI.CubicEisenstein.unramifiedGaussResidue line 335
  27. theorem OAI.CubicEisenstein.continuedUnramifiedGauss_meromorphicAt_center line 339
  28. theorem OAI.CubicEisenstein.continuedUnramifiedGauss_meromorphicOn_upper line 345
  29. theorem OAI.CubicEisenstein.continuedUnramifiedGauss_residue_limit line 352
  30. theorem OAI.CubicEisenstein.continuedUnramifiedGauss_initial line 367
  31. theorem OAI.CubicEisenstein.continuedUnramifiedGauss_initial_open line 373
  32. lemma OAI.CubicEisenstein.gaussRep_mk_congr line 399
  33. def OAI.CubicEisenstein.cubicUnitCRTMap line 405
  34. lemma OAI.CubicEisenstein.cubicUnitCRTMap_injective line 416
  35. lemma OAI.CubicEisenstein.cubicUnitCRTMap_surjective line 435
  36. def OAI.CubicEisenstein.cubicUnitCRTEquiv line 471
  37. lemma OAI.CubicEisenstein.residueAdditive_unit_crt line 476
  38. lemma OAI.CubicEisenstein.cubicUnitCRT_summand line 491
  39. theorem OAI.CubicEisenstein.cubicUnitGaussSum_crt line 513
  40. theorem OAI.CubicEisenstein.cubicUnitGaussSum_coprime_product line 540
  41. lemma OAI.CubicEisenstein.ramifiedCongruence_zero line 571
  42. lemma OAI.CubicEisenstein.arithmeticResidueSum_zero_ramified line 585
  43. lemma OAI.CubicEisenstein.arithmeticDirichletSeries_zero_separate line 608
  44. def OAI.CubicEisenstein.ramifiedCubeExponent line 639
  45. lemma OAI.CubicEisenstein.zero_ramified_geometric line 650
  46. lemma OAI.CubicEisenstein.zero_ramified_factor line 671
  47. theorem OAI.CubicEisenstein.arithmeticDirichletSeries_zero_unramified line 687