OAI/NumberTheory/PrimePackets/PacketAlgebra.lean

GitHub source file

251 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.PrimeDegreePackets.G line 11

   Also declared: ComparatorChallenges/DukePrimeDegree.lean:11 (same declaration text).

2. def OAI.PrimeDegreePackets.integralGroup line 14

   Also declared: ComparatorChallenges/DukePrimeDegree.lean:13 (same declaration text).

3. abbrev OAI.PrimeDegreePackets.X line 18

   Also declared: ComparatorChallenges/DukePrimeDegree.lean:16 (same declaration text).

4. instance OAI.PrimeDegreePackets.xMeasurableSpace line 20

   Also declared: ComparatorChallenges/DukePrimeDegree.lean:18 (same declaration text).

5. instance OAI.PrimeDegreePackets.xBorelSpace line 21

   Also declared: ComparatorChallenges/DukePrimeDegree.lean:19 (same declaration text).

6. def OAI.PrimeDegreePackets.rightAction line 24

   Also declared: ComparatorChallenges/DukePrimeDegree.lean:21 (same declaration text).

7. theorem OAI.PrimeDegreePackets.rightAction_one line 32

   Also declared: ComparatorChallenges/DukePrimeDegree.lean:29 (same declaration text).

8. theorem OAI.PrimeDegreePackets.rightAction_mul line 36

   Also declared: ComparatorChallenges/DukePrimeDegree.lean:33 (same declaration text).

9. def OAI.PrimeDegreePackets.LogHyperplane line 43
10. def OAI.PrimeDegreePackets.positiveDiagonal line 46
11. def OAI.PrimeDegreePackets.signMatrices line 50

    Also declared: ComparatorChallenges/DukePrimeDegree.lean:38 (same declaration text).

12. def OAI.PrimeDegreePackets.rowLattice line 54

    Also declared: ComparatorChallenges/DukePrimeDegree.lean:41 (same declaration text).

13. structure OAI.PrimeDegreePackets.FullLattice line 59

    Also declared: ComparatorChallenges/DukePrimeDegree.lean:44 (same declaration text).

14. def OAI.PrimeDegreePackets.multiplierOrder line 65

    Also declared: ComparatorChallenges/DukePrimeDegree.lean:49 (same declaration text).

15. def OAI.PrimeDegreePackets.integralElements line 76

    Also declared: ComparatorChallenges/DukePrimeDegree.lean:59 (same declaration text).

16. def OAI.PrimeDegreePackets.multiplierDiscriminant line 80

    Also declared: ComparatorChallenges/DukePrimeDegree.lean:62 (same declaration text).

17. abbrev OAI.PrimeDegreePackets.OrderedEmbeddings line 86

    Also declared: ComparatorChallenges/DukePrimeDegree.lean:67 (same declaration text).

18. def OAI.PrimeDegreePackets.embeddingMatrix line 89

    Also declared: ComparatorChallenges/DukePrimeDegree.lean:69 (same declaration text).

19. def OAI.PrimeDegreePackets.normalizedLattice line 94

    Also declared: ComparatorChallenges/DukePrimeDegree.lean:73 (same declaration text).

20. def OAI.PrimeDegreePackets.latticePoint line 101

    Also declared: ComparatorChallenges/DukePrimeDegree.lean:78 (same declaration text).

21. abbrev OAI.PrimeDegreePackets.LogCoordinates line 108

    Also declared: ComparatorChallenges/DukePrimeDegree.lean:84 (same declaration text).

22. def OAI.PrimeDegreePackets.diagonalFlow line 111

    Also declared: ComparatorChallenges/DukePrimeDegree.lean:86 (same declaration text).

23. theorem OAI.PrimeDegreePackets.diagonalFlow_zero line 117

    Also declared: ComparatorChallenges/DukePrimeDegree.lean:92 (same declaration text).

24. theorem OAI.PrimeDegreePackets.diagonalFlow_add line 124

    Also declared: ComparatorChallenges/DukePrimeDegree.lean:99 (same declaration text).

25. def OAI.PrimeDegreePackets.orbitMap line 136

    Also declared: ComparatorChallenges/DukePrimeDegree.lean:110 (same declaration text).

26. theorem OAI.PrimeDegreePackets.orbitMap_zero line 139

    Also declared: ComparatorChallenges/DukePrimeDegree.lean:113 (same declaration text).

