OAI/NumberTheory/DirichletL/Cusp/MatrixPhases.lean

GitHub source file

97 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ShortDraftCusp.U line 19
  2. def OAI.ShortDraftCusp.L line 20
  3. def OAI.ShortDraftCusp.E line 21
  4. theorem OAI.ShortDraftCusp.upper_inversion_lower line 23
  5. theorem OAI.ShortDraftCusp.lower_add line 27
  6. theorem OAI.ShortDraftCusp.cusp19_matrix line 30
  7. theorem OAI.ShortDraftCusp.cusp10_matrix line 36
  8. theorem OAI.ShortDraftCusp.ramified_plus_matrix line 41
  9. theorem OAI.ShortDraftCusp.ramified_minus_matrix line 47
  10. theorem OAI.ShortDraftCusp.principal_case_div_three line 53
  11. theorem OAI.ShortDraftCusp.principal_case_ramified line 64
  12. theorem OAI.ShortDraftCusp.principal_case_unramified line 75
  13. theorem OAI.ShortDraftConcretePhase.concrete_fixed_phase_congr line 91
  14. theorem OAI.ShortDraftGauss.norm_gaussSum_eq_sqrt_card line 120
  15. theorem OAI.ShortDraftGauss.norm_normalized_gaussSum line 139
  16. abbrev OAI.EisensteinRayPhase.SquareClass line 154
  17. def OAI.EisensteinRayPhase.R line 156
  18. theorem OAI.EisensteinRayPhase.R_symmetric line 159
  19. theorem OAI.EisensteinRayPhase.R_mul_left line 162
  20. theorem OAI.EisensteinRayPhase.R_mul_right line 165
  21. theorem OAI.EisensteinRayPhase.R_self line 168
  22. theorem OAI.ShortDraftSextic.sextic_power_is_unit_mask line 177
  23. theorem OAI.ShortDraftGaussJacobi.sum_cubic_jacobi_reduction_zero line 193
  24. theorem OAI.ShortDraftGaussJacobi.jacobiSum_reduction_zero line 216
  25. theorem OAI.ShortDraftGaussJacobi.cubic_jacobi_product line 225
  26. theorem OAI.ShortDraftGaussJacobi.cubic_gauss_cube line 241
  27. theorem OAI.ShortDraftGaussJacobi.normalized_cubic_gauss_cube line 266
  28. theorem OAI.ShortDraftQuadraticGauss.quadratic_gauss_as_square_phase line 289
  29. theorem OAI.ShortDraftQuotientPhase.quotient_phase line 322
  30. abbrev OAI.EisensteinEPrimaryPhase.Coord line 361
  31. abbrev OAI.EisensteinEPrimaryPhase.Bit line 362
  32. def OAI.EisensteinEPrimaryPhase.mul line 364
  33. def OAI.EisensteinEPrimaryPhase.odd line 368
  34. instance OAI.EisensteinEPrimaryPhase.(instance at line 370) line 370
  35. def OAI.EisensteinEPrimaryPhase.rep line 373
  36. def OAI.EisensteinEPrimaryPhase.norm line 377
  37. def OAI.EisensteinEPrimaryPhase.ePrimary line 380
  38. instance OAI.EisensteinEPrimaryPhase.(instance at line 384) line 384
  39. theorem OAI.EisensteinEPrimaryPhase.exists_squareclass line 388
  40. theorem OAI.EisensteinEPrimaryPhase.squareclass_bits_unique line 392
  41. theorem OAI.EisensteinEPrimaryPhase.ePrimary_squareclass line 398
  42. theorem OAI.EisensteinEPrimaryPhase.norm_squareclass line 402
  43. def OAI.EisensteinEPrimaryPhase.signBit line 406
  44. def OAI.EisensteinEPrimaryPhase.normBit line 407
  45. def OAI.EisensteinEPrimaryPhase.bits line 408
  46. theorem OAI.EisensteinEPrimaryPhase.bits_squareclass line 410
  47. theorem OAI.EisensteinEPrimaryPhase.odd_mul line 414
  48. theorem OAI.EisensteinEPrimaryPhase.bits_mul line 417
  49. abbrev OAI.ShortDraftGaussianPhaseTable.SquareClass line 424
  50. def OAI.ShortDraftGaussianPhaseTable.phase line 426
  51. def OAI.ShortDraftGaussianPhaseTable.reciprocity line 429
  52. theorem OAI.ShortDraftGaussianPhaseTable.phase_cocycle line 432
  53. abbrev OAI.ActualEisensteinCoordinates.K line 439
  54. abbrev OAI.ActualEisensteinCoordinates.O line 440
  55. instance OAI.ActualEisensteinCoordinates.(instance at line 441) line 441
  56. theorem OAI.ActualEisensteinCoordinates.hζ line 442
  57. def OAI.ActualEisensteinCoordinates.omega line 444
  58. def OAI.ActualEisensteinCoordinates.pb line 445
  59. theorem OAI.ActualEisensteinCoordinates.pb_dim line 447
  60. theorem OAI.ActualEisensteinCoordinates.pb_gen line 450
  61. theorem OAI.ActualEisensteinCoordinates.exists_coordinates line 453
  62. def OAI.ActualEisensteinCoordinates.i0 line 479
  63. def OAI.ActualEisensteinCoordinates.i1 line 480
  64. def OAI.ActualEisensteinCoordinates.eval line 482
  65. theorem OAI.ActualEisensteinCoordinates.eval_basis line 484
  66. theorem OAI.ActualEisensteinCoordinates.unique_coordinates line 488
  67. theorem OAI.ActualEisensteinCoordinates.omega_sq line 502
  68. theorem OAI.ActualEisensteinCoordinates.conventional_lambda_eq_neg_delta_square line 505
  69. theorem OAI.ActualEisensteinCoordinates.eval_mul line 517
  70. theorem OAI.ActualEisensteinCoordinates.eval_congr_mod_four line 529
  71. theorem OAI.ActualEisensteinCoordinates.exists_pair line 542
  72. def OAI.ActualEisensteinCoordinates.coords line 547
  73. theorem OAI.ActualEisensteinCoordinates.eval_coords line 549
  74. def OAI.ActualEisensteinCoordinates.residue line 552
  75. theorem OAI.ActualEisensteinCoordinates.residue_eval line 555
  76. theorem OAI.ActualEisensteinCoordinates.residue_mul line 561
  77. theorem OAI.ActualEisensteinCoordinates.residue_pow_two line 570
  78. theorem OAI.ActualEisensteinCoordinates.congr_mod_four_of_residue_eq line 574
  79. def OAI.ActualEisensteinCoordinates.lift line 581
  80. theorem OAI.ActualEisensteinCoordinates.residue_lift line 584
  81. theorem OAI.ActualEisensteinCoordinates.exists_squareclass_mod_four line 588
  82. theorem OAI.ActualEisensteinCoordinates.ePrimary_squareclass_actual line 599
  83. theorem OAI.ActualEisensteinCoordinates.norm_squareclass_actual line 607
  84. theorem OAI.ActualEisensteinCoordinates.residue_two line 616
  85. theorem OAI.ActualEisensteinCoordinates.not_odd_mul_two line 621
  86. theorem OAI.ActualEisensteinCoordinates.not_odd_cast_zero line 626
  87. theorem OAI.ActualEisensteinCoordinates.odd_residue_iff_not_two_dvd line 632
  88. def OAI.ActualEisensteinCoordinates.rayBits line 655
  89. theorem OAI.ActualEisensteinCoordinates.rayBits_mul line 658
  90. def OAI.ActualEisensteinCoordinates.rayPhaseBits line 667
  91. theorem OAI.ActualEisensteinCoordinates.rayPhaseBits_symmetric line 670
  92. theorem OAI.ActualEisensteinCoordinates.rayPhaseBits_mul_left line 674
  93. theorem OAI.ActualEisensteinCoordinates.rayPhaseBits_mul_right line 679
  94. def OAI.ActualEisensteinCoordinates.rayPhase line 684
  95. theorem OAI.ActualEisensteinCoordinates.rayPhase_symmetric line 686
  96. theorem OAI.ActualEisensteinCoordinates.rayPhase_mul_left line 689
  97. theorem OAI.ActualEisensteinCoordinates.rayPhase_mul_right line 696