OAI/Algebra/Drinfeld/KZTransport.lean

GitHub source file

248 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.DeligneDrinfeld.GenericIhara.above_zero line 14
2. theorem OAI.DeligneDrinfeld.GenericIhara.tree_depth line 17
3. theorem OAI.DeligneDrinfeld.GenericIhara.homogeneous_depth line 35
4. theorem OAI.DeligneDrinfeld.GenericIhara.evalIhara_homogeneous line 48
5. theorem OAI.DeligneDrinfeld.GenericIhara.evalIhara_depth line 65
6. def OAI.DeligneDrinfeld.GenericIhara.depthOneWord line 82
7. theorem OAI.DeligneDrinfeld.GenericIhara.degree_depthOneWord line 84
8. theorem OAI.DeligneDrinfeld.GenericIhara.depthOne_zero line 92
9. abbrev OAI.DeligneDrinfeld.CutoffDepth.Q line 102
10. abbrev OAI.DeligneDrinfeld.CutoffDepth.quotient line 103
11. def OAI.DeligneDrinfeld.CutoffDepth.gen line 104
12. abbrev OAI.DeligneDrinfeld.CutoffDepth.coeff line 105
13. theorem OAI.DeligneDrinfeld.CutoffDepth.degree_pow line 107
14. theorem OAI.DeligneDrinfeld.CutoffDepth.length_depthOne line 113
15. theorem OAI.DeligneDrinfeld.CutoffDepth.depth_le_length line 117
16. def OAI.DeligneDrinfeld.CutoffDepth.depthSpace line 124
17. theorem OAI.DeligneDrinfeld.CutoffDepth.depth_antitone line 127
18. theorem OAI.DeligneDrinfeld.CutoffDepth.depth_one line 131
19. theorem OAI.DeligneDrinfeld.CutoffDepth.depth_mul line 134
20. theorem OAI.DeligneDrinfeld.CutoffDepth.depth_terminal line 140
21. theorem OAI.DeligneDrinfeld.CutoffDepth.gen_depth line 146
22. theorem OAI.DeligneDrinfeld.CutoffDepth.gen_weight line 150
23. theorem OAI.DeligneDrinfeld.CutoffDepth.coeff_zero_of_depth line 154
24. theorem OAI.DeligneDrinfeld.CutoffDepth.left_power_match line 162
25. theorem OAI.DeligneDrinfeld.CutoffDepth.coeff_prefix line 182
26. theorem OAI.DeligneDrinfeld.CutoffDepth.middle_power_match line 200
27. theorem OAI.DeligneDrinfeld.CutoffDepth.coeff_monomial line 221
28. theorem OAI.DeligneDrinfeld.CutoffDepth.coeff_Y_prefix line 232
29. theorem OAI.DeligneDrinfeld.LogCollar.intervalIntegrable_of_at_zero line 259
30. theorem OAI.DeligneDrinfeld.LogCollar.log_pow_at_zero line 275
31. theorem OAI.DeligneDrinfeld.LogCollar.log_pow line 286
32. def OAI.DeligneDrinfeld.KZCollar.gauge line 298
33. def OAI.DeligneDrinfeld.KZCollar.regularForm line 300
34. theorem OAI.DeligneDrinfeld.KZCollar.exp_smul_finite line 303
35. theorem OAI.DeligneDrinfeld.KZCollar.gauge_finite line 318
36. theorem OAI.DeligneDrinfeld.KZCollar.gauge_neg_mul line 324
37. theorem OAI.DeligneDrinfeld.KZCollar.gauge_mul_neg line 330
38. theorem OAI.DeligneDrinfeld.KZCollar.gauge_derivative line 336
39. theorem OAI.DeligneDrinfeld.KZCollar.regularForm_finite line 341
40. theorem OAI.DeligneDrinfeld.KZCollar.regularForm_integrable line 365
41. theorem OAI.DeligneDrinfeld.KZCollar.regularForm_continuous line 393
42. theorem OAI.DeligneDrinfeld.KZCollar.regularForm_mem line 404
43. def OAI.DeligneDrinfeld.KZCollar.normalizedSolution line 416
44. theorem OAI.DeligneDrinfeld.KZCollar.normalizedSolution_derivative line 421
45. theorem OAI.DeligneDrinfeld.KZCollar.normalizedSolution_limit line 439
46. theorem OAI.DeligneDrinfeld.FinitePicard.transport_sub_one_mem line 462
47. theorem OAI.DeligneDrinfeld.FinitePicard.transport_isUnit line 470
48. theorem OAI.DeligneDrinfeld.FinitePicard.inverse_derivative line 478
49. theorem OAI.DeligneDrinfeld.FinitePicard.transition_derivative line 489
50. theorem OAI.DeligneDrinfeld.FinitePicard.transition_constant line 498
51. def OAI.DeligneDrinfeld.KZCollar.bulkForm line 517
52. def OAI.DeligneDrinfeld.KZCollar.gaugeUnit line 519
53. theorem OAI.DeligneDrinfeld.KZCollar.normalizedSolution_isUnit line 527
54. theorem OAI.DeligneDrinfeld.KZCollar.normalizedSolution_derivative_on line 532
55. def OAI.DeligneDrinfeld.KZCollar.rightSolution line 540
56. theorem OAI.DeligneDrinfeld.KZCollar.rightSolution_isUnit line 543
57. theorem OAI.DeligneDrinfeld.KZCollar.rightSolution_derivative line 547
58. def OAI.DeligneDrinfeld.KZCollar.associator line 562
59. theorem OAI.DeligneDrinfeld.KZCollar.associator_is_transition line 565
60. theorem OAI.DeligneDrinfeld.KZCollar.left_eq_right_mul_associator line 572
61. theorem OAI.DeligneDrinfeld.KZCollar.associator_isUnit line 578
62. theorem OAI.DeligneDrinfeld.FinitePicard.map_term line 591
63. theorem OAI.DeligneDrinfeld.FinitePicard.map_transport line 609
64. theorem OAI.DeligneDrinfeld.KZCollar.map_gauge line 621
65. theorem OAI.DeligneDrinfeld.KZCollar.map_regularForm line 627
66. theorem OAI.DeligneDrinfeld.KZCollar.map_normalizedSolution line 634
67. theorem OAI.DeligneDrinfeld.KZCollar.map_unit_inverse line 647
68. theorem OAI.DeligneDrinfeld.KZCollar.map_associator line 657
69. theorem OAI.DeligneDrinfeld.FinitePicard.transition_constant_closed line 674
70. theorem OAI.DeligneDrinfeld.FinitePicard.transport_eq_fundamental line 697
71. theorem OAI.DeligneDrinfeld.KZCollar.bulkForm_mem line 723
72. theorem OAI.DeligneDrinfeld.KZCollar.bulkForm_continuous line 729
73. theorem OAI.DeligneDrinfeld.KZCollar.bulk_transport line 735
74. def OAI.DeligneDrinfeld.KZCollar.regularizedBulk line 750
75. theorem OAI.DeligneDrinfeld.KZCollar.regularizedBulk_eq line 753
76. theorem OAI.DeligneDrinfeld.KZCollar.regularTransport_limit line 775
77. theorem OAI.DeligneDrinfeld.KZCollar.regularizedBulk_limit line 781
78. def OAI.DeligneDrinfeld.DepthIntegral.kernel line 803
79. theorem OAI.DeligneDrinfeld.DepthIntegral.kernel_left line 805
80. theorem OAI.DeligneDrinfeld.DepthIntegral.slope_continuous line 820
81. theorem OAI.DeligneDrinfeld.DepthIntegral.kernel_eq line 825
82. theorem OAI.DeligneDrinfeld.DepthIntegral.kernel_integrable line 834
83. theorem OAI.DeligneDrinfeld.DepthIntegral.kernel_pos line 849
84. theorem OAI.DeligneDrinfeld.DepthIntegral.integral_pos line 854
85. theorem OAI.DeligneDrinfeld.DepthIntegral.coefficient_ne_zero line 858
86. theorem OAI.DeligneDrinfeld.DepthIntegral.integral_zero line 864
87. theorem OAI.DeligneDrinfeld.DepthIntegral.integral_limit line 875
88. theorem OAI.DeligneDrinfeld.DepthIntegral.one_sub_limit line 885
89. theorem OAI.DeligneDrinfeld.DepthIntegral.log_endpoint_product line 895
90. instance OAI.DeligneDrinfeld.CutoffKZ.normedRing line 923
91. instance OAI.DeligneDrinfeld.CutoffKZ.normedAlgebra line 924
92. def OAI.DeligneDrinfeld.CutoffKZ.weight line 926
93. def OAI.DeligneDrinfeld.CutoffKZ.depth line 934
94. abbrev OAI.DeligneDrinfeld.CutoffKZ.X line 942
95. abbrev OAI.DeligneDrinfeld.CutoffKZ.Y line 943
96. abbrev OAI.DeligneDrinfeld.CutoffKZ.c line 944
97. theorem OAI.DeligneDrinfeld.CutoffKZ.X_nilpotent line 946
98. theorem OAI.DeligneDrinfeld.CutoffKZ.X_pow_depth line 948
99. theorem OAI.DeligneDrinfeld.CutoffKZ.regularForm_depth line 953
100. theorem OAI.DeligneDrinfeld.CutoffKZ.coeff_one line 962
101. theorem OAI.DeligneDrinfeld.CutoffKZ.coeff_high_term line 974
102. theorem OAI.DeligneDrinfeld.CutoffKZ.coeff_form line 979
103. theorem OAI.DeligneDrinfeld.CutoffKZ.coeff_first_term line 998
104. theorem OAI.DeligneDrinfeld.CutoffKZ.coeff_transport line 1009
105. theorem OAI.DeligneDrinfeld.KZCollar.gauge_sub_one_mem line 1027
106. theorem OAI.DeligneDrinfeld.KZCollar.product_sub_one_mem line 1035
107. theorem OAI.DeligneDrinfeld.KZCollar.inverse_sub_one_mem line 1042
108. theorem OAI.DeligneDrinfeld.KZCollar.normalizedSolution_sub_one_mem line 1055
109. theorem OAI.DeligneDrinfeld.KZCollar.associator_sub_one_mem line 1061
110. theorem OAI.DeligneDrinfeld.FinitePicard.term_above_cutoff line 1075
111. theorem OAI.DeligneDrinfeld.FinitePicard.stabilize line 1080
112. def OAI.DeligneDrinfeld.FinitePicard.extend line 1090
113. theorem OAI.DeligneDrinfeld.KZCollar.normalized_extend line 1104
114. theorem OAI.DeligneDrinfeld.KZCollar.associator_extend line 1111
115. theorem OAI.DeligneDrinfeld.KZCollar.map_normalized_general line 1120
116. theorem OAI.DeligneDrinfeld.KZCollar.map_associator_general line 1131
117. def OAI.DeligneDrinfeld.CutoffDiagonal.left line 1152
118. def OAI.DeligneDrinfeld.CutoffDiagonal.right line 1153
119. theorem OAI.DeligneDrinfeld.CutoffDiagonal.commute line 1154
120. def OAI.DeligneDrinfeld.CutoffDiagonal.tensorWeight line 1157
121. theorem OAI.DeligneDrinfeld.CutoffDiagonal.left_mem line 1159
122. theorem OAI.DeligneDrinfeld.CutoffDiagonal.right_mem line 1161
123. def OAI.DeligneDrinfeld.CutoffDiagonal.diagonal line 1163
124. theorem OAI.DeligneDrinfeld.CutoffDiagonal.diagonal_gen line 1166
125. theorem OAI.DeligneDrinfeld.CutoffDiagonal.diagonal_mem line 1168
126. def OAI.DeligneDrinfeld.CutoffDiagonal.drop line 1171
127. theorem OAI.DeligneDrinfeld.CutoffDiagonal.drop_gen line 1173
128. theorem OAI.DeligneDrinfeld.CutoffDiagonal.drop_mem line 1175
129. theorem OAI.DeligneDrinfeld.CutoffDiagonal.drop_associator line 1178
130. def OAI.DeligneDrinfeld.RegularSingular.regular line 1191
131. theorem OAI.DeligneDrinfeld.RegularSingular.regular_finite line 1193
132. theorem OAI.DeligneDrinfeld.RegularSingular.regular_integrable line 1214
133. theorem OAI.DeligneDrinfeld.RegularSingular.regular_mem line 1236
134. def OAI.DeligneDrinfeld.RegularSingular.solution line 1247
135. theorem OAI.DeligneDrinfeld.RegularSingular.regular_continuous line 1252
136. theorem OAI.DeligneDrinfeld.RegularSingular.solution_limit line 1260
137. theorem OAI.DeligneDrinfeld.RegularSingular.solution_derivative line 1273
138. theorem OAI.DeligneDrinfeld.RegularSingular.solution_isUnit line 1286
139. def OAI.DeligneDrinfeld.FinitePicard.integralNorm line 1297
140. theorem OAI.DeligneDrinfeld.FinitePicard.integralNorm_nonneg line 1300
141. theorem OAI.DeligneDrinfeld.FinitePicard.norm_term_le line 1303
142. theorem OAI.DeligneDrinfeld.FinitePicard.integrable_partial line 1326
143. theorem OAI.DeligneDrinfeld.FinitePicard.integralNorm_partial line 1333
144. theorem OAI.DeligneDrinfeld.FinitePicard.norm_term_bound line 1338
145. theorem OAI.DeligneDrinfeld.FinitePicard.norm_term_sub_le line 1344
146. def OAI.DeligneDrinfeld.FinitePicard.transportPoly line 1394
147. def OAI.DeligneDrinfeld.FinitePicard.errorPoly line 1396
148. theorem OAI.DeligneDrinfeld.FinitePicard.norm_transport_le line 1398
149. theorem OAI.DeligneDrinfeld.FinitePicard.norm_transport_sub_le line 1409
150. def OAI.DeligneDrinfeld.PowerAsymptotic.Subpower line 1431
151. def OAI.DeligneDrinfeld.PowerAsymptotic.PowerSmall line 1434
152. lemma OAI.DeligneDrinfeld.PowerAsymptotic.rpow_mul_eventually line 1439
153. theorem OAI.DeligneDrinfeld.PowerAsymptotic.log_pow_subpower line 1444
154. theorem OAI.DeligneDrinfeld.PowerAsymptotic.Subpower.add line 1451
155. theorem OAI.DeligneDrinfeld.PowerAsymptotic.Subpower.mul line 1455
156. theorem OAI.DeligneDrinfeld.PowerAsymptotic.const_subpower line 1465
157. theorem OAI.DeligneDrinfeld.PowerAsymptotic.continuousAt_subpower line 1472
158. theorem OAI.DeligneDrinfeld.PowerAsymptotic.gauge_subpower line 1477
159. theorem OAI.DeligneDrinfeld.PowerAsymptotic.PowerSmall.mul_subpower line 1491
160. theorem OAI.DeligneDrinfeld.PowerAsymptotic.Subpower.mul_powerSmall line 1503
161. theorem OAI.DeligneDrinfeld.PowerAsymptotic.PowerSmall.tendsto_zero line 1514
162. theorem OAI.DeligneDrinfeld.PowerAsymptotic.integralNorm_isBigO line 1523
163. theorem OAI.DeligneDrinfeld.PowerAsymptotic.transport_sub_one_isBigO_integralNorm line 1554
164. theorem OAI.DeligneDrinfeld.PowerAsymptotic.transport_sub_one_powerSmall line 1583
165. theorem OAI.DeligneDrinfeld.PowerAsymptotic.tendsto_subpower line 1599
166. theorem OAI.DeligneDrinfeld.PowerAsymptotic.continuousOn_subpower line 1605
167. theorem OAI.DeligneDrinfeld.PowerAsymptotic.PowerSmall.of_isBigO line 1612
168. theorem OAI.DeligneDrinfeld.PowerAsymptotic.Subpower.of_isBigO line 1618
169. theorem OAI.DeligneDrinfeld.PowerAsymptotic.PowerSmall.congr line 1622
170. theorem OAI.DeligneDrinfeld.PowerAsymptotic.regular_subpower line 1627
171. theorem OAI.DeligneDrinfeld.PowerAsymptotic.solution_sub_gauge line 1631
172. theorem OAI.DeligneDrinfeld.PowerAsymptotic.Subpower.pow line 1640
173. theorem OAI.DeligneDrinfeld.PowerAsymptotic.Subpower.sum line 1646
174. theorem OAI.DeligneDrinfeld.PowerAsymptotic.errorPoly_subpower line 1654
175. theorem OAI.DeligneDrinfeld.PowerAsymptotic.inverse_tendsto_one line 1663
176. theorem OAI.DeligneDrinfeld.PowerAsymptotic.inverse_sub_one_powerSmall line 1668
177. theorem OAI.DeligneDrinfeld.PowerAsymptotic.inverse_mul_of_units line 1681
178. theorem OAI.DeligneDrinfeld.PowerAsymptotic.inverse_gauge line 1688
179. theorem OAI.DeligneDrinfeld.PowerAsymptotic.inverse_solution_sub_gauge line 1698
180. theorem OAI.DeligneDrinfeld.KZCollar.subpower_congrEventual line 1722
181. theorem OAI.DeligneDrinfeld.KZCollar.linear_powerSmall line 1725
182. theorem OAI.DeligneDrinfeld.KZCollar.gauge_at_larger_subpower line 1730
183. theorem OAI.DeligneDrinfeld.KZCollar.gauge_mul_scale line 1744
184. theorem OAI.DeligneDrinfeld.KZCollar.gauge_add_of_commute line 1751
185. theorem OAI.DeligneDrinfeld.KZCollar.gauge_continuousAt line 1757
186. theorem OAI.DeligneDrinfeld.KZCollar.gauge_one line 1761
187. theorem OAI.DeligneDrinfeld.KZCollar.gauge_ratio_limit line 1763
188. def OAI.DeligneDrinfeld.FinitePicard.centralizer line 1778
189. theorem OAI.DeligneDrinfeld.FinitePicard.term_commute line 1786
190. theorem OAI.DeligneDrinfeld.FinitePicard.transport_commute line 1794
191. theorem OAI.DeligneDrinfeld.FinitePicard.gauge_commute line 1799
192. theorem OAI.DeligneDrinfeld.FinitePicard.transport_add_commute line 1809
193. theorem OAI.DeligneDrinfeld.KZProduct.shuffle line 1850
194. theorem OAI.DeligneDrinfeld.KZProduct.gauge_sum line 1856
195. theorem OAI.DeligneDrinfeld.KZProduct.regular_sum line 1862
196. theorem OAI.DeligneDrinfeld.KZProduct.normalized_sum line 1876
197. theorem OAI.DeligneDrinfeld.KZProduct.associator_product line 1909
198. theorem OAI.DeligneDrinfeld.CutoffKZ.coeff_gauge_Y line 1933
199. def OAI.DeligneDrinfeld.CutoffKZ.prefactor line 1951
200. theorem OAI.DeligneDrinfeld.CutoffKZ.coeff_normalized line 1955
201. theorem OAI.DeligneDrinfeld.CutoffKZ.prefactor_limit line 1971
202. theorem OAI.DeligneDrinfeld.CutoffKZ.coeff_normalized_limit line 2005
203. theorem OAI.DeligneDrinfeld.CutoffKZ.left_regularized_limit line 2015
204. theorem OAI.DeligneDrinfeld.CutoffKZ.associator_coefficient line 2027
205. theorem OAI.DeligneDrinfeld.CutoffKZ.associator_coefficient_ne_zero line 2040
206. theorem OAI.DeligneDrinfeld.CutoffKZ.depth_initial line 2045
207. theorem OAI.DeligneDrinfeld.CutoffKZ.gaugeX_depth_zero line 2052
208. theorem OAI.DeligneDrinfeld.CutoffKZ.left_regularized_depth line 2055
209. theorem OAI.DeligneDrinfeld.CutoffKZ.associator_depth_one line 2073
210. theorem OAI.DeligneDrinfeld.ConjugateComparison.mem_zero line 2092
211. theorem OAI.DeligneDrinfeld.ConjugateComparison.inverse_normalized line 2094
212. def OAI.DeligneDrinfeld.ConjugateComparison.family line 2101
213. theorem OAI.DeligneDrinfeld.ConjugateComparison.family_mem line 2105
214. theorem OAI.DeligneDrinfeld.ConjugateComparison.family_leading line 2111
215. def OAI.DeligneDrinfeld.ConjugateComparison.transport line 2127
216. theorem OAI.DeligneDrinfeld.ConjugateComparison.transport_gen line 2130
217. def OAI.DeligneDrinfeld.ConjugateComparison.theta line 2133
218. def OAI.DeligneDrinfeld.ConjugateComparison.unitArrow line 2136
219. theorem OAI.DeligneDrinfeld.ConjugateComparison.exact_comparison line 2139
220. theorem OAI.DeligneDrinfeld.ConjugateComparison.theta_transport line 2145
221. theorem OAI.DeligneDrinfeld.ConjugateComparison.theta_x line 2149
222. theorem OAI.DeligneDrinfeld.ConjugateComparison.theta_y line 2153
223. theorem OAI.DeligneDrinfeld.ConjugateComparison.transport_raises line 2172
224. theorem OAI.DeligneDrinfeld.ConjugateComparison.transport_inverse_preserves line 2176
225. theorem OAI.DeligneDrinfeld.ConjugateComparison.theta_raises line 2190
226. theorem OAI.DeligneDrinfeld.ConjugateComparison.theta_preserves line 2197
227. theorem OAI.DeligneDrinfeld.ConjugateComparison.mul_normalized line 2203
228. theorem OAI.DeligneDrinfeld.ConjugateComparison.unitArrow_normalized line 2209
229. theorem OAI.DeligneDrinfeld.DepthSubstitution.initial line 2224
230. theorem OAI.DeligneDrinfeld.DepthSubstitution.all_zero line 2230
231. theorem OAI.DeligneDrinfeld.DepthSubstitution.lift_word_mem line 2232
232. theorem OAI.DeligneDrinfeld.DepthSubstitution.lift_word_difference line 2240
233. theorem OAI.DeligneDrinfeld.DepthSubstitution.subst_raises line 2256
234. theorem OAI.DeligneDrinfeld.DepthSubstitution.family_mem line 2269
235. theorem OAI.DeligneDrinfeld.DepthSubstitution.family_leading line 2275
236. def OAI.DeligneDrinfeld.CutoffScaling.map line 2299
237. theorem OAI.DeligneDrinfeld.CutoffScaling.map_gen line 2302
238. theorem OAI.DeligneDrinfeld.CutoffScaling.lift_word line 2304
239. theorem OAI.DeligneDrinfeld.CutoffScaling.map_word line 2314
240. theorem OAI.DeligneDrinfeld.CutoffScaling.coefficient line 2318
241. theorem OAI.DeligneDrinfeld.CutoffScaling.preserves_depth line 2335
242. theorem OAI.DeligneDrinfeld.ConjugateComparison.transport_depth_raises line 2353
243. theorem OAI.DeligneDrinfeld.ConjugateComparison.transport_inverse_depth line 2359
244. theorem OAI.DeligneDrinfeld.ConjugateComparison.theta_depth_raises line 2374
245. theorem OAI.DeligneDrinfeld.ConjugateComparison.theta_depth_preserves line 2382
246. theorem OAI.DeligneDrinfeld.ConjugateComparison.units_product_depth line 2389
247. theorem OAI.DeligneDrinfeld.ConjugateComparison.units_inverse_depth line 2394
248. theorem OAI.DeligneDrinfeld.ConjugateComparison.unitArrow_depth line 2401