OAI/Geometry/ConjugatePoints/Passages.lean

GitHub source file

138 declarations, 0 contain sorry, 0 declared as axioms

Passage supports, extension, and compact metric estimates.

  1. def OAI.ThreeManifold.TwoGluing.descend line 18
  2. lemma OAI.ThreeManifold.TwoGluing.descend_inclusion line 20
  3. lemma OAI.ThreeManifold.CompactMetric.logCuspMap_change line 39
  4. def OAI.ThreeManifold.CompactMetric.piecePosition line 47
  5. lemma OAI.ThreeManifold.CompactMetric.piecePosition_collar line 50
  6. lemma OAI.ThreeManifold.CompactMetric.piecePosition_match line 56
  7. def OAI.ThreeManifold.CompactMetric.neckPosition line 61
  8. lemma OAI.ThreeManifold.CompactMetric.neckPosition_inclusion line 63
  9. def OAI.ThreeManifold.CompactMetric.extendedPiece line 67
  10. lemma OAI.ThreeManifold.CompactMetric.extendedPiece_isOpen line 68
  11. lemma OAI.ThreeManifold.CompactMetric.collar_subset_extended line 70
  12. lemma OAI.ThreeManifold.CompactMetric.extendedPiece_cusp line 74
  13. def OAI.ThreeManifold.CompactMetric.extendedNeck line 80
  14. lemma OAI.ThreeManifold.CompactMetric.extendedNeck_isOpen line 82
  15. lemma OAI.ThreeManifold.CompactMetric.openNeck_subset_extended line 85
  16. lemma OAI.ThreeManifold.CompactMetric.extendedNeck_representative line 88
  17. lemma OAI.ThreeManifold.CompactMetric.neckPosition_germ line 93
  18. lemma OAI.ThreeManifold.CompactMetric.piecePosition_smooth line 100
  19. lemma OAI.ThreeManifold.CompactMetric.neckPosition_smooth line 106
  20. lemma OAI.ThreeManifold.CompactMetric.pieceMetric_cusp line 118
  21. lemma OAI.ThreeManifold.CompactMetric.piecePosition_metric line 130
  22. lemma OAI.ThreeManifold.CompactMetric.neckPosition_metric line 154
  23. def OAI.ThreeManifold.CompactMetric.neckPositionIsometry line 170
  24. lemma OAI.ThreeManifold.CompactMetric.inclusion_mem_neck_iff line 177
  25. def OAI.ThreeManifold.CompactMetric.interfaceBand line 186
  26. lemma OAI.ThreeManifold.CompactMetric.interfaceBand_compact line 188
  27. lemma OAI.ThreeManifold.CompactMetric.interfaceBand_subset_extended line 194
  28. lemma OAI.ThreeManifold.CompactMetric.openNeck_subset_bands line 196
  29. lemma OAI.ThreeManifold.CompactMetric.closure_openNeck_subset_extended line 204
  30. lemma OAI.ThreeManifold.CompactMetric.piecePosition_height line 213
  31. lemma OAI.ThreeManifold.CompactMetric.log_eight line 225
  32. lemma OAI.ThreeManifold.CompactMetric.neckPosition_mem_iff line 228
  33. lemma OAI.ThreeManifold.CylinderConstruction.lift_smoothAt line 259
  34. theorem OAI.ThreeManifold.CylinderConstruction.exists_smooth_lift line 279
  35. lemma OAI.ThreeManifold.CylinderConstruction.exists_euclidean_smooth_lift line 311
  36. def OAI.ThreeManifold.CompactMetric.normalizedNeck line 332
  37. lemma OAI.ThreeManifold.CompactMetric.normalizedNeck_apply line 338
  38. def OAI.ThreeManifold.CompactMetric.normalize line 345
  39. def OAI.ThreeManifold.CompactMetric.normalizationIsometry line 350
  40. lemma OAI.ThreeManifold.CompactMetric.ell_sq_eq_inv line 365
  41. lemma OAI.ThreeManifold.CompactMetric.normalizedNeck_bilin line 369
  42. lemma OAI.ThreeManifold.CompactMetric.normalizedNeck_matrix line 380
  43. lemma OAI.ThreeManifold.CompactMetric.normalizedNeck_matrix_germ line 392
  44. lemma OAI.ThreeManifold.RiemannianCoordinates.LocalMetricIsometry.deriv_invertible line 410
  45. def OAI.ThreeManifold.RiemannianCoordinates.LocalMetricIsometry.unmapField line 416
  46. lemma OAI.ThreeManifold.RiemannianCoordinates.LocalMetricIsometry.map_unmap line 419
  47. lemma OAI.ThreeManifold.RiemannianCoordinates.LocalMetricIsometry.coordinate_invertible line 422
  48. lemma OAI.ThreeManifold.RiemannianCoordinates.LocalMetricIsometry.unmapField_coordinates line 429
  49. lemma OAI.ThreeManifold.RiemannianCoordinates.LocalMetricIsometry.unmapField_smooth line 441
  50. lemma OAI.ThreeManifold.RiemannianCoordinates.fieldCoordinates_germ line 467
  51. lemma OAI.ThreeManifold.RiemannianCoordinates.covariantDerivative_curve_germ line 474
  52. lemma OAI.ThreeManifold.RiemannianCoordinates.curvatureAlong_curve_germ line 483
  53. lemma OAI.ThreeManifold.RiemannianCoordinates.indexPairDensity_curve_germ line 493
  54. lemma OAI.ThreeManifold.RiemannianCoordinates.smoothField_curve_congrOn line 503
  55. theorem OAI.ThreeManifold.CompactMetric.actual_neck_lift line 519
  56. lemma OAI.ThreeManifold.FinitePassage.bounded_open_interval line 574
  57. lemma OAI.ThreeManifold.FinitePassage.closure_component_boundary line 591
  58. theorem OAI.ThreeManifold.FinitePassage.bounded_component line 602
  59. lemma OAI.ThreeManifold.FinitePassage.endpoint_alternative line 636
  60. lemma OAI.ThreeManifold.CompactMetric.finite_neck_neighborhood line 672
  61. lemma OAI.ThreeManifold.CompactMetric.finite_neck_height_boundary line 694
  62. theorem OAI.ThreeManifold.CompactMetric.actual_finite_neck_lift line 722
  63. def OAI.ThreeManifold.PassageDynamics.reflectEven line 745
  64. def OAI.ThreeManifold.PassageDynamics.reflectOdd line 746
  65. lemma OAI.ThreeManifold.PassageDynamics.scalar_reflection_germ line 748
  66. lemma OAI.ThreeManifold.PassageDynamics.reflectEven_germ_center line 769
  67. lemma OAI.ThreeManifold.PassageDynamics.reflectOdd_germ_center line 774
  68. lemma OAI.ThreeManifold.PassageDynamics.reflectEven_germ_left line 780
  69. lemma OAI.ThreeManifold.PassageDynamics.reflectOdd_germ_left line 784
  70. lemma OAI.ThreeManifold.PassageDynamics.reflectEven_germ_right line 788
  71. lemma OAI.ThreeManifold.PassageDynamics.reflectOdd_germ_right line 792
  72. lemma OAI.ThreeManifold.PassageDynamics.reflected_scalar_equations line 797
  73. lemma OAI.ThreeManifold.PassageDynamics.reflected_scalar_smooth line 822
  74. lemma OAI.ThreeManifold.PassageDynamics.reflected_closed_equations line 843
  75. lemma OAI.ThreeManifold.PassageDynamics.reflected_closed_smooth line 869
  76. theorem OAI.ThreeManifold.PassageDynamics.finite_turn_completion line 892
  77. def OAI.ThreeManifold.SupportExtension.cut line 932
  78. lemma OAI.ThreeManifold.SupportExtension.cut_germ_left line 934
  79. lemma OAI.ThreeManifold.SupportExtension.cut_germ_right line 938
  80. lemma OAI.ThreeManifold.SupportExtension.cut_germ_center line 942
  81. lemma OAI.ThreeManifold.SupportExtension.cut_smoothAt line 948
  82. lemma OAI.ThreeManifold.SupportExtension.cut_eq line 955
  83. lemma OAI.ThreeManifold.SupportExtension.cut_deriv line 956
  84. lemma OAI.ThreeManifold.SupportExtension.cut_zero line 962
  85. lemma OAI.ThreeManifold.SupportExtension.cut_deriv_zero line 963
  86. lemma OAI.ThreeManifold.CompactMetric.normalizedNeck_connection line 976
  87. lemma OAI.ThreeManifold.CompactMetric.euclidean_curve_smooth line 984
  88. lemma OAI.ThreeManifold.CompactMetric.euclidean_fieldCoordinates line 987
  89. lemma OAI.ThreeManifold.CompactMetric.euclidean_field_smooth line 993
  90. lemma OAI.ThreeManifold.CompactMetric.normalized_velocity_equation line 1002
  91. lemma OAI.ThreeManifold.CompactMetric.normalized_momentum_hasDerivAt line 1017
  92. lemma OAI.ThreeManifold.CompactMetric.normalized_momentum_constant line 1038
  93. lemma OAI.ThreeManifold.CompactMetric.Q_deriv_jet_closed line 1049
  94. lemma OAI.ThreeManifold.CompactMetric.normalized_velocity_torus line 1058
  95. lemma OAI.ThreeManifold.CompactMetric.normalized_scalar_equation line 1064
  96. lemma OAI.ThreeManifold.CompactMetric.euclidean_velocity line 1092
  97. lemma OAI.ThreeManifold.CompactMetric.normalized_energy_identity line 1098
  98. lemma OAI.ThreeManifold.CompactMetric.normalized_energy_constant line 1111
  99. lemma OAI.ThreeManifold.CompactMetric.normalizedNeck_curvature line 1119
  100. lemma OAI.ThreeManifold.CompactMetric.normalizedNeck_covariant line 1132
  101. lemma OAI.ThreeManifold.CompactMetric.normalizedNeck_curvatureAlong line 1146
  102. lemma OAI.ThreeManifold.CompactMetric.normalizedNeck_index_density line 1161
  103. def OAI.ThreeManifold.CompactMetric.fromRightLinear line 1183
  104. def OAI.ThreeManifold.CompactMetric.fromRight line 1193
  105. lemma OAI.ThreeManifold.CompactMetric.fromRight_apply line 1194
  106. lemma OAI.ThreeManifold.CompactMetric.fromRight_smooth line 1196
  107. lemma OAI.ThreeManifold.CompactMetric.fromRight_deriv line 1198
  108. def OAI.ThreeManifold.CompactMetric.normalizedRight line 1203
  109. def OAI.ThreeManifold.CompactMetric.fromRightIsometry line 1207
  110. lemma OAI.ThreeManifold.CompactMetric.right_inverse_formula line 1214
  111. lemma OAI.ThreeManifold.CompactMetric.right_frame_pairing line 1221
  112. lemma OAI.ThreeManifold.CompactMetric.normalizedRight_bilin line 1233
  113. lemma OAI.ThreeManifold.CompactMetric.normalizedRight_matrix line 1250
  114. lemma OAI.ThreeManifold.CompactMetric.normalizedRight_matrix_germ line 1263
  115. def OAI.ThreeManifold.CompactMetric.framedNeck line 1271
  116. lemma OAI.ThreeManifold.CompactMetric.framedNeck_bilin line 1274
  117. lemma OAI.ThreeManifold.CompactMetric.framedNeck_matrix_germ line 1282
  118. lemma OAI.ThreeManifold.CompactMetric.frame_elliptic line 1290
  119. lemma OAI.ThreeManifold.CompactMetric.frame_det_ne line 1299
  120. lemma OAI.ThreeManifold.CompactMetric.frame_QP line 1304
  121. lemma OAI.ThreeManifold.CompactMetric.frame_PQ line 1308
  122. lemma OAI.ThreeManifold.CompactMetric.framedNeck_connection line 1312
  123. lemma OAI.ThreeManifold.CompactMetric.framed_velocity_equation line 1323
  124. lemma OAI.ThreeManifold.CompactMetric.framed_momentum_hasDerivAt line 1338
  125. lemma OAI.ThreeManifold.CompactMetric.framed_momentum_constant line 1359
  126. lemma OAI.ThreeManifold.CompactMetric.framed_velocity_torus line 1367
  127. lemma OAI.ThreeManifold.CompactMetric.framed_scalar_equation line 1373
  128. lemma OAI.ThreeManifold.CompactMetric.framed_energy_identity line 1400
  129. lemma OAI.ThreeManifold.CompactMetric.framed_P_hasDerivAt line 1412
  130. lemma OAI.ThreeManifold.CompactMetric.framedNeck_curvature line 1424
  131. lemma OAI.ThreeManifold.CompactMetric.framedNeck_covariant line 1439
  132. lemma OAI.ThreeManifold.CompactMetric.framedNeck_curvatureAlong line 1453
  133. lemma OAI.ThreeManifold.CompactMetric.framedNeck_index_density line 1468
  134. lemma OAI.ThreeManifold.CompactMetric.split_deriv line 1494
  135. lemma OAI.ThreeManifold.CompactMetric.normalized_return_density line 1498
  136. theorem OAI.ThreeManifold.CompactMetric.normalized_left_return_index line 1514
  137. lemma OAI.ThreeManifold.CompactMetric.framed_return_density line 1583
  138. theorem OAI.ThreeManifold.CompactMetric.framed_return_index line 1598