OAI/Geometry/ConjugatePoints/Geodesics.lean

GitHub source file

120 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ThreeManifold.ODEVariation.remainder_bound line 19
2. lemma OAI.ThreeManifold.ODEVariation.hasFDerivAt_of_quadratic_error line 65
3. lemma OAI.ThreeManifold.ODEVariation.flow_hasFDerivAt line 76
4. lemma OAI.ThreeManifold.ODEVariation.quadratic_taylor line 94
5. lemma OAI.ThreeManifold.ODEVariation.local_bounds line 107
6. def OAI.ThreeManifold.ODEVariation.variationVector line 136
7. lemma OAI.ThreeManifold.ODEVariation.variationVector_smoothAt line 139
8. lemma OAI.ThreeManifold.ODEVariation.exists_variation_flow line 146
9. lemma OAI.ThreeManifold.ODEVariation.flow_derivative_on line 200
10. lemma OAI.ThreeManifold.ODEVariation.shrink_flow_image line 258
11. lemma OAI.ThreeManifold.ODEVariation.exists_contDiff_variation_flow line 288
12. lemma OAI.ThreeManifold.ODEVariation.exists_contDiff_flow line 355
13. lemma OAI.ThreeManifold.ODEVariation.solution_smooth line 370
14. def OAI.ThreeManifold.RiemannianCoordinates.geodesicPhase line 385
15. lemma OAI.ThreeManifold.RiemannianCoordinates.geodesicPhase_smoothAt line 388
16. lemma OAI.ThreeManifold.RiemannianCoordinates.chart_geodesic line 402
17. theorem OAI.ThreeManifold.RiemannianCoordinates.exists_geodesic_local_flow line 439
18. theorem OAI.ThreeManifold.fiberBundle_t2 line 480
19. def OAI.ThreeManifold.RiemannianCoordinates.phaseLift line 505
20. def OAI.ThreeManifold.RiemannianCoordinates.chartPhase line 507
21. lemma OAI.ThreeManifold.RiemannianCoordinates.phaseLift_chart line 510
22. lemma OAI.ThreeManifold.RiemannianCoordinates.phaseLift_continuousAt line 519
23. lemma OAI.ThreeManifold.RiemannianCoordinates.chartPhase_contDiffAt line 540
24. lemma OAI.ThreeManifold.RiemannianCoordinates.geodesic_chartPhase_ode line 547
25. lemma OAI.ThreeManifold.RiemannianCoordinates.geodesic_eventuallyEq line 560
26. lemma OAI.ThreeManifold.RiemannianCoordinates.phaseLift_eventuallyEq line 594
27. theorem OAI.ThreeManifold.RiemannianCoordinates.geodesic_unique line 604
28. lemma OAI.ThreeManifold.CompactEnergy.continuous_fiberNorm line 637
29. theorem OAI.ThreeManifold.CompactEnergy.isCompact_fiberDisk line 647
30. def OAI.ThreeManifold.RiemannianCoordinates.phaseEnergy line 698
31. lemma OAI.ThreeManifold.RiemannianCoordinates.continuous_phaseEnergy line 700
32. theorem OAI.ThreeManifold.RiemannianCoordinates.isCompact_phaseEnergy line 710
33. structure OAI.ThreeManifold.FlowContinuation.Equation line 729
34. def OAI.ThreeManifold.FlowContinuation.Equation.CurveOn line 738
35. lemma OAI.ThreeManifold.FlowContinuation.Equation.CurveOn.mono line 739
36. lemma OAI.ThreeManifold.FlowContinuation.Equation.CurveOn.congr line 741
37. lemma OAI.ThreeManifold.FlowContinuation.Equation.CurveOn.comp_add line 745
38. lemma OAI.ThreeManifold.FlowContinuation.Equation.eqOn_piecewise line 749
39. lemma OAI.ThreeManifold.FlowContinuation.Equation.curveOn_piecewise line 763
40. lemma OAI.ThreeManifold.FlowContinuation.Equation.global_of_arbitrarily_long line 776
41. theorem OAI.ThreeManifold.FlowContinuation.Equation.exists_global_of_uniform_invariant line 794
42. theorem OAI.ThreeManifold.FlowContinuation.Equation.exists_global_of_compact_invariant line 847
43. lemma OAI.ThreeManifold.RiemannianCoordinates.deriv_comp_translate line 877
44. lemma OAI.ThreeManifold.RiemannianCoordinates.geodesic_translate line 882
45. lemma OAI.ThreeManifold.RiemannianCoordinates.phaseLift_translate line 905
46. def OAI.ThreeManifold.RiemannianCoordinates.PhaseGeodesicAt line 922
47. lemma OAI.ThreeManifold.RiemannianCoordinates.phaseGeodesic_germ line 925
48. lemma OAI.ThreeManifold.RiemannianCoordinates.phaseGeodesic_translate line 933
49. lemma OAI.ThreeManifold.RiemannianCoordinates.phaseGeodesicOn_base line 941
50. def OAI.ThreeManifold.RiemannianCoordinates.geodesicEquation line 962
51. lemma OAI.ThreeManifold.RiemannianCoordinates.phaseGeodesic_local_existence line 982
52. lemma OAI.ThreeManifold.RiemannianCoordinates.phaseEnergy_conserved line 1014
53. theorem OAI.ThreeManifold.RiemannianCoordinates.exists_global_geodesic line 1029
54. lemma OAI.ThreeManifold.FlowContinuation.flow_contMDiff line 1058
55. def OAI.ThreeManifold.RiemannianCoordinates.globalGeodesic line 1127
56. lemma OAI.ThreeManifold.RiemannianCoordinates.globalGeodesic_initial line 1129
57. lemma OAI.ThreeManifold.RiemannianCoordinates.globalGeodesic_isGeodesic line 1131
58. def OAI.ThreeManifold.RiemannianCoordinates.geodesicFlow line 1134
59. lemma OAI.ThreeManifold.RiemannianCoordinates.geodesicFlow_zero line 1136
60. lemma OAI.ThreeManifold.RiemannianCoordinates.geodesicFlow_continuous line 1138
61. lemma OAI.ThreeManifold.RiemannianCoordinates.geodesicFlow_add line 1141
62. lemma OAI.ThreeManifold.RiemannianCoordinates.geodesicFlow_eq_chart line 1157
63. lemma OAI.ThreeManifold.RiemannianCoordinates.geodesicFlow_contMDiffAt_zero line 1192
64. theorem OAI.ThreeManifold.RiemannianCoordinates.geodesicFlow_contMDiff line 1222
65. theorem OAI.ThreeManifold.RiemannianCoordinates.exists_geodesic_local_variation line 1231
66. lemma OAI.ThreeManifold.RiemannianCoordinates.geodesicPhase_fderiv_apply line 1277
67. lemma OAI.ThreeManifold.RiemannianCoordinates.geodesicPhase_variation_smooth line 1304
68. lemma OAI.ThreeManifold.RiemannianCoordinates.linearized_geodesic_jacobi line 1319
69. lemma OAI.ThreeManifold.RiemannianCoordinates.geodesic_family_contMDiffAt line 1372
70. theorem OAI.ThreeManifold.RiemannianCoordinates.geodesic_variation_representation line 1377
71. theorem OAI.ThreeManifold.RiemannianCoordinates.geodesic_family_linearization line 1421
72. lemma OAI.ThreeManifold.RiemannianCoordinates.geodesic_family_linearization_at line 1454
73. lemma OAI.ThreeManifold.RiemannianCoordinates.smoothField_of_local_coordinates line 1483
74. lemma OAI.ThreeManifold.RiemannianCoordinates.jacobi_of_local_coordinates line 1500
75. def OAI.ThreeManifold.RiemannianCoordinates.geodesicFamily line 1534
76. def OAI.ThreeManifold.RiemannianCoordinates.geodesicVariation line 1537
77. lemma OAI.ThreeManifold.RiemannianCoordinates.geodesicFamily_isGeodesic line 1541
78. lemma OAI.ThreeManifold.RiemannianCoordinates.geodesicFamily_parameter_smooth line 1547
79. lemma OAI.ThreeManifold.RiemannianCoordinates.geodesicVariation_coordinates line 1553
80. theorem OAI.ThreeManifold.RiemannianCoordinates.geodesicVariation_isJacobi line 1580
81. lemma OAI.ThreeManifold.RiemannianCoordinates.curvatureAlong_pairing_nonpos line 1623
82. lemma OAI.ThreeManifold.RiemannianCoordinates.npc_noConjugatePoints line 1633
83. def OAI.ThreeManifold.RiemannianCoordinates.jacobiNormSq line 1647
84. def OAI.ThreeManifold.RiemannianCoordinates.jacobiNormSqSlope line 1649
85. lemma OAI.ThreeManifold.RiemannianCoordinates.jacobiNormSq_hasDerivAt line 1653
86. lemma OAI.ThreeManifold.RiemannianCoordinates.jacobiNormSqSlope_hasDerivAt line 1665
87. lemma OAI.ThreeManifold.RiemannianCoordinates.npc_jacobiNormSqSlope_deriv_lower line 1672
88. lemma OAI.ThreeManifold.RiemannianCoordinates.npc_jacobiNormSq_convex line 1684
89. def OAI.ThreeManifold.RiemannianCoordinates.fiberPhase line 1711
90. lemma OAI.ThreeManifold.RiemannianCoordinates.fiberPhase_contMDiff line 1713
91. lemma OAI.ThreeManifold.RiemannianCoordinates.fiberPhase_extChart line 1728
92. def OAI.ThreeManifold.RiemannianCoordinates.exponential line 1738
93. lemma OAI.ThreeManifold.RiemannianCoordinates.exponential_contMDiff line 1741
94. lemma OAI.ThreeManifold.RiemannianCoordinates.exponentialFamily_zero line 1746
95. lemma OAI.ThreeManifold.RiemannianCoordinates.exponentialVariation_zero line 1752
96. lemma OAI.ThreeManifold.RiemannianCoordinates.fiberPhase_extChart_fderiv line 1760
97. theorem OAI.ThreeManifold.RiemannianCoordinates.exponential_mfderiv_injective line 1771
98. lemma OAI.ThreeManifold.RiemannianCoordinates.isLocalHomeomorph_of_mfderiv_injective line 1822
99. theorem OAI.ThreeManifold.RiemannianCoordinates.exponential_isLocalHomeomorph line 1869
100. theorem OAI.ThreeManifold.RiemannianCoordinates.npc_exponential_isLocalHomeomorph line 1874
101. lemma OAI.ThreeManifold.RiemannianCoordinates.metric_cauchy_schwarz line 1886
102. def OAI.ThreeManifold.RiemannianCoordinates.jacobiNorm line 1896
103. def OAI.ThreeManifold.RiemannianCoordinates.jacobiRadialPairing line 1899
104. lemma OAI.ThreeManifold.RiemannianCoordinates.jacobiNorm_hasDerivAt line 1903
105. lemma OAI.ThreeManifold.RiemannianCoordinates.npc_jacobiNormSlope_hasDerivAt line 1916
106. theorem OAI.ThreeManifold.RiemannianCoordinates.npc_jacobiNorm_convex_Ici line 1948
107. lemma OAI.ThreeManifold.RiemannianCoordinates.connectionTerm_zero_right line 1974
108. lemma OAI.ThreeManifold.RiemannianCoordinates.jacobiNorm_initial_rightDerivative line 1979
109. theorem OAI.ThreeManifold.RiemannianCoordinates.npc_jacobiNorm_lower line 2033
110. lemma OAI.ThreeManifold.RiemannianCoordinates.exponentialVariation_initial_covariantDerivative line 2074
111. theorem OAI.ThreeManifold.RiemannianCoordinates.npc_exponential_differential_expanding line 2119
112. lemma OAI.ThreeManifold.RiemannianCoordinates.deriv_comp_mul line 2135
113. lemma OAI.ThreeManifold.RiemannianCoordinates.geodesic_scale line 2140
114. lemma OAI.ThreeManifold.RiemannianCoordinates.geodesic_const line 2174
115. lemma OAI.ThreeManifold.RiemannianCoordinates.exponential_zero line 2182
116. lemma OAI.ThreeManifold.RiemannianCoordinates.exponential_scale line 2193
117. lemma OAI.ThreeManifold.RiemannianCoordinates.curvatureAlong_velocity_pairing line 2244
118. lemma OAI.ThreeManifold.RiemannianCoordinates.jacobi_velocity_pairing line 2260
119. lemma OAI.ThreeManifold.RiemannianCoordinates.exponential_radial_differential line 2295
120. theorem OAI.ThreeManifold.RiemannianCoordinates.exponential_gauss line 2316