OAI/NumberTheory/DirichletL/Eisenstein/IntegralCover.lean

GitHub source file

72 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CubicEisenstein.ramifiedOmegaUnit line 85
  2. lemma OAI.CubicEisenstein.ramifiedOmegaUnit_val line 86
  3. lemma OAI.CubicEisenstein.onceCusp_q_as_scale line 89
  4. lemma OAI.CubicEisenstein.onceCusp_q_congr_scale line 94
  5. lemma OAI.CubicEisenstein.onceCusp_q_dvd_three line 103
  6. lemma OAI.CubicEisenstein.onceCusp_q_trace_dvd line 108
  7. lemma OAI.CubicEisenstein.onceCusp_q_dvd_frequency line 114
  8. lemma OAI.CubicEisenstein.onceCusp_period_congruence line 122
  9. def OAI.CubicEisenstein.onceCuspFrequencyQuotient line 130
  10. lemma OAI.CubicEisenstein.onceCuspFrequencyQuotient_spec line 134
  11. def OAI.CubicEisenstein.onceCuspRayUnit line 139
  12. def OAI.CubicEisenstein.onceCuspRayIndex line 141
  13. lemma OAI.CubicEisenstein.onceCuspRayIndex_spec line 144
  14. def OAI.CubicEisenstein.onceCuspGaussSeries line 159
  15. theorem OAI.CubicEisenstein.onceCusp_eisenstein_fourier line 166
  16. lemma OAI.CubicEisenstein.hyperbolicAction_contMDiff line 188
  17. lemma OAI.CubicEisenstein.kernel_contMDiff_of_lift line 206
  18. lemma OAI.CubicEisenstein.kernelSource_comp_contMDiff line 242
  19. def OAI.CubicEisenstein.kernelSourceTest line 248
  20. def OAI.CubicEisenstein.kernelSourceTestLinear line 252
  21. lemma OAI.CubicEisenstein.kernelSourceTest_field line 257
  22. lemma OAI.CubicEisenstein.kernelSourceTest_energyDensity line 266
  23. lemma OAI.CubicEisenstein.kernelSourceTest_quotientDensity line 284
  24. lemma OAI.CubicEisenstein.kernelSourceTest_energy line 291
  25. lemma OAI.CubicEisenstein.kernelSourceTest_mass line 298
  26. lemma OAI.CubicEisenstein.kernelSourceTest_graph_norm line 307
  27. def OAI.CubicEisenstein.kernelSourceEnergyPullback line 313
  28. lemma OAI.CubicEisenstein.kernelSourceEnergyPullback_core line 317
  29. lemma OAI.CubicEisenstein.kernelSourceEnergyPullback_mass line 322
  30. lemma OAI.CubicEisenstein.kernelSourceEnergyPullback_inverse line 338
  31. lemma OAI.CubicEisenstein.kernelSourceEnergyPullback_surjective line 344
  32. theorem OAI.CubicEisenstein.kernelSource_variationalSolution line 348
  33. theorem OAI.CubicEisenstein.kernelSource_variationalResolvent line 358
  34. theorem OAI.CubicEisenstein.kernelSource_operatorGraph line 365
  35. theorem OAI.CubicEisenstein.kernelSource_eigenvector line 371
  36. def OAI.CubicKubota.cubeCuspHeightWeight line 385
  37. lemma OAI.CubicKubota.cubeCuspHeightWeight_zero line 388
  38. lemma OAI.CubicKubota.cubeCuspHeightWeight_three line 394
  39. theorem OAI.CubicKubota.actualCubeCuspPhaseSum_height line 400
  40. theorem OAI.CubicKubota.actualCubeCuspPhaseSum_normalized line 417
  41. def OAI.CubicEisenstein.cubeDilationRoot line 436
  42. lemma OAI.CubicEisenstein.cubeDilationRoot_sq line 439
  43. lemma OAI.CubicEisenstein.cubeDilationRoot_ne_zero line 442
  44. def OAI.CubicEisenstein.cubeAverageMatrix line 448
  45. lemma OAI.CubicEisenstein.cubeAverageMatrix_entries line 452
  46. lemma OAI.CubicEisenstein.cubeAverageMatrix_add_multiple line 462
  47. lemma OAI.CubicEisenstein.cubeAverageMatrix_translate_one line 477
  48. def OAI.CubicEisenstein.cubeAverage line 494
  49. lemma OAI.CubicEisenstein.cubeAverage_summand_congr line 499
  50. lemma OAI.CubicEisenstein.cubeAverageMatrix_action line 512
  51. theorem OAI.CubicEisenstein.cubeAverage_period_one line 526
  52. def OAI.CubicEisenstein.integralCoverMap line 569
  53. lemma OAI.CubicEisenstein.integralCoverMap_projection line 575
  54. lemma OAI.CubicEisenstein.integralCoverMap_measurable line 578
  55. lemma OAI.CubicEisenstein.integralCoverMap_continuous line 583
  56. lemma OAI.CubicEisenstein.integralCoverMap_surjective line 586
  57. abbrev OAI.CubicEisenstein.IntegralCoverCosets line 592
  58. def OAI.CubicEisenstein.integralCoverRep line 594
  59. def OAI.CubicEisenstein.integralCoverSheet line 596
  60. def OAI.CubicEisenstein.integralCoverDomain line 599
  61. lemma OAI.CubicEisenstein.integralCoverSheet_measurable line 602
  62. lemma OAI.CubicEisenstein.integralCoverDomain_measurable line 606
  63. lemma OAI.CubicEisenstein.fundamental_reduction_unique line 611
  64. lemma OAI.CubicEisenstein.integralCoverSheet_pairwiseDisjoint line 621
  65. lemma OAI.CubicEisenstein.integralCoverRep_mul_projection line 631
  66. lemma OAI.CubicEisenstein.integralCover_inclusion_smul line 637
  67. lemma OAI.CubicEisenstein.mul_smul_mem_set_iff line 641
  68. lemma OAI.CubicEisenstein.mem_integralCoverSheet line 646
  69. lemma OAI.CubicEisenstein.integralCoverSheet_membership line 651
  70. lemma OAI.CubicEisenstein.integralCoverDomain_covers line 659
  71. lemma OAI.CubicEisenstein.integralCoverDomain_unique line 675
  72. theorem OAI.CubicEisenstein.integralCoverDomain_isFundamentalDomain line 694