OAI/Algebra/Drinfeld/Flatness.lean

GitHub source file

138 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.RealDeligneDrinfeld.WeightBridge.tree_word line 10
  2. theorem OAI.RealDeligneDrinfeld.WeightBridge.word_tree line 15
  3. theorem OAI.RealDeligneDrinfeld.WeightBridge.piece_eq line 24
  4. theorem OAI.RealDeligneDrinfeld.WeightBridge.embed_homogeneous line 34
  5. theorem OAI.RealDeligneDrinfeld.WeightBridge.bracket_mem line 40
  6. theorem OAI.RealDeligneDrinfeld.WeightBridge.map_mem line 53
  7. theorem OAI.RealDeligneDrinfeld.WeightBridge.eval_mem line 67
  8. theorem OAI.RealDeligneDrinfeld.WeightBridge.x_mem line 72
  9. theorem OAI.RealDeligneDrinfeld.WeightBridge.y_mem line 73
  10. def OAI.DeligneDrinfeld.UnitConjugation.hom line 80
  11. theorem OAI.DeligneDrinfeld.UnitConjugation.hom_apply line 91
  12. theorem OAI.DeligneDrinfeld.UnitConjugation.inverse line 93
  13. theorem OAI.DeligneDrinfeld.UnitConjugation.mul_apply line 97
  14. theorem OAI.DeligneDrinfeld.UnitConjugation.natural line 100
  15. theorem OAI.DeligneDrinfeld.KZCollar.associator_swap line 111
  16. def OAI.DeligneDrinfeld.KZSwap.swap line 126
  17. theorem OAI.DeligneDrinfeld.KZSwap.swap_gen line 128
  18. theorem OAI.DeligneDrinfeld.KZSwap.swap_twice line 131
  19. theorem OAI.DeligneDrinfeld.KZSwap.positive_swap line 139
  20. theorem OAI.DeligneDrinfeld.KZSwap.negative_swap line 148
  21. theorem OAI.DeligneDrinfeld.KZSwap.transport_swap line 160
  22. theorem OAI.DeligneDrinfeld.KZSwap.theta_swap line 187
  23. theorem OAI.DeligneDrinfeld.KZSwap.arrow_swap line 208
  24. theorem OAI.DeligneDrinfeld.KZSwap.category_swap line 232
  25. theorem OAI.DeligneDrinfeld.KZSwap.value_swap line 248
  26. theorem OAI.DeligneDrinfeld.FinitePicard.parameter_integral_derivative line 272
  27. def OAI.DeligneDrinfeld.FinitePicard.dterm line 293
  28. theorem OAI.DeligneDrinfeld.FinitePicard.dterm_zero line 297
  29. theorem OAI.DeligneDrinfeld.FinitePicard.dterm_base line 298
  30. theorem OAI.DeligneDrinfeld.FinitePicard.continuous_term_parameter line 301
  31. theorem OAI.DeligneDrinfeld.FinitePicard.continuous_dterm line 309
  32. theorem OAI.DeligneDrinfeld.FinitePicard.derivative_term_parameter line 319
  33. theorem OAI.DeligneDrinfeld.FinitePicard.dterm_flat_formula line 342
  34. theorem OAI.DeligneDrinfeld.FinitePicard.derivative_transport_flat line 377
  35. theorem OAI.DeligneDrinfeld.FinitePicard.transport_flat_constant line 401
  36. theorem OAI.DeligneDrinfeld.FinitePicard.term_congr line 429
  37. theorem OAI.DeligneDrinfeld.FinitePicard.transport_congr line 442
  38. def OAI.DeligneDrinfeld.FinitePicard.rectExtend line 448
  39. theorem OAI.DeligneDrinfeld.FinitePicard.rectExtend_eq line 452
  40. theorem OAI.DeligneDrinfeld.FinitePicard.continuous_rectExtend line 457
  41. theorem OAI.DeligneDrinfeld.FinitePicard.rectExtend_derivative line 465
  42. theorem OAI.DeligneDrinfeld.FinitePicard.derivative_transport_flat_local line 476
  43. theorem OAI.DeligneDrinfeld.FinitePicard.continuousOn_transport_parameter line 515
  44. theorem OAI.DeligneDrinfeld.FinitePicard.transport_flat_constant_local line 533
  45. def OAI.DeligneDrinfeld.KZFlat.wedge line 566
  46. theorem OAI.DeligneDrinfeld.KZFlat.arnold line 568
  47. def OAI.DeligneDrinfeld.KZFlat.combine line 577
  48. theorem OAI.DeligneDrinfeld.KZFlat.expand line 580
  49. theorem OAI.DeligneDrinfeld.KZFlat.adjacent line 613
  50. theorem OAI.DeligneDrinfeld.KZFlat.outer line 619
  51. def OAI.DeligneDrinfeld.KZFlat.dlog line 625
  52. def OAI.DeligneDrinfeld.KZFlat.coefficients line 627
  53. def OAI.DeligneDrinfeld.KZFlat.connection line 630
  54. theorem OAI.DeligneDrinfeld.KZFlat.arnold_dlog line 633
  55. theorem OAI.DeligneDrinfeld.KZFlat.flat line 644
  56. def OAI.DeligneDrinfeld.LogRectangle.form line 675
  57. def OAI.DeligneDrinfeld.LogRectangle.mixed line 677
  58. theorem OAI.DeligneDrinfeld.LogRectangle.derivative_s line 680
  59. theorem OAI.DeligneDrinfeld.LogRectangle.derivative_t line 689
  60. theorem OAI.DeligneDrinfeld.LogRectangle.continuousOn_form line 698
  61. theorem OAI.DeligneDrinfeld.LogRectangle.continuousOn_mixed line 709
  62. theorem OAI.DeligneDrinfeld.LogRectangle.transport_derivative line 724
  63. theorem OAI.DeligneDrinfeld.LogRectangle.transport_constant line 755
  64. def OAI.DeligneDrinfeld.ComplexLogChamber.field line 797
  65. def OAI.DeligneDrinfeld.ComplexLogChamber.connection line 799
  66. theorem OAI.DeligneDrinfeld.ComplexLogChamber.form_eq line 801
  67. theorem OAI.DeligneDrinfeld.ComplexLogChamber.connection_commute line 805
  68. theorem OAI.DeligneDrinfeld.ComplexLogChamber.connection_mem line 810
  69. theorem OAI.DeligneDrinfeld.ComplexLogChamber.connection_zero line 815
  70. theorem OAI.DeligneDrinfeld.ComplexLogChamber.connection_continuousOn line 818
  71. def OAI.DeligneDrinfeld.ComplexLogChamber.segment line 826
  72. theorem OAI.DeligneDrinfeld.ComplexLogChamber.segment_zero line 828
  73. theorem OAI.DeligneDrinfeld.ComplexLogChamber.segment_one line 829
  74. theorem OAI.DeligneDrinfeld.ComplexLogChamber.segment_mem line 831
  75. theorem OAI.DeligneDrinfeld.ComplexLogChamber.segment_derivative line 835
  76. def OAI.DeligneDrinfeld.ComplexLogChamber.fundamental line 840
  77. theorem OAI.DeligneDrinfeld.ComplexLogChamber.fundamental_isUnit line 846
  78. theorem OAI.DeligneDrinfeld.ComplexLogChamber.fundamental_derivative line 850
  79. theorem OAI.DeligneDrinfeld.ComplexLogChamber.fundamental_continuousOn line 883
  80. theorem OAI.DeligneDrinfeld.ComplexLogChamber.transport_eq_ratio line 897
  81. theorem OAI.DeligneDrinfeld.KZCollar.regularizedBulk_two_eq line 919
  82. theorem OAI.DeligneDrinfeld.KZCollar.regularizedBulk_two_limit line 937
  83. def OAI.DeligneDrinfeld.ComplexKZ.form line 963
  84. def OAI.DeligneDrinfeld.ComplexKZ.poles line 965
  85. def OAI.DeligneDrinfeld.ComplexKZ.residues line 967
  86. theorem OAI.DeligneDrinfeld.ComplexKZ.form_eq line 969
  87. def OAI.DeligneDrinfeld.ComplexKZ.domain line 974
  88. theorem OAI.DeligneDrinfeld.ComplexKZ.real_mem line 976
  89. theorem OAI.DeligneDrinfeld.ComplexKZ.star_avoids line 979
  90. def OAI.DeligneDrinfeld.ComplexKZ.turn line 994
  91. def OAI.DeligneDrinfeld.ComplexKZ.turnDeriv line 996
  92. theorem OAI.DeligneDrinfeld.ComplexKZ.turn_nonzero line 998
  93. theorem OAI.DeligneDrinfeld.ComplexKZ.turn_sub_one line 1001
  94. theorem OAI.DeligneDrinfeld.ComplexKZ.turn_ne_one line 1006
  95. theorem OAI.DeligneDrinfeld.ComplexKZ.turn_mem line 1012
  96. theorem OAI.DeligneDrinfeld.ComplexKZ.turn_twice line 1017
  97. theorem OAI.DeligneDrinfeld.ComplexKZ.turn_thrice line 1022
  98. theorem OAI.DeligneDrinfeld.ComplexKZ.form_turn line 1028
  99. theorem OAI.DeligneDrinfeld.ComplexKZ.turn_derivative line 1043
  100. theorem OAI.DeligneDrinfeld.ComplexKZ.turn_continuousOn line 1051
  101. theorem OAI.DeligneDrinfeld.ComplexKZ.turnDeriv_continuousOn line 1055
  102. theorem OAI.DeligneDrinfeld.ComplexKZ.form_real line 1059
  103. theorem OAI.DeligneDrinfeld.PowerAsymptotic.powerSmall_of_real_bound line 1073
  104. theorem OAI.DeligneDrinfeld.PowerAsymptotic.subpower_of_real_bound line 1079
  105. theorem OAI.DeligneDrinfeld.PowerAsymptotic.transportPoly_subpower line 1083
  106. theorem OAI.DeligneDrinfeld.PowerAsymptotic.transport_subpower line 1089
  107. theorem OAI.DeligneDrinfeld.PowerAsymptotic.transport_perturbation_powerSmall line 1098
  108. theorem OAI.DeligneDrinfeld.PowerAsymptotic.normalized_perturbation_limit line 1116
  109. def OAI.DeligneDrinfeld.ComplexKZ.arc line 1130
  110. def OAI.DeligneDrinfeld.ComplexKZ.angular line 1132
  111. theorem OAI.DeligneDrinfeld.ComplexKZ.arc_zero line 1134
  112. theorem OAI.DeligneDrinfeld.ComplexKZ.arc_one line 1137
  113. theorem OAI.DeligneDrinfeld.ComplexKZ.norm_arc line 1139
  114. theorem OAI.DeligneDrinfeld.ComplexKZ.arc_mem line 1142
  115. theorem OAI.DeligneDrinfeld.ComplexKZ.arc_derivative line 1153
  116. theorem OAI.DeligneDrinfeld.ComplexKZ.arc_continuous line 1161
  117. theorem OAI.DeligneDrinfeld.ComplexKZ.norm_angular line 1164
  118. def OAI.DeligneDrinfeld.ComplexKZ.arcForm line 1169
  119. theorem OAI.DeligneDrinfeld.ComplexKZ.arcForm_eq line 1171
  120. theorem OAI.DeligneDrinfeld.ComplexKZ.norm_arcForm_sub_le line 1177
  121. theorem OAI.DeligneDrinfeld.ComplexKZ.arcForm_continuousOn line 1191
  122. theorem OAI.DeligneDrinfeld.ComplexKZ.constant_transport line 1204
  123. structure OAI.DeligneDrinfeld.ComplexKZ.Path line 1220
  124. def OAI.DeligneDrinfeld.ComplexKZ.Path.rotate line 1232
  125. def OAI.DeligneDrinfeld.ComplexKZ.Path.interval line 1241
  126. def OAI.DeligneDrinfeld.ComplexKZ.Path.semicircle line 1250
  127. def OAI.DeligneDrinfeld.ComplexKZ.Path.holonomy line 1261
  128. theorem OAI.DeligneDrinfeld.ComplexKZ.Path.rotate_holonomy line 1264
  129. theorem OAI.DeligneDrinfeld.ComplexKZ.Path.rotate_twice_holonomy line 1271
  130. theorem OAI.DeligneDrinfeld.ComplexKZ.Path.interval_holonomy line 1277
  131. def OAI.DeligneDrinfeld.ComplexKZ.Path.frame line 1287
  132. theorem OAI.DeligneDrinfeld.ComplexKZ.Path.frame_isUnit line 1291
  133. theorem OAI.DeligneDrinfeld.ComplexKZ.Path.holonomy_ratio line 1300
  134. theorem OAI.DeligneDrinfeld.ComplexKZ.cycle_identity line 1316
  135. def OAI.DeligneDrinfeld.ComplexKZ.bulkEndpoint line 1334
  136. theorem OAI.DeligneDrinfeld.ComplexKZ.bulkEndpoint_bounds line 1336
  137. theorem OAI.DeligneDrinfeld.ComplexKZ.bulkEndpoint_turn line 1346
  138. theorem OAI.DeligneDrinfeld.ComplexKZ.bulk_arc_identity line 1349