27. theorem OAI.PrimeDegreePackets.orbitMap_add line 142

    Also declared: ComparatorChallenges/DukePrimeDegree.lean:116 (same declaration text).

28. def OAI.PrimeDegreePackets.periodGroup line 147

    Also declared: ComparatorChallenges/DukePrimeDegree.lean:120 (same declaration text).

29. def OAI.PrimeDegreePackets.diagonalOrbit line 161

    Also declared: ComparatorChallenges/DukePrimeDegree.lean:133 (same declaration text).

30. def OAI.PrimeDegreePackets.orbitVolume line 164

    Also declared: ComparatorChallenges/DukePrimeDegree.lean:135 (same declaration text).

31. def OAI.PrimeDegreePackets.orbitalHaar line 169

    Also declared: ComparatorChallenges/DukePrimeDegree.lean:138 (same declaration text).

32. def OAI.PrimeDegreePackets.orbitProbability line 175

    Also declared: ComparatorChallenges/DukePrimeDegree.lean:143 (same declaration text).

33. abbrev OAI.PrimeDegreePackets.LocalAlgebra line 179

    Also declared: ComparatorChallenges/DukePrimeDegree.lean:146 (same declaration text).

34. def OAI.PrimeDegreePackets.completedLattice line 183

    Also declared: ComparatorChallenges/DukePrimeDegree.lean:149 (same declaration text).

35. def OAI.PrimeDegreePackets.LocallyHomothetic line 190

    Also declared: ComparatorChallenges/DukePrimeDegree.lean:155 (same declaration text).

36. def OAI.PrimeDegreePackets.packetOrbits line 199

    Also declared: ComparatorChallenges/DukePrimeDegree.lean:162 (same declaration text).

37. def OAI.PrimeDegreePackets.orbitBasepoint line 207

    Also declared: ComparatorChallenges/DukePrimeDegree.lean:168 (same declaration text).

38. def OAI.PrimeDegreePackets.packetMeasure line 214

    Also declared: ComparatorChallenges/DukePrimeDegree.lean:173 (same declaration text).

39. def OAI.PrimeDegreePackets.IsHaarProbability line 221

    Also declared: ComparatorChallenges/DukePrimeDegree.lean:179 (same declaration text).

40. def OAI.PrimeDegreePackets.WeakProbabilityConvergence line 226

    Also declared: ComparatorChallenges/DukePrimeDegree.lean:182 (same declaration text).

