OAI/Geometry/Relativity/CKS/ConstructedOuterMetric.lean

GitHub source file

864 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CKSSphericalChart.sphericalAngularMetric line 18
2. lemma OAI.CKSSphericalChart.sphericalAngularMetric_posDef line 21
3. lemma OAI.CKSSphericalChart.outerMetric_foliation line 29
4. theorem OAI.CKSSphericalChart.constructed_outer_metric_lower line 39
5. def OAI.CKSLorentz.minkowski line 80
6. def OAI.CKSLorentz.mass line 82
7. lemma OAI.CKSLorentz.energy_pos line 84
8. lemma OAI.CKSLorentz.mass_pos line 85
9. lemma OAI.CKSLorentz.mass_sq line 88
10. lemma OAI.CKSLorentz.inner_momentum line 91
11. def OAI.CKSLorentz.boost line 94
12. lemma OAI.CKSLorentz.boost_minkowski line 98
13. lemma OAI.CKSLorentz.boost_neg_inverse line 107
14. lemma OAI.CKSLorentz.boost_smooth line 128
15. lemma OAI.CKSLorentz.boost_mass line 135
16. lemma OAI.CKSLorentz.sphere_norm line 138
17. def OAI.CKSLorentz.denominator line 140
18. def OAI.CKSLorentz.boundarySpatial line 142
19. lemma OAI.CKSLorentz.denominator_pos line 145
20. lemma OAI.CKSLorentz.boundarySpatial_norm line 153
21. def OAI.CKSLorentz.boundary line 168
22. def OAI.CKSLorentz.boostCLM line 186
23. lemma OAI.CKSLorentz.boostCLM_apply line 206
24. lemma OAI.CKSLorentz.mass_neg line 209
25. lemma OAI.CKSLorentz.boost_neg_right_inverse line 211
26. def OAI.CKSLorentz.boostEquiv line 215
27. def OAI.CKSLorentz.boundaryAmbient line 226
28. lemma OAI.CKSLorentz.boundary_null line 229
29. lemma OAI.CKSLorentz.boundary_inverse line 239
30. lemma OAI.CKSLorentz.boundaryAmbient_smooth line 266
31. instance OAI.CKSLorentz.(instance at line 276) line 276
32. lemma OAI.CKSLorentz.boundary_smooth line 278
33. def OAI.CKSLorentz.boundaryHomeomorph line 287
34. def OAI.CKSLorentz.hyperTime line 306
35. def OAI.CKSLorentz.hyperboloid line 307
36. def OAI.CKSLorentz.hyperbolicMap line 308
37. lemma OAI.CKSLorentz.hyperTime_pos line 310
38. lemma OAI.CKSLorentz.hyperTime_sq line 311
39. lemma OAI.CKSLorentz.norm_lt_hyperTime line 312
40. lemma OAI.CKSLorentz.hyperTime_smooth line 316
41. lemma OAI.CKSLorentz.hyperboloid_smooth line 318
42. lemma OAI.CKSLorentz.hyperbolicMap_smooth line 319
43. lemma OAI.CKSLorentz.boosted_time_pos line 322
44. lemma OAI.CKSLorentz.hyperboloid_minkowski line 334
45. theorem OAI.CKSLorentz.hyperboloid_boost line 338
46. lemma OAI.CKSLorentz.hyperbolicMap_inverse line 353
47. def OAI.CKSLorentz.hyperbolicHomeomorph line 360
48. def OAI.CKSLorentz.hyperbolicMetric line 369
49. lemma OAI.CKSLorentz.hyperTime_derivative line 372
50. lemma OAI.CKSLorentz.hyperboloid_derivative_pair line 380
51. theorem OAI.CKSLorentz.hyperbolicMap_isometry line 390
52. def OAI.CKSLorentz.timeDifferential line 420
53. def OAI.CKSLorentz.spaceDifferential line 422
54. lemma OAI.CKSLorentz.timeDifferential_apply line 425
55. lemma OAI.CKSLorentz.spaceDifferential_apply line 427
56. lemma OAI.CKSLorentz.denominator_derivative line 431
57. lemma OAI.CKSLorentz.boundarySpatial_derivative line 435
58. lemma OAI.CKSLorentz.boundaryAmbient_fderiv line 440
59. lemma OAI.CKSLorentz.minkowski_null_tangent line 454
60. lemma OAI.CKSLorentz.minkowski_tangent_tangent line 461
61. theorem OAI.CKSLorentz.boundary_conformal line 468
62. def OAI.CKSLorentz.compactRoot line 509
63. def OAI.CKSLorentz.compactSpatial line 510
64. def OAI.CKSLorentz.compactScale line 512
65. def OAI.CKSLorentz.spatialCorrection line 513
66. def OAI.CKSLorentz.squareCorrection line 515
67. def OAI.CKSLorentz.radialCorrection line 517
68. def OAI.CKSLorentz.angularCorrection line 519
69. lemma OAI.CKSLorentz.compactRoot_pos line 524
70. lemma OAI.CKSLorentz.compactRoot_add_one_pos line 525
71. lemma OAI.CKSLorentz.compactRoot_sq line 526
72. lemma OAI.CKSLorentz.compactRoot_zero line 527
73. lemma OAI.CKSLorentz.compactRoot_sub line 528
74. lemma OAI.CKSLorentz.compactRoot_smooth line 531
75. lemma OAI.CKSLorentz.compactSpatial_smooth line 534
76. lemma OAI.CKSLorentz.compactSpatial_zero line 539
77. lemma OAI.CKSLorentz.compactSpatial_expansion line 543
78. lemma OAI.CKSLorentz.compactScale_sq line 555
79. lemma OAI.CKSLorentz.compactScale_expansion line 578
80. lemma OAI.CKSLorentz.compactAngle_expansion line 590
81. lemma OAI.CKSLorentz.compactScale_smooth_at_zero line 609
82. lemma OAI.CKSLorentz.spatialCorrection_smooth line 616
83. lemma OAI.CKSLorentz.squareCorrection_smooth line 625
84. lemma OAI.CKSLorentz.radialCorrection_smooth_at_zero line 630
85. lemma OAI.CKSLorentz.angularCorrection_smooth_at_zero line 641
86. def OAI.CKSLorentz.compactRegion line 668
87. def OAI.CKSLorentz.correctionPair line 671
88. lemma OAI.CKSLorentz.denominator_joint_smooth line 674
89. lemma OAI.CKSLorentz.boundarySpatial_joint_smooth line 678
90. lemma OAI.CKSLorentz.compactRegion_open line 684
91. lemma OAI.CKSLorentz.compactScale_smooth_region line 688
92. lemma OAI.CKSLorentz.correctionPair_smooth_region line 692
93. theorem OAI.CKSLorentz.exists_compact_collar line 701
94. lemma OAI.CKSLorentz.correction_jets_continuous_region line 721
95. theorem OAI.CKSLorentz.coordinate_coefficients_all_orders line 728
96. lemma OAI.CKSLorentz.hyperTime_polar line 748
97. lemma OAI.CKSLorentz.hyperbolicMap_polar line 757
98. theorem OAI.CKSLorentz.actual_radius_expansion line 764
99. theorem OAI.CKSLorentz.actual_angle_expansion line 773
100. lemma OAI.CKSMixedGeometry.sum_coordinate_basis line 794
101. lemma OAI.CKSMixedGeometry.multilinear_norm_of_components line 798
102. lemma OAI.CKSMixedGeometry.iteratedFDeriv_basis_ofFn line 827
103. lemma OAI.CKSMixedGeometry.coordinateIter_le_iteratedFDeriv line 847
104. lemma OAI.CKSMixedGeometry.source_scaledComponent_norm_derivative line 857
105. def OAI.CKSMixedGeometry.inverseLogRadiusChart line 886
106. def OAI.CKSMixedGeometry.backwardFactor line 890
107. def OAI.CKSMixedGeometry.backwardScaledD line 894
108. def OAI.CKSMixedGeometry.backwardScaledIter line 897
109. lemma OAI.CKSMixedGeometry.backwardScaledIter_nil line 900
110. lemma OAI.CKSMixedGeometry.backwardScaledIter_cons line 904
111. lemma OAI.CKSMixedGeometry.inverseLogRadiusChart_smooth line 910
112. lemma OAI.CKSMixedGeometry.backwardFactor_smooth line 915
113. def OAI.CKSMixedGeometry.inverseChartDerivative line 919
114. lemma OAI.CKSMixedGeometry.inverseLogRadiusChart_hasFDerivAt line 926
115. lemma OAI.CKSMixedGeometry.inverseChartDerivative_basis line 941
116. lemma OAI.CKSMixedGeometry.D_inverse_pullback line 950
117. lemma OAI.CKSMixedGeometry.backwardScaledIter_contDiffAt line 961
118. lemma OAI.CKSMixedGeometry.coordinateIter_inverse_pullback line 972
119. theorem OAI.CKSMixedGeometry.compactified_scalar_uniform_jets line 992
120. theorem OAI.CKSMixedGeometry.compactified_vector_uniform_jets line 1028
121. lemma OAI.CKSMixedGeometry.linear_positive_jet_bound line 1057
122. def OAI.CKSMixedGeometry.logAffineCompactMap line 1070
123. theorem OAI.CKSMixedGeometry.logAffineCompactMap_uniform_jets line 1073
124. def OAI.CKSLorentz.radialLinear line 1110
125. def OAI.CKSLorentz.compactPolar line 1113
126. def OAI.CKSLorentz.compactAngle line 1116
127. def OAI.CKSLorentz.compactLorentzCoefficients line 1119
128. def OAI.CKSLorentz.logLorentzChart line 1124
129. def OAI.CKSLorentz.lorentzPolarChart line 1127
130. lemma OAI.CKSLorentz.compactPolar_contDiffAt line 1143
131. lemma OAI.CKSLorentz.compactAngle_contDiffAt line 1148
132. lemma OAI.CKSLorentz.compactLorentzCoefficients_contDiffAt line 1153
133. lemma OAI.CKSLorentz.logLorentzChart_contDiffAt line 1169
134. theorem OAI.CKSLorentz.logLorentzChart_uniform_jets line 1179
135. lemma OAI.CKSLorentz.angularProjection_inverseLogRadiusChart line 1190
136. lemma OAI.CKSLorentz.angularProjection_logRadiusChart line 1195
137. lemma OAI.CKSLorentz.logLorentzChart_eq_slice line 1200
138. lemma OAI.CKSLorentz.logLorentzChart_radial_exp line 1210
139. lemma OAI.CKSLorentz.logRadiusChart_slice line 1216
140. theorem OAI.CKSLorentz.lorentzPolarChart_logRadiusChart line 1223
141. lemma OAI.CKSMixedGeometry.local_norm_iteratedFDeriv_comp line 1260
142. theorem OAI.CKSMixedGeometry.source_scaledComponent_pullback line 1297
143. theorem OAI.CKSLorentz.lorentz_finite_remainder_pullback line 1341
144. def OAI.CKSMixedGeometry.LogJetBound line 1407
145. lemma OAI.CKSMixedGeometry.local_norm_iteratedFDeriv_mul line 1410
146. lemma OAI.CKSMixedGeometry.LogJetBound.mul line 1430
147. lemma OAI.CKSMixedGeometry.LogJetBound.of_source line 1465
148. def OAI.CKSMixedGeometry.radialEigenvalue line 1488
149. lemma OAI.CKSMixedGeometry.radialEigenvalue_nil line 1492
150. lemma OAI.CKSMixedGeometry.radialEigenvalue_cons line 1496
151. lemma OAI.CKSMixedGeometry.coordinateIter_radiusPower line 1502
152. lemma OAI.CKSMixedGeometry.abs_radialEigenvalue line 1513
153. lemma OAI.CKSMixedGeometry.radiusPower_logJet line 1525
154. lemma OAI.CKSMixedGeometry.compactified_uniform_logJet line 1547
155. theorem OAI.CKSMixedGeometry.weighted_compactified_logJet line 1559
156. def OAI.CKSMixedGeometry.boundaryProjection line 1585
157. lemma OAI.CKSMixedGeometry.boundaryProjection_zero line 1589
158. lemma OAI.CKSMixedGeometry.boundaryProjection_sub line 1592
159. lemma OAI.CKSMixedGeometry.boundaryProjection_idem line 1595
160. lemma OAI.CKSMixedGeometry.norm_sub_boundaryProjection line 1599
161. lemma OAI.CKSMixedGeometry.angular_D_vanishes_boundary line 1603
162. lemma OAI.CKSMixedGeometry.backwardScaledIter_vanishes_boundary line 1617
163. lemma OAI.CKSMixedGeometry.coefficient_difference_vanishes line 1629
164. theorem OAI.CKSMixedGeometry.compactified_vanishing_jets line 1646
165. structure OAI.CKSMixedGeometry.FiniteLogDecay line 1712
166. lemma OAI.CKSMixedGeometry.FiniteLogDecay.germ_congr line 1719
167. lemma OAI.CKSMixedGeometry.FiniteLogDecay.congr line 1727
168. lemma OAI.CKSMixedGeometry.FiniteLogDecay.add line 1729
169. lemma OAI.CKSMixedGeometry.FiniteLogDecay.neg line 1741
170. lemma OAI.CKSMixedGeometry.FiniteLogDecay.sub line 1749
171. lemma OAI.CKSMixedGeometry.FiniteLogDecay.mul line 1753
172. lemma OAI.CKSMixedGeometry.FiniteLogDecay.weaken line 1760
173. lemma OAI.CKSMixedGeometry.FiniteLogDecay.zero line 1769
174. lemma OAI.CKSMixedGeometry.FiniteLogDecay.sum line 1774
175. lemma OAI.CKSMixedGeometry.FiniteLogDecay.radiusPower line 1784
176. lemma OAI.CKSMixedGeometry.FiniteLogDecay.compactified line 1789
177. lemma OAI.CKSMixedGeometry.FiniteLogDecay.vanishing line 1797
178. lemma OAI.CKSMixedGeometry.FiniteLogDecay.mono line 1827
179. lemma OAI.CKSMixedGeometry.FiniteLogDecay.compactified_difference line 1832
180. lemma OAI.CKSMixedGeometry.FiniteLogDecay.weighted_compactified line 1842
181. lemma OAI.CKSMixedGeometry.FiniteLogDecay.weighted_difference line 1848
182. theorem OAI.CKSLorentz.lorentz_source_remainder_decay line 1869
183. lemma OAI.CKSLorentz.radiusPower_add line 1911
184. lemma OAI.CKSLorentz.logLorentzChart_radial_coeff line 1915
185. lemma OAI.CKSLorentz.logLorentzChart_angular_coeff line 1921
186. lemma OAI.CKSLorentz.radiusPower_lorentz line 1928
187. def OAI.CKSLorentz.compactLeadingCoefficient line 1933
188. lemma OAI.CKSLorentz.ordinaryLeadingComponent_log_lorentz line 1938
189. lemma OAI.CKSLorentz.weighted_ordinary_leading line 1946
190. lemma OAI.CKSLorentz.compactLeadingCoefficient_regular line 1956
191. lemma OAI.CKSLorentz.lorentz_radius_weight_decay line 1967
192. lemma OAI.CKSLorentz.source_remainder_lorentz_decay line 2003
193. lemma OAI.CKSLorentz.weighted_source_remainder_lorentz_decay line 2016
194. lemma OAI.CKSLorentz.weighted_source_leading_remainder line 2031
195. def OAI.CKSLorentz.squareRadialChart line 2059
196. def OAI.CKSLorentz.squaredCompactSpatial line 2061
197. def OAI.CKSLorentz.squaredLorentzCoefficients line 2065
198. lemma OAI.CKSLorentz.squareRadialChart_smooth line 2070
199. lemma OAI.CKSLorentz.angularProjection_squareRadialChart line 2079
200. lemma OAI.CKSLorentz.squaredCompactSpatial_square line 2084
201. lemma OAI.CKSLorentz.compactLorentzCoefficients_squared line 2089
202. lemma OAI.CKSLorentz.squaredCompactSpatial_contDiffAt line 2096
203. lemma OAI.CKSLorentz.squaredLorentzCoefficients_contDiffAt line 2106
204. lemma OAI.CKSLorentz.squaredLorentzCoefficients_regular line 2122
205. def OAI.CKSLorentz.squareRadialDerivative line 2147
206. lemma OAI.CKSLorentz.squareRadialChart_hasFDerivAt line 2151
207. lemma OAI.CKSLorentz.squareRadialDerivative_zero line 2166
208. lemma OAI.CKSLorentz.D_zero_square_pullback line 2173
209. def OAI.CKSLorentz.lorentzLogJac line 2184
210. def OAI.CKSLorentz.lorentzRadialJacCorrection line 2189
211. lemma OAI.CKSLorentz.lorentzLogJac_radial line 2193
212. lemma OAI.CKSLorentz.lorentzLogJac_contDiffAt line 2209
213. lemma OAI.CKSLorentz.lorentzRadialJacCorrection_contDiffAt line 2218
214. lemma OAI.CKSLorentz.D_logLorentzChart line 2228
215. lemma OAI.CKSLorentz.lorentzLogJac_radial_of_differentiable line 2263
216. lemma OAI.CKSLorentz.lorentzLogJac_radial_germ line 2277
217. lemma OAI.CKSLorentz.lorentzLogJac_radial_log_germ line 2291
218. theorem OAI.CKSLorentz.lorentz_jacobian_decay line 2320
219. def OAI.CKSMixedGeometry.logTensorRate line 2354
220. def OAI.CKSMixedGeometry.logJacRate line 2357
221. def OAI.CKSMixedGeometry.logCovariantPullback line 2359
222. lemma OAI.CKSMixedGeometry.tensor_rate_inequality line 2362
223. theorem OAI.CKSMixedGeometry.finite_log_tensor_pullback_rates line 2368
224. def OAI.CKSMixedGeometry.angularLeadingEntry line 2391
225. def OAI.CKSMixedGeometry.transformedAngularLeading line 2394
226. lemma OAI.CKSMixedGeometry.angular_leading_term_decay line 2397
227. theorem OAI.CKSMixedGeometry.finite_log_tensor_angular_leading line 2443
228. lemma OAI.CKSMixedGeometry.radial_leading_00_decay line 2479
229. lemma OAI.CKSMixedGeometry.radial_off_diagonal_entry_decay line 2511
230. theorem OAI.CKSMixedGeometry.finite_log_tensor_radial_leading line 2524
231. def OAI.CKSMixedGeometry.radialIndexWeight line 2561
232. structure OAI.CKSLorentz.LorentzChartDomain line 2574
233. def OAI.CKSLorentz.oldLogTensor line 2585
234. def OAI.CKSLorentz.lorentzLogTensor line 2590
235. def OAI.CKSLorentz.compactAngularCoefficient line 2595
236. lemma OAI.CKSLorentz.oldLogTensor_radial_remainder line 2610
237. lemma OAI.CKSLorentz.oldLogTensor_angular_remainder line 2621
238. lemma OAI.CKSLorentz.oldLogTensor_mixed_decay line 2630
239. lemma OAI.CKSLorentz.lorentz_compact_radial_leading_regular line 2644
240. lemma OAI.CKSLorentz.lorentz_compact_angular_leading_regular line 2654
241. lemma OAI.CKSLorentz.oldLogTensor_decay line 2665
242. lemma OAI.CKSLorentz.lorentz_jacobian_sharp_decay line 2706
243. theorem OAI.CKSLorentz.lorentz_CKS_finite_components line 2718
244. def OAI.CKSMixedGeometry.radialLogChart line 2765
245. lemma OAI.CKSMixedGeometry.radialLogChart_logRadiusChart line 2769
246. lemma OAI.CKSMixedGeometry.logRadiusChart_radialLogChart line 2774
247. lemma OAI.CKSMixedGeometry.radialLogChart_contDiffAt line 2779
248. theorem OAI.CKSMixedGeometry.FiniteLogDecay.to_source line 2789
249. theorem OAI.CKSMixedGeometry.FiniteLogDecay.source_of_log line 2817
250. def OAI.CKSLorentz.lorentzOrdinaryTensor line 2854
251. def OAI.CKSLorentz.lorentzRadialLeading line 2859
252. def OAI.CKSLorentz.lorentzAngularLeading line 2863
253. lemma OAI.CKSLorentz.boundary_inverseLogRadiusChart line 2868
254. lemma OAI.CKSLorentz.ordinaryLeadingComponent_log line 2873
255. lemma OAI.CKSLorentz.lorentzOrdinaryTensor_log line 2878
256. lemma OAI.CKSLorentz.lorentzOrdinaryTensor_mixed line 2895
257. lemma OAI.CKSLorentz.lorentzOrdinaryTensor_radial_rough line 2910
258. lemma OAI.CKSLorentz.lorentzOrdinaryTensor_radial_sharp line 2920
259. lemma OAI.CKSLorentz.lorentzOrdinaryTensor_angular_sharp line 2941
260. theorem OAI.CKSLorentz.lorentz_metric_CKS line 2968
261. theorem OAI.CKSLorentz.lorentz_second_CKS line 2983
262. def OAI.CKSMixedGeometry.coordinateTensorPullback line 3010
263. def OAI.CKSMixedGeometry.ordinaryConjugate line 3015
264. lemma OAI.CKSMixedGeometry.chartDerivative_apply line 3029
265. lemma OAI.CKSMixedGeometry.D_logRadius_comp line 3033
266. lemma OAI.CKSMixedGeometry.ordinaryConjugate_differentiableAt line 3046
267. lemma OAI.CKSMixedGeometry.radialFactor_pos line 3054
268. lemma OAI.CKSMixedGeometry.D_ordinaryConjugate line 3057
269. lemma OAI.CKSMixedGeometry.radialFactor_pair line 3080
270. lemma OAI.CKSMixedGeometry.radialFactor_inv_pair line 3086
271. theorem OAI.CKSMixedGeometry.coordinateTensorPullback_log line 3092
272. lemma OAI.CKSMixedGeometry.coordinateTensorPullback_congr line 3119
273. lemma OAI.CKSLorentz.lorentzPolarChart_germ line 3137
274. theorem OAI.CKSLorentz.lorentzOrdinaryTensor_eq_pullback line 3165
275. def OAI.CKSLorentz.boundaryChart line 3191
276. def OAI.CKSLorentz.angularCoordinatePullback line 3194
277. lemma OAI.CKSLorentz.angularProjection_slice line 3211
278. lemma OAI.CKSLorentz.compactPolar_slice line 3215
279. lemma OAI.CKSLorentz.compactScale_boundary line 3219
280. lemma OAI.CKSLorentz.compactAngle_boundary line 3227
281. lemma OAI.CKSLorentz.compactRegion_boundary line 3233
282. lemma OAI.CKSLorentz.compactLorentzCoefficients_boundary line 3240
283. lemma OAI.CKSLorentz.compactLeadingCoefficient_boundary line 3249
284. theorem OAI.CKSLorentz.lorentzRadialLeading_boundary line 3259
285. lemma OAI.CKSLorentz.lorentzLogJac_boundary_angular line 3267
286. theorem OAI.CKSLorentz.lorentzAngularLeading_boundary line 3300
287. lemma OAI.CKSLorentz.lorentzRadialLeading_contDiffAt line 3323
288. lemma OAI.CKSLorentz.lorentzAngularLeading_contDiffAt line 3336
289. def OAI.CKSLorentz.angularLogTail line 3373
290. lemma OAI.CKSLorentz.boundaryProjection_closedBall line 3387
291. lemma OAI.CKSLorentz.inverseLogRadius_mem_closedBall line 3401
292. lemma OAI.CKSLorentz.eventually_full_log_tail line 3414
293. theorem OAI.CKSLorentz.exists_lorentzChartDomain_regular line 3436
294. theorem OAI.CKSLorentz.exists_lorentzChartDomain line 3524
295. theorem OAI.CKSLorentz.stereoDimension line 3554
296. def OAI.CKSLorentz.stereoAngleEquiv line 3558
297. def OAI.CKSLorentz.stereoOrthogonalEquiv line 3561
298. def OAI.CKSLorentz.stereoAngularChart line 3564
299. def OAI.CKSLorentz.stereoAngularExtension line 3567
300. def OAI.CKSLorentz.stereoAmbientDomain line 3570
301. lemma OAI.CKSLorentz.stereoAngularChart_source line 3591
302. lemma OAI.CKSLorentz.stereoAngularChart_target line 3595
303. lemma OAI.CKSLorentz.stereoAngularChart_param line 3599
304. lemma OAI.CKSLorentz.stereoAngularChart_param_smooth line 3603
305. lemma OAI.CKSLorentz.stereoAmbientDomain_open line 3611
306. lemma OAI.CKSLorentz.stereoAngularExtension_smooth line 3614
307. lemma OAI.CKSLorentz.stereoAngularChart_source_domain line 3620
308. lemma OAI.CKSLorentz.stereoAngularExtension_eq line 3627
309. def OAI.CKSLorentz.stereoSmoothPatch line 3630
310. theorem OAI.CKSLorentz.exists_smoothAngularPatch line 3640
311. lemma OAI.CKSLorentz.SmoothAngularPatch.param_sphere line 3649
312. lemma OAI.CKSLorentz.SmoothAngularPatch.param_norm line 3652
313. lemma OAI.CKSLorentz.SmoothAngularPatch.param_contDiffAt line 3655
314. lemma OAI.CKSLorentz.SmoothAngularPatch.sphereRegion_open line 3659
315. lemma OAI.CKSLorentz.SmoothAngularPatch.param_chart line 3663
316. structure OAI.CKSLorentz.BoostPatchEstimates line 3678
317. def OAI.CKSLorentz.boostedDirection line 3708
318. structure OAI.CKSLorentz.GenuineBoostPatch line 3712
319. def OAI.CKSLorentz.spatialTensorPullback line 3735
320. structure OAI.CKSLorentz.SpatialBoostPatch line 3748
321. lemma OAI.CKSMixedGeometry.SourceRemainderOn.mono line 3771
322. lemma OAI.CKSMixedGeometry.angularProjection_radialLogChart line 3776
323. lemma OAI.CKSMixedGeometry.slice_mem_closedBall line 3781
324. lemma OAI.CKSLorentz.SourceCKSComponents.mono line 3800
325. lemma OAI.CKSLorentz.angularRadialTail_subset_log line 3807
326. lemma OAI.CKSLorentz.BoostPatchEstimates.mono_radius line 3816
327. theorem OAI.CKSLorentz.exists_boostPatchEstimates line 3836
328. theorem OAI.CKSLorentz.exists_finite_boost_atlas line 3907
329. def OAI.CKSLorentz.angularJacobian line 3944
330. lemma OAI.CKSLorentz.SmoothAngularPatch.extension_param line 3959
331. lemma OAI.CKSLorentz.SmoothAngularPatch.extension_contDiffAt_param line 3965
332. lemma OAI.CKSLorentz.SmoothAngularPatch.param_fderiv_leftInverse line 3970
333. lemma OAI.CKSLorentz.SmoothAngularPatch.param_fderiv_injective line 3984
334. lemma OAI.CKSLorentz.SmoothAngularPatch.param_tangent line 3994
335. lemma OAI.CKSLorentz.SmoothAngularPatch.roundMetric_posDef line 4010
336. lemma OAI.CKSLorentz.angular_vector_expansion line 4022
337. lemma OAI.CKSLorentz.angularJacobian_apply line 4027
338. lemma OAI.CKSLorentz.polarParam_contDiffAt line 4047
339. lemma OAI.CKSLorentz.polarParam_norm line 4051
340. lemma OAI.CKSLorentz.fderiv_coordinate_expansion line 4055
341. lemma OAI.CKSLorentz.coordinateTensorPullback_polar line 4062
342. lemma OAI.CKSLorentz.polarTensor_covariance line 4078
343. lemma OAI.CKSLorentz.homeomorph_full_tail line 4105
344. theorem OAI.CKSLorentz.hyperbolic_boost_full_tails line 4117
345. lemma OAI.CKSLorentz.angularRadialTail_open line 4139
346. lemma OAI.CKSLorentz.GenuineBoostPatch.spatial_nonzero line 4144
347. lemma OAI.CKSLorentz.GenuineBoostPatch.polar_commutes line 4156
348. lemma OAI.CKSLorentz.GenuineBoostPatch.old_angle line 4173
349. lemma OAI.CKSLorentz.GenuineBoostPatch.chart_contDiffAt line 4184
350. lemma OAI.CKSLorentz.GenuineBoostPatch.tensor_components line 4207
351. lemma OAI.CKSMixedGeometry.scaledIter_congr_germ line 4232
352. lemma OAI.CKSMixedGeometry.SourceRemainderOn.congrOn line 4239
353. lemma OAI.CKSLorentz.SourceCKSComponents.congrOn line 4260
354. theorem OAI.CKSLorentz.exists_lorentzChartDomain_image line 4281
355. lemma OAI.CKSLorentz.SmoothAngularPatch.exists_exact_domain line 4382
356. lemma OAI.CKSLorentz.compactAngle_sphere line 4391
357. lemma OAI.CKSLorentz.boostedDirection_log line 4397
358. theorem OAI.CKSLorentz.exists_genuineBoostPatch line 4424
359. lemma OAI.CKSLorentz.GenuineBoostPatch.mono_radius line 4529
360. theorem OAI.CKSLorentz.exists_finite_genuine_boost_atlas line 4538
361. lemma OAI.CKSLorentz.GenuineBoostPatch.toSpatial line 4576
362. theorem OAI.CKSLorentz.exists_spatialBoostPatch line 4612
363. lemma OAI.CKSLorentz.SpatialBoostPatch.mono_radius line 4629
364. theorem OAI.CKSLorentz.exists_precompact_spatial_boost_atlas line 4647
365. def OAI.CKSLorentz.cksSourceFields line 4689
366. def OAI.CKSLorentz.cksReference line 4703
367. lemma OAI.CKSMixedGeometry.ScaledComponentBound.mono line 4714
368. lemma OAI.CKSMixedGeometry.finite_sourceRemainder_bound line 4719
369. theorem OAI.CKSLorentz.cksSourceFields_bounds line 4740
370. def OAI.CKSLorentz.boostSourceFields line 4788
371. lemma OAI.CKSMixedGeometry.D_translation_invariant line 4806
372. lemma OAI.CKSMixedGeometry.scalarJet_translation_invariant line 4813
373. lemma OAI.CKSMixedGeometry.threeJet_translation_invariant line 4825
374. lemma OAI.CKSMixedGeometry.angularLift_translate line 4834
375. lemma OAI.CKSMixedGeometry.slice_add_radial line 4837
376. lemma OAI.CKSMixedGeometry.actualScalarJet_angularLift_slice line 4842
377. lemma OAI.CKSMixedGeometry.actualThreeJet_angularLift_slice line 4846
378. lemma OAI.CKSMixedGeometry.matrixScalarJets_angularLift_slice line 4850
379. lemma OAI.CKSMixedGeometry.matrixThreeJets_angularLift_slice line 4854
380. lemma OAI.CKSMixedGeometry.angularProjection_slice_eq line 4868
381. lemma OAI.CKSMixedGeometry.actualScalarJet_continuousAt line 4871
382. lemma OAI.CKSMixedGeometry.actualThreeJet_continuousAt line 4884
383. lemma OAI.CKSMixedGeometry.matrixScalarJets_continuousAt line 4890
384. lemma OAI.CKSMixedGeometry.matrixThreeJets_continuousAt line 4897
385. lemma OAI.CKSMixedGeometry.angular_threeJets_continuousOn line 4904
386. lemma OAI.CKSMixedGeometry.angular_scalarJets_continuousOn line 4913
387. theorem OAI.CKSMixedGeometry.compact_angular_source_jets line 4922
388. lemma OAI.CKSLorentz.SmoothAngularPatch.roundMetric_contDiffAt line 4971
389. lemma OAI.CKSMixedGeometry.SourceTensorFields.ComponentBounds.mono line 4989
390. theorem OAI.CKSLorentz.SpatialBoostPatch.uniform_collar_input line 5008
391. def OAI.CKSMixedGeometry.SourceTensorFields.UniformCollarInput line 5066
392. theorem OAI.CKSLorentz.exists_uniform_boost_collar_atlas line 5086
393. abbrev OAI.CKSTensorNaturality.Bilinear line 5131
394. def OAI.CKSTensorNaturality.tensorPullback line 5132
395. def OAI.CKSTensorNaturality.tensorLie line 5135
396. lemma OAI.CKSTensorNaturality.differentiableAt_flip line 5149
397. lemma OAI.CKSTensorNaturality.differentiableAt_bilinearComp line 5156
398. lemma OAI.CKSTensorNaturality.fderiv_bilinear_apply line 5160
399. lemma OAI.CKSTensorNaturality.fderiv_bilinear_const line 5170
400. lemma OAI.CKSTensorNaturality.differentiableAt_tensorPullback line 5175
401. lemma OAI.CKSTensorNaturality.fderiv_tensorPullback line 5193
402. theorem OAI.CKSTensorNaturality.tensorLie_natural line 5213
403. def OAI.CKSAngularGeometry.physicalAngularJet line 5250
404. def OAI.CKSAngularGeometry.physicalAngularScalarJet line 5255
405. lemma OAI.CKSAngularGeometry.angular_frame_covector_contract line 5260
406. lemma OAI.CKSAngularGeometry.metric_inverse_covector_contract line 5275
407. lemma OAI.CKSAngularGeometry.physical_christoffel_lower line 5286
408. lemma OAI.CKSAngularGeometry.inverse_symm_entry line 5294
409. lemma OAI.CKSAngularGeometry.induced_connection_covector line 5300
410. lemma OAI.CKSAngularGeometry.D_angular_sum line 5318
411. lemma OAI.CKSAngularGeometry.D_angular_direction line 5323
412. lemma OAI.CKSAngularGeometry.extracted_leaf_connection line 5331
413. lemma OAI.CKSAngularGeometry.physical_leaf_connection_extracted line 5335
414. lemma OAI.CKSAngularGeometry.angular_frame_tensor_contract line 5348
415. lemma OAI.CKSAngularGeometry.physical_covector_divergence line 5363
416. lemma OAI.CKSAngularGeometry.physical_acceleration_divergence line 5408
417. theorem OAI.CKSAngularGeometry.physical_acceleration_laplacian line 5460
418. def OAI.CKSAngularGeometry.angularTensorFrame line 5495
419. lemma OAI.CKSAngularGeometry.angularFrame_component_diff line 5501
420. lemma OAI.CKSAngularGeometry.D_angularTensorFrame line 5509
421. lemma OAI.CKSAngularGeometry.induced_tensor_connection_left line 5537
422. lemma OAI.CKSAngularGeometry.induced_tensor_connection_right line 5556
423. lemma OAI.CKSAngularGeometry.physical_leaf_connection_direct line 5575
424. lemma OAI.CKSAngularGeometry.physical_leaf_tensor_covariant line 5588
425. theorem OAI.CKSAngularGeometry.physical_leaf_tensor_divergence line 5614
426. lemma OAI.CKSAngularGeometry.foliationNormal_succ line 5664
427. lemma OAI.CKSAngularGeometry.tangential_frame_covector_expansion line 5668
428. lemma OAI.CKSAngularGeometry.adaptedFrame_normal_bracket line 5699
429. lemma OAI.CKSAngularGeometry.physical_normal_tangential_connection line 5727
430. theorem OAI.CKSAngularGeometry.physical_normal_covector_lie line 5755
431. def OAI.CKSAngularGeometry.leafTensorTrace line 5802
432. def OAI.CKSAngularGeometry.leafTensorTraceFree line 5804
433. lemma OAI.CKSAngularGeometry.foliationTensor_hermitian line 5806
434. lemma OAI.CKSAngularGeometry.metricPair_foliationTensor_normal line 5810
435. lemma OAI.CKSAngularGeometry.metricPair_foliationTensor_mixed line 5817
436. lemma OAI.CKSAngularGeometry.frameTensorData_eta line 5837
437. lemma OAI.CKSAngularGeometry.frameTensorDerivative_eta line 5842
438. lemma OAI.CKSAngularGeometry.foliation_frame_tensor_eta line 5848
439. lemma OAI.CKSAngularGeometry.foliation_frame_tensor_tangential line 5858
440. lemma OAI.CKSAngularGeometry.angularTensorFrame_trace line 5868
441. lemma OAI.CKSAngularGeometry.angularTensorFrame_metric line 5876
442. lemma OAI.CKSAngularGeometry.angularTensorFrame_traceFree line 5884
443. lemma OAI.CKSAngularGeometry.foliation_frame_tensor_trace line 5895
444. lemma OAI.CKSAngularGeometry.tensor_tau_entry line 5907
445. lemma OAI.CKSAngularGeometry.foliation_frame_tensor_tau line 5912
446. lemma OAI.CKSAngularGeometry.frameTensorDerivative_L line 5933
447. lemma OAI.CKSAngularGeometry.frameTensorDerivative_p line 5938
448. lemma OAI.CKSAngularGeometry.frameTensorDerivative_tau line 5946
449. lemma OAI.CKSAngularGeometry.foliationTensor_differentiableAt line 5969
450. lemma OAI.CKSAngularGeometry.leafTensorTrace_contDiffAt line 5996
451. lemma OAI.CKSAngularGeometry.leafTensorTraceFree_contDiffAt line 6017
452. lemma OAI.CKSAngularGeometry.leafConnection_skew line 6035
453. theorem OAI.CKSAngularGeometry.physical_eta_divergence line 6039
454. theorem OAI.CKSAngularGeometry.physical_tau_divergence line 6075
455. theorem OAI.CKSAngularGeometry.physical_eta_normal_lie line 6104
456. lemma OAI.CKSAngularGeometry.angularTensorFrame_pair line 6140
457. lemma OAI.CKSAngularGeometry.angularTensorFrame_covector line 6159
458. lemma OAI.CKSAngularGeometry.physical_shear_components line 6178
459. lemma OAI.CKSAngularGeometry.shearNormSq_sum line 6193
460. lemma OAI.CKSAngularGeometry.tauNormSq_sum line 6200
461. lemma OAI.CKSAngularGeometry.shearTau_sum line 6205
462. lemma OAI.CKSAngularGeometry.physical_shear_norm line 6211
463. lemma OAI.CKSAngularGeometry.physical_tau_norm line 6225
464. lemma OAI.CKSAngularGeometry.physical_shear_tau line 6237
465. lemma OAI.CKSAngularGeometry.physical_eta_norm line 6253
466. lemma OAI.CKSAngularGeometry.physical_eta_acceleration line 6266
467. lemma OAI.CKSAngularGeometry.accelTensor_traceFree line 6285
468. lemma OAI.CKSAngularGeometry.foliation_frame_tensor_L line 6289
469. lemma OAI.CKSAngularGeometry.physical_mean_curvature_C1 line 6307
470. lemma OAI.CKSAngularGeometry.physical_normal_mean line 6322
471. lemma OAI.CKSAngularGeometry.physical_tensor_derivative_L line 6359
472. lemma OAI.CKSAngularGeometry.physical_tensor_derivative_p line 6371
473. lemma OAI.CKSAngularGeometry.physical_tensor_tangential_trace_derivative line 6388
474. lemma OAI.CKSAngularGeometry.physical_acceleration_tensor line 6413
475. abbrev OAI.CKSLeafCalculus.A line 6448
476. abbrev OAI.CKSLeafCalculus.P line 6449
477. abbrev OAI.CKSLeafCalculus.Vect line 6450
478. abbrev OAI.CKSLeafCalculus.Symbols line 6451
479. def OAI.CKSLeafCalculus.lift line 6453
480. def OAI.CKSLeafCalculus.delta line 6455
481. lemma OAI.CKSLeafCalculus.delta_expansion line 6457
482. lemma OAI.CKSLeafCalculus.delta_mul line 6462
483. lemma OAI.CKSLeafCalculus.delta_add line 6467
484. lemma OAI.CKSLeafCalculus.delta_sum line 6472
485. def OAI.CKSLeafCalculus.bracket line 6477
486. lemma OAI.CKSLeafCalculus.delta_moving line 6480
487. lemma OAI.CKSLeafCalculus.delta_commutator line 6495
488. def OAI.CKSLeafCalculus.nabla line 6506
489. def OAI.CKSLeafCalculus.curvature line 6509
490. def OAI.CKSLeafCalculus.coordCurvature line 6513
491. lemma OAI.CKSLeafCalculus.delta_nabla line 6518
492. theorem OAI.CKSLeafCalculus.curvature_coordinate line 6558
493. lemma OAI.CKSLeafCalculus.nabla_congr line 6575
494. lemma OAI.CKSLeafCalculus.nabla_expansion line 6584
495. lemma OAI.CKSLeafCalculus.nabla_direction_expansion line 6596
496. lemma OAI.CKSLeafCalculus.nabla_torsion line 6603
497. def OAI.CKSLeafCalculus.frameCurvature line 6611
498. lemma OAI.CKSLeafCalculus.nabla_second_frame line 6617
499. theorem OAI.CKSLeafCalculus.curvature_frame line 6633
500. lemma OAI.CKSAngularGeometry.physical_component_diff line 6666
501. lemma OAI.CKSAngularGeometry.physical_inverse_component_diff line 6670
502. lemma OAI.CKSAngularGeometry.physical_D_determinant line 6681
503. theorem OAI.CKSAngularGeometry.physical_derivative_inverse line 6690
504. lemma OAI.CKSAngularGeometry.physical_D_sum line 6708
505. lemma OAI.CKSAngularGeometry.physical_D_div_const line 6713
506. lemma OAI.CKSAngularGeometry.physical_first_diff line 6720
507. theorem OAI.CKSAngularGeometry.physical_derivative_connection line 6724
508. def OAI.CKSLeafCalculus.pair line 6766
509. lemma OAI.CKSLeafCalculus.pair_frame_sum line 6768
510. lemma OAI.CKSLeafCalculus.inverse_metric_trace line 6778
511. theorem OAI.CKSLeafCalculus.scalar_frame_contraction line 6785
512. lemma OAI.CKSAngularGeometry.lift_angularFrame line 6816
513. lemma OAI.CKSAngularGeometry.leafConnection_derivative line 6823
514. lemma OAI.CKSAngularGeometry.physical_christoffel_differentiable line 6830
515. lemma OAI.CKSAngularGeometry.physical_christoffel_symmetric line 6846
516. lemma OAI.CKSAngularGeometry.physical_nabla_angularFrame line 6861
517. theorem OAI.CKSAngularGeometry.physical_leaf_curvature_coordinates line 6875
518. lemma OAI.CKSAngularGeometry.physical_coordinate_scalar line 6937
519. lemma OAI.CKSAngularGeometry.angularFrame_orthonormal_pair line 6983
520. theorem OAI.CKSAngularGeometry.physical_leaf_scalar line 6992
521. theorem OAI.CKSAngularGeometry.physical_source_constraints line 7051
522. lemma OAI.CKSAngularGeometry.sourceChi_contDiffAt line 7140
523. theorem OAI.CKSAngularGeometry.physical_source_mass_identity line 7156
524. def OAI.CKSAngularGeometry.physicalEnergy line 7217
525. def OAI.CKSAngularGeometry.physicalDEC line 7222
526. def OAI.CKSAngularGeometry.sourceH line 7227
527. def OAI.CKSAngularGeometry.sourceP line 7230
528. def OAI.CKSAngularGeometry.sourceB line 7232
529. def OAI.CKSAngularGeometry.sourceQ line 7235
530. def OAI.CKSAngularGeometry.sourceZ line 7242
531. theorem OAI.CKSAngularGeometry.physical_source_momentum_norm line 7251
532. theorem OAI.CKSAngularGeometry.physical_source_DEC_iff line 7281
533. def OAI.CKSAngularGeometry.sourceD line 7309
534. def OAI.CKSAngularGeometry.sourceMass line 7313
535. def OAI.CKSAngularGeometry.physicalBaseLapse line 7317
536. def OAI.CKSAngularGeometry.physicalMomentumInput line 7319
537. def OAI.CKSAngularGeometry.physicalNullInput line 7335
538. lemma OAI.CKSAngularGeometry.inverse_radius_smul_cancel line 7351
539. lemma OAI.CKSAngularGeometry.physicalBaseLapse_ne line 7356
540. lemma OAI.CKSAngularGeometry.physicalBaseLapse_eq line 7359
541. lemma OAI.CKSAngularGeometry.physical_input_L line 7370
542. lemma OAI.CKSAngularGeometry.physical_input_t line 7379
543. lemma OAI.CKSAngularGeometry.physical_input_lapseJet line 7387
544. lemma OAI.CKSAngularGeometry.physical_input_speed line 7396
545. lemma OAI.CKSAngularGeometry.physical_input_d line 7406
546. lemma OAI.CKSAngularGeometry.physical_input_mean line 7412
547. lemma OAI.CKSAngularGeometry.physical_input_ratio line 7420
548. lemma OAI.CKSAngularGeometry.physical_input_acceleration line 7433
549. lemma OAI.CKSAngularGeometry.rescale_composition line 7458
550. lemma OAI.CKSAngularGeometry.rescale_one line 7466
551. lemma OAI.CKSAngularGeometry.physical_input_q line 7473
552. lemma OAI.CKSAngularGeometry.physical_input_s line 7481
553. lemma OAI.CKSAngularGeometry.physical_input_eta line 7486
554. lemma OAI.CKSAngularGeometry.physical_input_tau line 7491
555. lemma OAI.CKSAngularGeometry.physical_input_X line 7497
556. lemma OAI.CKSAngularGeometry.physical_input_Er line 7503
557. lemma OAI.CKSAngularGeometry.physical_input_tau_value line 7508
558. lemma OAI.CKSAngularGeometry.physical_input_eta_value line 7515
559. lemma OAI.CKSAngularGeometry.physical_normal_derivative line 7521
560. lemma OAI.CKSAngularGeometry.physical_input_Np line 7531
561. lemma OAI.CKSAngularGeometry.physical_input_Q line 7546
562. lemma OAI.CKSAngularGeometry.physical_input_Z line 7557
563. lemma OAI.CKSAngularGeometry.lapseLaplacian_lapse_smul line 7582
564. lemma OAI.CKSAngularGeometry.physical_input_massrow line 7593
565. lemma OAI.CKSAngularGeometry.physical_input_smallNull_formula line 7610
566. lemma OAI.CKSAngularGeometry.physical_input_smallNull line 7659
567. lemma OAI.CKSAngularGeometry.physical_input_energy line 7703
568. theorem OAI.CKSAngularGeometry.physical_normalized_DEC_iff line 7726
569. def OAI.CKSAngularGeometry.leafRadialRate line 7768
570. def OAI.CKSAngularGeometry.radialExpansion line 7775
571. def OAI.CKSAngularGeometry.radialMassRadical line 7778
572. def OAI.CKSAngularGeometry.radialMassLapse line 7781
573. def OAI.CKSAngularGeometry.radialTangential line 7785
574. def OAI.CKSAngularGeometry.leafBilinear line 7800
575. def OAI.CKSAngularGeometry.radialFlow line 7805
576. lemma OAI.CKSAngularGeometry.leafBilinear_apply line 7817
577. lemma OAI.CKSAngularGeometry.leafBilinear_apply_basis line 7820
578. lemma OAI.CKSAngularGeometry.leafBilinear_basis_apply line 7826
579. lemma OAI.CKSAngularGeometry.leafBilinear_basis line 7830
580. lemma OAI.CKSAngularGeometry.leafBilinear_differentiableAt line 7834
581. lemma OAI.CKSAngularGeometry.radialFlow_succ line 7846
582. lemma OAI.CKSAngularGeometry.radialFlow_differentiableAt line 7849
583. lemma OAI.CKSAngularGeometry.fderiv_radialFlow_succ line 7853
584. theorem OAI.CKSAngularGeometry.leafRadialRate_eq_tensorLie line 7876
585. def OAI.CKSAngularGeometry.angularBlock line 7903
586. def OAI.CKSAngularGeometry.angularCongruence line 7906
587. def OAI.CKSAngularGeometry.angularCovector line 7908
588. lemma OAI.CKSAngularGeometry.foliationMetric_covariant line 7919
589. lemma OAI.CKSAngularGeometry.foliationTensor_covariant line 7931
590. theorem OAI.CKSAngularGeometry.foliation_reconstruction_covariant line 7943
591. lemma OAI.CKSAngularGeometry.angularCongruence_inverse line 7950
592. lemma OAI.CKSAngularGeometry.leafTensorTrace_covariant line 7958
593. theorem OAI.CKSAngularGeometry.leaf_trace_covariant line 7968
594. def OAI.CKSAngularGeometry.angularChange line 7986
595. def OAI.CKSAngularGeometry.angularJacobian line 7989
596. def OAI.CKSAngularGeometry.angularMetricPullback line 7992
597. lemma OAI.CKSAngularGeometry.angularChange_zero line 8004
598. lemma OAI.CKSAngularGeometry.angularChange_succ line 8006
599. lemma OAI.CKSAngularGeometry.angularChange_contDiffAt line 8008
600. lemma OAI.CKSAngularGeometry.angularChange_differentiableAt line 8020
601. lemma OAI.CKSAngularGeometry.fderiv_angularChange_zero line 8032
602. lemma OAI.CKSAngularGeometry.fderiv_angularChange_succ line 8042
603. lemma OAI.CKSAngularGeometry.angularJacobian_mulVec line 8054
604. lemma OAI.CKSAngularGeometry.fderiv_angularChange_basis line 8067
605. lemma OAI.CKSAngularGeometry.leafBilinear_congruence line 8090
606. lemma OAI.CKSAngularGeometry.leafBilinear_angularPullback line 8097
607. lemma OAI.CKSAngularGeometry.radialFlow_zero line 8112
608. lemma OAI.CKSAngularGeometry.angularProjection_radialFlow line 8114
609. lemma OAI.CKSAngularGeometry.radialFlow_angular_related line 8118
610. lemma OAI.CKSAngularGeometry.tensorLie_angular_expansion line 8128
611. lemma OAI.CKSAngularGeometry.leafRadialRate_angular_natural line 8148
612. theorem OAI.CKSAngularGeometry.radial_lapse_angular_natural line 8186
613. lemma OAI.CKSAngularGeometry.leafTensorTrace_add line 8218
614. lemma OAI.CKSAngularGeometry.leafTensorTrace_sub line 8222
615. lemma OAI.CKSAngularGeometry.leafTensorTrace_smul line 8226
616. lemma OAI.CKSAngularGeometry.leafTensorTrace_self line 8230
617. lemma OAI.CKSAngularGeometry.leafTensorTrace_traceFree line 8234
618. lemma OAI.CKSAngularGeometry.sourceChi_radialRate line 8240
619. lemma OAI.CKSAngularGeometry.sourceH_radialExpansion line 8244
620. lemma OAI.CKSAngularGeometry.sourceP_radialTangential line 8252
621. lemma OAI.CKSAngularGeometry.radialMassLapse_pos line 8259
622. lemma OAI.CKSAngularGeometry.sourceH_radialMassLapse line 8265
623. theorem OAI.CKSAngularGeometry.physical_radial_reconstruction line 8273
624. def OAI.CKSAngularGeometry.radiusLogPoint line 8311
625. def OAI.CKSAngularGeometry.logPointDerivative line 8314
626. lemma OAI.CKSAngularGeometry.radiusLogPoint_smoothAt line 8318
627. lemma OAI.CKSAngularGeometry.radiusLogPoint_hasFDerivAt line 8330
628. lemma OAI.CKSAngularGeometry.logPointDerivative_basis line 8342
629. lemma OAI.CKSAngularGeometry.D_radiusLogPoint line 8352
630. lemma OAI.CKSAngularGeometry.radiusLogPoint_slice line 8363
631. lemma OAI.CKSAngularGeometry.radiusLogPoint_logRadiusChart line 8370
632. lemma OAI.CKSAngularGeometry.logRadiusChart_radiusLogPoint line 8377
633. lemma OAI.CKSAngularGeometry.physicalAngularScalarJet_slice line 8384
634. lemma OAI.CKSAngularGeometry.physicalAngularJet_slice line 8389
635. structure OAI.CKSAngularSlice.LogCollarData.SmoothAt line 8412
636. lemma OAI.CKSAngularSlice.LogCollarData.SmoothAt.regularAt line 8423
637. def OAI.CKSAngularGeometry.physicalCollarGamma line 8440
638. def OAI.CKSAngularGeometry.physicalCollarShift line 8442
639. def OAI.CKSAngularGeometry.physicalCollarT line 8444
640. def OAI.CKSAngularGeometry.physicalCollarF line 8446
641. def OAI.CKSAngularGeometry.physicalCollarL line 8448
642. def OAI.CKSAngularGeometry.physicalCollarEta line 8450
643. def OAI.CKSAngularGeometry.physicalCollarRawTau line 8453
644. def OAI.CKSAngularGeometry.physicalCollarU line 8455
645. def OAI.CKSAngularGeometry.physicalCollarTangential line 8458
646. def OAI.CKSAngularGeometry.physicalCollarMetric line 8460
647. def OAI.CKSAngularGeometry.physicalCollarTensor line 8462
648. def OAI.CKSAngularGeometry.physicalCollarFrame line 8465
649. lemma OAI.CKSAngularSlice.radialLift_smoothAt line 8480
650. lemma OAI.CKSAngularSlice.collarWeight_smoothAt line 8484
651. lemma OAI.CKSAngularSlice.collarQ_smoothAt line 8488
652. lemma OAI.CKSAngularSlice.collarShift_smoothAt line 8492
653. lemma OAI.CKSAngularSlice.collarT_smoothAt line 8496
654. lemma OAI.CKSAngularSlice.collarLb_smoothAt line 8500
655. lemma OAI.CKSAngularSlice.collarL_smoothAt line 8504
656. lemma OAI.CKSAngularSlice.collarF_smoothAt line 8511
657. lemma OAI.CKSAngularSlice.collarEta_smoothAt line 8517
658. lemma OAI.CKSAngularSlice.collarQ_regularAt line 8521
659. lemma OAI.CKSAngularSlice.collarShift_regularAt line 8526
660. lemma OAI.CKSAngularSlice.LogCollarData.SmoothAt.eventually_regularAt line 8531
661. lemma OAI.CKSAngularGeometry.physicalCollarGamma_smoothAt line 8552
662. lemma OAI.CKSAngularGeometry.physicalCollarShift_smoothAt line 8558
663. lemma OAI.CKSAngularGeometry.physicalCollarT_smoothAt line 8563
664. lemma OAI.CKSAngularGeometry.physicalCollarF_smoothAt line 8568
665. lemma OAI.CKSAngularGeometry.physicalCollarL_smoothAt line 8573
666. lemma OAI.CKSAngularGeometry.physicalCollarEta_smoothAt line 8578
667. lemma OAI.CKSAngularGeometry.physicalCollarRawTau_smoothAt line 8584
668. lemma OAI.CKSAngularGeometry.physicalCollarGamma_regularAt line 8591
669. lemma OAI.CKSAngularGeometry.physicalCollarShift_regularAt line 8598
670. structure OAI.CKSAngularSlice.LogCollarData.AngularRelatedAt line 8614
671. lemma OAI.CKSAngularGeometry.angularProjection_radiusLogPoint line 8634
672. lemma OAI.CKSAngularGeometry.angularJacobian_radiusLogPoint line 8638
673. lemma OAI.CKSAngularGeometry.angularChange_radiusLogPoint line 8642
674. lemma OAI.CKSAngularGeometry.angularCongruence_add line 8645
675. lemma OAI.CKSAngularGeometry.angularCongruence_smul line 8648
676. lemma OAI.CKSAngularGeometry.angularCovector_smul line 8651
677. lemma OAI.CKSAngularGeometry.physicalCollarGamma_angular_covariant line 8654
678. lemma OAI.CKSAngularGeometry.physicalCollarShift_angular_covariant line 8661
679. lemma OAI.CKSAngularGeometry.physicalCollarT_angular_covariant line 8671
680. lemma OAI.CKSAngularGeometry.physicalCollarF_angular_covariant line 8678
681. lemma OAI.CKSAngularGeometry.physicalCollarL_angular_covariant line 8685
682. lemma OAI.CKSAngularGeometry.physicalCollarEta_angular_covariant line 8692
683. lemma OAI.CKSAngularGeometry.physicalCollarRawTau_angular_covariant line 8700
684. lemma OAI.CKSAngularGeometry.physicalCollarU_angular_covariant line 8718
685. lemma OAI.CKSAngularGeometry.physicalCollarTangential_angular_covariant line 8743
686. theorem OAI.CKSAngularGeometry.physicalCollar_angular_covariant line 8756
687. lemma OAI.CKSAngularGeometry.physicalCollarGamma_slice line 8793
688. lemma OAI.CKSAngularGeometry.physicalCollarShift_slice line 8799
689. lemma OAI.CKSAngularGeometry.physicalCollarT_slice line 8806
690. lemma OAI.CKSAngularGeometry.physicalCollarF_slice line 8814
691. lemma OAI.CKSAngularGeometry.physicalCollarL_slice line 8820
692. lemma OAI.CKSAngularGeometry.physicalCollarEta_slice line 8829
693. lemma OAI.CKSAngularGeometry.physicalCollarRawTau_slice line 8837
694. lemma OAI.CKSAngularGeometry.physicalCollarGamma_radial line 8855
695. lemma OAI.CKSAngularGeometry.physicalCollarGamma_angular line 8884
696. lemma OAI.CKSAngularGeometry.physicalCollarShift_angular line 8907
697. lemma OAI.CKSAngularGeometry.physicalCollarRadialRate line 8937
698. lemma OAI.CKSAngularGeometry.leafTensorTrace_eq line 8964
699. lemma OAI.CKSAngularGeometry.leafTensorTrace_metric_smul line 8968
700. lemma OAI.CKSAngularGeometry.leafTensorTraceFree_add line 8974
701. lemma OAI.CKSAngularGeometry.leafTensorTraceFree_smul line 8982
702. lemma OAI.CKSAngularGeometry.leafTensorTraceFree_self line 8990
703. lemma OAI.CKSAngularGeometry.leafTensorTraceFree_metric_smul line 8995
704. lemma OAI.CKSAngularGeometry.traceFreeField_eq line 9003
705. lemma OAI.CKSAngularGeometry.physicalCollarGamma_pos_iff line 9010
706. lemma OAI.CKSAngularGeometry.physicalCollarExpansion_slice line 9021
707. lemma OAI.CKSAngularGeometry.physicalCollarShear_unscaled line 9035
708. lemma OAI.CKSAngularGeometry.leafRadialRate_smoothAt line 9064
709. lemma OAI.CKSAngularGeometry.radialExpansion_smoothAt line 9083
710. lemma OAI.CKSAngularGeometry.radialMassRadical_smoothAt line 9090
711. lemma OAI.CKSAngularGeometry.radialMassLapse_smoothAt line 9097
712. lemma OAI.CKSAngularGeometry.radialTangential_smoothAt line 9107
713. lemma OAI.CKSAngularGeometry.lapseNormalizedField_rad line 9124
714. lemma OAI.CKSAngularGeometry.physicalCollarRadical_slice line 9133
715. lemma OAI.CKSAngularGeometry.physicalCollarRadical_pos_iff line 9144
716. lemma OAI.CKSAngularGeometry.physicalCollarU_slice line 9151
717. lemma OAI.CKSAngularGeometry.physicalCollarU_coefficient line 9166
718. lemma OAI.CKSAngularGeometry.physicalCollarTangential_trace line 9184
719. lemma OAI.CKSAngularGeometry.radialTangential_traceFree line 9190
720. lemma OAI.CKSAngularGeometry.physicalCollarTau_slice line 9199
721. lemma OAI.CKSAngularSlice.collarT_regularAt line 9224
722. lemma OAI.CKSAngularSlice.collarF_regularAt line 9229
723. lemma OAI.CKSAngularSlice.collarEta_regularAt line 9237
724. lemma OAI.CKSAngularGeometry.physicalCollarT_radial line 9253
725. lemma OAI.CKSAngularGeometry.physicalCollarEta_radial line 9267
726. lemma OAI.CKSAngularGeometry.physicalCollarF_radial line 9287
727. lemma OAI.CKSAngularGeometry.physicalAngularScalarJet_congr line 9318
728. lemma OAI.CKSAngularGeometry.D_eventually_congr line 9331
729. lemma OAI.CKSAngularGeometry.radial_positive_eventually line 9336
730. lemma OAI.CKSAngularGeometry.radial_reconstruction_eventually line 9347
731. lemma OAI.CKSAngularGeometry.physicalCollar_positive_eventually line 9368
732. lemma OAI.CKSAngularGeometry.physicalCollar_reconstruction_eventually line 9381
733. lemma OAI.CKSAngularGeometry.rescale_eq_smul line 9408
734. lemma OAI.CKSAngularGeometry.radius_inverse_smul_cancel line 9410
735. lemma OAI.CKSAngularGeometry.actualScalarJet_affine line 9415
736. lemma OAI.CKSAngularGeometry.physicalAngularScalarJet_affine line 9420
737. lemma OAI.CKSAngularGeometry.physicalCollarGamma_jet line 9426
738. lemma OAI.CKSAngularGeometry.physicalCollarT_jet line 9444
739. lemma OAI.CKSAngularGeometry.physicalCollarL_jet line 9457
740. lemma OAI.CKSAngularSlice.LogCollarData.SmoothAt.angular_regular line 9481
741. lemma OAI.CKSAngularGeometry.physicalAngularScalarJet_scaled line 9495
742. lemma OAI.CKSAngularGeometry.physicalCollarShift_jets line 9502
743. lemma OAI.CKSAngularGeometry.physicalCollarEta_jets line 9517
744. lemma OAI.CKSAngularGeometry.physicalCollarEta_radial_scaled line 9533
745. lemma OAI.CKSAngularGeometry.physicalCollarF_jet line 9542
746. lemma OAI.CKSAngularGeometry.physicalCollarTr_jet line 9554
747. lemma OAI.CKSAngularGeometry.physicalCollarU_smoothAt line 9582
748. lemma OAI.CKSAngularGeometry.physicalCollarTangential_smoothAt line 9592
749. lemma OAI.CKSAngularGeometry.physicalCollarU_jet line 9599
750. lemma OAI.CKSAngularGeometry.physicalCollarExpansion_jet line 9639
751. lemma OAI.CKSAngularGeometry.physicalCollarTau_jets line 9676
752. lemma OAI.CKSAngularGeometry.physicalCollarShear_scaled line 9704
753. theorem OAI.CKSAngularGeometry.physical_collar_null_realization line 9728
754. lemma OAI.CKSAngularGeometry.leafTensorTraceFree_isHermitian line 9788
755. lemma OAI.CKSAngularGeometry.physicalCollarTangential_isHermitian line 9791
756. theorem OAI.CKSAngularGeometry.physical_collar_DEC_iff line 9797
757. lemma OAI.CKSAngularGeometry.positiveAngular_posDef line 9846
758. lemma OAI.CKSAngularGeometry.positiveAngular_continuousAt line 9869
759. lemma OAI.CKSAngularGeometry.posDef_eventually_of_symmetric line 9878
760. lemma OAI.CKSAngularGeometry.physicalCollarGamma_isHermitian line 9885
761. lemma OAI.CKSAngularGeometry.physicalCollarGamma_eventually_posDef line 9891
762. def OAI.CKSMixedGeometry.sourceFrame line 9912
763. lemma OAI.CKSMixedGeometry.sourceLapse_pos line 9915
764. lemma OAI.CKSMixedGeometry.source_metric_foliation line 9918
765. lemma OAI.CKSMixedGeometry.source_tensor_foliation line 9938
766. lemma OAI.CKSMixedGeometry.source_radialExpansion_eq line 9972
767. lemma OAI.CKSMixedGeometry.source_radialMassRadical_eq line 9978
768. lemma OAI.CKSMixedGeometry.source_radialMassLapse_eq line 9985
769. lemma OAI.CKSMixedGeometry.source_radialTangential_eq line 9993
770. lemma OAI.CKSBending.collarParams_initial line 10024
771. lemma OAI.CKSAngularGeometry.radiusLogPoint_exp line 10042
772. lemma OAI.CKSAngularGeometry.inner_collar_fields line 10045
773. lemma OAI.CKSAngularGeometry.radialExpansion_congr line 10061
774. lemma OAI.CKSMixedGeometry.source_inner_collar_fields line 10084
775. lemma OAI.CKSAngularGeometry.actualMetricFirstJet_congr line 10154
776. lemma OAI.CKSAngularGeometry.coordinateChristoffel_congr line 10159
777. lemma OAI.CKSAngularGeometry.covariantVector_congr line 10164
778. lemma OAI.CKSAngularGeometry.frameCoefficient_congr line 10172
779. lemma OAI.CKSAngularGeometry.actualFrameBracket_congr line 10181
780. lemma OAI.CKSAngularGeometry.frameBracketCoefficient_congr line 10190
781. lemma OAI.CKSAngularGeometry.actualFrameCurvature_congr line 10198
782. lemma OAI.CKSAngularGeometry.actualFrameScalar_congr line 10212
783. lemma OAI.CKSAngularGeometry.coordinateConnectionVector_congr line 10219
784. lemma OAI.CKSAngularGeometry.coordinateTensorCovariant_congr line 10225
785. lemma OAI.CKSAngularGeometry.coordinateMomentum_congr line 10232
786. lemma OAI.CKSAngularGeometry.momentumCovector_congr line 10244
787. theorem OAI.CKSAngularGeometry.physicalDEC_congr line 10250
788. lemma OAI.CKSMixedGeometry.source_inner_collar_fields_eventually line 10269
789. lemma OAI.CKSMixedGeometry.source_inner_collar_lapse line 10285
790. lemma OAI.CKSMixedGeometry.source_inner_collar_recovery line 10301
791. theorem OAI.CKSMixedGeometry.physical_source_inner_collar_DEC_iff line 10326
792. structure OAI.CKSMixedGeometry.SourceTensorFields.AngularRelatedAt line 10356
793. lemma OAI.CKSAngularGeometry.angular_inverse_mulVec line 10385
794. lemma OAI.CKSAngularGeometry.angular_dual_contraction line 10393
795. lemma OAI.CKSAngularGeometry.angular_bilinear_contraction line 10397
796. lemma OAI.CKSAngularGeometry.angular_covector_tensor line 10402
797. lemma OAI.CKSMixedGeometry.angularProjection_angularChange line 10417
798. lemma OAI.CKSMixedGeometry.sourceGamma_angular line 10420
799. lemma OAI.CKSMixedGeometry.sourceTangentialK_angular line 10427
800. lemma OAI.CKSMixedGeometry.sourceRadialMetric_angular line 10434
801. lemma OAI.CKSMixedGeometry.sourceRadialK_angular line 10438
802. lemma OAI.CKSMixedGeometry.sourceShift_angular line 10442
803. lemma OAI.CKSMixedGeometry.sourceSchur_angular line 10454
804. lemma OAI.CKSMixedGeometry.sourceLapse_angular line 10463
805. lemma OAI.CKSMixedGeometry.sourceT_angular line 10468
806. lemma OAI.CKSMixedGeometry.sourceOriginalL_angular line 10476
807. lemma OAI.CKSMixedGeometry.sourceOriginalEta_angular line 10488
808. lemma OAI.CKSMixedGeometry.sourceOriginalTau_angular line 10503
809. lemma OAI.CKSAngularGeometry.angularJacobian_contDiffAt line 10524
810. lemma OAI.CKSAngularGeometry.matrix_det_isUnit_eventually line 10534
811. lemma OAI.CKSMixedGeometry.sourceExpansion_angular line 10548
812. lemma OAI.CKSMixedGeometry.sourcePhysicalMass_angular line 10580
813. lemma OAI.CKSMixedGeometry.sourceAspect_angular line 10596
814. def OAI.CKSLorentz.angleTransition line 10615
815. def OAI.CKSLorentz.angularOverlap line 10616
816. lemma OAI.CKSLorentz.sourceRemainder_leading_limit line 10628
817. lemma OAI.CKSLorentz.angularOverlap_open line 10661
818. lemma OAI.CKSLorentz.angleTransition_eq_chart line 10663
819. lemma OAI.CKSLorentz.angleTransition_target line 10666
820. lemma OAI.CKSLorentz.param_angleTransition line 10670
821. lemma OAI.CKSLorentz.angleTransition_smoothAt line 10674
822. lemma OAI.CKSLorentz.polar_angularTransition_eq line 10678
823. lemma OAI.CKSLorentz.polar_angularTransition_eventuallyEq line 10683
824. lemma OAI.CKSLorentz.polarTensor_angularTransition line 10689
825. lemma OAI.CKSAngularGeometry.angularCongruence_entries line 10712
826. lemma OAI.CKSAngularGeometry.fderiv_angularChange_radial line 10716
827. lemma OAI.CKSLorentz.polarTensor_angular_radial line 10737
828. lemma OAI.CKSLorentz.polarTensor_angular_tangential line 10749
829. lemma OAI.CKSLorentz.CKS_tangential_leading_overlap line 10779
830. theorem OAI.CKSLorentz.CKS_angular_leading_overlap line 10829
831. lemma OAI.CKSLorentz.polarTensor_angular_mixed line 10859
832. lemma OAI.CKSLorentz.angularRoundMetric_overlap line 10876
833. theorem OAI.CKSLorentz.actual_CKS_fields_angular_related line 10912
834. lemma OAI.CKSLorentz.actual_angleTransition_isUnit line 10977
835. lemma OAI.CKSLorentz.actual_CKS_fields_angular_related_eventually line 10987
836. lemma OAI.CKSAngularGeometry.angularJacobian_logRadiusChart line 11015
837. lemma OAI.CKSAngularGeometry.angularChange_logRadiusChart line 11019
838. lemma OAI.CKSMixedGeometry.source_log_leading_angular line 11035
839. lemma OAI.CKSMixedGeometry.source_logGamma_angular line 11046
840. lemma OAI.CKSMixedGeometry.source_logSigma_angular line 11055
841. lemma OAI.CKSMixedGeometry.source_logQError_angular line 11061
842. theorem OAI.CKSMixedGeometry.sourceCollarData_angular_related line 11068
843. structure OAI.CKSMixedGeometry.SourceMassFields.SmoothAt line 11132
844. structure OAI.CKSMixedGeometry.SourceTensorFields.SmoothAt line 11142
845. lemma OAI.CKSMixedGeometry.SourceMassFields.SmoothAt.regularAt line 11147
846. lemma OAI.CKSMixedGeometry.SourceTensorFields.SmoothAt.regularAt line 11152
847. lemma OAI.CKSMixedGeometry.inverse_smoothAt line 11156
848. lemma OAI.CKSMixedGeometry.traceProduct_smoothAt line 11172
849. lemma OAI.CKSMixedGeometry.sourceGamma_smoothAt line 11179
850. lemma OAI.CKSMixedGeometry.sourceTangentialK_smoothAt line 11185
851. lemma OAI.CKSMixedGeometry.sourceRadialMetric_smoothAt line 11191
852. lemma OAI.CKSMixedGeometry.sourceShift_smoothAt line 11197
853. lemma OAI.CKSMixedGeometry.sourceSchur_smoothAt line 11205
854. lemma OAI.CKSMixedGeometry.sourceLapse_smoothAt line 11213
855. lemma OAI.CKSMixedGeometry.sourceExpansion_smoothAt line 11218
856. lemma OAI.CKSMixedGeometry.sourceT_smoothAt line 11226
857. lemma OAI.CKSMixedGeometry.sourcePhysicalMass_smoothAt line 11234
858. lemma OAI.CKSMixedGeometry.sourceRadialK_smoothAt line 11245
859. lemma OAI.CKSMixedGeometry.sourceOriginalL_smoothAt line 11250
860. lemma OAI.CKSMixedGeometry.sourceOriginalEta_smoothAt line 11261
861. lemma OAI.CKSMixedGeometry.sourceOriginalTau_smoothAt line 11272
862. abbrev OAI.CKSLorentz.spatialSourceFields line 11291
863. lemma OAI.CKSMixedGeometry.SourceTensorFields.RegularAt.eventually line 11305
864. theorem OAI.CKSLorentz.actual_log_collar_angular_related line 11320