OAI/Combinatorics/SumProduct/Alignment/WordPlan01.lean

GitHub source file

227 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.AllLevelFactorization.Factorization.smoothAction line 37
2. def OAI.AllLevelFactorization.Factorization.pointMixture line 41
3. lemma OAI.AllLevelFactorization.Factorization.pointMixture_integral line 46
4. def OAI.AllLevelFactorization.Factorization.empiricalPointLaw line 61
5. theorem OAI.AllLevelFactorization.Factorization.weak_point_law line 67
6. structure OAI.ConstructedWordPlan.CubeFaces.Filtration line 103
7. def OAI.ConstructedWordPlan.CubeFaces.face line 109
8. lemma OAI.ConstructedWordPlan.CubeFaces.face_apply line 114
9. lemma OAI.ConstructedWordPlan.CubeFaces.face_commutator line 117
10. def OAI.ConstructedWordPlan.CubeFaces.cube line 125
11. lemma OAI.ConstructedWordPlan.CubeFaces.face_mem_cube line 128
12. def OAI.ConstructedWordPlan.CubeFaces.upper line 136
13. lemma OAI.ConstructedWordPlan.CubeFaces.upper_face line 141
14. lemma OAI.ConstructedWordPlan.CubeFaces.map_upper_cube line 147
15. lemma OAI.ConstructedWordPlan.CubeFaces.upper_face_apply line 153
16. lemma OAI.ConstructedWordPlan.CubeFaces.face_upper_commutator_mem line 157
17. lemma OAI.ConstructedWordPlan.CubeFaces.cube_le_normalizer_upper line 171
18. lemma OAI.ConstructedWordPlan.CubeFaces.cube_insert_le line 203
19. lemma OAI.ConstructedWordPlan.CubeFaces.cube_decompose line 228
20. def OAI.ConstructedWordPlan.CubeFaces.evaluation line 238
21. lemma OAI.ConstructedWordPlan.CubeFaces.cube_insert_irrelevant line 243
22. lemma OAI.ConstructedWordPlan.CubeFaces.cube_eval_mem line 260
23. lemma OAI.ConstructedWordPlan.CubeFaces.cube_shift_le line 272
24. lemma OAI.ConstructedWordPlan.CubeFaces.cube_restrict line 278
25. lemma OAI.ConstructedWordPlan.CubeFaces.cube_normalizes line 288
26. def OAI.ConstructedWordPlan.CubeFaces.commModulo line 319
27. lemma OAI.ConstructedWordPlan.CubeFaces.face_cube_commutator_mem line 340
28. lemma OAI.ConstructedWordPlan.CubeFaces.cube_commutator_mem line 358
29. lemma OAI.ConstructedWordPlan.CubeFaces.cube_mono line 373
30. lemma OAI.ConstructedWordPlan.CubeFaces.upper_cube_mem line 378
31. def OAI.ConstructedWordPlan.CubePolynomials.pattern line 399
32. def OAI.ConstructedWordPlan.CubePolynomials.polynomials line 404
33. lemma OAI.ConstructedWordPlan.CubePolynomials.mem_polynomials line 407
34. lemma OAI.ConstructedWordPlan.CubePolynomials.polynomials_antitone line 411
35. lemma OAI.ConstructedWordPlan.CubePolynomials.eval_mem line 417
36. lemma OAI.ConstructedWordPlan.CubePolynomials.const_mem line 422
37. lemma OAI.ConstructedWordPlan.CubePolynomials.polynomials_eq_bot line 430
38. def OAI.ConstructedWordPlan.CubePolynomials.shift line 439
39. lemma OAI.ConstructedWordPlan.CubePolynomials.shift_mem line 446
40. lemma OAI.ConstructedWordPlan.CubePolynomials.derivative_mem line 456
41. lemma OAI.ConstructedWordPlan.CubePolynomials.mem_of_derivatives line 500
42. lemma OAI.ConstructedWordPlan.CubePolynomials.commutator_mem line 542
43. lemma OAI.ConstructedWordPlan.CubePolynomials.normalizes line 550
44. lemma OAI.ConstructedWordPlan.CubePolynomials.power_polynomial_mem line 568
45. lemma OAI.ConstructedWordPlan.FilteredPET.decrease_of_high_embedding line 616
46. structure OAI.ConstructedWordPlan.FilteredPET.Filtration line 652
47. instance OAI.ConstructedWordPlan.FilteredPET.Filtration.level_normal line 661
48. def OAI.ConstructedWordPlan.FilteredPET.Filtration.degree line 663
49. lemma OAI.ConstructedWordPlan.FilteredPET.Filtration.degree_mem line 667
50. lemma OAI.ConstructedWordPlan.FilteredPET.Filtration.degree_le_iff line 671
51. lemma OAI.ConstructedWordPlan.FilteredPET.Filtration.degree_one line 678
52. lemma OAI.ConstructedWordPlan.FilteredPET.Filtration.degree_eq_zero line 682
53. lemma OAI.ConstructedWordPlan.FilteredPET.Filtration.degree_pos line 685
54. lemma OAI.ConstructedWordPlan.FilteredPET.Filtration.degree_mul_le line 688
55. lemma OAI.ConstructedWordPlan.FilteredPET.Filtration.degree_inv line 693
56. abbrev OAI.ConstructedWordPlan.FilteredPET.Filtration.Signature line 698
57. def OAI.ConstructedWordPlan.FilteredPET.Filtration.signature line 700
58. lemma OAI.ConstructedWordPlan.FilteredPET.Filtration.signature_at line 703
59. lemma OAI.ConstructedWordPlan.FilteredPET.Filtration.degree_mul_eq_left line 708
60. lemma OAI.ConstructedWordPlan.FilteredPET.Filtration.degree_eq_of_lower line 722
61. lemma OAI.ConstructedWordPlan.FilteredPET.Filtration.signature_eq_of_lower line 743
62. def OAI.ConstructedWordPlan.FilteredPET.Filtration.leaderShift line 757
63. lemma OAI.ConstructedWordPlan.FilteredPET.Filtration.leaderShift_degree line 765
64. lemma OAI.ConstructedWordPlan.FilteredPET.Filtration.quotient_eq_one_iff line 768
65. lemma OAI.ConstructedWordPlan.FilteredPET.Filtration.signature_mul_high line 773
66. lemma OAI.ConstructedWordPlan.FilteredPET.Filtration.signature_mul_equal line 781
67. lemma OAI.ConstructedWordPlan.FilteredPET.Filtration.signature_eq_lower line 794
68. lemma OAI.ConstructedWordPlan.FilteredPET.Filtration.reduction_signature line 808
69. lemma OAI.ConstructedWordPlan.FilteredPET.Filtration.reduction_same line 824
70. def OAI.ConstructedWordPlan.FilteredPET.Filtration.leaders line 835
71. def OAI.ConstructedWordPlan.FilteredPET.Filtration.weight line 839
72. theorem OAI.ConstructedWordPlan.FilteredPET.Filtration.weight_lt line 843
73. structure OAI.ConstructedWordPlan.GroupPET.System line 879
74. def OAI.ConstructedWordPlan.GroupPET.System.reduce line 894
75. def OAI.ConstructedWordPlan.GroupPET.System.reducedFamily line 896
76. lemma OAI.ConstructedWordPlan.GroupPET.System.reduce_eval line 900
77. lemma OAI.ConstructedWordPlan.GroupPET.System.reducedFamily_weight_lt line 904
78. lemma OAI.ConstructedWordPlan.GroupPET.System.conjugate_signature line 916
79. lemma OAI.ConstructedWordPlan.GroupPET.System.conjugate_eq_one_iff line 920
80. def OAI.ConstructedWordPlan.GroupPET.System.conjugateFamily line 925
81. lemma OAI.ConstructedWordPlan.GroupPET.System.conjugateFamily_leaders line 929
82. lemma OAI.ConstructedWordPlan.GroupPET.System.conjugateFamily_weight line 950
83. theorem OAI.ConstructedWordPlan.MinimalSubsystem.exists_closed_minimal line 963
84. theorem OAI.ConstructedWordPlan.MinimalSubsystem.exists_minimal_subaction line 990
85. def OAI.ConstructedWordPlan.GroupPETRecurrence.ClopenRecurrence line 1031
86. def OAI.ConstructedWordPlan.GroupPETRecurrence.Focused line 1037
87. lemma OAI.ConstructedWordPlan.GroupPETRecurrence.Focused.monotone line 1045
88. lemma OAI.ConstructedWordPlan.GroupPETRecurrence.focused_singleton line 1054
89. lemma OAI.ConstructedWordPlan.GroupPETRecurrence.focused_extend line 1067
90. lemma OAI.ConstructedWordPlan.GroupPETRecurrence.focused_arbitrary line 1142
91. lemma OAI.ConstructedWordPlan.GroupPETRecurrence.monochromatic_of_lower line 1154
92. theorem OAI.ConstructedWordPlan.GroupPETRecurrence.clopen_polynomial_recurrence line 1180
93. theorem OAI.ConstructedWordPlan.GroupPETRecurrence.continuous_polynomial_recurrence line 1245
94. theorem OAI.ConstructedWordPlan.GroupPETRecurrence.coloring_polynomial_recurrence line 1269
95. def OAI.ConstructedWordPlan.CubePolynomials.evaluation line 1324
96. def OAI.ConstructedWordPlan.CubePolynomials.normalized line 1329
97. lemma OAI.ConstructedWordPlan.CubePolynomials.mem_normalized line 1332
98. lemma OAI.ConstructedWordPlan.CubePolynomials.normalized_antitone line 1335
99. lemma OAI.ConstructedWordPlan.CubePolynomials.normalized_normalizes line 1339
100. def OAI.ConstructedWordPlan.CubePolynomials.reversedFiltration line 1357
101. def OAI.ConstructedWordPlan.CubePolynomials.normalizeShift line 1383
102. lemma OAI.ConstructedWordPlan.CubePolynomials.normalizeShift_mem line 1385
103. lemma OAI.ConstructedWordPlan.CubePolynomials.normalizeShift_lower line 1394
104. def OAI.ConstructedWordPlan.CubePolynomials.conjugateSequence line 1418
105. lemma OAI.ConstructedWordPlan.CubePolynomials.conjugateSequence_mem line 1420
106. lemma OAI.ConstructedWordPlan.CubePolynomials.conjugateSequence_lower line 1432
107. def OAI.ConstructedWordPlan.CubePolynomials.system line 1447
108. lemma OAI.ConstructedWordPlan.StretchedFiltration.rotate_le line 1510
109. theorem OAI.ConstructedWordPlan.StretchedFiltration.lower_bracket line 1527
110. def OAI.ConstructedWordPlan.StretchedFiltration.stretch line 1552
111. lemma OAI.ConstructedWordPlan.StretchedFiltration.stretch_antitone line 1555
112. lemma OAI.ConstructedWordPlan.StretchedFiltration.stretch_zero line 1559
113. lemma OAI.ConstructedWordPlan.StretchedFiltration.stretch_one line 1562
114. lemma OAI.ConstructedWordPlan.StretchedFiltration.stretch_eq_top line 1565
115. lemma OAI.ConstructedWordPlan.StretchedFiltration.stretch_terminal line 1570
116. lemma OAI.ConstructedWordPlan.StretchedFiltration.stretch_bracket line 1575
117. def OAI.ConstructedWordPlan.NilpotentPolynomialRecurrence.word line 1609
118. lemma OAI.ConstructedWordPlan.NilpotentPolynomialRecurrence.word_mem line 1612
119. theorem OAI.ConstructedWordPlan.NilpotentPolynomialRecurrence.coloring_recurrence line 1634
120. def OAI.ConstructedWordPlan.UniformRecurrence.Recurs line 1689
121. theorem OAI.ConstructedWordPlan.UniformRecurrence.finite_alternatives line 1694
122. structure OAI.ConstructedWordPlan.UniformRecurrence.PolynomialWord line 1727
123. def OAI.ConstructedWordPlan.UniformRecurrence.PolynomialWord.eval line 1733
124. lemma OAI.ConstructedWordPlan.UniformRecurrence.PolynomialWord.map_eval line 1736
125. lemma OAI.ConstructedWordPlan.UniformRecurrence.PolynomialWord.eval_zero line 1740
126. def OAI.ConstructedWordPlan.UniformRecurrence.FreeNilpotent line 1750
127. instance OAI.ConstructedWordPlan.UniformRecurrence.(instance at line 1753) line 1753
128. def OAI.ConstructedWordPlan.UniformRecurrence.FreeNilpotent.of line 1760
129. theorem OAI.ConstructedWordPlan.UniformRecurrence.FreeNilpotent.lower_eq_bot line 1764
130. instance OAI.ConstructedWordPlan.UniformRecurrence.FreeNilpotent.(instance at line 1776) line 1776
131. instance OAI.ConstructedWordPlan.UniformRecurrence.FreeNilpotent.(instance at line 1779) line 1779
132. theorem OAI.ConstructedWordPlan.UniformRecurrence.FreeNilpotent.lift_kernel line 1786
133. def OAI.ConstructedWordPlan.UniformRecurrence.FreeNilpotent.lift line 1798
134. theorem OAI.ConstructedWordPlan.UniformRecurrence.FreeNilpotent.lift_of line 1802
135. lemma OAI.ConstructedWordPlan.UniformRecurrence.FreeNilpotent.lift_polynomialWord line 1808
136. theorem OAI.ConstructedWordPlan.UniformRecurrence.universal_quotient_alternatives line 1826
137. theorem OAI.ConstructedWordPlan.UniformRecurrence.universal_finite_alternatives line 1851
138. def OAI.ConstructedWordPlan.FiniteWordPlan.inflate line 1893
139. def OAI.ConstructedWordPlan.FiniteWordPlan.polynomial line 1896
140. lemma OAI.ConstructedWordPlan.FiniteWordPlan.eval_polynomial line 1907
141. lemma OAI.ConstructedWordPlan.FiniteWordPlan.interpretation_inflation line 1922
142. theorem OAI.ConstructedWordPlan.FiniteWordPlan.update_options line 1933
143. def OAI.ConstructedWordPlan.FiniteWordPlan.Requirement line 1954
144. def OAI.ConstructedWordPlan.FiniteWordPlan.predecessor line 1960
145. lemma OAI.ConstructedWordPlan.FiniteWordPlan.protect_jump line 1969
146. structure OAI.ConstructedWordPlan.FiniteWordPlan.ScaleSystem line 2000
147. def OAI.ConstructedWordPlan.FiniteWordPlan.run line 2015
148. lemma OAI.ConstructedWordPlan.FiniteWordPlan.run_append line 2021
149. theorem OAI.ConstructedWordPlan.FiniteWordPlan.pivot_plan line 2034
150. def OAI.ConstructedWordPlan.AlignmentScales.weight line 2133
151. def OAI.ConstructedWordPlan.AlignmentScales.weightSum line 2134
152. lemma OAI.ConstructedWordPlan.AlignmentScales.geom_sum line 2136
153. lemma OAI.ConstructedWordPlan.AlignmentScales.sum_later_lt line 2142
154. lemma OAI.ConstructedWordPlan.AlignmentScales.weightSum_nonneg line 2172
155. lemma OAI.ConstructedWordPlan.AlignmentScales.exponent_pos line 2177
156. def OAI.ConstructedWordPlan.AlignmentScales.updateExponent line 2187
157. def OAI.ConstructedWordPlan.AlignmentScales.multiplier line 2191
158. def OAI.ConstructedWordPlan.AlignmentScales.blockProduct line 2194
159. def OAI.ConstructedWordPlan.AlignmentScales.update line 2196
160. lemma OAI.ConstructedWordPlan.AlignmentScales.multiplier_pos line 2199
161. lemma OAI.ConstructedWordPlan.AlignmentScales.blockProduct_update line 2202
162. lemma OAI.ConstructedWordPlan.AlignmentScales.blockProduct_multiplier line 2207
163. lemma OAI.ConstructedWordPlan.AlignmentScales.exponentSum_before line 2218
164. lemma OAI.ConstructedWordPlan.AlignmentScales.exponentSum_target line 2226
165. lemma OAI.ConstructedWordPlan.AlignmentScales.target_preserved line 2236
166. lemma OAI.ConstructedWordPlan.AlignmentScales.ratio_update line 2243
167. def OAI.ConstructedWordPlan.RationalPivotPlan.tailAt line 2265
168. lemma OAI.ConstructedWordPlan.RationalPivotPlan.tailAt_fin line 2267
169. def OAI.ConstructedWordPlan.RationalPivotPlan.block line 2270
170. def OAI.ConstructedWordPlan.RationalPivotPlan.transport line 2272
171. lemma OAI.ConstructedWordPlan.RationalPivotPlan.transport_tag line 2275
172. def OAI.ConstructedWordPlan.RationalPivotPlan.transportPos line 2280
173. lemma OAI.ConstructedWordPlan.RationalPivotPlan.transportPos_tag line 2283
174. lemma OAI.ConstructedWordPlan.RationalPivotPlan.transportPos_fix line 2288
175. def OAI.ConstructedWordPlan.RationalPivotPlan.exponent line 2304
176. def OAI.ConstructedWordPlan.RationalPivotPlan.lam line 2307
177. lemma OAI.ConstructedWordPlan.RationalPivotPlan.exponent_positive line 2309
178. lemma OAI.ConstructedWordPlan.RationalPivotPlan.lam_positive line 2314
179. abbrev OAI.ConstructedWordPlan.RationalPivotPlan.State line 2324
180. def OAI.ConstructedWordPlan.RationalPivotPlan.system line 2326
181. theorem OAI.ConstructedWordPlan.RationalPivotPlan.rational_pivot_plan line 2343
182. def OAI.ConstructedWordPlan.RationalPivotPlan.qExponent line 2375
183. lemma OAI.ConstructedWordPlan.RationalPivotPlan.qExponent_update line 2378
184. def OAI.ConstructedWordPlan.RationalPivotPlan.Realizes line 2397
185. lemma OAI.ConstructedWordPlan.RationalPivotPlan.realizes_update line 2401
186. lemma OAI.ConstructedWordPlan.RationalPivotPlan.realizes_run line 2418
187. def OAI.ConstructedWordPlan.RationalPivotPlan.letters line 2435
188. lemma OAI.ConstructedWordPlan.RationalPivotPlan.lift_congr_on_letters line 2439
189. def OAI.ConstructedWordPlan.RationalPivotPlan.letter line 2453
190. lemma OAI.ConstructedWordPlan.RationalPivotPlan.realizes_lift line 2456
191. theorem OAI.ConstructedWordPlan.RationalPivotPlan.finite_denominator line 2466
192. def OAI.ConstructedWordPlan.RationalPivotPlan.exactRun line 2497
193. lemma OAI.ConstructedWordPlan.RationalPivotPlan.run_eq_exact line 2503
194. lemma OAI.ConstructedWordPlan.RationalPivotPlan.realizes_letter line 2526
195. theorem OAI.ConstructedWordPlan.RationalPivotPlan.integral_pivot_plan line 2535
196. structure OAI.ConstructedWordPlan.GlobalWordPlan.Pivot line 2606
197. abbrev OAI.ConstructedWordPlan.GlobalWordPlan.Scale line 2618
198. abbrev OAI.ConstructedWordPlan.GlobalWordPlan.Alphabet line 2619
199. abbrev OAI.ConstructedWordPlan.GlobalWordPlan.Path line 2620
200. def OAI.ConstructedWordPlan.GlobalWordPlan.scaleRun line 2622
201. lemma OAI.ConstructedWordPlan.GlobalWordPlan.update_mul line 2626
202. lemma OAI.ConstructedWordPlan.GlobalWordPlan.scaleRun_mul line 2632
203. lemma OAI.ConstructedWordPlan.GlobalWordPlan.scaleRun_eq_mul line 2638
204. lemma OAI.ConstructedWordPlan.GlobalWordPlan.exactRun_fst line 2642
205. lemma OAI.ConstructedWordPlan.GlobalWordPlan.blockProduct_mul line 2649
206. def OAI.ConstructedWordPlan.GlobalWordPlan.adjust line 2653
207. lemma OAI.ConstructedWordPlan.GlobalWordPlan.qExponent_adjust line 2657
208. lemma OAI.ConstructedWordPlan.GlobalWordPlan.lift_adjust line 2664
209. def OAI.ConstructedWordPlan.GlobalWordPlan.baseWord line 2681
210. def OAI.ConstructedWordPlan.GlobalWordPlan.terminal line 2684
211. def OAI.ConstructedWordPlan.GlobalWordPlan.Good line 2691
212. lemma OAI.ConstructedWordPlan.GlobalWordPlan.good_future line 2699
213. theorem OAI.ConstructedWordPlan.GlobalWordPlan.pivot_future_plan line 2720
214. def OAI.ConstructedWordPlan.GlobalWordPlan.Plan line 2755
215. def OAI.ConstructedWordPlan.GlobalWordPlan.ChoicePath line 2759
216. def OAI.ConstructedWordPlan.GlobalWordPlan.Admitted line 2763
217. def OAI.ConstructedWordPlan.GlobalWordPlan.positivePlan line 2767
218. def OAI.ConstructedWordPlan.GlobalWordPlan.pathMultiplier line 2771
219. def OAI.ConstructedWordPlan.GlobalWordPlan.multipliers line 2775
220. lemma OAI.ConstructedWordPlan.GlobalWordPlan.pathMultiplier_mem line 2780
221. structure OAI.ConstructedWordPlan.GlobalWordPlan.Action line 2788
222. def OAI.ConstructedWordPlan.GlobalWordPlan.Actions line 2799
223. def OAI.ConstructedWordPlan.GlobalWordPlan.States line 2803
224. def OAI.ConstructedWordPlan.GlobalWordPlan.execute line 2808
225. def OAI.ConstructedWordPlan.GlobalWordPlan.allGood line 2816
226. lemma OAI.ConstructedWordPlan.GlobalWordPlan.execute_fst line 2822
227. theorem OAI.ConstructedWordPlan.GlobalWordPlan.finite_word_plan line 2833