OAI/NumberTheory/DirichletL/Eisenstein/AffineCuspFourier.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CubicEisenstein.affineLowerTerm_eq_shifted line 86
  2. lemma OAI.CubicEisenstein.affineLowerTerm_integrable line 95
  3. lemma OAI.CubicEisenstein.affineLowerTerm_fourier_integral line 101
  4. lemma OAI.CubicEisenstein.affineCuspGaussTerm_factor line 113
  5. lemma OAI.CubicEisenstein.affineCuspTwistedCoefficient_add line 132
  6. lemma OAI.CubicEisenstein.affineLowerTerm_weighted_translate line 145
  7. lemma OAI.CubicEisenstein.affineLowerIntegral_sum_translate line 194
  8. lemma OAI.CubicEisenstein.affineDenominator_integral_formula line 217
  9. lemma OAI.CubicEisenstein.affineCuspFrequency_lift line 257
  10. lemma OAI.CubicEisenstein.affineCusp_norm_factor line 266
  11. theorem OAI.CubicEisenstein.affineCusp_branch_fourier line 272
  12. lemma OAI.CubicEisenstein.hasSum_diagonal_unit_integrals line 318
  13. theorem OAI.CubicEisenstein.diagonal_unit_eisenstein_fourier line 334
  14. lemma OAI.CubicEisenstein.onceCusp_q_norm line 351
  15. lemma OAI.CubicEisenstein.onceCusp_q_absNorm line 363
  16. theorem OAI.CubicEisenstein.diagonal_once_branch_fourier line 369
  17. theorem OAI.CubicEisenstein.quotient_weighted_period_unfold line 399
  18. theorem OAI.CubicEisenstein.character_weighted_period_unfold line 440
  19. def OAI.CubicEisenstein.affinePeriodChar line 464
  20. lemma OAI.CubicEisenstein.affinePeriodChar_mk line 468
  21. lemma OAI.CubicEisenstein.affinePeriodChar_eq_one line 474
  22. lemma OAI.CubicEisenstein.affineCusp_general_weighted_translate line 488
  23. lemma OAI.CubicEisenstein.affineCusp_masked_inner line 543
  24. lemma OAI.CubicEisenstein.affineDenominator_zero line 567
  25. theorem OAI.CubicEisenstein.affineCusp_branch_fourier_masked line 609
  26. theorem OAI.CubicEisenstein.diagonal_once_eisenstein_fourier line 628