41. lemma OAI.PrimeDegreePackets.fullLattice_span_basis line 238
42. lemma OAI.PrimeDegreePackets.fullLattice_rat_span_basis line 245
43. def OAI.PrimeDegreePackets.fullLatticeRatBasis line 252
44. lemma OAI.PrimeDegreePackets.fullLatticeRatBasis_apply line 257
45. lemma OAI.PrimeDegreePackets.completedLattice_eq_span_basis line 262
46. lemma OAI.PrimeDegreePackets.completedLattice_basis_independent line 289
47. def OAI.PrimeDegreePackets.completedLatticeBasis line 302
48. lemma OAI.PrimeDegreePackets.completedLatticeBasis_coe line 308
49. def OAI.PrimeDegreePackets.completedReduction line 318
50. lemma OAI.PrimeDegreePackets.completedReduction_surjective line 326
51. lemma OAI.PrimeDegreePackets.completedReduction_eq_zero_iff line 340
52. theorem OAI.PrimeDegreePackets.completedReduction_index line 365
53. def OAI.PrimeDegreePackets.completionEmbedding line 374
54. lemma OAI.PrimeDegreePackets.completionEmbedding_basis line 387
55. lemma OAI.PrimeDegreePackets.completionEmbedding_coordinates line 394
56. theorem OAI.PrimeDegreePackets.completedReduction_global_surjective line 407
57. theorem OAI.PrimeDegreePackets.completedReduction_simultaneous_surjective line 423
58. theorem OAI.PrimeDegreePackets.exists_fullLattice_of_between line 457
59. def OAI.PrimeDegreePackets.residueConditions line 490
60. lemma OAI.PrimeDegreePackets.smul_mem_residueConditions line 505
61. theorem OAI.PrimeDegreePackets.exists_fullLattice_residueConditions line 529
62. theorem OAI.PrimeDegreePackets.residueConditions_surjective line 565
63. lemma OAI.PrimeDegreePackets.completedReduction_mem_image_iff line 579
64. lemma OAI.PrimeDegreePackets.completedLattice_mono line 597
65. lemma OAI.PrimeDegreePackets.completedLattice_smul_mem line 605
66. lemma OAI.PrimeDegreePackets.completedLattice_primePower_mem line 629
67. lemma OAI.PrimeDegreePackets.prime_coprime_other_factors line 646
68. theorem OAI.PrimeDegreePackets.patch_fullLattice_completions line 657
69. lemma OAI.PrimeDegreePackets.rat_integral_of_padic_integral line 742
70. lemma OAI.PrimeDegreePackets.fullLatticeRatBasis_repr_integral line 761
71. lemma OAI.PrimeDegreePackets.completedLattice_coordinate_integral line 786
72. theorem OAI.PrimeDegreePackets.mem_fullLattice_iff_forall_completed line 815
73. theorem OAI.PrimeDegreePackets.fullLattice_carrier_eq_of_completions_eq line 847
74. theorem OAI.PrimeDegreePackets.patch_fullLattice_completions_unique line 858
75. def OAI.PrimeDegreePackets.completedFractionalIdeal line 890
76. lemma OAI.PrimeDegreePackets.completedFractionalIdeal_mono line 896
77. lemma OAI.PrimeDegreePackets.completedFractionalIdeal_fg line 901
78. lemma OAI.PrimeDegreePackets.completedFractionalIdeal_add line 936
79. lemma OAI.PrimeDegreePackets.completedFractionalIdeal_zero line 950
80. lemma OAI.PrimeDegreePackets.completedFractionalIdeal_ne_bot line 958
81. lemma OAI.PrimeDegreePackets.completedFractionalIdeal_singleton_mul line 974
82. lemma OAI.PrimeDegreePackets.completedFractionalIdeal_nat_mul line 993
83. theorem OAI.PrimeDegreePackets.completedFractionalIdeal_principal line 1004
84. lemma OAI.PrimeDegreePackets.completedFractionalIdeal_mul_mem line 1042
85. lemma OAI.PrimeDegreePackets.completedFractionalIdeal_mul line 1069
86. def OAI.PrimeDegreePackets.completedMaximalOrder line 1087
87. lemma OAI.PrimeDegreePackets.completedMaximalOrder_toSubmodule line 1102
88. theorem OAI.PrimeDegreePackets.completedMaximalOrder_unit_of_smul_eq line 1107
89. def OAI.PrimeDegreePackets.saturationFractionalIdeal line 1128
90. lemma OAI.PrimeDegreePackets.saturationFractionalIdeal_ne_zero line 1134
91. def OAI.PrimeDegreePackets.fractionalIdealFullLattice line 1146
92. lemma OAI.PrimeDegreePackets.completedLattice_fractionalIdealFullLattice line 1158
93. theorem OAI.PrimeDegreePackets.completed_saturation line 1165
94. theorem OAI.PrimeDegreePackets.fractionalIdeal_eq_of_completions_eq line 1229
95. lemma OAI.PrimeDegreePackets.completedMaximalOrder_unit_smul line 1241
96. lemma OAI.PrimeDegreePackets.local_saturation_homothety line 1260
97. theorem OAI.PrimeDegreePackets.local_scalar_choice line 1270
98. def OAI.PrimeDegreePackets.saturation line 1304
99. lemma OAI.PrimeDegreePackets.le_saturation line 1308
100. lemma OAI.PrimeDegreePackets.saturation_fg line 1313
101. lemma OAI.PrimeDegreePackets.fullLattice_clear_denominator line 1321
102. def OAI.PrimeDegreePackets.saturationIndex line 1332
103. lemma OAI.PrimeDegreePackets.saturationIndex_ne_zero line 1335
104. lemma OAI.PrimeDegreePackets.saturationIndex_smul_mem line 1354
105. lemma OAI.PrimeDegreePackets.exists_idealLocalGenerator line 1361
106. def OAI.PrimeDegreePackets.idealLocalGenerator line 1377
107. lemma OAI.PrimeDegreePackets.idealLocalGenerator_spec line 1381
108. def OAI.PrimeDegreePackets.saturationIdealUnit line 1389
109. lemma OAI.PrimeDegreePackets.saturationLocalGenerator_spec line 1393
110. lemma OAI.PrimeDegreePackets.local_smul_mono line 1400
111. def OAI.PrimeDegreePackets.normalizedLocalModule line 1409
112. lemma OAI.PrimeDegreePackets.normalizedLocalModule_le line 1415
113. lemma OAI.PrimeDegreePackets.normalizedLocalModule_saturation line 1425
114. lemma OAI.PrimeDegreePackets.normalizedLocalModule_saturationIndex_mem line 1432
115. def OAI.PrimeDegreePackets.localModuleChoices line 1453
116. lemma OAI.PrimeDegreePackets.localModuleChoices_nonempty line 1460
117. lemma OAI.PrimeDegreePackets.localModuleChoices_le line 1465
118. lemma OAI.PrimeDegreePackets.localModuleChoices_saturation line 1479
119. lemma OAI.PrimeDegreePackets.localModuleChoices_saturationIndex_mem line 1489
120. lemma OAI.PrimeDegreePackets.localModuleChoices_primePower_mem line 1518
121. lemma OAI.PrimeDegreePackets.localModuleChoices_eq_off line 1539
122. theorem OAI.PrimeDegreePackets.finite_completedModule_interval line 1553
123. theorem OAI.PrimeDegreePackets.localModuleChoices_finite line 1578
124. lemma OAI.PrimeDegreePackets.localModuleChoices_transport line 1589
125. def OAI.PrimeDegreePackets.localModuleChoicesEquiv line 1602
126. lemma OAI.PrimeDegreePackets.localModuleChoices_homothety line 1617
127. lemma OAI.PrimeDegreePackets.completedLattice_mem_localModuleChoices line 1629
128. abbrev OAI.PrimeDegreePackets.labelPrimes line 1647
129. instance OAI.PrimeDegreePackets.labelPrime_fact line 1650
130. theorem OAI.PrimeDegreePackets.patch_localModuleChoices line 1656
131. def OAI.PrimeDegreePackets.globalLabels line 1701
132. def OAI.PrimeDegreePackets.globalLabelLattice line 1706
133. lemma OAI.PrimeDegreePackets.globalLabelLattice_spec line 1710
134. def OAI.PrimeDegreePackets.globalLabelCompletions line 1717
135. lemma OAI.PrimeDegreePackets.globalLabelCompletions_injective line 1724
136. lemma OAI.PrimeDegreePackets.globalLabelCompletions_surjective line 1744
137. def OAI.PrimeDegreePackets.globalLabelEquiv line 1761
138. theorem OAI.PrimeDegreePackets.globalLabels_finite line 1768
139. def OAI.PrimeDegreePackets.globalLabelsEquiv line 1776
140. theorem OAI.PrimeDegreePackets.globalLabels_ncard_eq line 1784
141. abbrev OAI.PrimeDegreePackets.localLatticeQuotient line 1790
142. def OAI.PrimeDegreePackets.localLatticeQuotientMap line 1795
143. theorem OAI.PrimeDegreePackets.localLatticeQuotientMap_simultaneous_surjective line 1804
144. theorem OAI.PrimeDegreePackets.fullLattice_relIndex_eq_prod_local line 1832
145. lemma OAI.PrimeDegreePackets.local_relIndex_smul line 1868
146. lemma OAI.PrimeDegreePackets.saturation_completed_primePower_mem line 1875
147. lemma OAI.PrimeDegreePackets.saturation_completed_eq_off line 1888
148. theorem OAI.PrimeDegreePackets.saturationIndex_eq_prod_local line 1901
149. theorem OAI.PrimeDegreePackets.saturationIndex_eq_of_locallyHomothetic line 1919
150. theorem OAI.PrimeDegreePackets.globalLabel_relIndex line 1970
151. lemma OAI.PrimeDegreePackets.globalLabel_contains_iff line 1986
152. def OAI.PrimeDegreePackets.localContainmentLabels line 2010
153. def OAI.PrimeDegreePackets.globalContainmentEquiv line 2016
154. theorem OAI.PrimeDegreePackets.globalLabels_card_prod line 2032
155. theorem OAI.PrimeDegreePackets.globalLabels_card_pos line 2039
156. def OAI.PrimeDegreePackets.localContainmentProbability line 2053
157. theorem OAI.PrimeDegreePackets.globalContainmentProbability_eq_prod line 2060
158. instance OAI.PrimeDegreePackets.(instance at line 2073) line 2073
159. instance OAI.PrimeDegreePackets.(instance at line 2075) line 2075
160. instance OAI.PrimeDegreePackets.(instance at line 2077) line 2077
161. instance OAI.PrimeDegreePackets.(instance at line 2079) line 2079
162. def OAI.PrimeDegreePackets.localAlgebraCoordinates line 2081
163. instance OAI.PrimeDegreePackets.(instance at line 2087) line 2087
164. instance OAI.PrimeDegreePackets.(instance at line 2089) line 2089
165. def OAI.PrimeDegreePackets.localIntegralSpan line 2093
166. lemma OAI.PrimeDegreePackets.localIntegralSpan_mem line 2097
167. lemma OAI.PrimeDegreePackets.localIntegralSpan_compact line 2136
168. lemma OAI.PrimeDegreePackets.localIntegralSpan_open line 2155
169. theorem OAI.PrimeDegreePackets.isClosed_unit_smul_submodule_eq line 2172
170. lemma OAI.PrimeDegreePackets.completedLattice_compact line 2215
171. lemma OAI.PrimeDegreePackets.completedLattice_open line 2221
172. instance OAI.PrimeDegreePackets.completedMaximalOrderCompactSpace line 2227
173. example OAI.PrimeDegreePackets.(example at line 2232) line 2232
174. instance OAI.PrimeDegreePackets.localUnitsMeasurableSpace line 2235
175. instance OAI.PrimeDegreePackets.localUnitsBorelSpace line 2237
176. lemma OAI.PrimeDegreePackets.compact_smul_submodule line 2240
177. lemma OAI.PrimeDegreePackets.normalizedLocalModule_compact line 2249
178. lemma OAI.PrimeDegreePackets.localModuleChoices_compact line 2254
179. lemma OAI.PrimeDegreePackets.localModule_denominator line 2265
180. def OAI.PrimeDegreePackets.scaleFullLattice line 2296
181. lemma OAI.PrimeDegreePackets.scaleFullLattice_basis line 2307
182. lemma OAI.PrimeDegreePackets.scaleFullLattice_carrier line 2311
183. lemma OAI.PrimeDegreePackets.completedLattice_scale line 2315
184. lemma OAI.PrimeDegreePackets.completedLattice_scale_rat line 2327
185. lemma OAI.PrimeDegreePackets.patch_localOvermodule line 2342
186. theorem OAI.PrimeDegreePackets.completedMaximalOrder_maximal_finite line 2398
187. theorem OAI.PrimeDegreePackets.mem_completedMaximalOrder_iff_isIntegral line 2453
188. theorem OAI.PrimeDegreePackets.completedMaximalOrder_eq_integralClosure line 2473
189. theorem OAI.PrimeDegreePackets.isIntegral_padicInt_iff_spectralNorm_le_one line 2483
190. lemma OAI.PrimeDegreePackets.compactSpace_norm_integer line 2527
191. lemma OAI.PrimeDegreePackets.dvr_norm_integer line 2535
192. lemma OAI.PrimeDegreePackets.finite_residue_norm_integer line 2541
193. def OAI.PrimeDegreePackets.integralClosureEquivInteger line 2554
194. lemma OAI.PrimeDegreePackets.compactSpace_integralClosure_padic line 2565
195. theorem OAI.PrimeDegreePackets.integralClosure_padicInt_isDiscreteValuationRing line 2581
196. instance OAI.PrimeDegreePackets.integralClosure_padicInt_dvr line 2594
197. instance OAI.PrimeDegreePackets.integralClosure_padicInt_finite_residue line 2601
198. lemma OAI.PrimeDegreePackets.isIntegral_pi_iff line 2618
199. def OAI.PrimeDegreePackets.integralClosurePiEquiv line 2635
200. def OAI.PrimeDegreePackets.integralClosureEquiv line 2647
201. lemma OAI.PrimeDegreePackets.localAlgebra_etale line 2659
202. theorem OAI.PrimeDegreePackets.localAlgebra_exists_product line 2667
203. lemma OAI.PrimeDegreePackets.cardQuot_span_prime_of_free line 2686
204. theorem OAI.PrimeDegreePackets.finite_padic_dvr_degree line 2734
205. theorem OAI.PrimeDegreePackets.completedMaximalOrder_exists_dvr_product line 2783
206. def OAI.PrimeDegreePackets.completedLocalIntegralEquiv line 2802
207. lemma OAI.PrimeDegreePackets.continuous_completedLocalIntegralEquiv line 2813
208. lemma OAI.PrimeDegreePackets.continuous_completedLocalIntegralEquiv_symm line 2825
209. instance OAI.PrimeDegreePackets.completedMaximalOrderModuleFinite line 2838
210. lemma OAI.PrimeDegreePackets.completedMaximalOrder_finrank line 2843
211. theorem OAI.PrimeDegreePackets.completedMaximalOrder_exists_topological_dvr_product line 2859
212. theorem OAI.PrimeDegreePackets.completedMaximalOrder_exists_full_local_model line 2910
213. lemma OAI.PrimeDegreePackets.ideal_span_comap_top_of_mul line 2940
214. lemma OAI.PrimeDegreePackets.ideal_span_map_equiv_top line 2957
215. lemma OAI.PrimeDegreePackets.cardQuot_map_equiv line 2965
216. def OAI.PrimeDegreePackets.integralNormalizedModule line 2971
217. lemma OAI.PrimeDegreePackets.integralNormalizedModule_saturated line 2976
218. lemma OAI.PrimeDegreePackets.integralNormalizedModule_open line 2982
219. lemma OAI.PrimeDegreePackets.integralNormalizedModule_finiteQuotient line 2991
220. lemma OAI.PrimeDegreePackets.integralNormalizedModule_cardQuot line 2997
221. lemma OAI.PrimeDegreePackets.saturationIndex_eq_prod_integralNormalizedModule line 3010
222. def OAI.PrimeDegreePackets.modelLocalModule line 3020
223. lemma OAI.PrimeDegreePackets.modelLocalModule_saturated line 3026
224. lemma OAI.PrimeDegreePackets.modelLocalModule_open line 3033
225. lemma OAI.PrimeDegreePackets.modelLocalModule_finiteQuotient line 3041
226. lemma OAI.PrimeDegreePackets.modelLocalModule_cardQuot line 3049
227. theorem OAI.PrimeDegreePackets.haar_stabilizer_eq_inv_card line 3059
228. theorem OAI.PrimeDegreePackets.haar_orbit_fiber line 3078
229. lemma OAI.PrimeDegreePackets.measurable_orbit_fiber line 3093
230. theorem OAI.PrimeDegreePackets.haar_orbit_subset line 3107
231. def OAI.PrimeDegreePackets.localChoiceBase line 3144
232. lemma OAI.PrimeDegreePackets.localUnit_smul_base line 3149
233. lemma OAI.PrimeDegreePackets.localModuleChoices_eq_orbit line 3159
234. lemma OAI.PrimeDegreePackets.localChoiceStabilizer_measurable line 3167
235. def OAI.PrimeDegreePackets.localUnitHaarProbability line 3183
236. instance OAI.PrimeDegreePackets.localUnitHaarProbability_isProbability line 3188
237. instance OAI.PrimeDegreePackets.localUnitHaarProbability_isHaar line 3193
238. theorem OAI.PrimeDegreePackets.localUnitHaarProbability_fiber line 3199
239. theorem OAI.PrimeDegreePackets.localUnitHaarProbability_containment line 3219
240. lemma OAI.PrimeDegreePackets.haar_smul_containment line 3241
241. lemma OAI.PrimeDegreePackets.local_generators_associated line 3253
242. lemma OAI.PrimeDegreePackets.completedFractionalIdeal_generator_mul line 3268
243. def OAI.PrimeDegreePackets.localIdealWeight line 3279
244. lemma OAI.PrimeDegreePackets.localIdealWeight_eq_of_generator line 3286
245. def OAI.PrimeDegreePackets.relativeElementIdeal line 3303
246. lemma OAI.PrimeDegreePackets.relativeElementIdeal_generator line 3307
247. theorem OAI.PrimeDegreePackets.localContainment_eq_relativeIdealWeight line 3336
248. def OAI.PrimeDegreePackets.globalIdealWeight line 3364
249. lemma OAI.PrimeDegreePackets.localIdealWeight_le_one line 3368
250. lemma OAI.PrimeDegreePackets.globalIdealWeight_le_one line 3373
251. theorem OAI.PrimeDegreePackets.globalContainment_eq_relativeIdealWeight line 3380