OAI/NumberTheory/DirichletL/Eisenstein/Rows.lean

GitHub source file

84 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.CubicEisenstein.K line 78
  2. abbrev OAI.CubicEisenstein.O line 79
  3. def OAI.CubicEisenstein.row line 82
  4. lemma OAI.CubicEisenstein.row_mul line 84
  5. lemma OAI.CubicEisenstein.row_ne_zero line 90
  6. lemma OAI.CubicEisenstein.character_eq_of_row_eq line 100
  7. lemma OAI.CubicEisenstein.row_eq_one_of_lower_left_zero line 115
  8. def OAI.CubicEisenstein.cuspStabilizer line 128
  9. lemma OAI.CubicEisenstein.mem_cuspStabilizer_iff line 142
  10. lemma OAI.CubicEisenstein.row_eq_iff_left_cusp line 149
  11. def OAI.CubicEisenstein.cuspRelation line 161
  12. abbrev OAI.CubicEisenstein.CuspCosets line 163
  13. def OAI.CubicEisenstein.cosetOf line 165
  14. lemma OAI.CubicEisenstein.cosetOf_eq_iff line 167
  15. def OAI.CubicEisenstein.cosetRow line 172
  16. lemma OAI.CubicEisenstein.cosetRow_cosetOf line 175
  17. lemma OAI.CubicEisenstein.cosetRow_injective line 177
  18. lemma OAI.CubicEisenstein.cosetRow_ne_zero line 184
  19. def OAI.CubicEisenstein.cosetCharacter line 187
  20. lemma OAI.CubicEisenstein.cosetCharacter_cosetOf line 190
  21. lemma OAI.CubicEisenstein.norm_cosetCharacter line 193
  22. def OAI.CubicEisenstein.rightTranslate line 196
  23. lemma OAI.CubicEisenstein.rightTranslate_cosetOf line 202
  24. lemma OAI.CubicEisenstein.rightTranslate_mul line 205
  25. lemma OAI.CubicEisenstein.rightTranslate_one line 211
  26. def OAI.CubicEisenstein.rightEquiv line 216
  27. lemma OAI.CubicEisenstein.cosetRow_rightEquiv line 222
  28. lemma OAI.CubicEisenstein.cosetCharacter_rightEquiv line 226
  29. def OAI.CubicEisenstein.complexMatrix line 230
  30. lemma OAI.CubicEisenstein.complexMatrix_apply line 233
  31. def OAI.CubicEisenstein.embeddedRow line 236
  32. lemma OAI.CubicEisenstein.embeddedRow_ne_zero line 238
  33. lemma OAI.CubicEisenstein.embeddedRow_rightEquiv line 245
  34. def OAI.CubicEisenstein.integerLattice line 256
  35. instance OAI.CubicEisenstein.(instance at line 259) line 259
  36. instance OAI.CubicEisenstein.(instance at line 263) line 263
  37. def OAI.CubicEisenstein.integerPoint line 267
  38. lemma OAI.CubicEisenstein.integerPoint_injective line 273
  39. lemma OAI.CubicEisenstein.integerPoint_norm line 280
  40. lemma OAI.CubicEisenstein.summable_integer_four_rpow line 290
  41. def OAI.CubicEisenstein.rowCoordinates line 301
  42. lemma OAI.CubicEisenstein.rowCoordinates_injective line 305
  43. lemma OAI.CubicEisenstein.coordinates_norm_bound line 313
  44. def OAI.CubicEisenstein.rowEnergy line 337
  45. lemma OAI.CubicEisenstein.rowEnergy_nonneg line 339
  46. lemma OAI.CubicEisenstein.norm_le_sqrt_rowEnergy line 342
  47. lemma OAI.CubicEisenstein.rowEnergy_pos line 348
  48. def OAI.CubicEisenstein.rowOperator line 353
  49. lemma OAI.CubicEisenstein.rowOperator_apply line 356
  50. lemma OAI.CubicEisenstein.rowOperator_mul line 359
  51. lemma OAI.CubicEisenstein.rowOperator_one line 363
  52. lemma OAI.CubicEisenstein.rowOperator_ne_zero line 366
  53. def OAI.CubicEisenstein.rowBound line 373
  54. lemma OAI.CubicEisenstein.rowBound_pos line 375
  55. lemma OAI.CubicEisenstein.coordinates_le_transformed_energy line 377
  56. lemma OAI.CubicEisenstein.norm_coordinates_ne_zero line 388
  57. def OAI.CubicEisenstein.summand line 405
  58. lemma OAI.CubicEisenstein.norm_summand line 409
  59. lemma OAI.CubicEisenstein.norm_summand_bound line 416
  60. theorem OAI.CubicEisenstein.summable_norm_summand line 440
  61. theorem OAI.CubicEisenstein.summable_summand line 452
  62. def OAI.CubicEisenstein.eisenstein line 455
  63. lemma OAI.CubicEisenstein.transformedRow_rightEquiv line 457
  64. lemma OAI.CubicEisenstein.summand_automorphy line 462
  65. theorem OAI.CubicEisenstein.eisenstein_automorphy line 474
  66. lemma OAI.CubicEisenstein.summand_differentiable line 483
  67. lemma OAI.CubicEisenstein.norm_summand_strip line 490
  68. theorem OAI.CubicEisenstein.eisenstein_differentiableOn_strip line 502
  69. theorem OAI.CubicEisenstein.eisenstein_differentiableAt line 514
  70. theorem OAI.CubicEisenstein.eisenstein_differentiableOn line 526
  71. def OAI.CubicEisenstein.upperSection line 537
  72. lemma OAI.CubicEisenstein.rowOperator_upperSection_zero line 542
  73. lemma OAI.CubicEisenstein.rowOperator_upperSection_one line 547
  74. def OAI.CubicEisenstein.heightDenominator line 553
  75. lemma OAI.CubicEisenstein.rowEnergy_upperSection line 556
  76. lemma OAI.CubicEisenstein.heightDenominator_pos line 565
  77. def OAI.CubicEisenstein.transformedHeight line 571
  78. lemma OAI.CubicEisenstein.summand_upperSection line 574
  79. def OAI.CubicEisenstein.upperEisenstein line 585
  80. theorem OAI.CubicEisenstein.upperEisenstein_eq_source_series line 588
  81. theorem OAI.CubicEisenstein.source_series_summable line 593
  82. lemma OAI.CubicEisenstein.ofReal_rowEnergy line 598
  83. lemma OAI.CubicEisenstein.rowEnergy_unitary line 603
  84. theorem OAI.CubicEisenstein.eisenstein_right_unitary line 614