OAI/Algebra/Drinfeld/Holonomy.lean

GitHub source file

126 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.DeligneDrinfeld.StraightKZ.connection_continuousOn line 15
  2. theorem OAI.DeligneDrinfeld.StraightKZ.segment_connection_continuousOn line 29
  3. theorem OAI.DeligneDrinfeld.StraightKZ.fundamental_continuousOn line 45
  4. theorem OAI.DeligneDrinfeld.StraightKZ.fundamental_refl line 53
  5. theorem OAI.DeligneDrinfeld.StraightKZ.transport_eq_ratio line 64
  6. theorem OAI.DeligneDrinfeld.StraightKZ.fundamental_ratio line 80
  7. theorem OAI.DeligneDrinfeld.StraightKZ.fundamental_comp line 91
  8. def OAI.DeligneDrinfeld.FourFrames.point line 106
  9. def OAI.DeligneDrinfeld.FourFrames.speed line 107
  10. def OAI.DeligneDrinfeld.FourFrames.path line 108
  11. def OAI.DeligneDrinfeld.FourFrames.tangent line 109
  12. theorem OAI.DeligneDrinfeld.FourFrames.point_strictMono line 112
  13. theorem OAI.DeligneDrinfeld.FourFrames.path_strictMono line 121
  14. theorem OAI.DeligneDrinfeld.FourFrames.path_derivative line 125
  15. theorem OAI.DeligneDrinfeld.FourFrames.path_continuous line 135
  16. theorem OAI.DeligneDrinfeld.FourFrames.tangent_continuous line 139
  17. theorem OAI.DeligneDrinfeld.FourFrames.form_eq line 158
  18. def OAI.DeligneDrinfeld.FourFrames.radial line 176
  19. theorem OAI.DeligneDrinfeld.FourFrames.radial_derivative line 180
  20. theorem OAI.DeligneDrinfeld.FourFrames.radial_isUnit line 187
  21. theorem OAI.DeligneDrinfeld.FourFrames.fundamental_path_derivative line 191
  22. def OAI.DeligneDrinfeld.FourFrames.corner line 207
  23. theorem OAI.DeligneDrinfeld.FourFrames.corner_eq line 211
  24. theorem OAI.DeligneDrinfeld.FourFrames.corner_isUnit line 219
  25. theorem OAI.DeligneDrinfeld.FourFrames.radial_eq line 226
  26. theorem OAI.DeligneDrinfeld.FourFrames.corner_cocycle line 234
  27. theorem OAI.DeligneDrinfeld.PowerAsymptotic.PowerSmall.add line 250
  28. theorem OAI.DeligneDrinfeld.PowerAsymptotic.PowerSmall.subpower line 264
  29. theorem OAI.DeligneDrinfeld.PowerAsymptotic.subpower_of_sub line 268
  30. theorem OAI.DeligneDrinfeld.PowerAsymptotic.frame_replacement line 273
  31. def OAI.DeligneDrinfeld.FourFrames.model line 293
  32. def OAI.DeligneDrinfeld.FourFrames.inverseModel line 296
  33. theorem OAI.DeligneDrinfeld.FourFrames.radial_error line 301
  34. theorem OAI.DeligneDrinfeld.FourFrames.inverse_radial_error line 306
  35. theorem OAI.DeligneDrinfeld.FourFrames.model_subpower line 314
  36. theorem OAI.DeligneDrinfeld.FourFrames.inverseModel_subpower line 319
  37. theorem OAI.DeligneDrinfeld.FourFrames.radial_replacement line 323
  38. theorem OAI.DeligneDrinfeld.FourFrames.normalized_transport_eq_corner line 342
  39. theorem OAI.DeligneDrinfeld.FourFrames.corner_eq_of_limit line 357
  40. theorem OAI.DeligneDrinfeld.BCBoundary.bulk_subpower line 379
  41. theorem OAI.DeligneDrinfeld.BCBoundary.edge_subpower line 392
  42. theorem OAI.DeligneDrinfeld.FourFrames.chord_triple line 407
  43. theorem OAI.DeligneDrinfeld.FourFrames.BC_commute_left line 414
  44. theorem OAI.DeligneDrinfeld.FourFrames.BC_commute_right line 420
  45. def OAI.DeligneDrinfeld.FourFrames.BCtransport line 423
  46. theorem OAI.DeligneDrinfeld.FourFrames.BC_model_limit line 428
  47. theorem OAI.DeligneDrinfeld.FourFrames.BC_transport_eq line 444
  48. theorem OAI.DeligneDrinfeld.FourFrames.BC_insertion line 479
  49. def OAI.DeligneDrinfeld.ADBoundary.endpoint line 496
  50. def OAI.DeligneDrinfeld.ADBoundary.movedPole line 498
  51. theorem OAI.DeligneDrinfeld.ADBoundary.bounds line 500
  52. theorem OAI.DeligneDrinfeld.ADBoundary.continuous line 506
  53. theorem OAI.DeligneDrinfeld.ADBoundary.error_bound line 516
  54. theorem OAI.DeligneDrinfeld.ADBoundary.bulk_bound line 529
  55. def OAI.DeligneDrinfeld.ADBoundary.mass line 536
  56. theorem OAI.DeligneDrinfeld.ADBoundary.mass_subpower line 539
  57. theorem OAI.DeligneDrinfeld.ADBoundary.estimates line 544
  58. theorem OAI.DeligneDrinfeld.ADBoundary.perturbation line 568
  59. theorem OAI.DeligneDrinfeld.ADBoundary.transport_subpower line 576
  60. theorem OAI.DeligneDrinfeld.ADBoundary.gauge_double line 583
  61. theorem OAI.DeligneDrinfeld.ADBoundary.square_tendsto line 591
  62. theorem OAI.DeligneDrinfeld.ADBoundary.model_bulk_eq line 601
  63. theorem OAI.DeligneDrinfeld.ADBoundary.limit line 619
  64. theorem OAI.DeligneDrinfeld.FourFrames.AD_commute_left line 647
  65. theorem OAI.DeligneDrinfeld.FourFrames.AD_commute_right line 651
  66. def OAI.DeligneDrinfeld.FourFrames.ADtransport line 657
  67. theorem OAI.DeligneDrinfeld.FourFrames.AD_model_limit line 662
  68. theorem OAI.DeligneDrinfeld.FourFrames.AD_form line 678
  69. theorem OAI.DeligneDrinfeld.FourFrames.AD_transport_eq line 686
  70. theorem OAI.DeligneDrinfeld.FourFrames.AD_insertion line 716
  71. def OAI.DeligneDrinfeld.ABBoundary.endpoint line 732
  72. def OAI.DeligneDrinfeld.ABBoundary.slope line 733
  73. def OAI.DeligneDrinfeld.ABBoundary.scale line 734
  74. def OAI.DeligneDrinfeld.ABBoundary.scaleV line 735
  75. theorem OAI.DeligneDrinfeld.ABBoundary.endpoint_bounds line 737
  76. theorem OAI.DeligneDrinfeld.ABBoundary.slope_bounds line 749
  77. theorem OAI.DeligneDrinfeld.ABBoundary.scale_start line 758
  78. theorem OAI.DeligneDrinfeld.ABBoundary.scale_end line 760
  79. theorem OAI.DeligneDrinfeld.ABBoundary.endpoint_mul_scale line 764
  80. theorem OAI.DeligneDrinfeld.ABBoundary.scale_bounds line 769
  81. theorem OAI.DeligneDrinfeld.ABBoundary.velocity_bounds line 779
  82. theorem OAI.DeligneDrinfeld.ABBoundary.coefficient_bounds line 789
  83. theorem OAI.DeligneDrinfeld.ABBoundary.chamber line 808
  84. theorem OAI.DeligneDrinfeld.ABBoundary.scale_deriv line 815
  85. theorem OAI.DeligneDrinfeld.ABBoundary.x_deriv line 818
  86. theorem OAI.DeligneDrinfeld.ABBoundary.scale_continuous line 821
  87. theorem OAI.DeligneDrinfeld.ABBoundary.form_eq line 824
  88. def OAI.DeligneDrinfeld.ABBoundary.error line 846
  89. def OAI.DeligneDrinfeld.ABBoundary.edgeForm line 849
  90. def OAI.DeligneDrinfeld.ABBoundary.errorConst line 851
  91. theorem OAI.DeligneDrinfeld.ABBoundary.errorConst_nonneg line 854
  92. theorem OAI.DeligneDrinfeld.ABBoundary.error_norm line 856
  93. theorem OAI.DeligneDrinfeld.ABBoundary.error_continuous line 868
  94. theorem OAI.DeligneDrinfeld.ABBoundary.bulk_continuous line 881
  95. theorem OAI.DeligneDrinfeld.ABBoundary.continuous line 885
  96. theorem OAI.DeligneDrinfeld.ABBoundary.error_bound line 889
  97. def OAI.DeligneDrinfeld.ABBoundary.mass line 902
  98. theorem OAI.DeligneDrinfeld.ABBoundary.gap_eq line 905
  99. theorem OAI.DeligneDrinfeld.ABBoundary.gap_bound line 910
  100. theorem OAI.DeligneDrinfeld.ABBoundary.bulk_bound line 916
  101. theorem OAI.DeligneDrinfeld.ABBoundary.mass_subpower line 929
  102. theorem OAI.DeligneDrinfeld.ABBoundary.estimates line 935
  103. theorem OAI.DeligneDrinfeld.ABBoundary.perturbation line 955
  104. theorem OAI.DeligneDrinfeld.ABBoundary.transport_subpower line 962
  105. theorem OAI.DeligneDrinfeld.ABBoundary.gap_tendsto line 974
  106. theorem OAI.DeligneDrinfeld.ABBoundary.bulk_limit line 985
  107. theorem OAI.DeligneDrinfeld.ABBoundary.limit line 1001
  108. theorem OAI.DeligneDrinfeld.FourFrames.AB_commute_left line 1028
  109. theorem OAI.DeligneDrinfeld.FourFrames.AB_commute_right line 1033
  110. def OAI.DeligneDrinfeld.FourFrames.ABtransport line 1036
  111. theorem OAI.DeligneDrinfeld.FourFrames.AB_model_limit line 1041
  112. theorem OAI.DeligneDrinfeld.FourFrames.AB_transport_eq line 1057
  113. theorem OAI.DeligneDrinfeld.FourFrames.AB_insertion line 1107
  114. theorem OAI.DeligneDrinfeld.FourFrames.ED_commute_left line 1126
  115. def OAI.DeligneDrinfeld.FourFrames.EDtransport line 1131
  116. theorem OAI.DeligneDrinfeld.FourFrames.ED_model_limit line 1136
  117. theorem OAI.DeligneDrinfeld.FourFrames.ED_form line 1153
  118. theorem OAI.DeligneDrinfeld.FourFrames.ED_transport_eq line 1165
  119. theorem OAI.DeligneDrinfeld.FourFrames.ED_insertion line 1200
  120. theorem OAI.DeligneDrinfeld.FourFrames.EC_commute_left line 1219
  121. theorem OAI.DeligneDrinfeld.FourFrames.EC_commute_right line 1224
  122. def OAI.DeligneDrinfeld.FourFrames.ECtransport line 1228
  123. theorem OAI.DeligneDrinfeld.FourFrames.EC_model_limit line 1233
  124. theorem OAI.DeligneDrinfeld.FourFrames.form_reflection line 1249
  125. theorem OAI.DeligneDrinfeld.FourFrames.EC_transport_eq line 1259
  126. theorem OAI.DeligneDrinfeld.FourFrames.EC_insertion line 1313