OAI/NumberTheory/PrimePackets/ZetaResidues.lean

GitHub source file

384 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PrimeDegreePackets.realDedekindZeta line 37
2. lemma OAI.PrimeDegreePackets.tendsto_residue_from_right line 42
3. lemma OAI.PrimeDegreePackets.fixed_field_residue_comparison line 56
4. theorem OAI.PrimeDegreePackets.finite_family_residue_comparison line 70
5. theorem OAI.PrimeDegreePackets.finite_family_residue_reciprocal_bound line 78
6. lemma OAI.PrimeDegreePackets.dedekindZeta_algEquiv line 93
7. lemma OAI.PrimeDegreePackets.dedekindZeta_residue_algEquiv line 107
8. abbrev OAI.PrimeDegreePackets.BoundedRealFields line 114
9. instance OAI.PrimeDegreePackets.boundedRealFields_numberField line 119
10. instance OAI.PrimeDegreePackets.boundedRealFields_finite line 122
11. theorem OAI.PrimeDegreePackets.bounded_discr_residue_data line 127
12. theorem OAI.PrimeDegreePackets.bounded_discr_residue_comparison line 146
13. theorem OAI.PrimeDegreePackets.no_quadratic_subfield line 178
14. theorem OAI.PrimeDegreePackets.weightedIdeal_interval_bounded_discr line 196
15. lemma OAI.PrimeDegreePackets.rounded_relative_interval line 239
16. lemma OAI.PrimeDegreePackets.eventual_rounding_parameters line 253
17. def OAI.PrimeDegreePackets.weightedIdealRealInterval line 282
18. lemma OAI.PrimeDegreePackets.weightedIdealRealInterval_le_rounded line 288
19. theorem OAI.PrimeDegreePackets.weightedIdeal_realInterval_zeta_bound line 305
20. theorem OAI.PrimeDegreePackets.weightedIdeal_realInterval_bounded_discr line 341
21. theorem OAI.PrimeDegreePackets.embeddingMatrix_det_ne_zero line 373
22. lemma OAI.PrimeDegreePackets.rowLattice_neg line 392
23. lemma OAI.PrimeDegreePackets.normalizedMatrix_abs_det line 402
24. theorem OAI.PrimeDegreePackets.exists_SL_normalizedLattice line 415
25. theorem OAI.PrimeDegreePackets.multiplierOrder_le_integralElements line 433
26. lemma OAI.PrimeDegreePackets.scaled_integralElements_le_multiplierOrder line 447
27. lemma OAI.PrimeDegreePackets.integralElements_scaled_index line 459
28. theorem OAI.PrimeDegreePackets.multiplierOrder_index_le line 473
29. def OAI.PrimeDegreePackets.packetScale line 486
30. lemma OAI.PrimeDegreePackets.fieldDiscriminant_one_le line 489
31. lemma OAI.PrimeDegreePackets.packetScale_pos line 493
32. theorem OAI.PrimeDegreePackets.multiplierDiscriminant_le_packetScale_pow line 501
33. theorem OAI.PrimeDegreePackets.packetScale_tendsto_of_multiplierDiscriminant_tendsto line 522
34. def OAI.PrimeDegreePackets.integralUnit line 539
35. def OAI.PrimeDegreePackets.unitStabilizer line 544
36. def OAI.PrimeDegreePackets.unitsReduction line 559
37. lemma OAI.PrimeDegreePackets.unitsReduction_one_preserves line 564
38. lemma OAI.PrimeDegreePackets.unitsReduction_ker_le_stabilizer line 586
39. theorem OAI.PrimeDegreePackets.unitStabilizer_finiteIndex line 599
40. def OAI.PrimeDegreePackets.unitSigns line 609
41. lemma OAI.PrimeDegreePackets.unitSigns_eq_one_iff line 616
42. def OAI.PrimeDegreePackets.positiveUnitStabilizer line 625
43. lemma OAI.PrimeDegreePackets.mem_positiveUnitStabilizer line 629
44. theorem OAI.PrimeDegreePackets.positiveUnitStabilizer_finiteIndex line 638
45. def OAI.PrimeDegreePackets.logSubgroup line 654
46. lemma OAI.PrimeDegreePackets.logSubgroup_le_unitLattice line 659
47. instance OAI.PrimeDegreePackets.logSubgroup_discrete line 663
48. theorem OAI.PrimeDegreePackets.logSubgroup_span_eq_top line 672
49. instance OAI.PrimeDegreePackets.logSubgroup_isZLattice line 692
50. def OAI.PrimeDegreePackets.realPlace line 698
51. theorem OAI.PrimeDegreePackets.realPlace_apply line 701
52. lemma OAI.PrimeDegreePackets.realPlace_injective line 705
53. lemma OAI.PrimeDegreePackets.realPlace_surjective line 714
54. def OAI.PrimeDegreePackets.orderedRealPlaces line 726
55. lemma OAI.PrimeDegreePackets.orderedRealPlaces_apply line 730
56. def OAI.PrimeDegreePackets.zeroSumSubmodule line 736
57. lemma OAI.PrimeDegreePackets.mem_zeroSumSubmodule line 745
58. def OAI.PrimeDegreePackets.insertDeleted line 750
59. lemma OAI.PrimeDegreePackets.insertDeleted_self line 756
60. lemma OAI.PrimeDegreePackets.insertDeleted_ne line 760
61. lemma OAI.PrimeDegreePackets.insertDeleted_sum line 764
62. def OAI.PrimeDegreePackets.deletedCoordinatesEquiv line 771
63. def OAI.PrimeDegreePackets.zeroSumReindex line 792
64. def OAI.PrimeDegreePackets.changeDeletedCoordinates line 809
65. theorem OAI.PrimeDegreePackets.changeDeletedCoordinates_apply line 814
66. def OAI.PrimeDegreePackets.orderedLogCoordinatesEquiv line 821
67. lemma OAI.PrimeDegreePackets.insertDeleted_logEmbedding line 828
68. def OAI.PrimeDegreePackets.orderedUnitLog line 846
69. lemma OAI.PrimeDegreePackets.orderedUnitLog_apply line 851
70. def OAI.PrimeDegreePackets.orderedLogSubgroup line 862
71. lemma OAI.PrimeDegreePackets.mem_orderedLogSubgroup line 867
72. instance OAI.PrimeDegreePackets.orderedLogSubgroup_discrete line 885
73. instance OAI.PrimeDegreePackets.orderedLogSubgroup_isZLattice line 892
74. theorem OAI.PrimeDegreePackets.positiveStabilizer_fullLogLattice line 901
75. lemma OAI.PrimeDegreePackets.rowLattice_int_mul_le line 911
76. lemma OAI.PrimeDegreePackets.rowLattice_integral_mul line 924
77. lemma OAI.PrimeDegreePackets.exists_int_matrix_of_rowLattice_le line 937
78. lemma OAI.PrimeDegreePackets.exists_integral_mul_of_rowLattice_eq line 951
79. theorem OAI.PrimeDegreePackets.quotient_eq_iff_rowLattice_eq line 969
80. def OAI.PrimeDegreePackets.realEmbeddingMap line 992
81. def OAI.PrimeDegreePackets.diagonalLinear line 1000
82. lemma OAI.PrimeDegreePackets.fullLattice_exists_ne_zero line 1005
83. lemma OAI.PrimeDegreePackets.realEmbeddingMap_injective line 1012
84. theorem OAI.PrimeDegreePackets.diagonal_into_lattice_is_field_multiplication line 1019
85. theorem OAI.PrimeDegreePackets.diagonal_lattice_equality_iff_homothety line 1035
86. lemma OAI.PrimeDegreePackets.rowLattice_embeddingMatrix line 1075
87. lemma OAI.PrimeDegreePackets.rowLattice_mul_diagonal line 1081
88. lemma OAI.PrimeDegreePackets.rowLattice_smul line 1090
89. lemma OAI.PrimeDegreePackets.diagonalLinear_commute line 1096
90. lemma OAI.PrimeDegreePackets.embeddedLattice_unit_invariant line 1104
91. lemma OAI.PrimeDegreePackets.normalizedLattice_unit_invariant line 1127
92. lemma OAI.PrimeDegreePackets.sum_orderedUnitLog_full line 1136
93. lemma OAI.PrimeDegreePackets.diagonalFlow_orderedUnitLog line 1145
94. lemma OAI.PrimeDegreePackets.latticePoint_eq_of_rowLattice_eq line 1162
95. theorem OAI.PrimeDegreePackets.orderedLogSubgroup_le_periodGroup line 1173
96. lemma OAI.PrimeDegreePackets.diagonalFlow_injective line 1190
97. lemma OAI.PrimeDegreePackets.continuous_diagonalFlow line 1197
98. lemma OAI.PrimeDegreePackets.continuous_orbitMap line 1216
99. instance OAI.PrimeDegreePackets.periodGroup_discrete line 1224
100. instance OAI.PrimeDegreePackets.periodSubmodule_discrete line 1246
101. theorem OAI.PrimeDegreePackets.periodGroup_hasFundamentalDomain line 1252
102. theorem OAI.PrimeDegreePackets.orbitVolume_ne_zero_ne_top line 1262
103. lemma OAI.PrimeDegreePackets.orbitalHaar_univ line 1270
104. theorem OAI.PrimeDegreePackets.orbitProbability_isProbabilityMeasure line 1281
105. theorem OAI.PrimeDegreePackets.latticePoint_period_isZLattice line 1290
106. theorem OAI.PrimeDegreePackets.latticePoint_diagonalOrbit_isCompact line 1304
107. theorem OAI.PrimeDegreePackets.latticePoint_orbitProbability line 1317
108. lemma OAI.PrimeDegreePackets.continuous_rightAction line 1324
109. lemma OAI.PrimeDegreePackets.rightAction_injective line 1329
110. lemma OAI.PrimeDegreePackets.diagonalFlow_commute_of_diagonal line 1335
111. lemma OAI.PrimeDegreePackets.orbitMap_rightAction_of_diagonal line 1346
112. lemma OAI.PrimeDegreePackets.periodGroup_rightAction_of_diagonal line 1351
113. lemma OAI.PrimeDegreePackets.periodGroup_orbitMap line 1359
114. lemma OAI.PrimeDegreePackets.mem_diagonalOrbit_self line 1365
115. lemma OAI.PrimeDegreePackets.periodGroup_eq_of_diagonalOrbit_eq line 1368
116. lemma OAI.PrimeDegreePackets.diagonalOrbit_orbitMap line 1375
117. lemma OAI.PrimeDegreePackets.diagonalOrbit_rightAction_of_diagonal line 1384
118. lemma OAI.PrimeDegreePackets.orbitVolume_eq_of_diagonalOrbit_eq line 1395
119. lemma OAI.PrimeDegreePackets.map_orbitMap_restrict_eq line 1402
120. lemma OAI.PrimeDegreePackets.map_orbitMap_add_restrict_eq line 1420
121. theorem OAI.PrimeDegreePackets.orbitalHaar_invariant line 1440
122. theorem OAI.PrimeDegreePackets.orbitProbability_invariant line 1457
123. theorem OAI.PrimeDegreePackets.orbitalHaar_orbitMap line 1463
124. theorem OAI.PrimeDegreePackets.orbitalHaar_eq_of_diagonalOrbit_eq line 1488
125. theorem OAI.PrimeDegreePackets.orbitProbability_eq_of_diagonalOrbit_eq line 1495
126. lemma OAI.PrimeDegreePackets.locallyHomothetic_refl line 1502
127. lemma OAI.PrimeDegreePackets.one_mem_signMatrices line 1507
128. lemma OAI.PrimeDegreePackets.packetOrbits_nonempty line 1514
129. lemma OAI.PrimeDegreePackets.orbitBasepoint_spec line 1521
130. theorem OAI.PrimeDegreePackets.packetOrbit_isCompact line 1531
131. theorem OAI.PrimeDegreePackets.packetBasepoint_period_isZLattice line 1541
132. theorem OAI.PrimeDegreePackets.packetBasepoint_volume_pos_finite line 1554
133. theorem OAI.PrimeDegreePackets.packetBasepoint_probability line 1562
134. theorem OAI.PrimeDegreePackets.packetMeasure_invariant line 1572
135. lemma OAI.PrimeDegreePackets.completedLattice_mul_mem line 1580
136. theorem OAI.PrimeDegreePackets.multiplierOrder_eq_of_locallyHomothetic line 1596
137. theorem OAI.PrimeDegreePackets.uniform_saturation_denominator line 1640
138. theorem OAI.PrimeDegreePackets.finite_submodules_between line 1666
139. theorem OAI.PrimeDegreePackets.finite_packet_labels line 1699
140. theorem OAI.PrimeDegreePackets.fractionalIdeal_same_class line 1715
141. def OAI.PrimeDegreePackets.classRepresentative line 1737
142. lemma OAI.PrimeDegreePackets.classRepresentative_spec line 1742
143. theorem OAI.PrimeDegreePackets.exists_scale_to_classRepresentative line 1751
144. lemma OAI.PrimeDegreePackets.locallyHomothetic_scale line 1763
145. lemma OAI.PrimeDegreePackets.locallyHomothetic_trans line 1771
146. lemma OAI.PrimeDegreePackets.saturationFractionalIdeal_scale line 1784
147. theorem OAI.PrimeDegreePackets.exists_scale_to_representative line 1800
148. theorem OAI.PrimeDegreePackets.finite_normalized_packet_carriers line 1811
149. lemma OAI.PrimeDegreePackets.abs_det_le_of_rowLattice_le line 1831
150. lemma OAI.PrimeDegreePackets.abs_det_eq_of_rowLattice_eq line 1846
151. theorem OAI.PrimeDegreePackets.normalizedLattice_eq_of_carrier_eq line 1854
152. theorem OAI.PrimeDegreePackets.latticePoint_eq_of_carrier_eq line 1866
153. theorem OAI.PrimeDegreePackets.normalizedLattice_scale_diagonal line 1876
154. theorem OAI.PrimeDegreePackets.latticePoint_scale_diagonal line 1907
155. theorem OAI.PrimeDegreePackets.exists_diagonalFlow_of_positive line 1940
156. theorem OAI.PrimeDegreePackets.diagonal_eq_sign_mul_flow line 1960
157. theorem OAI.PrimeDegreePackets.signMatrices_finite line 1998
158. lemma OAI.PrimeDegreePackets.diagonal_inv line 2016
159. lemma OAI.PrimeDegreePackets.diagonal_mul line 2024
160. theorem OAI.PrimeDegreePackets.packetOrbits_finite line 2037
161. theorem OAI.PrimeDegreePackets.packetVolume_ne_zero_ne_top line 2072
162. theorem OAI.PrimeDegreePackets.packetMeasure_isProbabilityMeasure line 2092
163. lemma OAI.PrimeDegreePackets.normalizedLattice_diagonal_invariant_iff line 2105
164. lemma OAI.PrimeDegreePackets.exists_integralUnit_of_carrier_preserving line 2126
165. theorem OAI.PrimeDegreePackets.periodGroup_le_orderedLogSubgroup line 2142
166. theorem OAI.PrimeDegreePackets.periodGroup_eq_orderedLogSubgroup line 2188
167. lemma OAI.PrimeDegreePackets.orderedLogSubgroup_toAddSubgroup line 2197
168. lemma OAI.PrimeDegreePackets.orderedUnitLog_ker line 2209
169. theorem OAI.PrimeDegreePackets.orderedLogSubgroup_relIndex line 2220
170. theorem OAI.PrimeDegreePackets.orderedLogSubgroup_covolume_ratio line 2229
171. theorem OAI.PrimeDegreePackets.orbitVolume_latticePoint_ratio line 2244
172. lemma OAI.PrimeDegreePackets.compact_quotient_of_isZLattice line 2255
173. def OAI.PrimeDegreePackets.normalizedLatticeQuotientMeasure line 2267
174. lemma OAI.PrimeDegreePackets.map_quotient_restrict_eq line 2271
175. lemma OAI.PrimeDegreePackets.normalizedLatticeQuotientMeasure_invariant line 2296
176. lemma OAI.PrimeDegreePackets.normalizedLatticeQuotientMeasure_probability line 2319
177. theorem OAI.PrimeDegreePackets.normalizedLatticeQuotientMeasure_eq line 2335
178. theorem OAI.PrimeDegreePackets.normalized_periodic_map_eq line 2358
179. lemma OAI.PrimeDegreePackets.spanSingleton_maximalOrder_unit line 2383
180. lemma OAI.PrimeDegreePackets.scaleFullLattice_unit_carrier line 2388
181. lemma OAI.PrimeDegreePackets.globalLabels_unit_smul_mem line 2395
182. instance OAI.PrimeDegreePackets.globalLabelsMulAction line 2408
183. lemma OAI.PrimeDegreePackets.globalLabels_smul_val line 2415
184. def OAI.PrimeDegreePackets.signValue line 2419
185. lemma OAI.PrimeDegreePackets.signValue_apply line 2422
186. lemma OAI.PrimeDegreePackets.signValue_eq_one_or_neg_one line 2424
187. lemma OAI.PrimeDegreePackets.signValue_sq line 2428
188. lemma OAI.PrimeDegreePackets.signValue_pow_odd line 2431
189. def OAI.PrimeDegreePackets.positiveSignMatrix line 2436
190. lemma OAI.PrimeDegreePackets.positiveSignMatrix_one line 2442
191. lemma OAI.PrimeDegreePackets.positiveSignMatrix_mul line 2446
192. lemma OAI.PrimeDegreePackets.positiveSignMatrix_diagonal line 2456
193. lemma OAI.PrimeDegreePackets.positiveSignMatrix_entries line 2460
194. theorem OAI.PrimeDegreePackets.orbitProbability_eq_normalized_map_sublattice line 2469
195. structure OAI.PrimeDegreePackets.SignedGlobalLabel line 2488
196. lemma OAI.PrimeDegreePackets.SignedGlobalLabel.ext line 2493
197. def OAI.PrimeDegreePackets.signedGlobalLabelMulAction line 2498
198. lemma OAI.PrimeDegreePackets.unit_smul_globalLabel_eq_iff line 2518
199. theorem OAI.PrimeDegreePackets.signedGlobalLabel_stabilizer line 2552
200. theorem OAI.PrimeDegreePackets.signedGlobalLabel_finite line 2568
201. lemma OAI.PrimeDegreePackets.positiveUnitStabilizer_inf_torsion line 2575
202. theorem OAI.PrimeDegreePackets.positiveUnitStabilizer_index_eq_twice line 2595
203. lemma OAI.PrimeDegreePackets.signedGlobalLabel_orbit_volume_ratio line 2609
204. lemma OAI.PrimeDegreePackets.positiveSignMatrix_mem_signMatrices line 2624
205. lemma OAI.PrimeDegreePackets.prod_abs_ordered_unit line 2628
206. lemma OAI.PrimeDegreePackets.normalizedLattice_scale_unit line 2641
207. lemma OAI.PrimeDegreePackets.diagonalFlow_abs_orderedUnitLog line 2659
208. lemma OAI.PrimeDegreePackets.signValue_unitSigns line 2676
209. lemma OAI.PrimeDegreePackets.submodule_map_signed_correction line 2681
210. lemma OAI.PrimeDegreePackets.unitDiagonal_matrix line 2693
211. theorem OAI.PrimeDegreePackets.latticePoint_scale_unit line 2709
212. def OAI.PrimeDegreePackets.signedGlobalLabelPoint line 2726
213. lemma OAI.PrimeDegreePackets.signedGlobalLabelPoint_mem_packet line 2731
214. lemma OAI.PrimeDegreePackets.signedGlobalLabelPoint_unit_action line 2738
215. lemma OAI.PrimeDegreePackets.diagonalLinear_comp_apply line 2762
216. lemma OAI.PrimeDegreePackets.diagonalLinear_one line 2767
217. lemma OAI.PrimeDegreePackets.normalizedLattice_as_map line 2771
218. theorem OAI.PrimeDegreePackets.normalizedLattice_diagonal_homothety line 2780
219. lemma OAI.PrimeDegreePackets.latticePoint_rightAction_diagonal_homothety line 2814
220. lemma OAI.PrimeDegreePackets.saturationFractionalIdeal_eq_of_carrier_eq line 2843
221. lemma OAI.PrimeDegreePackets.exists_integralUnit_of_same_saturation line 2852
222. lemma OAI.PrimeDegreePackets.rowLattice_positiveSignMatrix line 2874
223. lemma OAI.PrimeDegreePackets.signValue_sign line 2882
224. lemma OAI.PrimeDegreePackets.signUnits_sq line 2886
225. lemma OAI.PrimeDegreePackets.signUnits_inv line 2891
226. theorem OAI.PrimeDegreePackets.signedGlobalLabel_orbit_injective line 2896
227. lemma OAI.PrimeDegreePackets.signedGlobalLabel_orbit_eq_iff line 2963
228. lemma OAI.PrimeDegreePackets.signValue_injective line 2977
229. lemma OAI.PrimeDegreePackets.exists_fullSigns_of_signMatrix line 2982
230. lemma OAI.PrimeDegreePackets.saturation_class_eq_of_signed_orbit_eq line 3004
231. abbrev OAI.PrimeDegreePackets.AllSignedGlobalLabel line 3036
232. def OAI.PrimeDegreePackets.allSignedGlobalLabelMulAction line 3040
233. lemma OAI.PrimeDegreePackets.allSignedGlobalLabel_finite line 3045
234. def OAI.PrimeDegreePackets.allSignedGlobalLabelPoint line 3050
235. def OAI.PrimeDegreePackets.allSignedGlobalLabelOrbit line 3055
236. lemma OAI.PrimeDegreePackets.allSignedGlobalLabelOrbit_unit_action line 3061
237. lemma OAI.PrimeDegreePackets.allSignedGlobalLabelOrbit_eq_iff line 3074
238. lemma OAI.PrimeDegreePackets.allSignedGlobalLabelOrbit_surjective line 3108
239. def OAI.PrimeDegreePackets.signedPacketOrbitEquiv line 3134
240. lemma OAI.PrimeDegreePackets.finite_orbitFiber_card line 3161
241. theorem OAI.PrimeDegreePackets.sum_orbits_index_nsmul line 3175
242. lemma OAI.PrimeDegreePackets.sum_orbits_index_eq_card line 3188
243. theorem OAI.PrimeDegreePackets.sum_orbits_index_smul_measure line 3196
244. lemma OAI.PrimeDegreePackets.allSignedGlobalLabel_stabilizer line 3202
245. lemma OAI.PrimeDegreePackets.signedPacketOrbitEquiv_mk line 3214
246. lemma OAI.PrimeDegreePackets.allSignedGlobalLabel_volume line 3220
247. lemma OAI.PrimeDegreePackets.signedPacketOrbitEquiv_volume line 3250
248. lemma OAI.PrimeDegreePackets.signedPacketOrbitEquiv_probability_mk line 3268
249. theorem OAI.PrimeDegreePackets.packetVolume_eq_signedLabelCount line 3281
250. theorem OAI.PrimeDegreePackets.packetMeasure_eq_signedLabelAverage line 3296
251. theorem OAI.PrimeDegreePackets.normalized_measurable_periodic_map_eq line 3328
252. theorem OAI.PrimeDegreePackets.normalized_periodic_lintegral_eq line 3354
253. def OAI.PrimeDegreePackets.packetUnitKernel line 3372
254. lemma OAI.PrimeDegreePackets.packetUnitKernel_finiteIndex line 3377
255. lemma OAI.PrimeDegreePackets.packetUnitKernel_action line 3385
256. lemma OAI.PrimeDegreePackets.allSignedGlobalLabelPoint_unit_action line 3394
257. lemma OAI.PrimeDegreePackets.packetUnitKernel_log_le_period line 3405
258. lemma OAI.PrimeDegreePackets.allSignedGlobalLabelPoint_period_isZLattice line 3416
259. lemma OAI.PrimeDegreePackets.signedLabelSum_periodic line 3428
260. theorem OAI.PrimeDegreePackets.packetMeasure_lintegral_signedLogAverage line 3443
261. def OAI.PrimeDegreePackets.inverseQuotientHomeomorph line 3485
262. instance OAI.PrimeDegreePackets.integralGroup_discrete line 3494
263. instance OAI.PrimeDegreePackets.matrixSecondCountable line 3498
264. instance OAI.PrimeDegreePackets.matrixLocallyCompact line 3502
265. instance OAI.PrimeDegreePackets.gSecondCountable line 3506
266. instance OAI.PrimeDegreePackets.gLocallyCompact line 3509
267. instance OAI.PrimeDegreePackets.xT2Space line 3512
268. instance OAI.PrimeDegreePackets.xSecondCountable line 3515
269. instance OAI.PrimeDegreePackets.xLocallyCompact line 3518
270. instance OAI.PrimeDegreePackets.xMetrizable line 3521
271. def OAI.PrimeDegreePackets.integerRowMap line 3525
272. lemma OAI.PrimeDegreePackets.integerRowMap_apply line 3532
273. lemma OAI.PrimeDegreePackets.integerRowMap_range line 3537
274. lemma OAI.PrimeDegreePackets.integerRowMap_injective line 3551
275. def OAI.PrimeDegreePackets.integerRowEquiv line 3564
276. lemma OAI.PrimeDegreePackets.integerRowEquiv_val line 3568
277. def OAI.PrimeDegreePackets.nonzeroIntegerRowEquiv line 3571
278. lemma OAI.PrimeDegreePackets.continuous_integerRowMap line 3584
279. def OAI.PrimeDegreePackets.pointLattice line 3593
280. lemma OAI.PrimeDegreePackets.pointLattice_mk line 3603
281. def OAI.PrimeDegreePackets.siegelTransform line 3608
282. lemma OAI.PrimeDegreePackets.siegelTransform_mk line 3611
283. lemma OAI.PrimeDegreePackets.measurable_siegelTransform line 3619
284. lemma OAI.PrimeDegreePackets.pointLattice_latticePoint line 3633
285. lemma OAI.PrimeDegreePackets.pointLattice_rightAction_diagonal line 3642
286. def OAI.PrimeDegreePackets.nonzeroSubmoduleMapEquiv line 3652
287. lemma OAI.PrimeDegreePackets.tsum_nonzero_submodule_map line 3665
288. lemma OAI.PrimeDegreePackets.scaledRealEmbedding_injective line 3672
289. theorem OAI.PrimeDegreePackets.siegelTransform_latticePoint_diagonal line 3683
290. def OAI.PrimeDegreePackets.fullLatticeInclusionMatrix line 3706
291. lemma OAI.PrimeDegreePackets.embeddingMatrix_inclusion line 3710
292. lemma OAI.PrimeDegreePackets.fullLattice_relIndex_eq_natAbs_det line 3722
293. theorem OAI.PrimeDegreePackets.embeddingMatrix_abs_det_index line 3740
294. def OAI.PrimeDegreePackets.nonzeroSubmoduleInclusionEquiv line 3754
295. lemma OAI.PrimeDegreePackets.tsum_nonzero_submodule_inclusion line 3762
296. theorem OAI.PrimeDegreePackets.sum_nonzero_submodules line 3773
297. def OAI.PrimeDegreePackets.logFlowWeights line 3791
298. lemma OAI.PrimeDegreePackets.logFlowWeights_pos line 3794
299. lemma OAI.PrimeDegreePackets.pointLattice_rightAction_signs line 3798
300. lemma OAI.PrimeDegreePackets.pointLattice_signed_flow line 3805
301. lemma OAI.PrimeDegreePackets.signValue_ne_zero line 3816
302. theorem OAI.PrimeDegreePackets.siegelTransform_latticePoint_signed_flow line 3821
303. lemma OAI.PrimeDegreePackets.globalLabel_le_ideal line 3844
304. theorem OAI.PrimeDegreePackets.globalLabel_abs_det line 3854
305. lemma OAI.PrimeDegreePackets.relativeElementIdeal_le_one_iff line 3868
306. lemma OAI.PrimeDegreePackets.relativeElementIdeal_class line 3884
307. lemma OAI.PrimeDegreePackets.relativeElementIdeal_eq_iff line 3893
308. def OAI.PrimeDegreePackets.integralIdealClassFiber line 3902
309. def OAI.PrimeDegreePackets.nonzeroIdealElements line 3909
310. def OAI.PrimeDegreePackets.relativeElementClassMap line 3913
311. theorem OAI.PrimeDegreePackets.relativeElementClassMap_surjective line 3918
312. def OAI.PrimeDegreePackets.idealElementRepresentative line 3933
313. lemma OAI.PrimeDegreePackets.idealElementRepresentative_spec line 3937
314. def OAI.PrimeDegreePackets.idealElementUnitAction line 3944
315. lemma OAI.PrimeDegreePackets.relativeElementClassMap_unitAction line 3951
316. lemma OAI.PrimeDegreePackets.idealElementUnitAction_injective line 3957
317. theorem OAI.PrimeDegreePackets.exists_unique_unit_of_relativeElementClassMap_eq line 3970
318. def OAI.PrimeDegreePackets.idealElementDecompositionMap line 3985
319. def OAI.PrimeDegreePackets.idealElementDecomposition line 3992
320. def OAI.PrimeDegreePackets.nonzeroIdealElementEquiv line 4013
321. theorem OAI.PrimeDegreePackets.globalLabel_siegelTransform_average line 4024
322. theorem OAI.PrimeDegreePackets.tsum_comp_surjective_addHom line 4059
323. theorem OAI.PrimeDegreePackets.lintegral_tsum_addHom_fundamentalDomain line 4080
324. def OAI.PrimeDegreePackets.signedFlowSum line 4100
325. lemma OAI.PrimeDegreePackets.logFlowWeights_add line 4104
326. lemma OAI.PrimeDegreePackets.continuous_logFlowWeights line 4110
327. lemma OAI.PrimeDegreePackets.measurable_signedFlowSum line 4117
328. lemma OAI.PrimeDegreePackets.signedFlowSum_sign_log_translate line 4125
329. lemma OAI.PrimeDegreePackets.logFlowWeights_orderedUnitLog line 4140
330. lemma OAI.PrimeDegreePackets.signedFlowSum_mul_unit line 4150
331. def OAI.PrimeDegreePackets.orderedUnitLogOnto line 4163
332. lemma OAI.PrimeDegreePackets.orderedUnitLogOnto_surjective line 4169
333. lemma OAI.PrimeDegreePackets.orderedUnitLogOnto_ker line 4176
334. lemma OAI.PrimeDegreePackets.orderedUnitLogOnto_ker_card line 4181
335. theorem OAI.PrimeDegreePackets.lintegral_signedFlowSum_unit line 4193
336. def OAI.PrimeDegreePackets.productFiberVector line 4211
337. def OAI.PrimeDegreePackets.productFiberIntegral line 4215
338. lemma OAI.PrimeDegreePackets.lintegral_signedFlowSum_productFiberVector line 4220
339. theorem OAI.PrimeDegreePackets.lintegral_signedFlowSum_eq_productFiberIntegral line 4239
340. lemma OAI.PrimeDegreePackets.tsum_relativeElementIdeal line 4268
341. theorem OAI.PrimeDegreePackets.lintegral_weighted_idealElements line 4288
342. lemma OAI.PrimeDegreePackets.logSubgroup_top line 4321
343. def OAI.PrimeDegreePackets.orderedDeletedPlacesEquiv line 4326
344. lemma OAI.PrimeDegreePackets.orderedUnitRank line 4332
345. theorem OAI.PrimeDegreePackets.orderedLogSubgroup_covolume_eq_regulator line 4341
346. def OAI.PrimeDegreePackets.integralFractionalIdeals line 4382
347. def OAI.PrimeDegreePackets.idealClassPartitionEquiv line 4387
348. lemma OAI.PrimeDegreePackets.tsum_idealClassPartition line 4402
349. def OAI.PrimeDegreePackets.integralFractionalIdealsEquiv line 4413
350. lemma OAI.PrimeDegreePackets.tsum_integralFractionalIdeals line 4435
351. def OAI.PrimeDegreePackets.orderedComplexEmbeddings line 4442
352. lemma OAI.PrimeDegreePackets.integralEmbeddingMatrix_det_sq line 4453
353. lemma OAI.PrimeDegreePackets.embeddingMatrix_det_basisChange line 4475
354. theorem OAI.PrimeDegreePackets.embeddingMatrix_abs_det_fractionalIdeal line 4494
355. lemma OAI.PrimeDegreePackets.prod_orderedEmbeddings line 4515
356. lemma OAI.PrimeDegreePackets.prod_abs_orderedEmbeddings line 4526
357. lemma OAI.PrimeDegreePackets.fractionalIdeal_absNorm_pos line 4531
358. lemma OAI.PrimeDegreePackets.normalization_rpow_pow line 4537
359. lemma OAI.PrimeDegreePackets.normalized_ideal_coordinate_product line 4543
360. lemma OAI.PrimeDegreePackets.packetUnfoldingCoefficient line 4565
361. lemma OAI.PrimeDegreePackets.packetUnfoldingCoefficient_ennreal line 4579
362. def OAI.PrimeDegreePackets.signedGlobalLabelEquiv line 4597
363. lemma OAI.PrimeDegreePackets.allSignedGlobalLabel_card line 4605
364. lemma OAI.PrimeDegreePackets.sum_signedGlobalLabel line 4622
365. lemma OAI.PrimeDegreePackets.signedLabel_siegelTransform_average line 4636
366. lemma OAI.PrimeDegreePackets.signedLabel_siegelTransform_sum line 4659
367. theorem OAI.PrimeDegreePackets.signedLabel_siegelTransform_lintegral line 4675
368. lemma OAI.PrimeDegreePackets.orderedLogFundamentalDomain_volume line 4716
369. lemma OAI.PrimeDegreePackets.cancel_label_average line 4729
370. lemma OAI.PrimeDegreePackets.allSignedLabel_siegelTransform_lintegral line 4738
371. theorem OAI.PrimeDegreePackets.packetMeasure_siegel_unfolding_fractional line 4771
372. def OAI.PrimeDegreePackets.nonzeroIdealWeight line 4799
373. theorem OAI.PrimeDegreePackets.packetMeasure_siegel_unfolding line 4805
374. lemma OAI.PrimeDegreePackets.signValue_abs line 4823
375. def OAI.PrimeDegreePackets.coordinateBox line 4829
376. def OAI.PrimeDegreePackets.boxIndicator line 4832
377. lemma OAI.PrimeDegreePackets.measurableSet_coordinateBox line 4835
378. lemma OAI.PrimeDegreePackets.measurable_boxIndicator line 4842
379. lemma OAI.PrimeDegreePackets.abs_prod_sub_prod_bound line 4846
380. lemma OAI.PrimeDegreePackets.log_interval_width_bound line 4877
381. lemma OAI.PrimeDegreePackets.fiberPoint_abs_prod line 4890
382. theorem OAI.PrimeDegreePackets.productFiberIntegral_box_le line 4902
383. lemma OAI.PrimeDegreePackets.coordinateBox_product_bound line 4947
384. theorem OAI.PrimeDegreePackets.productFiberIntegral_box_supported line 4973