OAI/Algebra/Drinfeld/Hexagon.lean

GitHub source file

122 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.DeligneDrinfeld.ComplexKZ.bulkScale_limit line 16
  2. theorem OAI.DeligneDrinfeld.ComplexKZ.bulk_normalized_limit line 25
  3. theorem OAI.DeligneDrinfeld.ComplexKZ.mass_bound line 50
  4. theorem OAI.DeligneDrinfeld.ComplexKZ.arc_transport_error line 58
  5. theorem OAI.DeligneDrinfeld.ComplexKZ.gauge_exp_smul_commute line 85
  6. theorem OAI.DeligneDrinfeld.ComplexKZ.arc_normalized_limit line 90
  7. theorem OAI.DeligneDrinfeld.ComplexKZ.normalized_cycle line 117
  8. theorem OAI.DeligneDrinfeld.ComplexKZ.associator_hexagon line 133
  9. theorem OAI.DeligneDrinfeld.PairedHexagon.meridian line 160
  10. theorem OAI.DeligneDrinfeld.PairedHexagon.compared_meridian line 173
  11. theorem OAI.DeligneDrinfeld.PairedHexagon.compared_middle line 181
  12. theorem OAI.DeligneDrinfeld.NilpotentExp.power_difference line 199
  13. theorem OAI.DeligneDrinfeld.NilpotentExp.exp_linear line 213
  14. theorem OAI.DeligneDrinfeld.NilpotentExp.exp_difference line 226
  15. theorem OAI.DeligneDrinfeld.NilpotentExp.injective line 241
  16. theorem OAI.DeligneDrinfeld.NilpotentExp.map_exp line 255
  17. def OAI.DeligneDrinfeld.HexagonUnits.exp line 273
  18. theorem OAI.DeligneDrinfeld.HexagonUnits.exp_val line 275
  19. theorem OAI.DeligneDrinfeld.HexagonUnits.exp_neg line 277
  20. def OAI.DeligneDrinfeld.HexagonUnits.phi line 282
  21. theorem OAI.DeligneDrinfeld.HexagonUnits.phi_val line 284
  22. theorem OAI.DeligneDrinfeld.HexagonUnits.phi_swap line 287
  23. theorem OAI.DeligneDrinfeld.HexagonUnits.positive line 292
  24. theorem OAI.DeligneDrinfeld.HexagonUnits.negative line 301
  25. theorem OAI.DeligneDrinfeld.HexagonUnits.exp_square line 313
  26. theorem OAI.DeligneDrinfeld.HexagonUnits.exp_map line 318
  27. theorem OAI.DeligneDrinfeld.HexagonUnits.exp_conj line 325
  28. instance OAI.DeligneDrinfeld.ComplexCutoff.normedRing line 335
  29. instance OAI.DeligneDrinfeld.ComplexCutoff.normedAlgebraComplex line 337
  30. instance OAI.DeligneDrinfeld.ComplexCutoff.normedAlgebraReal line 339
  31. instance OAI.DeligneDrinfeld.ComplexCutoff.finiteReal line 341
  32. def OAI.DeligneDrinfeld.ComplexCutoff.filtration line 344
  33. abbrev OAI.DeligneDrinfeld.ComplexComparison.F line 358
  34. abbrev OAI.DeligneDrinfeld.ComplexComparison.X line 359
  35. abbrev OAI.DeligneDrinfeld.ComplexComparison.Y line 360
  36. abbrev OAI.DeligneDrinfeld.ComplexComparison.Z line 361
  37. theorem OAI.DeligneDrinfeld.ComplexComparison.xm line 363
  38. theorem OAI.DeligneDrinfeld.ComplexComparison.ym line 364
  39. theorem OAI.DeligneDrinfeld.ComplexComparison.zm line 365
  40. theorem OAI.DeligneDrinfeld.ComplexComparison.xc line 366
  41. theorem OAI.DeligneDrinfeld.ComplexComparison.yc line 368
  42. def OAI.DeligneDrinfeld.ComplexComparison.P line 371
  43. def OAI.DeligneDrinfeld.ComplexComparison.Qq line 372
  44. def OAI.DeligneDrinfeld.ComplexComparison.Rr line 373
  45. def OAI.DeligneDrinfeld.ComplexComparison.V line 374
  46. def OAI.DeligneDrinfeld.ComplexComparison.W line 375
  47. def OAI.DeligneDrinfeld.ComplexComparison.T line 376
  48. abbrev OAI.DeligneDrinfeld.ComplexComparison.a line 377
  49. abbrev OAI.DeligneDrinfeld.ComplexComparison.b line 378
  50. abbrev OAI.DeligneDrinfeld.ComplexComparison.c line 379
  51. theorem OAI.DeligneDrinfeld.ComplexComparison.p_hex line 381
  52. theorem OAI.DeligneDrinfeld.ComplexComparison.p_hex_neg line 383
  53. theorem OAI.DeligneDrinfeld.ComplexComparison.v_hex line 386
  54. theorem OAI.DeligneDrinfeld.ComplexComparison.v_hex_neg line 396
  55. theorem OAI.DeligneDrinfeld.ComplexComparison.P_weight line 406
  56. theorem OAI.DeligneDrinfeld.ComplexComparison.V_weight line 412
  57. def OAI.DeligneDrinfeld.ComplexComparison.theta line 420
  58. def OAI.DeligneDrinfeld.ComplexComparison.U line 421
  59. def OAI.DeligneDrinfeld.ComplexComparison.H line 422
  60. theorem OAI.DeligneDrinfeld.ComplexComparison.theta_x line 424
  61. theorem OAI.DeligneDrinfeld.ComplexComparison.theta_y line 425
  62. theorem OAI.DeligneDrinfeld.ComplexComparison.U_compare line 427
  63. theorem OAI.DeligneDrinfeld.ComplexComparison.H_compare line 431
  64. def OAI.DeligneDrinfeld.ComplexComparison.realMap line 435
  65. theorem OAI.DeligneDrinfeld.ComplexComparison.realMap_gen line 437
  66. theorem OAI.DeligneDrinfeld.ComplexComparison.positive_realMap line 440
  67. theorem OAI.DeligneDrinfeld.ComplexComparison.negative_realMap line 454
  68. theorem OAI.DeligneDrinfeld.ComplexComparison.theta_exp line 469
  69. theorem OAI.DeligneDrinfeld.ComplexComparison.exp_smul_conj line 473
  70. theorem OAI.DeligneDrinfeld.ComplexComparison.theta_a line 477
  71. theorem OAI.DeligneDrinfeld.ComplexComparison.theta_b line 480
  72. theorem OAI.DeligneDrinfeld.ComplexComparison.theta_meridian_y line 484
  73. theorem OAI.DeligneDrinfeld.ComplexComparison.theta_meridian_z line 490
  74. theorem OAI.DeligneDrinfeld.ComplexComparison.conj_weight line 499
  75. theorem OAI.DeligneDrinfeld.ComplexComparison.theta_z line 506
  76. theorem OAI.DeligneDrinfeld.ComplexComparison.theta_c line 538
  77. theorem OAI.DeligneDrinfeld.ComplexComparison.middle_compare line 542
  78. def OAI.DeligneDrinfeld.ComplexComparison.rho line 547
  79. theorem OAI.DeligneDrinfeld.ComplexComparison.rho_x line 550
  80. theorem OAI.DeligneDrinfeld.ComplexComparison.rho_y line 551
  81. theorem OAI.DeligneDrinfeld.ComplexComparison.rho_z line 552
  82. theorem OAI.DeligneDrinfeld.ComplexComparison.rho_three line 557
  83. theorem OAI.DeligneDrinfeld.ComplexComparison.rho_phi line 568
  84. theorem OAI.DeligneDrinfeld.ComplexComparison.rho_P line 577
  85. theorem OAI.DeligneDrinfeld.ComplexComparison.rho_Q line 581
  86. theorem OAI.DeligneDrinfeld.ComplexComparison.rho_R line 585
  87. theorem OAI.DeligneDrinfeld.ComplexComparison.rho_V line 589
  88. theorem OAI.DeligneDrinfeld.ComplexComparison.rho_W line 595
  89. theorem OAI.DeligneDrinfeld.ComplexComparison.rho_T line 601
  90. theorem OAI.DeligneDrinfeld.ComplexComparison.transport_y line 607
  91. theorem OAI.DeligneDrinfeld.ComplexComparison.rho_theta line 613
  92. theorem OAI.DeligneDrinfeld.ComplexComparison.rho_theta_unit line 645
  93. theorem OAI.DeligneDrinfeld.ComplexComparison.rho_U line 651
  94. theorem OAI.DeligneDrinfeld.ComplexComparison.rho_H line 656
  95. def OAI.DeligneDrinfeld.ComplexComparison.cycle line 665
  96. def OAI.DeligneDrinfeld.ComplexComparison.frames line 666
  97. def OAI.DeligneDrinfeld.ComplexComparison.rationalWeight line 667
  98. theorem OAI.DeligneDrinfeld.ComplexComparison.rationalWeight_initial line 670
  99. theorem OAI.DeligneDrinfeld.ComplexComparison.rationalWeight_terminal line 676
  100. theorem OAI.DeligneDrinfeld.ComplexComparison.U_weight line 682
  101. theorem OAI.DeligneDrinfeld.ComplexComparison.H_weight line 685
  102. theorem OAI.DeligneDrinfeld.ComplexComparison.frames_weight line 696
  103. def OAI.DeligneDrinfeld.ComplexComparison.category line 703
  104. def OAI.DeligneDrinfeld.ComplexComparison.value line 709
  105. theorem OAI.DeligneDrinfeld.ComplexComparison.rho_frames line 711
  106. theorem OAI.DeligneDrinfeld.ComplexComparison.category_rotate line 719
  107. theorem OAI.DeligneDrinfeld.ComplexComparison.delta_rotate line 730
  108. theorem OAI.DeligneDrinfeld.ComplexComparison.value_cyclic line 741
  109. theorem OAI.DeligneDrinfeld.ComplexComparison.transport_realMap line 759
  110. theorem OAI.DeligneDrinfeld.ComplexComparison.theta_realMap line 783
  111. theorem OAI.DeligneDrinfeld.ComplexComparison.arrow_realMap line 795
  112. theorem OAI.DeligneDrinfeld.ComplexComparison.S_realMap line 808
  113. theorem OAI.DeligneDrinfeld.ComplexComparison.value_realMap line 818
  114. theorem OAI.DeligneDrinfeld.ComplexComparison.realMap_word line 831
  115. theorem OAI.DeligneDrinfeld.ComplexComparison.realMap_coefficient line 841
  116. theorem OAI.DeligneDrinfeld.ComplexComparison.realMap_injective line 861
  117. def OAI.DeligneDrinfeld.ComplexComparison.realRotateFamily line 872
  118. theorem OAI.DeligneDrinfeld.ComplexComparison.realRotateFamily_mem line 875
  119. def OAI.DeligneDrinfeld.ComplexComparison.realRotate line 882
  120. theorem OAI.DeligneDrinfeld.ComplexComparison.realRotate_gen line 885
  121. theorem OAI.DeligneDrinfeld.ComplexComparison.rotate_realMap line 888
  122. theorem OAI.DeligneDrinfeld.ComplexComparison.real_value_cyclic line 903