OAI/Analysis/RecursivePotentials/Model.lean

GitHub source file

221 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.RecursivePotentials.leastPair_difference line 13
2. lemma OAI.RecursivePotentials.leastPair_nonneg line 22
3. lemma OAI.RecursivePotentials.leastPair_minimal line 26
4. lemma OAI.RecursivePotentials.sum_add_sq_le line 35
5. def OAI.RecursivePotentials.energy line 56
6. def OAI.RecursivePotentials.FiniteRootedTree.Upper line 66
7. lemma OAI.RecursivePotentials.FiniteRootedTree.depth_le_maxDepth line 69
8. lemma OAI.RecursivePotentials.FiniteRootedTree.child_depth line 73
9. lemma OAI.RecursivePotentials.FiniteRootedTree.child_measure line 77
10. lemma OAI.RecursivePotentials.FiniteRootedTree.fields_eq line 83
11. lemma OAI.RecursivePotentials.FiniteRootedTree.fields_nonneg line 91
12. lemma OAI.RecursivePotentials.FiniteRootedTree.fields_difference line 96
13. lemma OAI.RecursivePotentials.FiniteRootedTree.fields_upper line 101
14. theorem OAI.RecursivePotentials.FiniteRootedTree.fields_minimal line 111
15. lemma OAI.RecursivePotentials.FiniteRootedTree.mem_ancestors_self line 131
16. lemma OAI.RecursivePotentials.FiniteRootedTree.ancestors_parent_closed line 135
17. lemma OAI.RecursivePotentials.FiniteRootedTree.subset_ancestorClosure line 148
18. lemma OAI.RecursivePotentials.FiniteRootedTree.ancestorClosure_initial line 152
19. lemma OAI.RecursivePotentials.FiniteRootedTree.mem_restrict_children line 165
20. lemma OAI.RecursivePotentials.FiniteRootedTree.sum_restrict_children line 169
21. lemma OAI.RecursivePotentials.FiniteRootedTree.extend_mem line 183
22. lemma OAI.RecursivePotentials.FiniteRootedTree.extend_coe line 186
23. lemma OAI.RecursivePotentials.FiniteRootedTree.extend_not_mem line 189
24. lemma OAI.RecursivePotentials.FiniteRootedTree.extend_nonneg line 192
25. def OAI.RecursivePotentials.FiniteRootedTree.GlobalUpper line 199
26. lemma OAI.RecursivePotentials.FiniteRootedTree.GlobalUpper.restrict line 203
27. lemma OAI.RecursivePotentials.FiniteRootedTree.extend_upper line 209
28. lemma OAI.RecursivePotentials.FiniteRootedTree.GlobalUpper.add line 248
29. lemma OAI.RecursivePotentials.FiniteRootedTree.GlobalUpper.smul line 254
30. lemma OAI.RecursivePotentials.FiniteRootedTree.GlobalUpper.le_root line 261
31. lemma OAI.RecursivePotentials.FiniteRootedTree.head_initial line 272
32. lemma OAI.RecursivePotentials.FiniteRootedTree.support_subset_head line 275
33. lemma OAI.RecursivePotentials.FiniteRootedTree.zero_off_head line 278
34. def OAI.RecursivePotentials.FiniteRootedTree.P line 281
35. def OAI.RecursivePotentials.FiniteRootedTree.Q line 285
36. lemma OAI.RecursivePotentials.FiniteRootedTree.P_nonneg line 289
37. lemma OAI.RecursivePotentials.FiniteRootedTree.Q_nonneg line 292
38. lemma OAI.RecursivePotentials.FiniteRootedTree.P_upper line 295
39. lemma OAI.RecursivePotentials.FiniteRootedTree.Q_upper line 298
40. lemma OAI.RecursivePotentials.FiniteRootedTree.P_sub_Q line 301
41. lemma OAI.RecursivePotentials.FiniteRootedTree.potentials_minimal line 307
42. def OAI.RecursivePotentials.FiniteRootedTree.normSum line 319
43. lemma OAI.RecursivePotentials.FiniteRootedTree.potentials_zero line 321
44. lemma OAI.RecursivePotentials.FiniteRootedTree.potentials_add_le line 327
45. lemma OAI.RecursivePotentials.FiniteRootedTree.potentials_neg line 339
46. lemma OAI.RecursivePotentials.FiniteRootedTree.potentials_smul_le line 351
47. lemma OAI.RecursivePotentials.FiniteRootedTree.potentials_smul_nonneg line 361
48. lemma OAI.RecursivePotentials.FiniteRootedTree.normSum_nonneg line 374
49. lemma OAI.RecursivePotentials.FiniteRootedTree.normSum_zero line 377
50. lemma OAI.RecursivePotentials.FiniteRootedTree.normSum_neg line 381
51. lemma OAI.RecursivePotentials.FiniteRootedTree.normSum_add_le line 385
52. lemma OAI.RecursivePotentials.FiniteRootedTree.normSum_smul_nonneg line 390
53. lemma OAI.RecursivePotentials.FiniteRootedTree.normSum_smul line 396
54. lemma OAI.RecursivePotentials.FiniteRootedTree.abs_coordinate_le_normSum line 402
55. lemma OAI.RecursivePotentials.FiniteRootedTree.normSum_eq_zero_iff line 413
56. lemma OAI.RecursivePotentials.FiniteRootedTree.projectHead_apply line 423
57. lemma OAI.RecursivePotentials.FiniteRootedTree.projectHead_bound line 426
58. def OAI.RecursivePotentials.TreeVector line 447
59. instance OAI.RecursivePotentials.TreeVector.(instance at line 453) line 453
60. instance OAI.RecursivePotentials.TreeVector.(instance at line 455) line 455
61. instance OAI.RecursivePotentials.TreeVector.(instance at line 457) line 457
62. instance OAI.RecursivePotentials.TreeVector.(instance at line 459) line 459
63. theorem OAI.RecursivePotentials.TreeVector.normCore line 461
64. instance OAI.RecursivePotentials.TreeVector.(instance at line 470) line 470
65. instance OAI.RecursivePotentials.TreeVector.(instance at line 473) line 473
66. def OAI.RecursivePotentials.TreeVector.coordinateLinear line 475
67. def OAI.RecursivePotentials.TreeVector.coordinate line 480
68. def OAI.RecursivePotentials.TreeVector.projectionLinear line 486
69. def OAI.RecursivePotentials.TreeVector.projection line 501
70. lemma OAI.RecursivePotentials.TreeVector.projection_contracts line 508
71. abbrev OAI.RecursivePotentials.TreeSpace line 513
72. def OAI.RecursivePotentials.TreeSpace.coordinate line 522
73. def OAI.RecursivePotentials.TreeSpace.P line 524
74. def OAI.RecursivePotentials.TreeSpace.Q line 527
75. def OAI.RecursivePotentials.TreeSpace.projection line 530
76. def OAI.RecursivePotentials.TreeSpace.tail line 533
77. abbrev OAI.RecursivePotentials.XSigma line 538
78. abbrev OAI.RecursivePotentials.XJoined line 540
79. lemma OAI.RecursivePotentials.TreeVector.coordinate_projection line 546
80. def OAI.RecursivePotentials.ZeroTreeVector line 552
81. instance OAI.RecursivePotentials.ZeroTreeVector.(instance at line 559) line 559
82. instance OAI.RecursivePotentials.ZeroTreeVector.(instance at line 562) line 562
83. def OAI.RecursivePotentials.ZeroTreeVector.toTree line 565
84. lemma OAI.RecursivePotentials.ZeroTreeVector.toTree_injective line 568
85. lemma OAI.RecursivePotentials.ZeroTreeVector.root_zero line 570
86. instance OAI.RecursivePotentials.ZeroTreeVector.(instance at line 572) line 572
87. lemma OAI.RecursivePotentials.ZeroTreeVector.norm_half line 574
88. lemma OAI.RecursivePotentials.ZeroTreeVector.normCore line 581
89. instance OAI.RecursivePotentials.ZeroTreeVector.(instance at line 593) line 593
90. instance OAI.RecursivePotentials.ZeroTreeVector.(instance at line 595) line 595
91. def OAI.RecursivePotentials.ZeroTreeVector.inclusion line 597
92. def OAI.RecursivePotentials.ZeroTreeVector.projectionLinear line 600
93. def OAI.RecursivePotentials.ZeroTreeVector.projection line 606
94. abbrev OAI.RecursivePotentials.ZeroTreeSpace line 614
95. def OAI.RecursivePotentials.ZeroTreeSpace.inclusion line 623
96. def OAI.RecursivePotentials.ZeroTreeSpace.projection line 625
97. def OAI.RecursivePotentials.ZeroTreeSpace.tail line 628
98. abbrev OAI.RecursivePotentials.XZero line 633
99. def OAI.RecursivePotentials.ZeroTreeSpace.coordinate line 641
100. def OAI.RecursivePotentials.ZeroTreeSpace.P line 644
101. def OAI.RecursivePotentials.ZeroTreeSpace.Q line 646
102. abbrev OAI.RecursivePotentials.SquareSum.DualFamily line 661
103. def OAI.RecursivePotentials.SquareSum.pairing line 663
104. def OAI.RecursivePotentials.TreeVector.toSquareLinear line 677
105. lemma OAI.RecursivePotentials.ChildExponent.pos line 690
106. lemma OAI.RecursivePotentials.ChildExponent.ne_zero line 692
107. lemma OAI.RecursivePotentials.ChildExponent.inv_pos line 694
108. lemma OAI.RecursivePotentials.ChildExponent.agg_nonneg line 696
109. lemma OAI.RecursivePotentials.ChildExponent.agg_rpow line 699
110. lemma OAI.RecursivePotentials.ChildExponent.agg_mono line 704
111. lemma OAI.RecursivePotentials.ChildExponent.agg_mono_nonneg line 710
112. lemma OAI.RecursivePotentials.ChildExponent.agg_add_le line 714
113. lemma OAI.RecursivePotentials.ChildExponent.agg_zero line 717
114. lemma OAI.RecursivePotentials.ChildExponent.agg_empty line 720
115. lemma OAI.RecursivePotentials.ChildExponent.agg_smul line 723
116. lemma OAI.RecursivePotentials.ChildExponent.coordinate_le_agg line 730
117. lemma OAI.RecursivePotentials.ChildExponent.agg_subset line 736
118. lemma OAI.RecursivePotentials.ChildExponent.agg_congr line 742
119. def OAI.RecursivePotentials.FiniteRootedTree.PUpper line 755
120. lemma OAI.RecursivePotentials.FiniteRootedTree.pfields_eq line 757
121. lemma OAI.RecursivePotentials.FiniteRootedTree.pfields_nonneg line 766
122. lemma OAI.RecursivePotentials.FiniteRootedTree.pfields_difference line 771
123. lemma OAI.RecursivePotentials.FiniteRootedTree.pfields_upper line 775
124. theorem OAI.RecursivePotentials.FiniteRootedTree.pfields_minimal line 779
125. def OAI.RecursivePotentials.FiniteRootedTree.pRootSum line 791
126. lemma OAI.RecursivePotentials.FiniteRootedTree.pRootSum_nonneg line 793
127. lemma OAI.RecursivePotentials.VariableExponent.heightExponent_gt_one line 800
128. lemma OAI.RecursivePotentials.FiniteRootedTree.depth_eq_zero_iff line 811
129. def OAI.RecursivePotentials.FiniteRootedTree.headLevel line 818
130. def OAI.RecursivePotentials.FiniteRootedTree.childrenOf line 820
131. lemma OAI.RecursivePotentials.FiniteRootedTree.sum_children_on line 822
132. def OAI.RecursivePotentials.VariableTree.GlobalUpper line 843
133. lemma OAI.RecursivePotentials.VariableTree.GlobalUpper.restrict line 846
134. lemma OAI.RecursivePotentials.VariableTree.extend_upper line 856
135. lemma OAI.RecursivePotentials.VariableTree.GlobalUpper.add line 891
136. lemma OAI.RecursivePotentials.VariableTree.GlobalUpper.smul line 897
137. lemma OAI.RecursivePotentials.VariableTree.GlobalUpper.le_root line 905
138. def OAI.RecursivePotentials.VariableTree.P line 915
139. def OAI.RecursivePotentials.VariableTree.Q line 919
140. lemma OAI.RecursivePotentials.VariableTree.P_nonneg line 923
141. lemma OAI.RecursivePotentials.VariableTree.Q_nonneg line 926
142. lemma OAI.RecursivePotentials.VariableTree.P_upper line 929
143. lemma OAI.RecursivePotentials.VariableTree.Q_upper line 932
144. lemma OAI.RecursivePotentials.VariableTree.P_sub_Q line 935
145. lemma OAI.RecursivePotentials.VariableTree.potentials_minimal line 941
146. theorem OAI.RecursivePotentials.VariableTree.potentials_on_head line 953
147. def OAI.RecursivePotentials.VariableTree.normSum line 979
148. lemma OAI.RecursivePotentials.VariableTree.normSum_on_head line 981
149. lemma OAI.RecursivePotentials.VariableTree.potentials_zero line 986
150. lemma OAI.RecursivePotentials.VariableTree.potentials_add_le line 992
151. lemma OAI.RecursivePotentials.VariableTree.potentials_neg line 1004
152. lemma OAI.RecursivePotentials.VariableTree.potentials_smul_le line 1016
153. lemma OAI.RecursivePotentials.VariableTree.potentials_smul_nonneg line 1026
154. lemma OAI.RecursivePotentials.VariableTree.normSum_nonneg line 1039
155. lemma OAI.RecursivePotentials.VariableTree.normSum_zero line 1042
156. lemma OAI.RecursivePotentials.VariableTree.normSum_neg line 1046
157. lemma OAI.RecursivePotentials.VariableTree.normSum_add_le line 1050
158. lemma OAI.RecursivePotentials.VariableTree.normSum_smul_nonneg line 1055
159. lemma OAI.RecursivePotentials.VariableTree.normSum_smul line 1061
160. lemma OAI.RecursivePotentials.VariableTree.abs_coordinate_le_normSum line 1067
161. lemma OAI.RecursivePotentials.VariableTree.normSum_eq_zero_iff line 1078
162. def OAI.RecursivePotentials.AggregationVector line 1090
163. instance OAI.RecursivePotentials.AggregationVector.(instance at line 1097) line 1097
164. instance OAI.RecursivePotentials.AggregationVector.(instance at line 1099) line 1099
165. instance OAI.RecursivePotentials.AggregationVector.(instance at line 1101) line 1101
166. instance OAI.RecursivePotentials.AggregationVector.(instance at line 1103) line 1103
167. theorem OAI.RecursivePotentials.AggregationVector.normCore line 1105
168. instance OAI.RecursivePotentials.AggregationVector.(instance at line 1114) line 1114
169. instance OAI.RecursivePotentials.AggregationVector.(instance at line 1117) line 1117
170. def OAI.RecursivePotentials.AggregationVector.coordinateLinear line 1119
171. def OAI.RecursivePotentials.AggregationVector.coordinate line 1124
172. abbrev OAI.RecursivePotentials.AggregationSpace line 1132
173. def OAI.RecursivePotentials.AggregationSpace.coordinate line 1143
174. def OAI.RecursivePotentials.AggregationSpace.P line 1146
175. def OAI.RecursivePotentials.AggregationSpace.Q line 1149
176. def OAI.RecursivePotentials.AggregationVector.basisVector line 1159
177. lemma OAI.RecursivePotentials.FiniteRootedTree.level_zero line 1170
178. lemma OAI.RecursivePotentials.FiniteRootedTree.level_succ line 1176
179. lemma OAI.RecursivePotentials.FiniteRootedTree.agg_children_level line 1188
180. lemma OAI.RecursivePotentials.FiniteRootedTree.agg_level_zero line 1196
181. lemma OAI.RecursivePotentials.FiniteRootedTree.PUpper.level_le_root line 1202
182. def OAI.RecursivePotentials.FiniteRootedTree.pMaximum line 1210
183. lemma OAI.RecursivePotentials.FiniteRootedTree.pMaximum_nonneg line 1212
184. lemma OAI.RecursivePotentials.FiniteRootedTree.pMaximum_bound line 1215
185. lemma OAI.RecursivePotentials.FiniteRootedTree.pMaximum_level line 1229
186. lemma OAI.RecursivePotentials.FiniteRootedTree.pMaximum_level_sum line 1242
187. lemma OAI.RecursivePotentials.FiniteRootedTree.level_empty line 1252
188. lemma OAI.RecursivePotentials.FiniteRootedTree.sum_level_rpow line 1259
189. lemma OAI.RecursivePotentials.FiniteRootedTree.pRootSum_upper_comparison line 1276
190. lemma OAI.RecursivePotentials.FiniteRootedTree.pRootSum_level_lower line 1298
191. lemma OAI.RecursivePotentials.FiniteRootedTree.pRootSum_lower_comparison line 1314
192. instance OAI.RecursivePotentials.ChildExponent.(instance at line 1333) line 1333
193. abbrev OAI.RecursivePotentials.AggregationVector.CoordinateLp line 1345
194. def OAI.RecursivePotentials.AggregationVector.toLpLinear line 1347
195. lemma OAI.RecursivePotentials.AggregationVector.toLpLinear_norm_rpow line 1350
196. lemma OAI.RecursivePotentials.AggregationVector.toLpLinear_single line 1358
197. lemma OAI.RecursivePotentials.AggregationVector.lp_comparisons line 1364
198. def OAI.RecursivePotentials.AggregationVector.toLp line 1388
199. lemma OAI.RecursivePotentials.AggregationVector.toLp_dense line 1394
200. def OAI.RecursivePotentials.AggregationSpace.lpEquiv line 1418
201. def OAI.RecursivePotentials.Variable.exponent line 1432
202. abbrev OAI.RecursivePotentials.Variable.Component line 1434
203. abbrev OAI.RecursivePotentials.Variable.Xv line 1436
204. abbrev OAI.RecursivePotentials.Variable.Node line 1438
205. lemma OAI.RecursivePotentials.Variable.component_step line 1440
206. lemma OAI.RecursivePotentials.Variable.component_height line 1447
207. def OAI.RecursivePotentials.Variable.componentEquiv line 1449
208. def OAI.RecursivePotentials.Variable.componentCoordinate line 1454
209. def OAI.RecursivePotentials.Variable.coordinate line 1457
210. def OAI.RecursivePotentials.Variable.basis line 1460
211. def OAI.RecursivePotentials.Variable.FiniteTotalSupport line 1463
212. def OAI.RecursivePotentials.Variable.projection line 1465
213. def OAI.RecursivePotentials.Variable.AdmissibleHeads line 1467
214. def OAI.RecursivePotentials.Variable.weakTailConstant line 1472
215. def OAI.RecursivePotentials.Variable.theta line 1474
216. structure OAI.RecursivePotentials.RootSumCompletionStatement line 1478
217. structure OAI.RecursivePotentials.ZeroRootCompletionStatement line 1499
218. def OAI.RecursivePotentials.Variable.nu line 1527
219. structure OAI.RecursivePotentials.Variable.SourceNormStatement line 1531
220. def OAI.RecursivePotentials.Variable.aggregateChildren line 1539
221. def OAI.RecursivePotentials.Variable.lpPotentials line 1543