OAI/Geometry/ConjugatePoints/Curvature.lean

GitHub source file

138 declarations, 0 contain sorry, 0 declared as axioms

Local isometries, warped curvature, and compact curvature estimates.

  1. def OAI.ThreeManifold.RiemannianCoordinates.NonpositiveAt line 18
  2. lemma OAI.ThreeManifold.RiemannianCoordinates.nonpositiveAt_of_nonpositive line 22
  3. lemma OAI.ThreeManifold.RiemannianCoordinates.inner_self_nonneg line 28
  4. lemma OAI.ThreeManifold.RiemannianCoordinates.indexPairDensity_nonneg_of_nonpositiveAt line 34
  5. theorem OAI.ThreeManifold.RiemannianCoordinates.nonnegativeIndex_of_passages line 46
  6. theorem OAI.ThreeManifold.RiemannianCoordinates.noConjugatePoints_of_passages line 66
  7. theorem OAI.ThreeManifold.RiemannianCoordinates.noConjugatePoints_of_nonpositive line 77
  8. def OAI.ThreeManifold.RiemannianCoordinates.LocalMetricIsometry.mapField line 102
  9. lemma OAI.ThreeManifold.RiemannianCoordinates.LocalMetricIsometry.coordinate_derivative line 105
  10. lemma OAI.ThreeManifold.RiemannianCoordinates.LocalMetricIsometry.mapField_coordinates line 137
  11. lemma OAI.ThreeManifold.RiemannianCoordinates.LocalMetricIsometry.comp_smooth line 145
  12. lemma OAI.ThreeManifold.RiemannianCoordinates.LocalMetricIsometry.mapField_smooth line 151
  13. lemma OAI.ThreeManifold.RiemannianCoordinates.LocalMetricIsometry.coordinateDomain_mem line 178
  14. lemma OAI.ThreeManifold.RiemannianCoordinates.LocalMetricIsometry.coordinate_curve_germ line 187
  15. lemma OAI.ThreeManifold.RiemannianCoordinates.LocalMetricIsometry.mapField_coordinates_germ line 197
  16. lemma OAI.ThreeManifold.RiemannianCoordinates.LocalMetricIsometry.covariantDerivative_map line 208
  17. lemma OAI.ThreeManifold.RiemannianCoordinates.LocalMetricIsometry.velocity_map line 239
  18. lemma OAI.ThreeManifold.RiemannianCoordinates.LocalMetricIsometry.curvatureAlong_map line 246
  19. lemma OAI.ThreeManifold.RiemannianCoordinates.LocalMetricIsometry.nonpositiveAt line 280
  20. lemma OAI.ThreeManifold.RiemannianCoordinates.LocalMetricIsometry.indexPairDensity_map line 301
  21. lemma OAI.ThreeManifold.RiemannianCoordinates.covariantDerivative_germ line 318
  22. lemma OAI.ThreeManifold.RiemannianCoordinates.geodesic_of_acceleration_zero line 327
  23. lemma OAI.ThreeManifold.RiemannianCoordinates.LocalMetricIsometry.geodesic_map line 346
  24. def OAI.ThreeManifold.WarpedCurvature.diag line 363
  25. lemma OAI.ThreeManifold.WarpedCurvature.diag_transpose line 364
  26. lemma OAI.ThreeManifold.WarpedCurvature.diag_mul line 366
  27. lemma OAI.ThreeManifold.WarpedCurvature.diag_pairing line 368
  28. lemma OAI.ThreeManifold.WarpedCurvature.diag_deriv line 371
  29. def OAI.ThreeManifold.WarpedCurvature.Q line 384
  30. def OAI.ThreeManifold.WarpedCurvature.P line 385
  31. def OAI.ThreeManifold.WarpedCurvature.A line 386
  32. def OAI.ThreeManifold.WarpedCurvature.B line 387
  33. lemma OAI.ThreeManifold.WarpedCurvature.QP line 388
  34. lemma OAI.ThreeManifold.WarpedCurvature.PQ line 393
  35. lemma OAI.ThreeManifold.WarpedCurvature.Q_deriv line 398
  36. lemma OAI.ThreeManifold.WarpedCurvature.A_deriv line 401
  37. lemma OAI.ThreeManifold.WarpedCurvature.P_deriv line 409
  38. lemma OAI.ThreeManifold.WarpedCurvature.curvature_scalar line 419
  39. lemma OAI.ThreeManifold.WarpedCurvature.metric_of_block line 433
  40. lemma OAI.ThreeManifold.WarpedCurvature.warped_curvature line 442
  41. lemma OAI.ThreeManifold.WarpedCurvature.warped_nonpositive line 452
  42. def OAI.ThreeManifold.Rechart.realMetric line 472
  43. lemma OAI.ThreeManifold.Rechart.map_smoothAt line 481
  44. def OAI.ThreeManifold.Rechart.realIsometry line 491
  45. def OAI.ThreeManifold.Rechart.realTargetIsometry line 523
  46. def OAI.ThreeManifold.CylinderConstruction.euclideanMetric line 551
  47. def OAI.ThreeManifold.CylinderConstruction.realMetric line 554
  48. def OAI.ThreeManifold.CylinderConstruction.euclideanProjection line 555
  49. lemma OAI.ThreeManifold.CylinderConstruction.euclideanProjection_smooth line 556
  50. lemma OAI.ThreeManifold.CylinderConstruction.euclideanProjection_metric line 559
  51. def OAI.ThreeManifold.CylinderConstruction.projectionIsometry line 574
  52. lemma OAI.ThreeManifold.RiemannianCoordinates.nonpositiveAt_of_chart line 583
  53. lemma OAI.ThreeManifold.RiemannianCoordinates.LocalMetricIsometry.nonpositiveAt_image line 598
  54. def OAI.ThreeManifold.WarpedCurvature.warpedModel line 624
  55. lemma OAI.ThreeManifold.WarpedCurvature.warpedModel_matrix line 626
  56. lemma OAI.ThreeManifold.WarpedCurvature.warpedModel_nonpositiveAt line 641
  57. lemma OAI.ThreeManifold.CompactMetric.ell_convex_left line 651
  58. lemma OAI.ThreeManifold.CompactMetric.radius₁_convex_left line 660
  59. def OAI.ThreeManifold.CompactMetric.neckModel line 666
  60. lemma OAI.ThreeManifold.CompactMetric.neckModel_apply line 669
  61. lemma OAI.ThreeManifold.CompactMetric.neckModel_matrix_left line 679
  62. lemma OAI.ThreeManifold.CompactMetric.neckModel_nonpositive_left line 694
  63. lemma OAI.ThreeManifold.CompactMetric.warpedModel_apply line 707
  64. def OAI.ThreeManifold.CompactMetric.rightRadius line 718
  65. lemma OAI.ThreeManifold.CompactMetric.rightRadius_smooth line 719
  66. lemma OAI.ThreeManifold.CompactMetric.rightRadius_pos line 721
  67. lemma OAI.ThreeManifold.CompactMetric.rightRadius_convex_left line 723
  68. def OAI.ThreeManifold.CompactMetric.rightWidth line 728
  69. lemma OAI.ThreeManifold.CompactMetric.rightWidth_pos line 729
  70. def OAI.ThreeManifold.CompactMetric.neckFlipLinear line 733
  71. lemma OAI.ThreeManifold.CompactMetric.neckFlipLinear_apply line 737
  72. def OAI.ThreeManifold.CompactMetric.neckFlip line 739
  73. lemma OAI.ThreeManifold.CompactMetric.neckFlip_apply line 740
  74. lemma OAI.ThreeManifold.CompactMetric.neckFlip_smooth line 743
  75. lemma OAI.ThreeManifold.CompactMetric.neckFlip_deriv line 744
  76. def OAI.ThreeManifold.CompactMetric.rightWarpedModel line 748
  77. lemma OAI.ThreeManifold.CompactMetric.neckRight_tensor line 751
  78. def OAI.ThreeManifold.CompactMetric.neckRightIsometry line 766
  79. lemma OAI.ThreeManifold.CompactMetric.neckModel_nonpositive_right line 777
  80. def OAI.ThreeManifold.Rechart.realSourceIsometry line 797
  81. def OAI.ThreeManifold.CompactMetric.universalMetric line 828
  82. lemma OAI.ThreeManifold.CompactMetric.universalMetric_apply line 830
  83. def OAI.ThreeManifold.CompactMetric.exponentialRadius line 841
  84. lemma OAI.ThreeManifold.CompactMetric.exponentialRadius_smooth line 842
  85. lemma OAI.ThreeManifold.CompactMetric.exponentialRadius_deriv line 843
  86. lemma OAI.ThreeManifold.CompactMetric.exponentialRadius_second line 846
  87. def OAI.ThreeManifold.CompactMetric.hyperbolicWarped line 850
  88. lemma OAI.ThreeManifold.CompactMetric.hyperbolicWarped_nonpositive line 852
  89. def OAI.ThreeManifold.CompactMetric.universalLog line 859
  90. lemma OAI.ThreeManifold.CompactMetric.universalLog_smooth line 860
  91. lemma OAI.ThreeManifold.CompactMetric.universalLog_deriv line 862
  92. lemma OAI.ThreeManifold.CompactMetric.universalLog_tensor line 871
  93. lemma OAI.ThreeManifold.CompactMetric.universalLog_metric line 886
  94. def OAI.ThreeManifold.CompactMetric.realUniversalMetric line 902
  95. def OAI.ThreeManifold.CompactMetric.realCoreMetric line 904
  96. def OAI.ThreeManifold.CompactMetric.universalLogIsometry line 906
  97. lemma OAI.ThreeManifold.CompactMetric.realUniversalMetric_nonpositive line 910
  98. def OAI.ThreeManifold.CompactMetric.coreProjectionIsometry line 913
  99. lemma OAI.ThreeManifold.CompactMetric.realCoreMetric_nonpositive line 920
  100. lemma OAI.ThreeManifold.RiemannianCoordinates.geodesic_congrOn line 939
  101. lemma OAI.ThreeManifold.RiemannianCoordinates.LocalMetricIsometry.deriv_injective line 951
  102. lemma OAI.ThreeManifold.RiemannianCoordinates.LocalMetricIsometry.deriv_bijective line 960
  103. lemma OAI.ThreeManifold.RiemannianCoordinates.LocalMetricIsometry.geodesic_reflect line 964
  104. lemma OAI.ThreeManifold.WarpedCurvature.warped_fiber_geodesic line 985
  105. lemma OAI.ThreeManifold.CompactMetric.universal_fiber_smooth line 1017
  106. lemma OAI.ThreeManifold.CompactMetric.universal_fiber_geodesic line 1024
  107. lemma OAI.ThreeManifold.CompactMetric.core_fiber_geodesic line 1031
  108. def OAI.ThreeManifold.CompactMetric.realPieceMetric line 1047
  109. def OAI.ThreeManifold.CompactMetric.pieceInclusionIsometry line 1050
  110. def OAI.ThreeManifold.RiemannianCoordinates.LocalMetricIsometry.comp line 1064
  111. def OAI.ThreeManifold.RiemannianCoordinates.LocalMetricIsometry.identity line 1078
  112. lemma OAI.ThreeManifold.RiemannianCoordinates.LocalMetricIsometry.nonpositiveAt_congr line 1088
  113. def OAI.ThreeManifold.CompactMetric.realNeck line 1106
  114. def OAI.ThreeManifold.CompactMetric.neckProjectionIsometry line 1108
  115. lemma OAI.ThreeManifold.CompactMetric.realNeck_nonpositive line 1112
  116. def OAI.ThreeManifold.CompactMetric.radialIsometry line 1122
  117. def OAI.ThreeManifold.CompactMetric.switchIsometry line 1127
  118. lemma OAI.ThreeManifold.CompactMetric.radial_nonpos line 1132
  119. lemma OAI.ThreeManifold.CompactMetric.realLeftCylinder_nonpositive line 1138
  120. lemma OAI.ThreeManifold.CompactMetric.realRightCylinder_nonpositive line 1143
  121. def OAI.ThreeManifold.CompactMetric.heightToLog line 1156
  122. lemma OAI.ThreeManifold.CompactMetric.heightToLog_smooth line 1158
  123. lemma OAI.ThreeManifold.CompactMetric.heightToLog_metric line 1161
  124. def OAI.ThreeManifold.CompactMetric.wholeCuspLog line 1166
  125. lemma OAI.ThreeManifold.CompactMetric.cuspChart_source line 1168
  126. lemma OAI.ThreeManifold.CompactMetric.wholeCuspLog_smooth line 1171
  127. lemma OAI.ThreeManifold.CompactMetric.wholeCuspLog_metric line 1177
  128. lemma OAI.ThreeManifold.CompactMetric.cuspChart_apply line 1185
  129. lemma OAI.ThreeManifold.CompactMetric.wholeCuspLog_height line 1193
  130. def OAI.ThreeManifold.CompactMetric.wholeCuspIsometry line 1207
  131. def OAI.ThreeManifold.CompactMetric.wholeCoreIsometry line 1214
  132. lemma OAI.ThreeManifold.CompactMetric.whole_nonpositive line 1225
  133. def OAI.ThreeManifold.CompactMetric.pieceMapIsometry line 1250
  134. lemma OAI.ThreeManifold.CompactMetric.realPiece_nonpositive line 1255
  135. def OAI.ThreeManifold.CompactMetric.openNeck line 1267
  136. lemma OAI.ThreeManifold.CompactMetric.openNeck_isOpen line 1268
  137. lemma OAI.ThreeManifold.CompactMetric.inclusion_collar_mem_openNeck line 1270
  138. lemma OAI.ThreeManifold.CompactMetric.realCompactMetric_nonpositive_off_neck line 1277