OAI/Geometry/ConjugatePoints/NoConjugatePoints.lean

GitHub source file

75 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ThreeManifold.ReturningPassage.normalDensity_zero line 17
2. theorem OAI.ThreeManifold.ReturningPassage.truncated_return_nonnegative line 20
3. theorem OAI.ThreeManifold.CompactMetric.framed_truncated_return_index line 117
4. lemma OAI.ThreeManifold.CompactMetric.coordinateCometric_end_third line 211
5. lemma OAI.ThreeManifold.CompactMetric.metricInverse_end_warped line 226
6. lemma OAI.ThreeManifold.CompactMetric.ell_convex_nonnegative line 240
7. lemma OAI.ThreeManifold.CompactMetric.framed_neck_shallow_nonpositive line 257
8. lemma OAI.ThreeManifold.CompactMetric.framed_shallow_index line 270
9. lemma OAI.ThreeManifold.PassageDynamics.finite_turn_maximum line 281
10. theorem OAI.ThreeManifold.CompactMetric.framed_turn_index line 305
11. lemma OAI.ThreeManifold.CompactMetric.framed_boundary_hasDerivAt line 336
12. lemma OAI.ThreeManifold.CompactMetric.framed_index_energy line 375
13. lemma OAI.ThreeManifold.CompactMetric.framed_energy_nonneg line 394
14. lemma OAI.ThreeManifold.CompactMetric.framed_coordinate_index_integral line 418
15. lemma OAI.ThreeManifold.CompactMetric.framed_zero_endpoints_index line 488
16. lemma OAI.ThreeManifold.Neck.zeroHeight_covariant_pair line 519
17. lemma OAI.ThreeManifold.Neck.zeroHeight_normalDensity line 526
18. lemma OAI.ThreeManifold.Neck.transverse_energy_nonneg line 536
19. lemma OAI.ThreeManifold.Neck.zeroHeight_index_nonnegative line 545
20. lemma OAI.ThreeManifold.RiemannianCoordinates.euclidean_covariant line 602
21. lemma OAI.ThreeManifold.RiemannianCoordinates.euclidean_curvature line 611
22. lemma OAI.ThreeManifold.RiemannianCoordinates.euclidean_smoothField line 620
23. lemma OAI.ThreeManifold.RiemannianCoordinates.affine_hasDerivAt line 628
24. lemma OAI.ThreeManifold.RiemannianCoordinates.affine_deriv line 632
25. lemma OAI.ThreeManifold.RiemannianCoordinates.connection_smul_left line 635
26. lemma OAI.ThreeManifold.RiemannianCoordinates.connection_smul_right line 639
27. lemma OAI.ThreeManifold.RiemannianCoordinates.euclidean_affine_geodesic line 644
28. lemma OAI.ThreeManifold.RiemannianCoordinates.euclidean_affine_covariant line 670
29. lemma OAI.ThreeManifold.RiemannianCoordinates.curvature_smul_velocity line 679
30. lemma OAI.ThreeManifold.RiemannianCoordinates.euclidean_affine_index line 692
31. lemma OAI.ThreeManifold.CompactMetric.framed_metric_velocity_equations line 718
32. lemma OAI.ThreeManifold.CompactMetric.framed_zeroheight_normal_nonnegative line 745
33. lemma OAI.ThreeManifold.CompactMetric.framed_gauge_index_nonnegative line 833
34. def OAI.ThreeManifold.CompactMetric.regularGauge line 907
35. def OAI.ThreeManifold.CompactMetric.gaugeField line 909
36. lemma OAI.ThreeManifold.CompactMetric.regularGauge_zero_germ line 911
37. lemma OAI.ThreeManifold.CompactMetric.gaugeField_zero_germ line 915
38. lemma OAI.ThreeManifold.CompactMetric.regular_gauge_neighborhood line 920
39. lemma OAI.ThreeManifold.PassageDynamics.increasing_boundary_derivative line 964
40. lemma OAI.ThreeManifold.PassageDynamics.scalar_enter_transverse line 974
41. lemma OAI.ThreeManifold.PassageDynamics.force_end_nonnegative line 998
42. lemma OAI.ThreeManifold.PassageDynamics.neck_enter_transverse line 1007
43. def OAI.ThreeManifold.Cometric.flipFrame line 1023
44. lemma OAI.ThreeManifold.Cometric.coordinateCometric_flip line 1025
45. lemma OAI.ThreeManifold.Cometric.coordinateCometric_flip_deriv line 1036
46. lemma OAI.ThreeManifold.Cometric.force_far_end_nonpositive line 1052
47. lemma OAI.ThreeManifold.Cometric.inverse_jet_zero_nonpositive line 1062
48. lemma OAI.ThreeManifold.Cometric.inverse_jet_one_nonnegative line 1071
49. lemma OAI.ThreeManifold.Cometric.zeroheight_boundary_nonnegative line 1082
50. lemma OAI.ThreeManifold.Cometric.zeroheight_boundary_nonpositive line 1092
51. lemma OAI.ThreeManifold.PassageDynamics.neck_enter_upper_transverse line 1109
52. lemma OAI.ThreeManifold.PassageDynamics.neck_exit_transverse line 1122
53. theorem OAI.ThreeManifold.CompactMetric.framed_monotone_index line 1153
54. def OAI.ThreeManifold.CompactMetric.toRight line 1235
55. lemma OAI.ThreeManifold.CompactMetric.fromRight_toRight line 1236
56. lemma OAI.ThreeManifold.CompactMetric.toRight_height line 1239
57. lemma OAI.ThreeManifold.CompactMetric.toRight_smooth line 1242
58. theorem OAI.ThreeManifold.CompactMetric.right_frame_lift line 1245
59. def OAI.ThreeManifold.CompactMetric.PassageBounds line 1291
60. lemma OAI.ThreeManifold.CompactMetric.const_on_closed_of_deriv_zero line 1298
61. lemma OAI.ThreeManifold.CompactMetric.framed_closed_momentum line 1306
62. lemma OAI.ThreeManifold.CompactMetric.framed_unit_entry_zero_index line 1314
63. lemma OAI.ThreeManifold.CompactMetric.unit_entry_index line 1330
64. lemma OAI.ThreeManifold.RiemannianCoordinates.euclidean_affine_smoothField line 1367
65. lemma OAI.ThreeManifold.RiemannianCoordinates.affine_zero_germ line 1372
66. lemma OAI.ThreeManifold.RiemannianCoordinates.euclidean_affine_speed line 1375
67. lemma OAI.ThreeManifold.RiemannianCoordinates.euclidean_affine_index_integral line 1384
68. theorem OAI.ThreeManifold.CompactMetric.finite_unit_index line 1407
69. lemma OAI.ThreeManifold.RiemannianCoordinates.euclidean_index_nonnegative_zero_velocity line 1452
70. theorem OAI.ThreeManifold.CompactMetric.finite_neck_index line 1471
71. theorem OAI.ThreeManifold.CompactMetric.actual_finite_neck_index line 1531
72. lemma OAI.ThreeManifold.CompactMetric.compact_interval_window line 1567
73. theorem OAI.ThreeManifold.CompactMetric.realCompactMetric_nonnegative_index line 1575
74. theorem OAI.ThreeManifold.CompactMetric.realCompactMetric_noConjugatePoints line 1623
75. theorem OAI.ThreeManifold.CompactMetric.exists_uniform_compact_noConjugatePoints line 1630