OAI/NumberTheory/DirichletL/Eisenstein/ArbitraryCuspPullback.lean

GitHub source file

56 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CubicEisenstein.ramified_omega_relation line 84
  2. def OAI.CubicEisenstein.lowerCuspMatrix line 89
  3. def OAI.CubicEisenstein.ramifiedParabolic line 92
  4. lemma OAI.CubicEisenstein.ramifiedParabolic_mul_lower line 105
  5. lemma OAI.CubicEisenstein.ramifiedParabolic_character line 117
  6. lemma OAI.CubicEisenstein.ramifiedParabolic_omega_value line 127
  7. lemma OAI.CubicEisenstein.ramifiedParabolic_omega_sq_value line 141
  8. def OAI.CubicEisenstein.ramifiedSourceFunction line 162
  9. lemma OAI.CubicEisenstein.ramifiedSourceFunction_continuous line 165
  10. lemma OAI.CubicEisenstein.ramifiedSourceFunction_translate line 168
  11. lemma OAI.CubicEisenstein.ramifiedSourceFunction_omega_translate line 181
  12. lemma OAI.CubicEisenstein.ramifiedSourceFunction_omega_sq_translate line 188
  13. lemma OAI.CubicEisenstein.embedding_cubicExp line 205
  14. def OAI.CubicEisenstein.ramifiedShift10 line 223
  15. def OAI.CubicEisenstein.ramifiedShift19 line 225
  16. lemma OAI.CubicEisenstein.ramifiedShift10_explicit line 227
  17. lemma OAI.CubicEisenstein.ramifiedShift19_explicit line 234
  18. lemma OAI.CubicEisenstein.ramifiedShift10_period line 241
  19. lemma OAI.CubicEisenstein.ramifiedShift19_period line 262
  20. lemma OAI.CubicEisenstein.ramifiedSourceFunction_upper_shift10 line 282
  21. lemma OAI.CubicEisenstein.ramifiedSourceFunction_upper_shift19 line 296
  22. lemma OAI.CubicEisenstein.trace_dephase_periodic line 310
  23. lemma OAI.CubicEisenstein.ramifiedSourceFunction_dephase10_periodic line 327
  24. lemma OAI.CubicEisenstein.ramifiedSourceFunction_dephase19_periodic line 334
  25. def OAI.CubicEisenstein.arbitraryCuspCompact line 347
  26. lemma OAI.CubicEisenstein.arbitraryCuspCompact_isCompact line 350
  27. lemma OAI.CubicEisenstein.arbitraryCusp_image_restrict_le line 354
  28. lemma OAI.CubicEisenstein.arbitraryCusp_smul_measurePreserving line 360
  29. def OAI.CubicEisenstein.arbitraryCuspPullback line 366
  30. lemma OAI.CubicEisenstein.arbitraryCuspPullback_ae line 374
  31. lemma OAI.CubicEisenstein.arbitraryCusp_quasiMeasurePreserving line 389
  32. def OAI.CubicEisenstein.arbitraryCuspQuotientCompact line 407
  33. lemma OAI.CubicEisenstein.arbitraryCuspQuotientCompact_isCompact line 410
  34. lemma OAI.CubicEisenstein.arbitraryCusp_mem_compact line 414
  35. def OAI.CubicEisenstein.arbitraryCuspWeightedPhase line 425
  36. lemma OAI.CubicEisenstein.arbitraryCuspWeightedPhase_continuous line 429
  37. lemma OAI.CubicEisenstein.arbitraryCuspWeightedPhase_bound line 439
  38. lemma OAI.CubicEisenstein.arbitraryCuspFourierTest_memLp line 444
  39. def OAI.CubicEisenstein.arbitraryCuspFourierTestL2 line 452
  40. def OAI.CubicEisenstein.arbitraryCuspHeightFourier line 457
  41. lemma OAI.CubicEisenstein.arbitraryCuspHeightFourier_integral line 462
  42. lemma OAI.CubicEisenstein.arbitraryCuspHeightFourier_restrict line 476
  43. def OAI.CubicEisenstein.arbitraryCuspHeightFamily line 491
  44. lemma OAI.CubicEisenstein.arbitraryCuspHeightFamily_analyticAt line 497
  45. lemma OAI.CubicEisenstein.arbitraryCuspHeightFamily_residue_limit line 506
  46. lemma OAI.CubicEisenstein.arbitraryCuspHeightFamily_initial line 515
  47. lemma OAI.CubicEisenstein.inner_projection_sandwich line 534
  48. lemma OAI.CubicEisenstein.kernelThetaMassProjection_symmetric line 543
  49. lemma OAI.CubicEisenstein.kernelThetaMassProjection_eigenvector line 547
  50. theorem OAI.CubicEisenstein.kernelEisensteinResidueVector_pairing line 570
  51. theorem OAI.CubicEisenstein.kernelEisensteinResidueVector_orthogonal_of_defect line 579
  52. lemma OAI.CubicEisenstein.kernelLocalCorrectedSeed_initial_eq line 588
  53. lemma OAI.CubicEisenstein.kernelLocalCorrectedSeed_cutoff_eq line 606
  54. lemma OAI.CubicEisenstein.kernelEisensteinResidueVector_restrict_cutoff_eq line 632
  55. lemma OAI.CubicEisenstein.kernelL2_eq_of_compact_restrictions line 657
  56. theorem OAI.CubicEisenstein.kernelEisensteinResidueVector_cutoff_independent line 678