OAI/NumberTheory/DirichletL/Eisenstein/CuspResidues.lean

GitHub source file

67 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CubicEisenstein.levelThree_integral_eq_translation line 82
  2. lemma OAI.CubicEisenstein.periodDomain_unique_translate line 97
  3. def OAI.CubicEisenstein.cuspPeriodRegion line 104
  4. lemma OAI.CubicEisenstein.cuspPeriodRegion_measurable line 107
  5. lemma OAI.CubicEisenstein.kernelProjection_cuspPeriodRegion_injective line 111
  6. def OAI.CubicEisenstein.cuspPeriodStrip line 142
  7. lemma OAI.CubicEisenstein.cuspPeriodStrip_measurable line 145
  8. lemma OAI.CubicEisenstein.kernelProjection_cuspPeriodStrip_injective line 149
  9. lemma OAI.CubicEisenstein.kernelProjection_cuspPeriodStrip_measurePreserving line 155
  10. def OAI.CubicEisenstein.kernelCuspStripSet line 168
  11. lemma OAI.CubicEisenstein.kernelCuspStripSet_measurable line 171
  12. def OAI.CubicEisenstein.kernelCuspStripAverage line 176
  13. lemma OAI.CubicEisenstein.kernelCuspStripAverage_apply line 180
  14. lemma OAI.CubicEisenstein.kernelCuspStripAverage_hyperbolic line 185
  15. def OAI.CubicEisenstein.kernelCuspAverageCompact line 198
  16. lemma OAI.CubicEisenstein.kernelCuspAverageCompact_isCompact line 201
  17. lemma OAI.CubicEisenstein.kernelCuspStripSet_subset_compact line 204
  18. lemma OAI.CubicEisenstein.kernelCuspStripAverage_restrict line 213
  19. def OAI.CubicEisenstein.kernelCuspAverageFamily line 223
  20. lemma OAI.CubicEisenstein.kernelCuspAverageFamily_meromorphicAt line 227
  21. lemma OAI.CubicEisenstein.kernelCuspAverageFamily_residue_limit line 232
  22. lemma OAI.CubicEisenstein.kernelCuspAverageFamily_actual_integral line 239
  23. def OAI.CubicEisenstein.spatialComplexSplit line 255
  24. lemma OAI.CubicEisenstein.spatialComplexSplit_fst line 258
  25. lemma OAI.CubicEisenstein.spatialComplexSplit_snd line 259
  26. lemma OAI.CubicEisenstein.spatialComplexSplit_preserves_volume line 262
  27. lemma OAI.CubicEisenstein.spatialComplexSplit_coordinates line 266
  28. def OAI.CubicEisenstein.cuspCoordinateLift line 274
  29. lemma OAI.CubicEisenstein.cuspCoordinateLift_positive line 277
  30. def OAI.CubicEisenstein.cuspEuclideanStrip line 285
  31. lemma OAI.CubicEisenstein.cuspEuclideanStrip_measurable line 288
  32. lemma OAI.CubicEisenstein.cuspEuclideanStrip_positive line 291
  33. lemma OAI.CubicEisenstein.cuspEuclideanStrip_preimage line 297
  34. lemma OAI.CubicEisenstein.cuspPeriodStrip_integral_coordinates line 304
  35. lemma OAI.CubicEisenstein.hyperbolicEisenstein_continuous line 337
  36. lemma OAI.CubicEisenstein.spatialComplexSplit_symm_eq line 353
  37. lemma OAI.CubicEisenstein.spatialComplexSplit_symm_continuous line 361
  38. lemma OAI.CubicEisenstein.cuspCoordinateLift_continuousAt line 366
  39. lemma OAI.CubicEisenstein.cuspCoordinateLift_weighted_integrable line 374
  40. lemma OAI.CubicEisenstein.hyperbolicEisenstein_cusp_average line 390
  41. def OAI.CubicEisenstein.cuspMainHeightFactor line 416
  42. def OAI.CubicEisenstein.cuspScatterHeightFactor line 419
  43. lemma OAI.CubicEisenstein.cuspHeightPower_integrable line 422
  44. lemma OAI.CubicEisenstein.cuspMainHeightFactor_integral line 428
  45. lemma OAI.CubicEisenstein.cuspScatterHeightFactor_integral line 438
  46. lemma OAI.CubicEisenstein.cuspMainHeightFactor_differentiableAt line 448
  47. lemma OAI.CubicEisenstein.cuspScatterHeightFactor_differentiableAt line 454
  48. def OAI.CubicEisenstein.cuspConstantAverage line 460
  49. lemma OAI.CubicEisenstein.hyperbolicEisenstein_cusp_average_eq line 464
  50. lemma OAI.CubicEisenstein.cuspConstantAverage_differentiableAt line 494
  51. lemma OAI.CubicEisenstein.cuspScatterHeightFactor_center_re_pos line 505
  52. def OAI.CubicEisenstein.cuspConstantAverageResidue line 520
  53. lemma OAI.CubicEisenstein.cuspConstantAverageResidue_ne_zero line 524
  54. lemma OAI.CubicEisenstein.cuspConstantAverage_oneSidedResidue line 534
  55. lemma OAI.CubicEisenstein.kernelSpectralResolvent_analyticAt_of_isUnit line 559
  56. lemma OAI.CubicEisenstein.kernelEisensteinResolvent_analyticAt_of_isUnit line 568
  57. lemma OAI.CubicEisenstein.kernelCuspAverageFamily_analyticAt_of_isUnit line 574
  58. lemma OAI.CubicEisenstein.kernelCuspAverageFamily_analyticAt_nonreal line 591
  59. def OAI.CubicEisenstein.cuspUpperParameterRegion line 597
  60. lemma OAI.CubicEisenstein.cuspUpperParameterRegion_isOpen line 599
  61. lemma OAI.CubicEisenstein.cuspUpperParameterRegion_convex line 603
  62. lemma OAI.CubicEisenstein.cuspConstantAverage_analyticOn_upper line 607
  63. lemma OAI.CubicEisenstein.kernelCuspAverageFamily_eq_upper_of_overlap line 615
  64. lemma OAI.CubicEisenstein.kernelCuspAverageFamily_eq_real_of_upper line 634
  65. lemma OAI.CubicEisenstein.realAbove_tendsto_complex_punctured line 657
  66. lemma OAI.CubicEisenstein.kernelEisensteinResidueVector_average_of_overlap line 670
  67. lemma OAI.CubicEisenstein.kernelEisensteinResidueVector_ne_zero_of_overlap line 687