OAI/NumberTheory/DirichletL/Eisenstein/InverseCorrespondence.lean

GitHub source file

52 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CubicEisenstein.integralCoverFiber_memLp line 85
  2. theorem OAI.CubicEisenstein.integralCoverTraceFunction_memLp line 101
  3. lemma OAI.CubicEisenstein.integralCoverMap_fiberPoint line 115
  4. lemma OAI.CubicEisenstein.integralCoverTraceFunction_pairing line 121
  5. theorem OAI.CubicEisenstein.integralCoverTrace_toLp_ae line 135
  6. theorem OAI.CubicEisenstein.integralCoverTrace_representative line 181
  7. theorem OAI.CubicEisenstein.integralCoverTrace_cusp_representative line 199
  8. def OAI.CubicEisenstein.primaryDenominatorShift line 226
  9. def OAI.CubicEisenstein.unitLowerDataShift line 236
  10. lemma OAI.CubicEisenstein.affineCusp_term_weighted_period line 239
  11. def OAI.CubicEisenstein.affineCuspBlock line 263
  12. lemma OAI.CubicEisenstein.affineCuspBlock_weighted_periodic line 266
  13. lemma OAI.CubicEisenstein.period_integral_twisted_translation line 283
  14. lemma OAI.CubicEisenstein.affineCuspBlock_integral_translation line 298
  15. lemma OAI.CubicEisenstein.diagonal_unit_weighted_periodic line 316
  16. lemma OAI.CubicEisenstein.diagonal_once_block_expansion line 328
  17. lemma OAI.CubicEisenstein.diagonal_once_weighted_periodic line 342
  18. lemma OAI.CubicEisenstein.diagonal_unit_fourier_shift line 358
  19. lemma OAI.CubicEisenstein.diagonal_once_fourier_shift line 373
  20. def OAI.CubicEisenstein.ramifiedCuspRoot line 392
  21. def OAI.CubicEisenstein.ramifiedCuspScaleUnit line 394
  22. def OAI.CubicEisenstein.ramifiedCuspDirectIndex line 396
  23. def OAI.CubicEisenstein.ramifiedCuspOppositeIndex line 398
  24. lemma OAI.CubicEisenstein.ramified_omega_four line 400
  25. lemma OAI.CubicEisenstein.ramifiedCuspRoot_val line 403
  26. lemma OAI.CubicEisenstein.ramifiedCuspRoot_cube line 406
  27. lemma OAI.CubicEisenstein.ramifiedCuspRoot_primitive line 409
  28. lemma OAI.CubicEisenstein.ramifiedCuspScaleUnit_spec line 417
  29. lemma OAI.CubicEisenstein.ramifiedCusp_neg_inv_square line 425
  30. lemma OAI.CubicEisenstein.ramifiedCusp_opposite_character line 434
  31. lemma OAI.CubicEisenstein.ramifiedCusp_direct_period_constant line 443
  32. lemma OAI.CubicEisenstein.ramifiedCusp_opposite_period_constant line 456
  33. lemma OAI.CubicEisenstein.ramifiedCusp_unit_period_constant line 469
  34. lemma OAI.CubicEisenstein.ramifiedCusp_support_standard line 484
  35. def OAI.CubicEisenstein.unitCuspGaussSeries line 511
  36. lemma OAI.CubicEisenstein.unitCusp_eisenstein_fourier_base line 515
  37. lemma OAI.CubicEisenstein.unitCuspDiagonal_one line 538
  38. lemma OAI.CubicEisenstein.ramifiedCusp_direct_base line 543
  39. lemma OAI.CubicEisenstein.ramifiedCusp_opposite_base line 548
  40. lemma OAI.CubicEisenstein.ramifiedCusp_unit_base line 553
  41. lemma OAI.CubicKubota.cubeKernelLeftGlobal_injective line 568
  42. lemma OAI.CubicKubota.cubeKernelRightGlobal_injective line 576
  43. def OAI.CubicKubota.cubeKernelRangeEquiv line 584
  44. def OAI.CubicKubota.cubeCoverMatrix line 589
  45. lemma OAI.CubicKubota.cubeCoverMatrix_spec line 592
  46. lemma OAI.CubicKubota.cubeCoverMatrix_intertwines line 600
  47. lemma OAI.CubicKubota.cubeLeft_le_levelThree line 611
  48. lemma OAI.CubicKubota.cubeRight_le_levelThree line 615
  49. def OAI.CubicKubota.cubeForwardL2Pullback line 619
  50. def OAI.CubicKubota.cubeInverseL2Pullback line 625
  51. theorem OAI.CubicKubota.cubeInverseL2Pullback_ae line 632
  52. def OAI.CubicKubota.cubeInverseL2Correspondence line 639