OAI/NumberTheory/DirichletL/Eisenstein/FullFrequencyExpansion.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.CubicEisenstein.thetaFullFrequency_tsum line 84
  2. theorem OAI.CubicEisenstein.sourceFourier_tsum_full_index line 108
  3. theorem OAI.CubicEisenstein.ramifiedFourier_tsum_full_index line 122
  4. lemma OAI.CubicEisenstein.squarefreeCube_scale_le_norm_third line 145
  5. lemma OAI.CubicEisenstein.coefficient_polynomial_of_squarefree_cube_support line 166
  6. theorem OAI.CubicEisenstein.three_cusp_coefficients_polynomial_bound line 183
  7. lemma OAI.CubicEisenstein.coefficient_weighted_summable_of_polynomial line 205
  8. theorem OAI.CubicEisenstein.three_cusp_coefficients_weighted_summable line 232
  9. lemma OAI.CubicEisenstein.derivative_coefficient_weighted_summable line 243
  10. theorem OAI.CubicEisenstein.three_cusp_derivative_coefficients_weighted_summable line 261
  11. lemma OAI.CubicEisenstein.radial_inverse_weight line 275
  12. lemma OAI.CubicEisenstein.radialCoefficient_weighted_summable_of_fourth line 288
  13. theorem OAI.CubicEisenstein.three_cusp_radial_coefficients_weighted_summable line 311
  14. lemma OAI.CubicEisenstein.sourceCuspCoefficients_weighted_summable line 326
  15. theorem OAI.CubicEisenstein.sourceCuspRadialCoefficient_weighted_summable line 334
  16. lemma OAI.CubicEisenstein.SourceCuspDatum.cuspBarProfile_mellin_entire line 363
  17. lemma OAI.CubicEisenstein.SourceCuspDatum.reflection_radial line 368
  18. theorem OAI.CubicEisenstein.completedBesselProfile_eq_finite_cuspProfiles line 378
  19. def OAI.CubicEisenstein.SourceCuspDatum.smoothedKernel line 400
  20. lemma OAI.CubicEisenstein.thetaBesselScale_square line 414
  21. lemma OAI.CubicEisenstein.sourceCuspRadialScale_ratio line 417
  22. lemma OAI.CubicEisenstein.sourceCuspKernel_argument line 422
  23. lemma OAI.CubicEisenstein.SourceCuspDatum.smoothedKernel_eq line 428
  24. lemma OAI.CubicEisenstein.SourceCuspDatum.smoothedKernel_prefactor_norm line 436
  25. lemma OAI.CubicEisenstein.SourceCuspDatum.smoothedKernel_prefactor_norm_le line 443
  26. theorem OAI.CubicEisenstein.completedT_finite_smoothed_reflection line 454
  27. theorem OAI.CubicEisenstein.completedT_canonical_smoothed_reflection line 530
  28. def OAI.CubicEisenstein.fixedCuspReduction line 552
  29. abbrev OAI.CubicEisenstein.FixedCuspSector line 555
  30. instance OAI.CubicEisenstein.(instance at line 557) line 557
  31. def OAI.CubicEisenstein.fixedCuspSector line 561
  32. def OAI.CubicEisenstein.fixedCuspRepresentative line 564
  33. lemma OAI.CubicEisenstein.fixedCuspRepresentative_reduction line 566
  34. lemma OAI.CubicEisenstein.fixedCusp_difference_levelThree line 569
  35. theorem OAI.CubicEisenstein.exists_fixed_cusp_decomposition line 576