OAI/NumberTheory/DirichletL/Eisenstein/ScatteringCoefficients.lean

GitHub source file

69 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CubicEisenstein.cubicEisensteinResidue line 83
  2. lemma OAI.CubicEisenstein.cubicEisensteinResidue_nonzero_character line 86
  3. lemma OAI.CubicEisenstein.cubicEisensteinResidue_ne_zero line 94
  4. lemma OAI.CubicEisenstein.cubicEisensteinResidue_character line 97
  5. lemma OAI.CubicEisenstein.cubicEisensteinResidue_eigenvector line 102
  6. lemma OAI.CubicEisenstein.cubicEisensteinResidue_limit line 106
  7. lemma OAI.CubicEisenstein.cubicEisensteinResidue_cusp_average line 111
  8. lemma OAI.CubicEisenstein.cubicEisensteinCorrection_not_continuousAt line 118
  9. lemma OAI.CubicEisenstein.cubicEisensteinResidue_local_limit line 126
  10. lemma OAI.CubicEisenstein.cubicEisensteinLocalFamily_initial_ae line 133
  11. lemma OAI.CubicEisenstein.cubicEisensteinLocalFamily_meromorphicAt line 149
  12. lemma OAI.CubicEisenstein.cubicEisensteinLocalFamily_not_continuousAt line 153
  13. def OAI.CubicEisenstein.whittakerHeight line 175
  14. def OAI.CubicEisenstein.whittakerBase line 176
  15. def OAI.CubicEisenstein.whittakerIntegrand line 177
  16. def OAI.CubicEisenstein.whittakerIntegrandDeriv line 180
  17. def OAI.CubicEisenstein.whittakerProductVolume line 182
  18. lemma OAI.CubicEisenstein.whittakerHeight_ge_one line 185
  19. lemma OAI.CubicEisenstein.whittakerBase_ge line 188
  20. lemma OAI.CubicEisenstein.whittakerBase_ge_one line 191
  21. lemma OAI.CubicEisenstein.whittakerBase_pos line 194
  22. lemma OAI.CubicEisenstein.whittakerIntegrand_continuous line 197
  23. lemma OAI.CubicEisenstein.whittakerIntegrandDeriv_continuous line 216
  24. lemma OAI.CubicEisenstein.whittakerIntegrand_hasDerivAt line 222
  25. lemma OAI.CubicEisenstein.whittakerIntegrand_norm line 235
  26. lemma OAI.CubicEisenstein.whittakerIntegrand_norm_bound line 243
  27. lemma OAI.CubicEisenstein.whittakerIntegrandDeriv_norm_bound line 256
  28. lemma OAI.CubicEisenstein.whittaker_bound_integrable line 280
  29. lemma OAI.CubicEisenstein.whittakerIntegrand_integrable line 291
  30. lemma OAI.CubicEisenstein.whittakerProduct_differentiableAt line 297
  31. lemma OAI.CubicEisenstein.whittakerIntegrand_eq line 318
  32. lemma OAI.CubicEisenstein.whittakerProduct_eq_average line 330
  33. theorem OAI.CubicEisenstein.cuspWhittakerAverage_differentiableAt line 344
  34. lemma OAI.CubicEisenstein.arithmeticDirichletTerm_differentiable line 360
  35. lemma OAI.CubicEisenstein.arithmeticDirichletTerm_norm_mono line 370
  36. theorem OAI.CubicEisenstein.arithmeticDirichletSeries_differentiableAt line 386
  37. theorem OAI.CubicEisenstein.scatteringCoefficient_differentiableAt line 401
  38. theorem OAI.CubicEisenstein.scatteringCoefficient_analyticOnNhd line 406
  39. lemma OAI.CubicEisenstein.cuspPeriodStrip_measure_ne_top line 421
  40. instance OAI.CubicEisenstein.cuspStripFiniteVolume line 428
  41. abbrev OAI.CubicEisenstein.CuspStripL2 line 431
  42. def OAI.CubicEisenstein.kernelCuspPullback line 433
  43. lemma OAI.CubicEisenstein.kernelCuspPullback_ae_eq line 438
  44. def OAI.CubicEisenstein.cuspFourierPhase line 449
  45. lemma OAI.CubicEisenstein.cuspFourierPhase_continuous line 452
  46. lemma OAI.CubicEisenstein.cuspFourierPhase_norm line 459
  47. lemma OAI.CubicEisenstein.cuspFourierTest_memLp line 462
  48. def OAI.CubicEisenstein.cuspFourierTestL2 line 468
  49. def OAI.CubicEisenstein.kernelCuspFourier line 471
  50. lemma OAI.CubicEisenstein.kernelCuspFourier_integral line 474
  51. lemma OAI.CubicEisenstein.kernelCuspFourier_restrict line 484
  52. def OAI.CubicEisenstein.kernelCuspFourierFamily line 497
  53. lemma OAI.CubicEisenstein.kernelCuspFourierFamily_meromorphicAt line 501
  54. lemma OAI.CubicEisenstein.kernelCuspFourierFamily_residue_limit line 506
  55. lemma OAI.CubicEisenstein.kernelCuspFourierFamily_actual_integral line 513
  56. lemma OAI.CubicEisenstein.kernelCuspFourierFamily_of_initial_overlap line 527
  57. lemma OAI.CubicEisenstein.hyperbolicEisenstein_cusp_fourier_average line 555
  58. def OAI.CubicEisenstein.cuspWhittakerHeightFactor line 576
  59. lemma OAI.CubicEisenstein.hyperbolicEisenstein_cusp_fourier_nonzero line 579
  60. lemma OAI.CubicEisenstein.cuspWhittakerHeightFactor_bessel line 603
  61. def OAI.CubicEisenstein.kernelResidualFourierDatum line 616
  62. lemma OAI.CubicEisenstein.kernelCuspFourierFamily_nonzero_of_initial_overlap line 619
  63. lemma OAI.CubicEisenstein.sourceFourierKernel_continuous_freq line 635
  64. lemma OAI.CubicEisenstein.schlafliIntegrand_real line 647
  65. lemma OAI.CubicEisenstein.schlafliIntegral_real_re_pos line 657
  66. lemma OAI.CubicEisenstein.sourceFourierKernel_real_re_pos line 678
  67. lemma OAI.CubicEisenstein.cuspWhittakerHeightFactor_integrable line 690
  68. lemma OAI.CubicEisenstein.cuspWhittakerHeightFactor_real_re_pos line 700
  69. lemma OAI.CubicEisenstein.cuspWhittakerHeightFactor_center_ne_zero line 726