OAI/NumberTheory/DirichletL/Eisenstein/SourceCuspKernels.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CubicEisenstein.sourceCuspCoefficients line 86
  2. def OAI.CubicEisenstein.sourceCuspScale line 89
  3. def OAI.CubicEisenstein.sourceCuspBesselConstant line 90
  4. lemma OAI.CubicEisenstein.sourceCuspScale_pos line 92
  5. lemma OAI.CubicEisenstein.ramifiedSource_scaled_fullFunction line 95
  6. theorem OAI.CubicEisenstein.sourceCusp_bessel_expansion line 103
  7. def OAI.CubicEisenstein.sourceCuspZTerm line 118
  8. theorem OAI.CubicEisenstein.sourceCuspZFamily_series line 121
  9. theorem OAI.CubicEisenstein.sourceCuspZTerm_summable line 133
  10. lemma OAI.CubicEisenstein.sourceCuspZTerm_zero line 137
  11. lemma OAI.CubicEisenstein.sourceCuspZTerm_bessel line 140
  12. theorem OAI.CubicEisenstein.thetaTwistedCuspProfile_reflected_series line 149
  13. def OAI.CubicEisenstein.finiteReflectedSourceTerm line 162
  14. theorem OAI.CubicEisenstein.finiteReflectedSourceTerm_summable line 169
  15. theorem OAI.CubicEisenstein.thetaTwistedCuspProfile_reflected_single_series line 175
  16. def OAI.CubicEisenstein.sourceCuspRadialLength line 195
  17. def OAI.CubicEisenstein.sourceCuspRadialScale line 196
  18. def OAI.CubicEisenstein.sourceCuspRadialBaseCoefficient line 198
  19. def OAI.CubicEisenstein.sourceCuspRadialCoefficient line 202
  20. lemma OAI.CubicEisenstein.sourceCuspRadialLength_pos line 206
  21. lemma OAI.CubicEisenstein.sourceCuspRadialScale_pos line 212
  22. lemma OAI.CubicEisenstein.sourceCuspRadialCoefficient_norm line 215
  23. lemma OAI.CubicEisenstein.sourceCuspRadialCoefficient_zero line 219
  24. lemma OAI.CubicEisenstein.sourceCuspRadialLength_frequency line 224
  25. theorem OAI.CubicEisenstein.sourceCuspZTerm_eq_radial line 230
  26. theorem OAI.CubicEisenstein.sourceCuspZFamily_eq_radialBesselProfile line 249
  27. theorem OAI.CubicEisenstein.thetaTwistedCuspProfile_reflected_radial line 255
  28. lemma OAI.CompletedGauss.positive_nat_pow_cpow line 277
  29. lemma OAI.CompletedGauss.positive_reflection_powers line 285
  30. theorem OAI.CompletedGauss.bessel_reflection_scale line 322
  31. lemma OAI.CubicReflectionKernel.paperKernel_three_halves line 347
  32. lemma OAI.CubicReflectionKernel.paperKernel_three_halves_bound line 366
  33. lemma OAI.CompletedGauss.paperKernel_weighted_summable line 390
  34. theorem OAI.CompletedGauss.paperKernel_weighted_mellin line 409
  35. lemma OAI.CompletedGauss.besselSmoothingIntegrand_reflected_kernel_line line 446
  36. theorem OAI.CompletedGauss.completedT_smoothed_reflection line 479
  37. theorem OAI.CompletedGauss.reflected_paperKernel_summable line 541
  38. theorem OAI.CompletedGauss.besselSmoothingIntegral_reflected_kernel line 564
  39. theorem OAI.CompletedGauss.paperKernel_weighted_norm_summable line 608