OAI/Geometry/ConjugatePoints/Neck.lean

GitHub source file

304 declarations, 0 contain sorry, 0 declared as axioms

Tensor identities and the local and torus neck metrics.

  1. def OAI.ThreeManifold.Tensor.contract line 20
  2. lemma OAI.ThreeManifold.Tensor.derivative_contract line 23
  3. lemma OAI.ThreeManifold.Tensor.composition_contract line 45
  4. lemma OAI.ThreeManifold.Tensor.curvature_contract line 68
  5. abbrev OAI.ThreeManifold.Neck.TVec line 109
  6. abbrev OAI.ThreeManifold.Neck.TMat line 110
  7. abbrev OAI.ThreeManifold.Neck.Vec line 111
  8. def OAI.ThreeManifold.Neck.pairing line 113
  9. lemma OAI.ThreeManifold.Neck.pairing_add_left line 115
  10. lemma OAI.ThreeManifold.Neck.pairing_add_right line 118
  11. lemma OAI.ThreeManifold.Neck.pairing_sub_left line 121
  12. lemma OAI.ThreeManifold.Neck.pairing_sub_right line 124
  13. lemma OAI.ThreeManifold.Neck.pairing_smul_left line 127
  14. lemma OAI.ThreeManifold.Neck.pairing_smul_right line 130
  15. lemma OAI.ThreeManifold.Neck.pairing_matrix_sub line 133
  16. lemma OAI.ThreeManifold.Neck.pairing_matrix_mul line 136
  17. lemma OAI.ThreeManifold.Neck.pairing_symm line 139
  18. def OAI.ThreeManifold.Neck.metric line 144
  19. def OAI.ThreeManifold.Neck.gamma line 146
  20. def OAI.ThreeManifold.Neck.gammaPrime line 150
  21. def OAI.ThreeManifold.Neck.curvatureJet line 156
  22. lemma OAI.ThreeManifold.Neck.metric_add_right line 160
  23. lemma OAI.ThreeManifold.Neck.metric_sub_right line 164
  24. lemma OAI.ThreeManifold.Neck.metric_smul_right line 168
  25. lemma OAI.ThreeManifold.Neck.metric_symm line 172
  26. lemma OAI.ThreeManifold.Neck.pairing_inverse line 177
  27. lemma OAI.ThreeManifold.Neck.metric_gamma line 181
  28. lemma OAI.ThreeManifold.Neck.metric_gammaPrime line 191
  29. lemma OAI.ThreeManifold.Neck.metric_add_left line 204
  30. lemma OAI.ThreeManifold.Neck.sandwich_transpose line 209
  31. lemma OAI.ThreeManifold.Neck.pairing_sandwich line 213
  32. lemma OAI.ThreeManifold.Neck.pairing_sandwich_left line 217
  33. lemma OAI.ThreeManifold.Neck.curvature_contraction line 221
  34. def OAI.ThreeManifold.Neck.coordinateEnergyDensity line 239
  35. def OAI.ThreeManifold.Neck.boundaryTerm line 243
  36. lemma OAI.ThreeManifold.Neck.boundaryTerm_eq line 246
  37. def OAI.ThreeManifold.Neck.boundaryJet line 252
  38. lemma OAI.ThreeManifold.Neck.index_density_identity line 258
  39. lemma OAI.ThreeManifold.Neck.pairing_hasDerivAt line 276
  40. lemma OAI.ThreeManifold.Neck.pairing_matrix_smul line 295
  41. lemma OAI.ThreeManifold.Neck.boundaryTerm_hasDerivAt line 299
  42. lemma OAI.ThreeManifold.Neck.continuous_pairing line 320
  43. lemma OAI.ThreeManifold.Neck.Continuous.pairing line 325
  44. lemma OAI.ThreeManifold.Neck.continuousOn_pairing line 331
  45. lemma OAI.ThreeManifold.Neck.continuousOn_energy line 337
  46. lemma OAI.ThreeManifold.Neck.continuousOn_boundaryJet line 348
  47. lemma OAI.ThreeManifold.Neck.coordinate_index_integral line 365
  48. lemma OAI.ThreeManifold.Neck.pairing_matrix_add line 423
  49. lemma OAI.ThreeManifold.Neck.pairing_matrix_neg line 427
  50. lemma OAI.ThreeManifold.Neck.pairing_mulVec_left line 431
  51. lemma OAI.ThreeManifold.Neck.pairing_mulVec_right line 436
  52. lemma OAI.ThreeManifold.Neck.energy_cometric_identity line 440
  53. lemma OAI.ThreeManifold.Neck.matrix_mul_hasDerivAt line 465
  54. lemma OAI.ThreeManifold.Neck.mulVec_hasDerivAt line 478
  55. lemma OAI.ThreeManifold.Neck.inverse_first_jet line 488
  56. lemma OAI.ThreeManifold.Neck.momentum_hasDerivAt_zero line 503
  57. def OAI.ThreeManifold.Neck.splitVector line 514
  58. def OAI.ThreeManifold.Neck.joinVector line 515
  59. def OAI.ThreeManifold.Neck.blockMatrix line 516
  60. def OAI.ThreeManifold.Neck.blockJet line 518
  61. lemma OAI.ThreeManifold.Neck.join_split line 521
  62. lemma OAI.ThreeManifold.Neck.split_join line 524
  63. lemma OAI.ThreeManifold.Neck.blockMatrix_mul line 530
  64. lemma OAI.ThreeManifold.Neck.blockMatrix_one line 535
  65. lemma OAI.ThreeManifold.Neck.blockMatrix_inverse line 538
  66. lemma OAI.ThreeManifold.Neck.block_entry_hasDerivAt line 543
  67. lemma OAI.ThreeManifold.Neck.coordPartial_block line 551
  68. lemma OAI.ThreeManifold.Neck.coordPartial_congr_germ line 562
  69. lemma OAI.ThreeManifold.Neck.christoffel_product line 567
  70. lemma OAI.ThreeManifold.Neck.connectionTerm_product line 587
  71. lemma OAI.ThreeManifold.Neck.join_gamma_hasDerivAt line 602
  72. lemma OAI.ThreeManifold.Neck.connectionTerm_basis line 635
  73. lemma OAI.ThreeManifold.Neck.coordPartial_join_gamma line 641
  74. lemma OAI.ThreeManifold.Neck.christoffel_product_germ line 656
  75. lemma OAI.ThreeManifold.Neck.christoffel_partial_product line 671
  76. lemma OAI.ThreeManifold.Neck.join_add line 684
  77. lemma OAI.ThreeManifold.Neck.join_sub line 687
  78. lemma OAI.ThreeManifold.Neck.join_smul line 690
  79. lemma OAI.ThreeManifold.Neck.gammaPrime_contract line 694
  80. lemma OAI.ThreeManifold.Neck.curvatureTerm_product line 705
  81. abbrev OAI.ThreeManifold.Cometric.V2 line 747
  82. abbrev OAI.ThreeManifold.Cometric.Mat2 line 748
  83. def OAI.ThreeManifold.Cometric.sqnorm line 750
  84. def OAI.ThreeManifold.Cometric.qform line 752
  85. def OAI.ThreeManifold.Cometric.d₁ line 754
  86. def OAI.ThreeManifold.Cometric.d₂ line 755
  87. def OAI.ThreeManifold.Cometric.shear line 756
  88. def OAI.ThreeManifold.Cometric.H line 757
  89. def OAI.ThreeManifold.Cometric.P line 759
  90. def OAI.ThreeManifold.Cometric.Q line 763
  91. lemma OAI.ThreeManifold.Cometric.P_source_formula line 765
  92. lemma OAI.ThreeManifold.Cometric.d₁_smooth line 771
  93. lemma OAI.ThreeManifold.Cometric.d₂_smooth line 775
  94. lemma OAI.ThreeManifold.Cometric.shear_smooth line 779
  95. lemma OAI.ThreeManifold.Cometric.P_smooth line 783
  96. lemma OAI.ThreeManifold.Cometric.d₁_bounds line 790
  97. lemma OAI.ThreeManifold.Cometric.d₂_bounds line 799
  98. lemma OAI.ThreeManifold.Cometric.shear_bounds line 803
  99. lemma OAI.ThreeManifold.Cometric.sqnorm_nonneg line 814
  100. lemma OAI.ThreeManifold.Cometric.sqnorm_eq_zero_iff line 816
  101. lemma OAI.ThreeManifold.Cometric.sqnorm_pos line 820
  102. lemma OAI.ThreeManifold.Cometric.qform_P line 823
  103. lemma OAI.ThreeManifold.Cometric.shear_norm_upper line 828
  104. lemma OAI.ThreeManifold.Cometric.shear_norm_lower line 834
  105. lemma OAI.ThreeManifold.Cometric.P_elliptic line 841
  106. lemma OAI.ThreeManifold.Cometric.P_hermitian line 859
  107. lemma OAI.ThreeManifold.Cometric.P_posDef line 864
  108. lemma OAI.ThreeManifold.Cometric.Q_posDef line 873
  109. def OAI.ThreeManifold.Cometric.u₁ line 876
  110. def OAI.ThreeManifold.Cometric.u₂ line 877
  111. def OAI.ThreeManifold.Cometric.v line 878
  112. def OAI.ThreeManifold.Cometric.w₁ line 879
  113. def OAI.ThreeManifold.Cometric.w₂ line 880
  114. def OAI.ThreeManifold.Cometric.z line 881
  115. lemma OAI.ThreeManifold.Cometric.d₁_hasDerivAt line 883
  116. lemma OAI.ThreeManifold.Cometric.d₂_hasDerivAt line 887
  117. lemma OAI.ThreeManifold.Cometric.shear_hasDerivAt line 892
  118. lemma OAI.ThreeManifold.Cometric.u₁_hasDerivAt line 895
  119. lemma OAI.ThreeManifold.Cometric.u₂_hasDerivAt line 898
  120. lemma OAI.ThreeManifold.Cometric.v_hasDerivAt line 904
  121. def OAI.ThreeManifold.Cometric.P₁ line 907
  122. def OAI.ThreeManifold.Cometric.P₂ line 912
  123. lemma OAI.ThreeManifold.Cometric.P_hasDerivAt line 918
  124. lemma OAI.ThreeManifold.Cometric.P_deriv line 934
  125. lemma OAI.ThreeManifold.Cometric.P₁_hasDerivAt line 936
  126. lemma OAI.ThreeManifold.Cometric.P₂_deriv line 957
  127. lemma OAI.ThreeManifold.Cometric.Q_formula line 961
  128. lemma OAI.ThreeManifold.Cometric.qform_Q line 971
  129. lemma OAI.ThreeManifold.Cometric.Q_elliptic line 977
  130. def OAI.ThreeManifold.Cometric.T₂ line 1003
  131. def OAI.ThreeManifold.Cometric.C₂ line 1004
  132. def OAI.ThreeManifold.Cometric.PEnd line 1006
  133. lemma OAI.ThreeManifold.Cometric.frame_inverse line 1008
  134. lemma OAI.ThreeManifold.Cometric.P_left_endpoint line 1012
  135. lemma OAI.ThreeManifold.Cometric.P_right_endpoint line 1019
  136. def OAI.ThreeManifold.Cometric.N₁ line 1029
  137. def OAI.ThreeManifold.Cometric.N₂ line 1034
  138. lemma OAI.ThreeManifold.Cometric.P₁_split line 1043
  139. lemma OAI.ThreeManifold.Cometric.P₂_split line 1048
  140. lemma OAI.ThreeManifold.Cometric.a_deriv_smooth line 1053
  141. lemma OAI.ThreeManifold.Cometric.N₁_smooth line 1058
  142. lemma OAI.ThreeManifold.Cometric.N₂_smooth line 1065
  143. lemma OAI.ThreeManifold.Cometric.normalized_errors_bounded line 1072
  144. lemma OAI.ThreeManifold.Cometric.sqnorm_add_le line 1095
  145. lemma OAI.ThreeManifold.Cometric.sqnorm_smul line 1100
  146. lemma OAI.ThreeManifold.Cometric.qform_add line 1104
  147. lemma OAI.ThreeManifold.Cometric.qform_smul line 1108
  148. lemma OAI.ThreeManifold.Cometric.qform_neg line 1112
  149. lemma OAI.ThreeManifold.Cometric.qform_diag line 1115
  150. lemma OAI.ThreeManifold.Cometric.dotProduct_sq_le line 1120
  151. lemma OAI.ThreeManifold.Cometric.sq_le_of_abs_le line 1124
  152. lemma OAI.ThreeManifold.Cometric.sqnorm_mulVec_le line 1128
  153. lemma OAI.ThreeManifold.Cometric.abs_qform_le line 1143
  154. def OAI.ThreeManifold.Cometric.cutoffMargin line 1154
  155. lemma OAI.ThreeManifold.Cometric.cutoffMargin_pos line 1156
  156. lemma OAI.ThreeManifold.Cometric.middle_concavity line 1160
  157. lemma OAI.ThreeManifold.Cometric.a_sq_le_one line 1178
  158. lemma OAI.ThreeManifold.Cometric.diagonal_first_bound line 1181
  159. lemma OAI.ThreeManifold.Cometric.first_derivative_bound line 1190
  160. lemma OAI.ThreeManifold.Cometric.middle_domination line 1206
  161. lemma OAI.ThreeManifold.Cometric.outside_cutoff_derivatives line 1227
  162. lemma OAI.ThreeManifold.Cometric.stationary_first_formula line 1235
  163. lemma OAI.ThreeManifold.Cometric.stationary_second_formula line 1242
  164. lemma OAI.ThreeManifold.Cometric.outside_domination line 1249
  165. theorem OAI.ThreeManifold.Cometric.uniform_original_bounds line 1274
  166. def OAI.ThreeManifold.Cometric.congruenceCLM line 1319
  167. lemma OAI.ThreeManifold.Cometric.congruenceCLM_apply line 1323
  168. lemma OAI.ThreeManifold.Cometric.qform_congruence line 1325
  169. lemma OAI.ThreeManifold.Cometric.C₂_transpose line 1330
  170. lemma OAI.ThreeManifold.Cometric.T₂_transpose line 1334
  171. lemma OAI.ThreeManifold.Cometric.C₂_norm_bounds line 1338
  172. lemma OAI.ThreeManifold.Cometric.T₂_norm_bounds line 1348
  173. lemma OAI.ThreeManifold.Cometric.PEnd_hasDerivAt line 1358
  174. lemma OAI.ThreeManifold.Cometric.PEnd_deriv line 1368
  175. lemma OAI.ThreeManifold.Cometric.PEnd_deriv₂ line 1372
  176. lemma OAI.ThreeManifold.Cometric.QEnd_formula line 1387
  177. lemma OAI.ThreeManifold.Cometric.PEnd_elliptic line 1401
  178. lemma OAI.ThreeManifold.Cometric.QEnd_elliptic line 1409
  179. lemma OAI.ThreeManifold.Cometric.sqnorm_neg line 1417
  180. lemma OAI.ThreeManifold.Cometric.PEnd_derivative_norm line 1419
  181. lemma OAI.ThreeManifold.Cometric.PEnd_derivative_qform line 1425
  182. lemma OAI.ThreeManifold.Cometric.PEnd_derivative_bounds line 1431
  183. def OAI.ThreeManifold.Cometric.coordinateCometric line 1448
  184. theorem OAI.ThreeManifold.Cometric.uniform_cometric_bounds line 1451
  185. lemma OAI.ThreeManifold.Cometric.sqnorm_eq_euclidean line 1485
  186. def OAI.ThreeManifold.Cometric.euclideanOperator line 1489
  187. lemma OAI.ThreeManifold.Cometric.euclideanOperator_apply line 1493
  188. lemma OAI.ThreeManifold.Cometric.operator_norm_of_sqnorm line 1497
  189. theorem OAI.ThreeManifold.Cometric.uniform_cometric_operator_bound line 1508
  190. abbrev OAI.ThreeManifold.LocalNeck.Slab line 1527
  191. instance OAI.ThreeManifold.LocalNeck.(instance at line 1529) line 1529
  192. lemma OAI.ThreeManifold.LocalNeck.slab_isOpen line 1531
  193. theorem OAI.ThreeManifold.LocalNeck.slabEmbedding line 1534
  194. def OAI.ThreeManifold.LocalNeck.slabChart line 1537
  195. lemma OAI.ThreeManifold.LocalNeck.slabChart_source line 1540
  196. lemma OAI.ThreeManifold.LocalNeck.slabChart_apply line 1543
  197. instance OAI.ThreeManifold.LocalNeck.(instance at line 1545) line 1545
  198. instance OAI.ThreeManifold.LocalNeck.(instance at line 1546) line 1546
  199. lemma OAI.ThreeManifold.LocalNeck.chartAt_eq line 1548
  200. lemma OAI.ThreeManifold.LocalNeck.achart_eq line 1550
  201. lemma OAI.ThreeManifold.LocalNeck.slab_symmL line 1554
  202. lemma OAI.ThreeManifold.LocalNeck.slab_linearMapAt line 1564
  203. lemma OAI.ThreeManifold.LocalNeck.slab_val_smooth line 1575
  204. lemma OAI.ThreeManifold.LocalNeck.Q_formula_of_ne line 1581
  205. lemma OAI.ThreeManifold.LocalNeck.Q_smoothAt line 1589
  206. def OAI.ThreeManifold.LocalNeck.metricBilin line 1608
  207. lemma OAI.ThreeManifold.LocalNeck.metricBilin_apply line 1612
  208. lemma OAI.ThreeManifold.LocalNeck.metricBilin_smooth line 1622
  209. lemma OAI.ThreeManifold.LocalNeck.metricBilin_block line 1633
  210. lemma OAI.ThreeManifold.LocalNeck.blockMatrix_smooth line 1639
  211. lemma OAI.ThreeManifold.LocalNeck.neckBilin_lower line 1664
  212. lemma OAI.ThreeManifold.LocalNeck.neckBilin_pos line 1673
  213. lemma OAI.ThreeManifold.LocalNeck.neckBilin_symm line 1686
  214. lemma OAI.ThreeManifold.LocalNeck.neckBilin_bounded line 1693
  215. lemma OAI.ThreeManifold.LocalNeck.neckBilin_smooth line 1705
  216. def OAI.ThreeManifold.LocalNeck.neckMetric line 1719
  217. lemma OAI.ThreeManifold.LocalNeck.slabChart_mfderiv_symm line 1733
  218. lemma OAI.ThreeManifold.LocalNeck.neckMetric_matrix line 1742
  219. lemma OAI.ThreeManifold.LocalNeck.Q_mul_P line 1758
  220. lemma OAI.ThreeManifold.LocalNeck.P_mul_Q line 1762
  221. lemma OAI.ThreeManifold.LocalNeck.Q_transpose line 1766
  222. lemma OAI.ThreeManifold.LocalNeck.Q_hasDerivAt line 1770
  223. lemma OAI.ThreeManifold.LocalNeck.Q_deriv_transpose line 1774
  224. lemma OAI.ThreeManifold.LocalNeck.Q_deriv_jet line 1785
  225. lemma OAI.ThreeManifold.LocalNeck.P_hasDerivAt_Qjet line 1792
  226. lemma OAI.ThreeManifold.LocalNeck.Q_deriv_hasDerivAt line 1803
  227. lemma OAI.ThreeManifold.LocalNeck.slabChart_target line 1808
  228. lemma OAI.ThreeManifold.LocalNeck.neckMetric_germ line 1817
  229. lemma OAI.ThreeManifold.LocalNeck.neckMetric_connection line 1823
  230. lemma OAI.ThreeManifold.LocalNeck.neckMetric_curvature line 1833
  231. def OAI.ThreeManifold.LocalNeck.coordinates line 1846
  232. def OAI.ThreeManifold.LocalNeck.torusVelocity line 1848
  233. def OAI.ThreeManifold.LocalNeck.momentum line 1851
  234. lemma OAI.ThreeManifold.LocalNeck.coordinates_smooth line 1854
  235. lemma OAI.ThreeManifold.LocalNeck.coordinates_smoothAt line 1859
  236. lemma OAI.ThreeManifold.LocalNeck.coordinates_geodesic_equation line 1864
  237. lemma OAI.ThreeManifold.LocalNeck.momentum_hasDerivAt line 1874
  238. abbrev OAI.ThreeManifold.TorusNeck.Height line 1919
  239. abbrev OAI.ThreeManifold.TorusNeck.Neck line 1920
  240. abbrev OAI.ThreeManifold.TorusNeck.Deck line 1921
  241. instance OAI.ThreeManifold.TorusNeck.(instance at line 1924) line 1924
  242. lemma OAI.ThreeManifold.TorusNeck.height_cover line 1929
  243. instance OAI.ThreeManifold.TorusNeck.torusProductAction line 1941
  244. instance OAI.ThreeManifold.TorusNeck.neckProductAction line 1945
  245. def OAI.ThreeManifold.TorusNeck.split line 1948
  246. instance OAI.ThreeManifold.TorusNeck.deckAction line 1966
  247. def OAI.ThreeManifold.TorusNeck.projection line 1969
  248. lemma OAI.ThreeManifold.TorusNeck.projection_cover line 1972
  249. lemma OAI.ThreeManifold.TorusNeck.deck_val line 1980
  250. lemma OAI.ThreeManifold.TorusNeck.deck_smooth line 1994
  251. def OAI.ThreeManifold.TorusNeck.sectionMap line 2008
  252. lemma OAI.ThreeManifold.TorusNeck.sectionMap_rightInverse line 2011
  253. instance OAI.ThreeManifold.TorusNeck.neckCharts line 2015
  254. instance OAI.ThreeManifold.TorusNeck.neckSmooth line 2018
  255. lemma OAI.ThreeManifold.TorusNeck.projection_smooth line 2022
  256. lemma OAI.ThreeManifold.TorusNeck.neck_chart_eq line 2026
  257. lemma OAI.ThreeManifold.TorusNeck.chart_transition_germ line 2030
  258. lemma OAI.ThreeManifold.TorusNeck.chart_transition_derivative line 2061
  259. lemma OAI.ThreeManifold.TorusNeck.neck_oriented line 2069
  260. lemma OAI.ThreeManifold.TorusNeck.tangent_transition line 2077
  261. lemma OAI.ThreeManifold.TorusNeck.neck_symmL line 2089
  262. lemma OAI.ThreeManifold.TorusNeck.neck_linearMapAt line 2095
  263. lemma OAI.ThreeManifold.TorusNeck.height_smooth line 2102
  264. lemma OAI.ThreeManifold.TorusNeck.quotientBilin_smooth line 2121
  265. def OAI.ThreeManifold.TorusNeck.quotientMetric line 2133
  266. lemma OAI.ThreeManifold.TorusNeck.chart_symm_height line 2155
  267. lemma OAI.ThreeManifold.TorusNeck.chart_symm_mfderiv line 2165
  268. lemma OAI.ThreeManifold.TorusNeck.quotientMetric_matrix line 2177
  269. lemma OAI.ThreeManifold.TorusNeck.quotientMetric_germ line 2187
  270. lemma OAI.ThreeManifold.TorusNeck.chart_target_height line 2199
  271. lemma OAI.ThreeManifold.TorusNeck.quotientMetric_connection line 2204
  272. lemma OAI.ThreeManifold.TorusNeck.quotientMetric_curvature line 2213
  273. lemma OAI.ThreeManifold.TorusNeck.chart_mfderiv line 2226
  274. lemma OAI.ThreeManifold.TorusNeck.chart_height line 2234
  275. def OAI.ThreeManifold.TorusNeck.velocity line 2240
  276. lemma OAI.ThreeManifold.TorusNeck.velocity_eq_chart_deriv line 2243
  277. lemma OAI.ThreeManifold.TorusNeck.velocity_germ_chart line 2258
  278. lemma OAI.ThreeManifold.TorusNeck.coord_smoothAt line 2267
  279. lemma OAI.ThreeManifold.TorusNeck.velocity_smoothAt line 2275
  280. lemma OAI.ThreeManifold.TorusNeck.height_hasDerivAt line 2282
  281. lemma OAI.ThreeManifold.TorusNeck.velocity_geodesic_equation line 2295
  282. def OAI.ThreeManifold.TorusNeck.fieldComponents line 2311
  283. lemma OAI.ThreeManifold.TorusNeck.fieldCoordinates_eq line 2314
  284. lemma OAI.ThreeManifold.TorusNeck.fieldCoordinates_germ line 2320
  285. lemma OAI.ThreeManifold.TorusNeck.alongDerivative_eq line 2327
  286. lemma OAI.ThreeManifold.TorusNeck.split_add line 2342
  287. def OAI.ThreeManifold.TorusNeck.coordinateIndexDensity line 2347
  288. lemma OAI.ThreeManifold.TorusNeck.coordinateIndexDensity_eq line 2357
  289. lemma OAI.ThreeManifold.TorusNeck.Q_second_transpose line 2381
  290. lemma OAI.ThreeManifold.TorusNeck.actual_index_density_identity line 2393
  291. lemma OAI.ThreeManifold.TorusNeck.splitVector_hasDerivAt line 2410
  292. lemma OAI.ThreeManifold.TorusNeck.split_neg line 2420
  293. lemma OAI.ThreeManifold.TorusNeck.velocity_hasDerivAt line 2425
  294. lemma OAI.ThreeManifold.TorusNeck.actual_boundary_hasDerivAt line 2436
  295. lemma OAI.ThreeManifold.TorusNeck.Q_second_jet line 2474
  296. lemma OAI.ThreeManifold.TorusNeck.splitVector_smooth line 2490
  297. lemma OAI.ThreeManifold.TorusNeck.actual_index_integral line 2498
  298. def OAI.ThreeManifold.TorusNeck.momentum line 2572
  299. lemma OAI.ThreeManifold.TorusNeck.momentum_hasDerivAt line 2575
  300. lemma OAI.ThreeManifold.TorusNeck.velocity_eq_momentum line 2594
  301. lemma OAI.ThreeManifold.TorusNeck.P₁_transpose line 2603
  302. lemma OAI.ThreeManifold.TorusNeck.actual_energy_cometric line 2613
  303. lemma OAI.ThreeManifold.TorusNeck.pairing_eq_qform line 2632
  304. theorem OAI.ThreeManifold.TorusNeck.uniform_actual_energy_nonneg line 2634