OAI/NumberTheory/DirichletL/Eisenstein/MeromorphicResolvent.lean

GitHub source file

79 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CubicEisenstein.kernelSpectralFormOperator_analyticAt line 80
  2. def OAI.CubicEisenstein.kernelMassGram line 95
  3. lemma OAI.CubicEisenstein.selfAdjoint_adjoint_comp line 98
  4. lemma OAI.CubicEisenstein.kernelMassGram_selfAdjoint line 105
  5. def OAI.CubicEisenstein.kernelThetaNull line 108
  6. def OAI.CubicEisenstein.kernelThetaRegular line 111
  7. instance OAI.CubicEisenstein.kernelThetaNull_complete line 113
  8. instance OAI.CubicEisenstein.kernelThetaRegular_complete line 116
  9. instance OAI.CubicEisenstein.kernelThetaNull_finiteDimensional line 119
  10. lemma OAI.CubicEisenstein.kernelThetaNull_gram_eq line 122
  11. lemma OAI.CubicEisenstein.kernelThetaNull_spectral_eq line 131
  12. lemma OAI.CubicEisenstein.kernelMassGram_preserves_regular line 139
  13. lemma OAI.CubicEisenstein.kernelSpectralFormOperator_preserves_regular line 148
  14. def OAI.CubicEisenstein.kernelRegularGram line 153
  15. def OAI.CubicEisenstein.kernelRegularPencil line 156
  16. lemma OAI.CubicEisenstein.kernelRegularPencil_apply line 159
  17. lemma OAI.CubicEisenstein.kernelRegularPencil_center_isUnit line 162
  18. abbrev OAI.CubicEisenstein.endomorphismNormedSpace line 187
  19. lemma OAI.CubicEisenstein.kernelRegularPencil_analyticAt line 193
  20. lemma OAI.CubicEisenstein.kernelRegularPencil_eventually_isUnit line 203
  21. lemma OAI.CubicEisenstein.kernelRegularInverse_analyticAt line 210
  22. def OAI.CubicEisenstein.continuousLinearSandwich line 217
  23. def OAI.CubicEisenstein.kernelRegularLiftCLM line 225
  24. def OAI.CubicEisenstein.kernelRegularInverseLift line 231
  25. lemma OAI.CubicEisenstein.kernelRegularInverseLift_apply line 234
  26. lemma OAI.CubicEisenstein.kernelRegularInverseLift_analyticAt line 239
  27. def OAI.CubicEisenstein.kernelLocalEnergyResolvent line 247
  28. lemma OAI.CubicEisenstein.kernelLocalEnergyResolvent_meromorphicAt line 250
  29. lemma OAI.CubicEisenstein.kernelSpectralFormOperator_regularInverseLift line 264
  30. lemma OAI.CubicEisenstein.kernelLocalEnergyResolvent_right_inverse line 274
  31. lemma OAI.CubicEisenstein.selfAdjoint_one_sub_smul_normal line 289
  32. lemma OAI.CubicEisenstein.kernelSpectralFormOperator_normal line 295
  33. lemma OAI.CubicEisenstein.kernelSpectralFormOperator_isUnit_near line 298
  34. lemma OAI.CubicEisenstein.kernelLocalEnergyResolvent_left_inverse line 310
  35. lemma OAI.CubicEisenstein.kernelLocalEnergyResolvent_eq_inverse line 317
  36. lemma OAI.CubicEisenstein.kernelSpectralFormInverse_meromorphicAt line 329
  37. lemma OAI.CubicEisenstein.meromorphicAt_clm line 340
  38. lemma OAI.CubicEisenstein.meromorphicAt_bilinear line 348
  39. lemma OAI.CubicEisenstein.meromorphicAt_clm_apply line 361
  40. lemma OAI.CubicEisenstein.selfAdjoint_pencil_isUnit_nonreal line 369
  41. lemma OAI.CubicEisenstein.kernelSpectralFormOperator_isUnit_nonreal line 382
  42. lemma OAI.CubicEisenstein.kernelSpectralFormInverse_analyticAt_of_isUnit line 387
  43. lemma OAI.CubicEisenstein.kernelSpectralFormInverse_analyticAt_nonreal line 394
  44. def OAI.CubicEisenstein.kernelL2SandwichCLM line 401
  45. def OAI.CubicEisenstein.kernelSpectralResolvent line 405
  46. lemma OAI.CubicEisenstein.kernelSpectralResolvent_apply line 408
  47. lemma OAI.CubicEisenstein.meromorphicAt_operator_clm line 412
  48. lemma OAI.CubicEisenstein.kernelSpectralResolvent_meromorphicAt line 420
  49. lemma OAI.CubicEisenstein.kernelSpectralResolvent_analyticAt_nonreal line 427
  50. lemma OAI.CubicEisenstein.kernelSpectralResolvent_graph line 435
  51. lemma OAI.CubicEisenstein.kernelSpectralResolvent_left_inverse line 443
  52. lemma OAI.CubicEisenstein.kernelSpectralResolvent_unique line 456
  53. def OAI.CubicEisenstein.kernelEisensteinSpectralParameter line 466
  54. def OAI.CubicEisenstein.kernelEisensteinResolvent line 468
  55. lemma OAI.CubicEisenstein.kernelEisensteinSpectralParameter_center line 471
  56. lemma OAI.CubicEisenstein.kernelEisensteinResolvent_meromorphicAt line 475
  57. lemma OAI.CubicEisenstein.kernelEisensteinSpectralParameter_nonreal line 482
  58. lemma OAI.CubicEisenstein.kernelEisensteinResolvent_analyticAt_nonreal line 491
  59. lemma OAI.CubicEisenstein.kernelEisensteinResolvent_forcing_meromorphicAt line 497
  60. lemma OAI.CubicEisenstein.kernelEisensteinPencil_eventually_isUnit line 502
  61. def OAI.CubicEisenstein.kernelEisensteinL2Correction line 525
  62. lemma OAI.CubicEisenstein.kernelEisensteinL2Correction_meromorphicAt line 529
  63. lemma OAI.CubicEisenstein.kernelEisensteinL2Correction_analyticAt_nonreal line 534
  64. lemma OAI.CubicEisenstein.kernelEisensteinL2Correction_graph line 542
  65. lemma OAI.CubicEisenstein.kernelEisensteinL2Correction_graph_nonreal line 549
  66. lemma OAI.CubicEisenstein.kernelEisensteinL2Correction_graph_eventually line 557
  67. lemma OAI.CubicEisenstein.kernelEisensteinL2Correction_unique line 565
  68. def OAI.CubicEisenstein.kernelThetaMassProjection line 575
  69. def OAI.CubicEisenstein.kernelRegularL2Resolvent line 578
  70. lemma OAI.CubicEisenstein.kernelRegularL2Resolvent_analyticAt line 581
  71. lemma OAI.CubicEisenstein.kernelSpectralResolvent_decomposition line 588
  72. def OAI.CubicEisenstein.kernelEisensteinCorrectionNumerator line 597
  73. def OAI.CubicEisenstein.kernelEisensteinResidueVector line 603
  74. lemma OAI.CubicEisenstein.kernelEisensteinCorrectionNumerator_center line 606
  75. lemma OAI.CubicEisenstein.kernelEisensteinCorrectionNumerator_analyticAt line 612
  76. lemma OAI.CubicEisenstein.kernelEisensteinCorrectionNumerator_eventually line 629
  77. lemma OAI.CubicEisenstein.kernelEisensteinResidueVector_limit line 665
  78. instance OAI.CubicEisenstein.kernelThetaMassProjection_range_finiteDimensional line 673
  79. lemma OAI.CubicEisenstein.kernelEisensteinResidueVector_graph line 681