OAI/Geometry/Relativity/CKS/TailEnergy.lean

GitHub source file

389 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CKSSphericalChart.constructedEnergy line 18
2. theorem OAI.CKSSphericalChart.constructed_energy_tail_bound line 22
3. lemma OAI.CKSAngularGeometry.actual_inverse_derivative line 84
4. lemma OAI.CKSAngularGeometry.physicalMetricJet_dInv line 121
5. lemma OAI.CKSAngularGeometry.physicalMetricJet_gamma line 147
6. lemma OAI.CKSAngularGeometry.physicalMetricJet_dGamma line 156
7. abbrev OAI.CKSAmbientCalculus.A line 202
8. abbrev OAI.CKSAmbientCalculus.P line 203
9. abbrev OAI.CKSAmbientCalculus.Vect line 204
10. abbrev OAI.CKSAmbientCalculus.Symbols line 205
11. def OAI.CKSAmbientCalculus.delta line 207
12. lemma OAI.CKSAmbientCalculus.delta_expansion line 209
13. lemma OAI.CKSAmbientCalculus.delta_mul line 213
14. lemma OAI.CKSAmbientCalculus.delta_add line 218
15. lemma OAI.CKSAmbientCalculus.delta_sum line 223
16. def OAI.CKSAmbientCalculus.bracket line 228
17. lemma OAI.CKSAmbientCalculus.delta_moving line 231
18. lemma OAI.CKSAmbientCalculus.delta_commutator line 246
19. def OAI.CKSAmbientCalculus.nabla line 258
20. def OAI.CKSAmbientCalculus.curvature line 261
21. def OAI.CKSAmbientCalculus.coordCurvature line 265
22. lemma OAI.CKSAmbientCalculus.delta_nabla line 270
23. theorem OAI.CKSAmbientCalculus.curvature_coordinate line 310
24. def OAI.CKSAmbientCalculus.pair line 338
25. lemma OAI.CKSAmbientCalculus.pair_frame_sum line 340
26. lemma OAI.CKSAmbientCalculus.inverse_metric_trace line 350
27. lemma OAI.CKSAmbientCalculus.sum_three_rotate line 357
28. theorem OAI.CKSAmbientCalculus.scalar_frame_contraction line 366
29. def OAI.CKSAngularGeometry.physicalSymbols line 440
30. lemma OAI.CKSAngularGeometry.physicalSymbols_differentiableAt line 443
31. lemma OAI.CKSAngularGeometry.curvatureVector_coordinate line 451
32. lemma OAI.CKSAngularGeometry.physical_scalar_coordinate_trace line 463
33. lemma OAI.CKSAngularGeometry.physicalMetricJet_gamma_torsion line 496
34. lemma OAI.CKSAngularGeometry.physicalMetricJet_dGamma_torsion line 502
35. lemma OAI.CKSAngularGeometry.physicalMetricJet_ricci line 511
36. theorem OAI.CKSAngularGeometry.physicalMetricJet_scalar line 529
37. lemma OAI.CKSAngularGeometry.matrix_inverse_trace_coordinates line 555
38. lemma OAI.CKSAngularGeometry.physicalMetricJet_trace line 563
39. lemma OAI.CKSAngularGeometry.matrix_tensor_norm_coordinates line 568
40. lemma OAI.CKSAngularGeometry.physicalMetricJet_normSq line 585
41. lemma OAI.CKSAngularGeometry.physicalMetricJet_dTrace line 602
42. lemma OAI.CKSAngularGeometry.physicalMetricJet_tensorCovariant line 627
43. theorem OAI.CKSAngularGeometry.physicalMetricJet_momentum line 638
44. lemma OAI.CKSAngularGeometry.physicalMetricJet_energy line 659
45. theorem OAI.CKSAngularGeometry.physical_coordinate_DEC_iff line 670
46. lemma OAI.CKSRealizedRound.contDiffAt_normalEntry line 697
47. lemma OAI.CKSRealizedRound.contDiffAt_correctionCoeff line 703
48. lemma OAI.CKSRealizedRound.contDiffAt_correctedComponent line 710
49. lemma OAI.CKSRealizedRound.tensor_contDiffAt line 715
50. lemma OAI.CKSRealizedRound.tensor_hermitian line 737
51. lemma OAI.CKSRealizedRound.outerTensor_contDiffAt line 743
52. lemma OAI.CKSSphericalChart.sphericalAngularMetric_contDiff line 765
53. lemma OAI.CKSSphericalChart.roundAngularMetric_contDiff line 773
54. lemma OAI.CKSSphericalChart.roundAngularMetric_posDef line 779
55. lemma OAI.CKSSphericalChart.roundAngularMetric_eventually_posDef line 784
56. def OAI.CKSCartesianOuter.radicand line 804
57. def OAI.CKSCartesianOuter.metric line 806
58. def OAI.CKSCartesianOuter.tensor line 808
59. lemma OAI.CKSCartesianOuter.normal_smoothAt line 825
60. lemma OAI.CKSCartesianOuter.radicand_smoothAt line 831
61. lemma OAI.CKSCartesianOuter.metric_smoothAt line 839
62. lemma OAI.CKSCartesianOuter.cartTensorHeat_component_smoothAt line 852
63. lemma OAI.CKSCartesianOuter.cartTensorHeat_smoothAt line 864
64. lemma OAI.CKSCartesianOuter.tensor_smoothAt line 872
65. lemma OAI.CKSCartesianOuter.rankOne_positive line 893
66. lemma OAI.CKSCartesianOuter.metric_positive line 918
67. lemma OAI.CKSCartesianOuter.tensor_hermitian line 921
68. lemma OAI.CKSCartesianOuter.cartMass_uniform_bound line 942
69. lemma OAI.CKSCartesianOuter.cartesian_radicand_positive line 951
70. theorem OAI.CKSCartesianOuter.constructed_cartesian_outer_regular line 962
71. lemma OAI.CKSCartesianOuter.tensor_tail line 977
72. lemma OAI.CKSCartesianOuter.metric_tail line 984
73. lemma OAI.CKSCartesianOuter.metric_symbol line 992
74. structure OAI.CKSAngularGeometry.SmoothOrthonormalAt line 1009
75. structure OAI.CKSAngularGeometry.FrameChartAt line 1017
76. lemma OAI.CKSAngularGeometry.actualFrameBracket_eq_lieBracket line 1035
77. lemma OAI.CKSAngularGeometry.FrameChartAt.bracket_related line 1042
78. lemma OAI.CKSAngularGeometry.FrameChartAt.bracket_coefficients line 1057
79. lemma OAI.CKSAngularGeometry.FrameChartAt.connection_coefficients line 1064
80. lemma OAI.CKSAngularGeometry.D_chart_related line 1076
81. lemma OAI.CKSAngularGeometry.frame_connection_direction_chart line 1093
82. lemma OAI.CKSAngularGeometry.actualFrameCurvature_chart_covariance line 1105
83. lemma OAI.CKSAngularGeometry.actualFrameScalar_chart_covariance line 1112
84. lemma OAI.CKSAngularGeometry.frameTensor_chart_covariance line 1128
85. lemma OAI.CKSAngularGeometry.frame_tensor_direction_chart line 1137
86. lemma OAI.CKSAngularGeometry.actualFrameTensorCovariant_chart_covariance line 1151
87. theorem OAI.CKSAngularGeometry.actual_constraints_chart_covariance line 1162
88. lemma OAI.CKSAngularGeometry.FrameChartAt.target_adapted line 1192
89. lemma OAI.CKSAngularGeometry.FrameChartAt.source_adapted line 1203
90. theorem OAI.CKSAngularGeometry.physical_DEC_chart_covariance line 1212
91. def OAI.CKSAngularGeometry.coordinatePullback line 1244
92. def OAI.CKSAngularGeometry.coordinatePullbackFrame line 1248
93. lemma OAI.CKSAngularGeometry.metricPair_sum_right line 1260
94. lemma OAI.CKSAngularGeometry.coordinatePullback_pair line 1264
95. lemma OAI.CKSAngularGeometry.metricPair_dotProduct line 1282
96. lemma OAI.CKSAngularGeometry.coordinatePullback_symmetric line 1290
97. lemma OAI.CKSAngularGeometry.coordinatePullback_positive line 1297
98. lemma OAI.CKSAngularGeometry.coordinatePullback_smooth line 1304
99. lemma OAI.CKSAngularGeometry.chart_fderiv_left_inverse line 1315
100. lemma OAI.CKSAngularGeometry.chart_fderiv_right_inverse line 1324
101. lemma OAI.CKSAngularGeometry.coordinatePullbackFrame_smooth line 1332
102. theorem OAI.CKSAngularGeometry.smooth_coordinate_pullback_frame line 1349
103. theorem OAI.CKSAngularGeometry.actualFrameTensorCovariant_coordinate_general line 1391
104. lemma OAI.CKSAngularGeometry.frame_trace_derivative_general line 1416
105. theorem OAI.CKSAngularGeometry.actualFrameEnergy_coordinate_general line 1427
106. theorem OAI.CKSAngularGeometry.actualFrameMomentum_coordinate_general line 1441
107. theorem OAI.CKSAngularGeometry.physical_momentum_frame_norm_general line 1463
108. theorem OAI.CKSAngularGeometry.smooth_coordinate_DEC_pullback line 1483
109. lemma OAI.CKSAngularGeometry.smooth_coordinate_pullback_frame_at line 1528
110. theorem OAI.CKSAngularGeometry.local_coordinate_DEC_pullback line 1557
111. def OAI.CKSCartesianOuter.sphericalMap line 1605
112. def OAI.CKSCartesianOuter.sphericalBasis line 1606
113. def OAI.CKSCartesianOuter.physicalMetric line 1608
114. def OAI.CKSCartesianOuter.physicalTensor line 1610
115. lemma OAI.CKSCartesianOuter.sphericalMap_smooth line 1623
116. lemma OAI.CKSCartesianOuter.sphericalMap_euclidean line 1625
117. lemma OAI.CKSCartesianOuter.sphericalMap_norm line 1627
118. lemma OAI.CKSCartesianOuter.sphericalMap_unit line 1630
119. lemma OAI.CKSCartesianOuter.sphericalMap_fderiv line 1634
120. lemma OAI.CKSCartesianOuter.sphericalMap_mass line 1650
121. lemma OAI.CKSCartesianOuter.sphericalMap_radicand line 1654
122. lemma OAI.CKSCartesianOuter.metricPair_toPoint line 1659
123. lemma OAI.CKSCartesianOuter.pair_add_matrix line 1668
124. lemma OAI.CKSCartesianOuter.pair_smul_matrix line 1670
125. lemma OAI.CKSCartesianOuter.pair_one line 1677
126. lemma OAI.CKSCartesianOuter.pair_rankOne line 1679
127. lemma OAI.CKSCartesianOuter.normal_sphericalMap line 1683
128. lemma OAI.CKSCartesianOuter.pair_one_symm line 1701
129. def OAI.CKSCartesianOuter.unitBasis line 1706
130. def OAI.CKSCartesianOuter.sphericalScale line 1707
131. lemma OAI.CKSCartesianOuter.sphericalBasis_scaled line 1708
132. lemma OAI.CKSCartesianOuter.pair_one_unitBasis line 1711
133. lemma OAI.CKSCartesianOuter.pair_one_sphericalBasis line 1731
134. lemma OAI.CKSCartesianOuter.normalDot_sphericalBasis line 1739
135. lemma OAI.CKSCartesianOuter.pair_rankOne_sphericalBasis line 1745
136. lemma OAI.CKSCartesianOuter.pair_sum_right line 1761
137. lemma OAI.CKSCartesianOuter.sphericalMap_fderiv_component line 1764
138. lemma OAI.CKSCartesianOuter.sphericalMap_fderiv_injective line 1771
139. def OAI.CKSCartesianOuter.sphericalDerivativeEquiv line 1780
140. lemma OAI.CKSCartesianOuter.sphericalDerivative_hasFDerivAt line 1785
141. def OAI.CKSCartesianOuter.sphericalChart line 1799
142. lemma OAI.CKSCartesianOuter.sphericalChart_coe line 1803
143. lemma OAI.CKSCartesianOuter.sphericalChart_mem line 1805
144. lemma OAI.CKSCartesianOuter.sphericalChart_inverse_smooth line 1809
145. theorem OAI.CKSCartesianOuter.spherical_metric_pullback line 1837
146. lemma OAI.CKSCartesianOuter.pair_sub_matrix line 1865
147. lemma OAI.CKSCartesianOuter.heat_sphericalBasis line 1867
148. theorem OAI.CKSCartesianOuter.spherical_tensor_pullback line 1892
149. lemma OAI.CKSAngularGeometry.coordinatePullback_symm line 1923
150. lemma OAI.CKSAngularGeometry.physicalMetricJet_congr line 1935
151. lemma OAI.CKSAngularGeometry.physicalTensorJet_congr line 1949
152. theorem OAI.CKSAngularGeometry.local_coordinate_DEC_pushforward line 1958
153. lemma OAI.CKSSphericalChart.outer_physical_DEC_iff line 1996
154. theorem OAI.CKSSphericalChart.constructed_outer_physical_DEC line 2025
155. lemma OAI.CKSAngularGeometry.SmoothOrthonormalAt.congr_metric line 2065
156. lemma OAI.CKSAngularGeometry.round_smoothOrthonormalAt line 2075
157. lemma OAI.CKSCartesianOuter.spherical_physical_DEC_iff line 2106
158. theorem OAI.CKSCartesianOuter.sphericalMap_surjective_radial line 2170
159. structure OAI.CKSAngularGeometry.ContinuousMetricJetAt line 2211
160. structure OAI.CKSAngularGeometry.ContinuousTensorJetAt line 2215
161. lemma OAI.CKSAngularGeometry.ContinuousMetricJetAt.gamma line 2218
162. lemma OAI.CKSAngularGeometry.ContinuousMetricJetAt.dInv line 2225
163. lemma OAI.CKSAngularGeometry.ContinuousMetricJetAt.dGamma line 2232
164. lemma OAI.CKSAngularGeometry.ContinuousMetricJetAt.ricci line 2241
165. lemma OAI.CKSAngularGeometry.ContinuousMetricJetAt.scalar line 2248
166. lemma OAI.CKSAngularGeometry.ContinuousMetricJetAt.trace line 2254
167. lemma OAI.CKSAngularGeometry.ContinuousMetricJetAt.normSq line 2262
168. lemma OAI.CKSAngularGeometry.ContinuousMetricJetAt.dTrace line 2270
169. lemma OAI.CKSAngularGeometry.ContinuousMetricJetAt.tensorDivergence line 2280
170. lemma OAI.CKSAngularGeometry.ContinuousMetricJetAt.energy line 2290
171. lemma OAI.CKSAngularGeometry.ContinuousMetricJetAt.momentum line 2299
172. lemma OAI.CKSAngularGeometry.ContinuousMetricJetAt.momentumSq line 2307
173. lemma OAI.CKSAngularGeometry.physicalMetricJet_continuousAt line 2315
174. lemma OAI.CKSAngularGeometry.physicalTensorJet_continuousAt line 2324
175. theorem OAI.CKSAngularGeometry.physical_DEC_closed_along line 2330
176. lemma OAI.CKSCartesianOuter.regular_angular_approximation line 2351
177. lemma OAI.CKSCartesianOuter.spherical_DEC_extend_poles line 2375
178. theorem OAI.CKSCartesianOuter.constructed_cartesian_outer_DEC line 2397
179. lemma OAI.CKSBending.constant_halfline_full_jets line 2439
180. lemma OAI.CKSBending.roundingWeight_flat_initial line 2447
181. lemma OAI.CKSBending.roundingWeight_flat_final line 2452
182. lemma OAI.CKSBending.paddingWeight_flat_initial line 2457
183. lemma OAI.CKSBending.paddingWeight_flat_final line 2462
184. lemma OAI.CKSBending.paddingMass_flat_initial line 2467
185. lemma OAI.CKSBending.roundingWeight_deriv_final line 2472
186. lemma OAI.CKSAngularSlice.collar_fields_initial line 2491
187. lemma OAI.CKSAngularSlice.collar_fields_final line 2502
188. lemma OAI.CKSAngularSlice.collarQ_positive line 2511
189. lemma OAI.CKSSphericalChart.round_leafRadialRate line 2534
190. lemma OAI.CKSSphericalChart.round_radialExpansion line 2556
191. lemma OAI.CKSSphericalChart.final_collar_fields line 2569
192. lemma OAI.CKSSphericalChart.final_collar_radialExpansion line 2585
193. lemma OAI.CKSSphericalChart.bendingV_deriv_initial line 2599
194. theorem OAI.CKSSphericalChart.physical_collar_outer_overlap line 2618
195. def OAI.CKSLorentz.spatialMatrix line 2672
196. lemma OAI.CKSLorentz.angular_round_leafRadialRate line 2685
197. lemma OAI.CKSLorentz.angular_round_radialExpansion line 2712
198. lemma OAI.CKSLorentz.final_angular_collar_radialExpansion line 2724
199. lemma OAI.CKSLorentz.spatialMatrix_apply line 2749
200. lemma OAI.CKSLorentz.euclidean_inner_sum line 2756
201. lemma OAI.CKSLorentz.spatialMatrix_radial line 2758
202. lemma OAI.CKSLorentz.normal_polarParam line 2764
203. lemma OAI.CKSLorentz.radial_matrix_polar line 2780
204. lemma OAI.CKSLorentz.cartMass_polar_initial line 2827
205. lemma OAI.CKSLorentz.outer_tensor_initial_matrix line 2837
206. lemma OAI.CKSLorentz.collar_outer_blocks line 2866
207. theorem OAI.CKSLorentz.physical_collar_outer_spatial_overlap line 2912
208. def OAI.CKSLorentz.SourceCollarAtlas.HasMassAspect line 2970
209. def OAI.CKSLorentz.SourceCollarAtlas.replacementMetric line 2976
210. def OAI.CKSLorentz.SourceCollarAtlas.replacementTensor line 2980
211. lemma OAI.CKSLorentz.CollarSourcePatch.aspect_eq line 2994
212. lemma OAI.CKSLorentz.SourceCollarAtlas.fstar_mass line 3001
213. lemma OAI.CKSLorentz.SourceCollarAtlas.eventually_outer_recovery line 3012
214. lemma OAI.CKSLorentz.SourceCollarAtlas.replacement_localization line 3040
215. lemma OAI.CKSLorentz.spatialMatrix_contDiffAt line 3105
216. lemma OAI.CKSLorentz.spatialMatrix_symm line 3117
217. lemma OAI.CKSLorentz.spatialMatrix_pos line 3121
218. lemma OAI.CKSMixedGeometry.metricBlock_smoothAt line 3136
219. lemma OAI.CKSMixedGeometry.sourceMetric_smoothAt line 3149
220. lemma OAI.CKSMixedGeometry.sourceTensor_smoothAt line 3152
221. lemma OAI.CKSLorentz.SourceCollarAtlas.source_spatial_regular line 3165
222. theorem OAI.CKSLorentz.actual_same_end_smooth_replacement line 3215
223. lemma OAI.CKSAngularGeometry.foliationMetric_lapse_ne_zero line 3369
224. lemma OAI.CKSAngularGeometry.foliation_smoothOrthonormalAt line 3380
225. lemma OAI.CKSAngularGeometry.radialMassLapse_denominators line 3390
226. lemma OAI.CKSAngularGeometry.physical_collar_frame_lapse line 3399
227. lemma OAI.CKSAngularGeometry.physical_collar_frame_leaf line 3403
228. lemma OAI.CKSAngularGeometry.physical_collar_smoothOrthonormalAt line 3407
229. lemma OAI.CKSLorentz.SourceCollarAtlas.source_orthonormal line 3432
230. lemma OAI.CKSLorentz.SourceCollarAtlas.collar_data_smooth line 3446
231. lemma OAI.CKSLorentz.SourceCollarAtlas.collar_symmetries line 3460
232. lemma OAI.CKSLorentz.SourceCollarAtlas.collar_orthonormal_eventually line 3472
233. abbrev OAI.CKSLorentz.cartesianPolar line 3502
234. lemma OAI.CKSLorentz.cartesianPolar_smoothAt line 3504
235. lemma OAI.CKSLorentz.cartesianPolar_fderiv line 3508
236. def OAI.CKSLorentz.polarDerivative line 3515
237. lemma OAI.CKSLorentz.polarDerivative_hasFDerivAt line 3524
238. def OAI.CKSLorentz.polarCartesianChart line 3528
239. lemma OAI.CKSLorentz.polarCartesianChart_coe line 3533
240. lemma OAI.CKSLorentz.polarCartesianChart_mem line 3536
241. lemma OAI.CKSLorentz.polarCartesianChart_smooth line 3541
242. lemma OAI.CKSLorentz.spatialCoefficients_pair line 3566
243. lemma OAI.CKSLorentz.spatialCoefficients_pullback line 3576
244. lemma OAI.CKSLorentz.spatialCoefficients_spatialMatrix line 3586
245. lemma OAI.CKSLorentz.spatialDEC_congr line 3602
246. lemma OAI.CKSLorentz.spatialDEC_of_polar line 3614
247. lemma OAI.CKSLorentz.SourceCollarAtlas.source_spatial_DEC line 3655
248. lemma OAI.CKSLorentz.polarTensorComponents_smoothAt line 3698
249. lemma OAI.CKSLorentz.original_source_fields_smooth line 3706
250. lemma OAI.CKSLorentz.sourceSpatial_symmetric line 3740
251. lemma OAI.CKSLorentz.polarTensorComponents_pair line 3748
252. lemma OAI.CKSLorentz.polarTensorComponents_posDef line 3758
253. lemma OAI.CKSLorentz.physicalDEC_of_spatial line 3771
254. theorem OAI.CKSLorentz.original_source_patch_properties line 3813
255. def OAI.CKSAngularGeometry.matrixLeaf line 3885
256. def OAI.CKSAngularGeometry.matrixMixed line 3887
257. def OAI.CKSAngularGeometry.matrixShift line 3889
258. def OAI.CKSAngularGeometry.matrixSchur line 3891
259. def OAI.CKSAngularGeometry.matrixLapse line 3893
260. def OAI.CKSAngularGeometry.matrixFrame line 3895
261. lemma OAI.CKSAngularGeometry.actual_matrix_block line 3907
262. lemma OAI.CKSAngularGeometry.actual_matrix_leaf_pos line 3914
263. lemma OAI.CKSAngularGeometry.actual_matrix_schur_pos line 3917
264. lemma OAI.CKSAngularGeometry.actual_matrix_foliation line 3921
265. lemma OAI.CKSAngularGeometry.actual_matrix_frame line 3940
266. lemma OAI.CKSLorentz.spatialTensorPullback_smooth line 3978
267. lemma OAI.CKSLorentz.spatialCoefficients_smooth line 3987
268. lemma OAI.CKSLorentz.spatialCoefficients_symmetric line 3994
269. lemma OAI.CKSLorentz.spatialCoefficients_positive line 4001
270. def OAI.CKSLorentz.spatialCoordinateHomeomorph line 4015
271. lemma OAI.CKSLorentz.spatialCoordinateHomeomorph_smooth line 4017
272. lemma OAI.CKSLorentz.spatialCoordinateHomeomorph_fderiv line 4023
273. lemma OAI.CKSLorentz.spatialCoefficients_general_pullback line 4030
274. lemma OAI.CKSLorentz.spatialDEC_pullback line 4051
275. theorem OAI.CKSLorentz.spatialBilinear_isScalarTower line 4113
276. lemma OAI.CKSLorentz.hyperbolicField_smooth line 4121
277. lemma OAI.CKSLorentz.sourceSpatial_smooth line 4125
278. lemma OAI.CKSLorentz.sourceSpatial_boost line 4127
279. lemma OAI.CKSLorentz.smoothHomeomorph_fderiv_injective line 4134
280. theorem OAI.CKSLorentz.hyperbolic_source_geometry line 4148
281. def OAI.CKSLorentz.SpatialBoostPatch.collarSourcePatch line 4196
282. lemma OAI.CKSLorentz.SpatialBoostPatch.collarSourcePatch_fields line 4212
283. lemma OAI.CKSLorentz.homeomorph_maps_far_tail line 4217
284. lemma OAI.CKSLorentz.trace_conformal_congruence line 4239
285. lemma OAI.CKSLorentz.angularGram_congruence line 4277
286. lemma OAI.CKSLorentz.boundaryChart_regular line 4289
287. lemma OAI.CKSLorentz.boundary_param_fderiv line 4307
288. lemma OAI.CKSLorentz.boundary_roundMetric_conformal line 4335
289. theorem OAI.CKSLorentz.lorentz_leading_trace line 4365
290. lemma OAI.CKSLorentz.angularMetricTrace_add line 4418
291. lemma OAI.CKSLorentz.angularMetricTrace_smul line 4421
292. lemma OAI.CKSLorentz.cksChartMassAspect_split line 4424
293. theorem OAI.CKSLorentz.lorentz_cks_massAspect line 4436
294. lemma OAI.CKSLorentz.genuine_patch_massAspect line 4470
295. theorem OAI.CKSLorentz.source_atlas_from_original line 4497
296. lemma OAI.CKSLorentz.polar_components_of_lift_eq line 4590
297. theorem OAI.CKSLorentz.actual_same_end_DEC line 4614
298. lemma OAI.CKSLorentz.spatialCartesian_spatialMatrix line 4703
299. lemma OAI.CKSLorentz.spatialCartesian_congr_at line 4708
300. lemma OAI.CKSLorentz.SourceCollarAtlas.replacement_tail line 4713
301. lemma OAI.CKSLorentz.SourceCollarAtlas.replacement_surfaceEnergy_tail line 4731
302. lemma OAI.CKSLorentz.SourceCollarAtlas.replacement_surfaceMomentum_tail line 4754
303. theorem OAI.CKSLorentz.actual_same_end_AF_ADM line 4768
304. abbrev OAI.CKSTailVolume.E line 4799
305. abbrev OAI.CKSTailVolume.Mat line 4800
306. def OAI.CKSTailVolume.direction line 4801
307. def OAI.CKSTailVolume.tailMetric line 4802
308. def OAI.CKSTailVolume.density line 4804
309. def OAI.CKSTailVolume.tailVolume line 4805
310. def OAI.CKSTailVolume.tailRegion line 4806
311. lemma OAI.CKSTailVolume.direction_sq_sum line 4816
312. lemma OAI.CKSTailVolume.det_rank_one line 4821
313. lemma OAI.CKSTailVolume.tailMetric_det line 4831
314. theorem OAI.CKSTailVolume.tail_density_bound line 4836
315. lemma OAI.CKSTailVolume.rate_le_japanese line 4864
316. lemma OAI.CKSTailVolume.tailRegion_measurable line 4877
317. lemma OAI.CKSTailVolume.constraint_integrable_dx line 4880
318. theorem OAI.CKSTailVolume.tail_constraint_integrable line 4896
319. def OAI.CKSLorentz.spatialMomentum line 4920
320. def OAI.CKSLorentz.spatialVolume line 4924
321. theorem OAI.CKSAngularGeometry.local_coordinate_energy_pullback line 4936
322. theorem OAI.CKSAngularGeometry.local_coordinate_energy_pushforward line 4970
323. lemma OAI.CKSCartesianOuter.spherical_physical_energy line 5008
324. lemma OAI.CKSCartesianOuter.spherical_energy_bound_extend_poles line 5072
325. theorem OAI.CKSCartesianOuter.constructed_cartesian_energy_tail_bound line 5088
326. lemma OAI.CKSLorentz.spatialCoefficients_congr line 5135
327. lemma OAI.CKSLorentz.spatialEnergy_congr line 5143
328. lemma OAI.CKSLorentz.SourceCollarAtlas.replacement_outer_eventually line 5147
329. lemma OAI.CKSLorentz.SourceCollarAtlas.replacement_outer_energy line 5157
330. lemma OAI.CKSLorentz.SourceCollarAtlas.replacement_momentum_tail line 5168
331. lemma OAI.CKSLorentz.SourceCollarAtlas.replacement_density_tail line 5180
332. lemma OAI.CKSLorentz.SourceCollarAtlas.replacement_energy_continuousAt line 5194
333. theorem OAI.CKSLorentz.actual_same_end_tail_integrable line 5223
334. lemma OAI.CKSLorentz.cartesian_metric_polar_block line 5292
335. lemma OAI.CKSLorentz.generic_outer_background_lower line 5299
336. lemma OAI.CKSLorentz.SourceCollarAtlas.eventually_outer_local_lower line 5343
337. lemma OAI.CKSLorentz.polar_spatial_quadratic line 5419
338. lemma OAI.CKSLorentz.SourceCollarAtlas.eventually_outer_spatial_lower line 5427
339. lemma OAI.CKSLorentz.SourceCollarAtlas.eventually_closed_collar_lower line 5453
340. theorem OAI.CKSLorentz.actual_same_end_uniform_lower line 5497
341. theorem OAI.CKSLorentz.original_CKS_end_replacement line 5547
342. lemma OAI.CKSLorentz.spatial_energy_continuousAt line 5635
343. lemma OAI.CKSLorentz.spatial_density_continuousAt line 5644
344. lemma OAI.CKSLorentz.spatial_integrableOn_compact line 5650
345. theorem OAI.CKSLorentz.end_constraints_integrable line 5664
346. theorem OAI.CKSLorentz.original_CKS_end_integrable_replacement line 5725
347. theorem OAI.CKSSpatialManifold.boosted_end_proper line 5790
348. def OAI.CKSReplacementCompleteness.tangentNorm line 5831
349. def OAI.CKSReplacementCompleteness.metricEDist line 5833
350. def OAI.CKSReplacementCompleteness.MetricLower line 5836
351. theorem OAI.CKSReplacementCompleteness.complete_of_emetricLower line 5849
352. lemma OAI.CKSReplacementCompleteness.metricEDist_eq line 5882
353. lemma OAI.CKSReplacementCompleteness.tangentNorm_lower line 5897
354. theorem OAI.CKSReplacementCompleteness.metricEDist_lower line 5904
355. lemma OAI.CKSReplacementCompleteness.metricSpace_topology line 5923
356. lemma OAI.CKSReplacementCompleteness.metricSpace_edist line 5925
357. theorem OAI.CKSReplacementCompleteness.complete_of_metricLower line 5928
358. def OAI.CKSGeometricCuts.rawHausdorffArea line 5955
359. def OAI.CKSGeometricCuts.OuterDomain.cut line 5962
360. def OAI.CKSGeometricCuts.IsEnclosingCut line 5964
361. def OAI.CKSGeometricCuts.area line 5966
362. def OAI.CKSGeometricCuts.minEnclosingArea line 5968
363. lemma OAI.CKSGeometricCuts.rawHausdorffArea_lower line 5982
364. theorem OAI.CKSGeometricCuts.area_lower line 6025
365. theorem OAI.CKSGeometricCuts.geometric_min_area_lower line 6046
366. def OAI.CKSGeometricCuts.identityOuterDomain line 6055
367. theorem OAI.CKSGeometricCuts.boundary_isEnclosingCut line 6070
368. lemma OAI.CKSGeometricCuts.IsEnclosingCut.isCompact line 6077
369. theorem OAI.CKSGeometricCuts.minEnclosingArea_le_boundary line 6082
370. theorem OAI.CKSSpatialManifold.covector_smulCommClass line 6101
371. abbrev OAI.CKSSpatialManifold.SpatialTangentTriv line 6109
372. def OAI.CKSSpatialManifold.spatialBilinearTriv line 6111
373. theorem OAI.CKSSpatialManifold.boosted_exterior_coordinates line 6130
374. instance OAI.CKSSpatialManifold.spatialBilinearTriv_atlas line 6217
375. lemma OAI.CKSSpatialManifold.spatialBilinearTriv_baseSet line 6219
376. lemma OAI.CKSSpatialManifold.spatialBilinearTriv_pair line 6221
377. lemma OAI.CKSSpatialManifold.mfderiv_gauge_smooth line 6237
378. lemma OAI.CKSSpatialManifold.bilinearComp_smoothAt line 6252
379. lemma OAI.CKSSpatialManifold.endInner_smoothAt line 6263
380. lemma OAI.CKSSpatialManifold.positive_bilinear_bounded line 6279
381. lemma OAI.CKSSpatialManifold.end_extend_smooth line 6332
382. theorem OAI.CKSSpatialManifold.extend_actual_end line 6379
383. lemma OAI.CKSSpatialManifold.endInner_fullRank line 6516
384. lemma OAI.CKSSpatialManifold.PhysicalDECAt.congr_nhds line 6533
385. theorem OAI.CKSSpatialManifold.extended_manifold_DEC line 6557
386. lemma OAI.CKSSpatialManifold.endInner_comp line 6608
387. theorem OAI.CKSSpatialManifold.endInner_balanced line 6635
388. theorem OAI.CKSSpatialManifold.compact_side_eventually line 6663
389. theorem OAI.CKSSpatialManifold.original_CKS_replacement_coordinate_package line 6708