OAI/NumberTheory/DirichletL/Eisenstein/CuspHeight.lean

GitHub source file

71 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CubicEisenstein.kernelCompact_smooth_cutoff line 82
  2. lemma OAI.CubicEisenstein.integral_upper_triangular_height_all line 102
  3. def OAI.CubicEisenstein.fullMatrixHeight line 108
  4. def OAI.CubicEisenstein.fullCuspHeightRelation line 111
  5. abbrev OAI.CubicEisenstein.FullCuspClasses line 112
  6. def OAI.CubicEisenstein.fullCuspOf line 114
  7. def OAI.CubicEisenstein.fullCuspHeight line 116
  8. lemma OAI.CubicEisenstein.fullCuspHeight_of line 119
  9. lemma OAI.CubicEisenstein.fullCuspHeight_continuous line 122
  10. lemma OAI.CubicEisenstein.fullMatrixHeight_eq_of_lower_zero line 126
  11. lemma OAI.CubicEisenstein.fullCuspOf_eq_iff line 132
  12. def OAI.CubicEisenstein.fullCuspTranslate line 151
  13. lemma OAI.CubicEisenstein.fullCuspTranslate_mul line 159
  14. lemma OAI.CubicEisenstein.fullCuspTranslate_one line 164
  15. def OAI.CubicEisenstein.fullCuspRightEquiv line 168
  16. lemma OAI.CubicEisenstein.fullCuspHeight_translate line 174
  17. lemma OAI.CubicEisenstein.fullCuspHeight_high_unique line 181
  18. lemma OAI.CubicEisenstein.fullCusp_profile_finite line 196
  19. def OAI.CubicEisenstein.fullCuspProfileSum line 205
  20. lemma OAI.CubicEisenstein.fullCuspProfileSum_summable line 208
  21. lemma OAI.CubicEisenstein.fullCuspProfileSum_invariant line 212
  22. lemma OAI.CubicEisenstein.fullCuspProfileSum_eq_single line 218
  23. def OAI.CubicEisenstein.cuspBarrierProfile line 233
  24. lemma OAI.CubicEisenstein.cuspBarrierProfile_smooth line 235
  25. lemma OAI.CubicEisenstein.cuspBarrierProfile_zero line 238
  26. lemma OAI.CubicEisenstein.cuspBarrierProfile_nonneg line 242
  27. def OAI.CubicEisenstein.cuspBarrier line 248
  28. lemma OAI.CubicEisenstein.cuspBarrier_summable line 251
  29. lemma OAI.CubicEisenstein.cuspBarrier_one_le line 255
  30. lemma OAI.CubicEisenstein.cuspBarrier_invariant line 259
  31. theorem OAI.CubicEisenstein.cuspBarrier_high line 263
  32. def OAI.CubicEisenstein.kernelQuotientBarrier line 274
  33. lemma OAI.CubicEisenstein.kernelQuotientBarrier_one_le line 280
  34. lemma OAI.CubicEisenstein.kernelQuotientBarrier_fordCusp line 285
  35. lemma OAI.CubicEisenstein.principal_high_locally_finite line 296
  36. def OAI.CubicEisenstein.fullCuspFromPrincipal line 309
  37. lemma OAI.CubicEisenstein.fullCuspFromPrincipal_height line 318
  38. lemma OAI.CubicEisenstein.fullCusp_finite_principal_cover line 326
  39. lemma OAI.CubicEisenstein.full_high_locally_finite line 341
  40. lemma OAI.CubicEisenstein.fullCuspProfileSum_locally_finite line 360
  41. lemma OAI.CubicEisenstein.fullCuspProfileSum_continuous line 370
  42. lemma OAI.CubicEisenstein.cuspBarrier_continuous line 378
  43. lemma OAI.CubicEisenstein.fullCuspHeight_chart_contDiffAt line 389
  44. lemma OAI.CubicEisenstein.fullCuspProfileSum_chart_contDiffAt line 404
  45. lemma OAI.CubicEisenstein.cuspBarrier_chart_contDiffAt line 414
  46. lemma OAI.CubicEisenstein.kernelQuotientBarrier_continuous line 421
  47. lemma OAI.CubicEisenstein.kernelQuotientBarrier_contMDiff line 425
  48. lemma OAI.CubicEisenstein.cuspBarrier_euclidean_contDiffAt line 444
  49. def OAI.CubicEisenstein.positiveHeightLaplacian line 455
  50. def OAI.CubicEisenstein.cuspBarrierDefectProfile line 458
  51. lemma OAI.CubicEisenstein.positiveHeightLaplacian_smooth line 461
  52. lemma OAI.CubicEisenstein.cuspBarrierDefectProfile_smooth line 466
  53. lemma OAI.CubicEisenstein.cuspBarrierDefectProfile_zero line 471
  54. lemma OAI.CubicEisenstein.cuspBarrierDefectProfile_one line 482
  55. def OAI.CubicEisenstein.cuspBarrierDefect line 495
  56. lemma OAI.CubicEisenstein.cuspBarrierDefect_invariant line 498
  57. lemma OAI.CubicEisenstein.cuspBarrierDefect_high line 503
  58. def OAI.CubicEisenstein.kernelQuotientBarrierDefect line 514
  59. lemma OAI.CubicEisenstein.kernelQuotientBarrierDefect_hasCompactSupport line 520
  60. lemma OAI.CubicEisenstein.kernelQuotientBarrierDefect_continuous line 536
  61. def OAI.CubicEisenstein.fullCuspRow line 546
  62. lemma OAI.CubicEisenstein.fullCuspRow_ne_zero line 549
  63. lemma OAI.CubicEisenstein.fullCuspRow_height line 552
  64. def OAI.CubicEisenstein.fullCuspProfileField line 560
  65. lemma OAI.CubicEisenstein.fullCuspProfileField_eq line 563
  66. lemma OAI.CubicEisenstein.fullCuspRows_locally_finite line 567
  67. lemma OAI.CubicEisenstein.fullCuspProfileField_locally_finite line 589
  68. lemma OAI.CubicEisenstein.cast_profile_deriv line 600
  69. lemma OAI.CubicEisenstein.cast_profile_deriv2 line 604
  70. lemma OAI.CubicEisenstein.fullCuspProfile_row_laplacian line 611
  71. lemma OAI.CubicEisenstein.fullCuspProfileField_laplacian line 620