OAI/NumberTheory/DirichletL/Eisenstein/SourceQuotient.lean

GitHub source file

63 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.CubicEisenstein.SourceKernelQuotient line 83
  2. def OAI.CubicEisenstein.sourceComplexMatrix line 85
  3. lemma OAI.CubicEisenstein.globalKubotaKernel_source_conjugate_mem line 88
  4. def OAI.CubicEisenstein.kernelSourceConjugate line 92
  5. lemma OAI.CubicEisenstein.kernelSourceConjugate_coe line 99
  6. lemma OAI.CubicEisenstein.source_action_respects_kernel line 102
  7. def OAI.CubicEisenstein.kernelSourceAction line 114
  8. lemma OAI.CubicEisenstein.kernelSourceAction_mk line 117
  9. lemma OAI.CubicEisenstein.kernelSourceAction_one line 121
  10. lemma OAI.CubicEisenstein.kernelSourceAction_mul line 127
  11. lemma OAI.CubicEisenstein.kernelSourceAction_continuous line 135
  12. def OAI.CubicEisenstein.kernelSourceHomeomorph line 138
  13. lemma OAI.CubicEisenstein.kernelSourceAction_fundamentalDomain line 146
  14. lemma OAI.CubicEisenstein.kernelSourceAction_measurePreserving line 164
  15. def OAI.CubicEisenstein.kernelSourcePullback line 194
  16. lemma OAI.CubicEisenstein.kernelSourcePullback_ae_eq line 197
  17. lemma OAI.CubicEisenstein.kernelSourcePullback_one line 202
  18. lemma OAI.CubicEisenstein.kernelSourcePullback_comp line 207
  19. lemma OAI.CubicEisenstein.kernelSourcePullback_surjective line 217
  20. def OAI.CubicEisenstein.kernelSourceUnitary line 222
  21. lemma OAI.CubicEisenstein.kernelSourceUnitary_apply line 225
  22. lemma OAI.CubicEisenstein.kernelSourceAction_of_kernel line 230
  23. lemma OAI.CubicEisenstein.rationalCongruenceThree_in_kernel line 237
  24. lemma OAI.CubicEisenstein.kernelSourceAction_rational_eq line 242
  25. lemma OAI.CubicEisenstein.kernelSourcePullback_rational_eq line 254
  26. def OAI.CubicEisenstein.kernelSourceProjection line 262
  27. lemma OAI.CubicEisenstein.kernelSourceProjection_apply line 266
  28. lemma OAI.CubicEisenstein.kernelSourceProjection_eq_twentyFour line 272
  29. lemma OAI.CubicEisenstein.norm_kernelSourceProjection_apply line 280
  30. lemma OAI.CubicEisenstein.norm_kernelSourceProjection line 295
  31. lemma OAI.CubicEisenstein.sourceSection_mul_reduction line 299
  32. lemma OAI.CubicEisenstein.kernelSourcePullback_projection line 305
  33. lemma OAI.CubicEisenstein.kernelSourceProjection_fixed line 318
  34. lemma OAI.CubicEisenstein.kernelSourceProjection_idempotent line 329
  35. def OAI.CubicKubota.sourceLevelInclusion line 338
  36. lemma OAI.CubicKubota.sourceLevelInclusion_character line 343
  37. lemma OAI.CubicKubota.sourceSection_factor line 347
  38. theorem OAI.CubicEisenstein.kernelSourceProjection_covariance line 378
  39. lemma OAI.CubicEisenstein.kernelSourceProjection_ae_eq line 400
  40. lemma OAI.CubicEisenstein.kernelSourceProjection_representative line 413
  41. lemma OAI.CubicEisenstein.kernelSourceProjection_hyperbolic_average line 430
  42. lemma OAI.CubicEisenstein.kernelSourceAction_level line 444
  43. lemma OAI.CubicEisenstein.kernelSourcePullback_level line 447
  44. theorem OAI.CubicEisenstein.kernelSourceProjection_covariance_of_level line 450
  45. def OAI.CubicEisenstein.periodVector line 468
  46. lemma OAI.CubicEisenstein.periodVector_apply line 470
  47. def OAI.CubicEisenstein.periodTorus line 477
  48. lemma OAI.CubicEisenstein.periodTorus_periodVector line 480
  49. def OAI.CubicEisenstein.periodFrequencyEquiv line 485
  50. lemma OAI.CubicEisenstein.periodFrequencyEquiv_apply line 488
  51. lemma OAI.CubicEisenstein.periodVector_character line 491
  52. lemma OAI.CubicEisenstein.periodTorus_mFourier line 512
  53. lemma OAI.CubicEisenstein.periodFrequencyEquiv_neg line 523
  54. lemma OAI.CubicEisenstein.cuspFrequency_neg line 532
  55. lemma OAI.CubicEisenstein.periodVector_eq_lattice line 535
  56. lemma OAI.CubicEisenstein.periodVector_map_volume line 540
  57. def OAI.CubicEisenstein.periodCube line 554
  58. lemma OAI.CubicEisenstein.periodVector_preimage_domain line 556
  59. lemma OAI.CubicEisenstein.periodDomain_integral_coordinates line 562
  60. lemma OAI.CubicEisenstein.periodCube_ae_Ioc line 579
  61. lemma OAI.CubicEisenstein.periodTorus_integral line 587
  62. lemma OAI.CubicEisenstein.periodTorus_fourierCoeff line 593
  63. lemma OAI.CubicEisenstein.periodTorus_L2_ext line 605