OAI/NumberTheory/DirichletL/Eisenstein/CubeEigenrelation.lean

GitHub source file

56 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CubicEisenstein.positive_cube_cpow_third line 84
  2. lemma OAI.CubicEisenstein.cubicBesselNormalizer_mul_cube line 95
  3. lemma OAI.CubicEisenstein.eisenstein_norm_eq_sqrt_norm line 112
  4. theorem OAI.CubicEisenstein.sourceResidualFourierCoefficient_cube_sqrt line 116
  5. theorem OAI.CubicEisenstein.sourceArithmeticResidue_cube_of_eigenrelation line 125
  6. def OAI.CubicEisenstein.cubeSourceDifference line 143
  7. lemma OAI.CubicEisenstein.cubeSourceDifference_continuous line 147
  8. lemma OAI.CubicEisenstein.cubeSourceDifference_period_three line 152
  9. lemma OAI.CubicEisenstein.cubeSourceDifference_period_one line 158
  10. lemma OAI.CubicEisenstein.sourceCusp_period_nine line 164
  11. lemma OAI.CubicEisenstein.cubeSource_summand_cusp_period line 172
  12. lemma OAI.CubicEisenstein.cubeSourceDifference_cusp_period line 203
  13. lemma OAI.CubicEisenstein.cubeSourceDifference_cusp_average_zero line 217
  14. lemma OAI.CubicEisenstein.cubeSourceDifference_decay line 223
  15. def OAI.FiniteAutomorphismCover.common line 240
  16. lemma OAI.FiniteAutomorphismCover.common_le line 243
  17. lemma OAI.FiniteAutomorphismCover.common_le_preimage line 246
  18. instance OAI.FiniteAutomorphismCover.common_finiteIndex line 250
  19. def OAI.FiniteAutomorphismCover.toSource line 257
  20. lemma OAI.FiniteAutomorphismCover.toSource_coe line 262
  21. lemma OAI.FiniteAutomorphismCover.toSource_injective line 265
  22. lemma OAI.FiniteAutomorphismCover.toSource_range line 271
  23. instance OAI.FiniteAutomorphismCover.toSource_range_finiteIndex line 284
  24. def OAI.FiniteAutomorphismCover.hom line 289
  25. lemma OAI.FiniteAutomorphismCover.hom_apply line 293
  26. lemma OAI.FiniteAutomorphismCover.hom_injective line 297
  27. def OAI.FiniteAutomorphismCover.target line 301
  28. lemma OAI.FiniteAutomorphismCover.target_le line 304
  29. lemma OAI.FiniteAutomorphismCover.target_le_common_ambient line 309
  30. lemma OAI.FiniteAutomorphismCover.target_eq_map line 313
  31. instance OAI.FiniteAutomorphismCover.target_finiteIndex line 317
  32. def OAI.FiniteAutomorphismCover.equiv line 326
  33. lemma OAI.FiniteAutomorphismCover.equiv_coe line 330
  34. lemma OAI.CubicKubota.literalCube_zero_pair line 342
  35. theorem OAI.CubicKubota.literalCube_zero_intertwines line 383
  36. lemma OAI.CubicKubota.cubeTranslation_complex line 394
  37. lemma OAI.CubicKubota.cubeAverageMatrix_factor_zero line 401
  38. theorem OAI.CubicKubota.literalCube_summand_intertwines line 411
  39. lemma OAI.CubicEisenstein.integralCoverIntertwines_trans line 430
  40. lemma OAI.CubicEisenstein.integralConjugateMap_trans line 439
  41. lemma OAI.CubicEisenstein.integralConjugatePullback_trans line 450
  42. def OAI.CubicEisenstein.kernelCoverLeg line 466
  43. lemma OAI.CubicEisenstein.kernelCoverLeg_representative line 475
  44. lemma OAI.CubicEisenstein.kernelCoverLeg_adjoint_apply line 491
  45. theorem OAI.CubicEisenstein.kernelCoverLeg_adjoint_comp line 509
  46. abbrev OAI.CubicKubota.CubeResidues line 541
  47. def OAI.CubicKubota.cubeCommonAutomorphism line 543
  48. def OAI.CubicKubota.cubeCommonCover line 546
  49. lemma OAI.CubicKubota.cubeCommonCover_le line 550
  50. lemma OAI.CubicKubota.cubeCommonCover_finiteIndex line 553
  51. def OAI.CubicKubota.cubeCommonTarget line 559
  52. lemma OAI.CubicKubota.cubeCommonTarget_le line 564
  53. lemma OAI.CubicKubota.cubeCommonTarget_finiteIndex line 568
  54. def OAI.CubicKubota.cubeCommonEquiv line 576
  55. lemma OAI.CubicKubota.cubeCommon_intertwines line 582
  56. def OAI.CubicKubota.cubeCommonLeg line 597