OAI/Algebra/Drinfeld/Logarithm.lean

GitHub source file

199 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DeligneDrinfeld.OperatorLog.binom line 14
  2. theorem OAI.DeligneDrinfeld.OperatorLog.binom_zero line 16
  3. theorem OAI.DeligneDrinfeld.OperatorLog.binom_eval_nat line 17
  4. theorem OAI.DeligneDrinfeld.OperatorLog.binom_coeff_zero line 21
  5. theorem OAI.DeligneDrinfeld.OperatorLog.desc_coeff_one line 28
  6. theorem OAI.DeligneDrinfeld.OperatorLog.binom_coeff_one_succ line 40
  7. def OAI.DeligneDrinfeld.OperatorLog.interpolate line 49
  8. def OAI.DeligneDrinfeld.OperatorLog.logarithm line 52
  9. theorem OAI.DeligneDrinfeld.OperatorLog.sum_range_extend line 55
  10. theorem OAI.DeligneDrinfeld.OperatorLog.interpolate_nat line 62
  11. theorem OAI.DeligneDrinfeld.OperatorLog.logarithm_eq line 82
  12. def OAI.DeligneDrinfeld.OperatorLog.valuePolynomial line 88
  13. theorem OAI.DeligneDrinfeld.OperatorLog.value_eval line 91
  14. theorem OAI.DeligneDrinfeld.OperatorLog.value_one line 95
  15. theorem OAI.DeligneDrinfeld.OperatorLog.polynomial_ext_nat line 99
  16. def OAI.DeligneDrinfeld.OperatorLog.pairPolynomial line 107
  17. theorem OAI.DeligneDrinfeld.OperatorLog.pair_eval line 112
  18. theorem OAI.DeligneDrinfeld.OperatorLog.pair_one line 124
  19. theorem OAI.DeligneDrinfeld.OperatorLog.powers_bilinear line 131
  20. theorem OAI.DeligneDrinfeld.OperatorLog.logarithm_bilinear line 139
  21. theorem OAI.DeligneDrinfeld.OperatorLog.powers_natural line 161
  22. theorem OAI.DeligneDrinfeld.OperatorLog.logarithm_natural line 167
  23. theorem OAI.DeligneDrinfeld.OperatorLog.logarithm_fixed line 173
  24. theorem OAI.DeligneDrinfeld.OperatorLog.nilpotent_of_raises line 181
  25. structure OAI.DeligneDrinfeld.LogCategory.Data line 199
  26. def OAI.DeligneDrinfeld.LogCategory.delta line 206
  27. theorem OAI.DeligneDrinfeld.LogCategory.delta_comp line 208
  28. theorem OAI.DeligneDrinfeld.LogCategory.delta_one_loop line 216
  29. def OAI.DeligneDrinfeld.LogCategory.derivation line 222
  30. theorem OAI.DeligneDrinfeld.LogCategory.unit_cocycle line 230
  31. theorem OAI.DeligneDrinfeld.LogCategory.delta_formula line 234
  32. def OAI.DeligneDrinfeld.GaugeAutomorphism.map line 247
  33. theorem OAI.DeligneDrinfeld.GaugeAutomorphism.map_apply line 250
  34. theorem OAI.DeligneDrinfeld.GaugeAutomorphism.composition line 255
  35. theorem OAI.DeligneDrinfeld.GaugeAutomorphism.map_one_loop line 260
  36. theorem OAI.DeligneDrinfeld.GaugeAutomorphism.raises line 263
  37. def OAI.DeligneDrinfeld.GaugeAutomorphism.data line 288
  38. theorem OAI.DeligneDrinfeld.OperatorLog.logarithm_depth_one line 304
  39. theorem OAI.DeligneDrinfeld.OperatorLog.comparison_depth_one line 321
  40. def OAI.DeligneDrinfeld.KZComparison.positive line 342
  41. theorem OAI.DeligneDrinfeld.KZComparison.positive_val line 345
  42. def OAI.DeligneDrinfeld.KZComparison.negative line 348
  43. theorem OAI.DeligneDrinfeld.KZComparison.negative_val line 350
  44. theorem OAI.DeligneDrinfeld.KZComparison.positive_weight line 357
  45. theorem OAI.DeligneDrinfeld.KZComparison.negative_weight line 362
  46. theorem OAI.DeligneDrinfeld.KZComparison.positive_depth line 370
  47. theorem OAI.DeligneDrinfeld.KZComparison.negative_depth line 373
  48. def OAI.DeligneDrinfeld.KZComparison.theta line 378
  49. def OAI.DeligneDrinfeld.KZComparison.arrow line 381
  50. theorem OAI.DeligneDrinfeld.KZComparison.exact_comparison line 384
  51. theorem OAI.DeligneDrinfeld.KZComparison.theta_x line 387
  52. theorem OAI.DeligneDrinfeld.KZComparison.theta_y line 388
  53. theorem OAI.DeligneDrinfeld.KZComparison.theta_depth line 391
  54. theorem OAI.DeligneDrinfeld.KZComparison.arrow_depth line 395
  55. def OAI.DeligneDrinfeld.KZComparison.frames line 398
  56. theorem OAI.DeligneDrinfeld.KZComparison.frames_depth line 400
  57. def OAI.DeligneDrinfeld.KZComparison.rationalDepth line 405
  58. theorem OAI.DeligneDrinfeld.KZComparison.rationalDepth_initial line 407
  59. theorem OAI.DeligneDrinfeld.KZComparison.rationalDepth_terminal line 413
  60. def OAI.DeligneDrinfeld.KZComparison.category line 419
  61. def OAI.DeligneDrinfeld.KZComparison.value line 424
  62. theorem OAI.DeligneDrinfeld.KZComparison.arrow_log_congruence line 426
  63. theorem OAI.DeligneDrinfeld.KZComparison.comparison_congruence line 435
  64. theorem OAI.DeligneDrinfeld.KZComparison.value_coefficient line 443
  65. theorem OAI.DeligneDrinfeld.KZComparison.odd_value_nonzero line 457
  66. theorem OAI.DeligneDrinfeld.KZGroupLike.associator_diagonal line 472
  67. theorem OAI.DeligneDrinfeld.KZGroupLike.positive_diagonal line 485
  68. theorem OAI.DeligneDrinfeld.KZGroupLike.negative_diagonal line 489
  69. theorem OAI.DeligneDrinfeld.TruncatedSubstitution.hom_ext line 514
  70. def OAI.DeligneDrinfeld.ConjugateCoalgebra.tensorUnit line 529
  71. theorem OAI.DeligneDrinfeld.ConjugateCoalgebra.inverse_diagonal line 535
  72. theorem OAI.DeligneDrinfeld.ConjugateCoalgebra.transport_cutoff_gen line 543
  73. theorem OAI.DeligneDrinfeld.ConjugateCoalgebra.congr_tmul line 547
  74. theorem OAI.DeligneDrinfeld.ConjugateCoalgebra.transport_diagonal line 550
  75. theorem OAI.DeligneDrinfeld.ConjugateCoalgebra.natural_inverse line 578
  76. theorem OAI.DeligneDrinfeld.ConjugateCoalgebra.theta_diagonal line 584
  77. theorem OAI.DeligneDrinfeld.ConjugateCoalgebra.arrow_diagonal line 603
  78. theorem OAI.DeligneDrinfeld.OperatorLog.logarithm_stable line 628
  79. def OAI.DeligneDrinfeld.OperatorLog.tensorDifference line 635
  80. theorem OAI.DeligneDrinfeld.OperatorLog.tensorDifference_nilpotent line 638
  81. theorem OAI.DeligneDrinfeld.OperatorLog.logarithm_tensor_tmul line 657
  82. theorem OAI.DeligneDrinfeld.OperatorLog.logarithm_tensor line 673
  83. theorem OAI.DeligneDrinfeld.OperatorLog.logarithm_coderivation line 682
  84. theorem OAI.DeligneDrinfeld.OperatorLog.logarithm_diagonal line 702
  85. theorem OAI.DeligneDrinfeld.KZPrimitiveValue.theta_diagonal line 725
  86. theorem OAI.DeligneDrinfeld.KZPrimitiveValue.arrow_diagonal line 731
  87. def OAI.DeligneDrinfeld.KZPrimitiveValue.S line 736
  88. theorem OAI.DeligneDrinfeld.KZPrimitiveValue.S_apply line 738
  89. theorem OAI.DeligneDrinfeld.KZPrimitiveValue.category_S line 740
  90. theorem OAI.DeligneDrinfeld.KZPrimitiveValue.S_diagonal line 747
  91. def OAI.DeligneDrinfeld.KZPrimitiveValue.tmulQ line 758
  92. theorem OAI.DeligneDrinfeld.KZPrimitiveValue.orbit_diagonal line 763
  93. theorem OAI.DeligneDrinfeld.KZPrimitiveValue.value_diagonal line 777
  94. theorem OAI.DeligneDrinfeld.KZCutoffComparison.transport_natural line 799
  95. theorem OAI.DeligneDrinfeld.KZCutoffComparison.theta_natural line 820
  96. theorem OAI.DeligneDrinfeld.KZCutoffComparison.arrow_natural line 833
  97. theorem OAI.DeligneDrinfeld.KZCutoffComparison.positive_drop line 849
  98. theorem OAI.DeligneDrinfeld.KZCutoffComparison.negative_drop line 854
  99. theorem OAI.DeligneDrinfeld.KZCutoffComparison.theta_drop line 863
  100. theorem OAI.DeligneDrinfeld.KZCutoffComparison.arrow_drop line 867
  101. theorem OAI.DeligneDrinfeld.KZCutoffComparison.S_drop line 870
  102. theorem OAI.DeligneDrinfeld.KZCutoffComparison.value_drop line 877
  103. def OAI.DeligneDrinfeld.CutoffPrimitiveExtract.truncVal line 896
  104. theorem OAI.DeligneDrinfeld.CutoffPrimitiveExtract.piece_trunc line 899
  105. theorem OAI.DeligneDrinfeld.CutoffPrimitiveExtract.totalPiece_trunc line 910
  106. def OAI.DeligneDrinfeld.CutoffPrimitiveExtract.leftPair line 922
  107. def OAI.DeligneDrinfeld.CutoffPrimitiveExtract.rightPair line 924
  108. theorem OAI.DeligneDrinfeld.CutoffPrimitiveExtract.leftPair_word line 926
  109. theorem OAI.DeligneDrinfeld.CutoffPrimitiveExtract.rightPair_word line 928
  110. theorem OAI.DeligneDrinfeld.CutoffPrimitiveExtract.pair_commute line 931
  111. def OAI.DeligneDrinfeld.CutoffPrimitiveExtract.pairMap line 945
  112. theorem OAI.DeligneDrinfeld.CutoffPrimitiveExtract.pairMap_coproduct line 948
  113. theorem OAI.DeligneDrinfeld.CutoffPrimitiveExtract.leftPair_eq line 959
  114. theorem OAI.DeligneDrinfeld.CutoffPrimitiveExtract.rightPair_eq line 967
  115. theorem OAI.DeligneDrinfeld.CutoffPrimitiveExtract.primitive_of_tensor line 976
  116. def OAI.DeligneDrinfeld.CutoffPrimitiveExtract.normalVal line 985
  117. theorem OAI.DeligneDrinfeld.CutoffPrimitiveExtract.normalVal_quotient line 987
  118. theorem OAI.DeligneDrinfeld.CutoffPrimitiveExtract.normalVal_one line 992
  119. theorem OAI.DeligneDrinfeld.CutoffPrimitiveExtract.diagonal_quotient line 999
  120. theorem OAI.DeligneDrinfeld.CutoffPrimitiveExtract.drop_quotient line 1012
  121. theorem OAI.DeligneDrinfeld.CutoffPrimitiveExtract.piece_primitive line 1020
  122. theorem OAI.DeligneDrinfeld.CutoffPrimitiveExtract.KZ_value_lie line 1052
  123. theorem OAI.DeligneDrinfeld.OperatorLog.value_taylor line 1067
  124. theorem OAI.DeligneDrinfeld.OperatorLog.value_derivative line 1074
  125. theorem OAI.DeligneDrinfeld.OperatorLog.value_zero line 1081
  126. theorem OAI.DeligneDrinfeld.OperatorLog.value_coeff line 1086
  127. theorem OAI.DeligneDrinfeld.OperatorLog.exp_logarithm line 1103
  128. theorem OAI.DeligneDrinfeld.OperatorExp.natural line 1131
  129. theorem OAI.DeligneDrinfeld.OperatorExp.bilinear line 1138
  130. theorem OAI.DeligneDrinfeld.OperatorExp.fixed line 1164
  131. structure OAI.DeligneDrinfeld.CategoryExp.Data line 1184
  132. def OAI.DeligneDrinfeld.CategoryExp.gauge line 1189
  133. def OAI.DeligneDrinfeld.CategoryExp.act line 1200
  134. theorem OAI.DeligneDrinfeld.CategoryExp.composition line 1202
  135. theorem OAI.DeligneDrinfeld.CategoryExp.one line 1207
  136. theorem OAI.DeligneDrinfeld.CategoryExp.natural line 1210
  137. theorem OAI.DeligneDrinfeld.CategoryExp.kills line 1217
  138. def OAI.DeligneDrinfeld.CategoryExp.neg line 1221
  139. theorem OAI.DeligneDrinfeld.CategoryExp.inverse line 1228
  140. def OAI.DeligneDrinfeld.CategoryExp.equivalence line 1233
  141. theorem OAI.DeligneDrinfeld.CategoryExp.pow_mem line 1241
  142. theorem OAI.DeligneDrinfeld.CategoryExp.nilpotent line 1251
  143. theorem OAI.DeligneDrinfeld.CategoryExp.preserves line 1257
  144. theorem OAI.DeligneDrinfeld.CategoryExp.pow_mem_shift line 1278
  145. theorem OAI.DeligneDrinfeld.CategoryExp.first_order line 1285
  146. theorem OAI.DeligneDrinfeld.CategoryExp.unit_leading line 1307
  147. theorem OAI.DeligneDrinfeld.CategoryExp.normalizes line 1317
  148. def OAI.DeligneDrinfeld.RealOperatorLog.logarithm line 1326
  149. theorem OAI.DeligneDrinfeld.RealOperatorLog.pow_restrict line 1328
  150. theorem OAI.DeligneDrinfeld.RealOperatorLog.restrict line 1333
  151. theorem OAI.DeligneDrinfeld.RealOperatorLog.raises line 1339
  152. theorem OAI.DeligneDrinfeld.RealOperatorLog.nilpotent line 1350
  153. theorem OAI.DeligneDrinfeld.RealOperatorLog.exp_restrict line 1357
  154. theorem OAI.DeligneDrinfeld.RealOperatorLog.exp_logarithm line 1367
  155. def OAI.DeligneDrinfeld.TruncatedDerivation.gen line 1393
  156. theorem OAI.DeligneDrinfeld.TruncatedDerivation.gen_mem line 1394
  157. def OAI.DeligneDrinfeld.TruncatedDerivation.jet line 1397
  158. theorem OAI.DeligneDrinfeld.TruncatedDerivation.jet_atom line 1400
  159. theorem OAI.DeligneDrinfeld.TruncatedDerivation.fst_jet line 1404
  160. def OAI.DeligneDrinfeld.TruncatedDerivation.raw line 1413
  161. theorem OAI.DeligneDrinfeld.TruncatedDerivation.raw_atom line 1416
  162. theorem OAI.DeligneDrinfeld.TruncatedDerivation.raw_one line 1420
  163. theorem OAI.DeligneDrinfeld.TruncatedDerivation.raw_mul line 1423
  164. theorem OAI.DeligneDrinfeld.TruncatedDerivation.raw_word_mem line 1429
  165. theorem OAI.DeligneDrinfeld.TruncatedDerivation.raw_mem line 1442
  166. def OAI.DeligneDrinfeld.TruncatedDerivation.descend line 1447
  167. theorem OAI.DeligneDrinfeld.TruncatedDerivation.descend_quotient line 1463
  168. theorem OAI.DeligneDrinfeld.TruncatedDerivation.descend_fst line 1468
  169. def OAI.DeligneDrinfeld.TruncatedDerivation.derivation line 1473
  170. theorem OAI.DeligneDrinfeld.TruncatedDerivation.derivation_quotient line 1477
  171. theorem OAI.DeligneDrinfeld.TruncatedDerivation.derivation_one line 1484
  172. theorem OAI.DeligneDrinfeld.TruncatedDerivation.derivation_mul line 1488
  173. theorem OAI.DeligneDrinfeld.TruncatedDerivation.derivation_mem line 1495
  174. theorem OAI.DeligneDrinfeld.CutoffCategory.initial line 1509
  175. def OAI.DeligneDrinfeld.CutoffCategory.filtration line 1515
  176. abbrev OAI.DeligneDrinfeld.CutoffCategory.data line 1524
  177. theorem OAI.DeligneDrinfeld.CutoffCategory.apply line 1526
  178. theorem OAI.DeligneDrinfeld.CutoffCategory.one line 1528
  179. theorem OAI.DeligneDrinfeld.CutoffCategory.raises line 1531
  180. theorem OAI.DeligneDrinfeld.CutoffCategory.nilpotent line 1540
  181. theorem OAI.DeligneDrinfeld.CutoffCategory.leading line 1546
  182. def OAI.DeligneDrinfeld.KZRealLog.S line 1557
  183. theorem OAI.DeligneDrinfeld.KZRealLog.S_apply line 1559
  184. theorem OAI.DeligneDrinfeld.KZRealLog.S_restrict line 1563
  185. def OAI.DeligneDrinfeld.KZRealLog.D line 1568
  186. theorem OAI.DeligneDrinfeld.KZRealLog.D_restrict line 1570
  187. theorem OAI.DeligneDrinfeld.KZRealLog.D_apply line 1581
  188. def OAI.DeligneDrinfeld.KZRealLog.data line 1584
  189. theorem OAI.DeligneDrinfeld.KZRealLog.value line 1588
  190. theorem OAI.DeligneDrinfeld.KZRealLog.frames_weight line 1589
  191. theorem OAI.DeligneDrinfeld.KZRealLog.S_raises line 1594
  192. theorem OAI.DeligneDrinfeld.KZRealLog.raises line 1603
  193. theorem OAI.DeligneDrinfeld.KZRealLog.nilpotent line 1606
  194. theorem OAI.DeligneDrinfeld.KZRealLog.exp_eq line 1608
  195. theorem OAI.DeligneDrinfeld.KZRealLog.exp_comparison line 1623
  196. theorem OAI.DeligneDrinfeld.KZRealLog.loop_x line 1627
  197. theorem OAI.DeligneDrinfeld.KZRealLog.loop_y line 1634
  198. theorem OAI.DeligneDrinfeld.KZRealLog.loop_false_y line 1641
  199. theorem OAI.DeligneDrinfeld.KZRealLog.edge_formula line 1650