OAI/Geometry/ConjugatePoints/Continuation.lean

GitHub source file

46 declarations, 0 contain sorry, 0 declared as axioms

Geodesic continuation and the covering exponential map.

  1. theorem OAI.ThreeManifold.FlowContinuation.Equation.exists_global_of_finite_time_extensions line 16
  2. theorem OAI.ThreeManifold.FlowContinuation.Equation.exists_global_of_compact_bounds line 77
  3. abbrev OAI.ThreeManifold.PathContinuation.State line 116
  4. def OAI.ThreeManifold.PathContinuation.Holds line 118
  5. lemma OAI.ThreeManifold.PathContinuation.holds_shift line 121
  6. lemma OAI.ThreeManifold.PathContinuation.holds_continuousAt line 133
  7. lemma OAI.ThreeManifold.PathContinuation.holds_time_derivative line 139
  8. lemma OAI.ThreeManifold.PathContinuation.holds_space_derivative line 144
  9. lemma OAI.ThreeManifold.PathContinuation.holds_unique line 150
  10. def OAI.ThreeManifold.PathContinuation.equation line 169
  11. lemma OAI.ThreeManifold.PathContinuation.time_affine line 178
  12. lemma OAI.ThreeManifold.RiemannianCoordinates.localInverseAt_contMDiffAt line 196
  13. lemma OAI.ThreeManifold.RiemannianCoordinates.localInverseAt_contMDiffOn line 232
  14. theorem OAI.ThreeManifold.PathContinuation.local_lift_exists line 261
  15. theorem OAI.ThreeManifold.positive_bilinear_norm_bound line 324
  16. lemma OAI.ThreeManifold.PathContinuation.lift_derivative_eq line 362
  17. lemma OAI.ThreeManifold.PathContinuation.continuous_phaseLift_C1 line 382
  18. theorem OAI.ThreeManifold.PathContinuation.exponential_lift_compact_bounds line 392
  19. def OAI.ThreeManifold.RiemannianCoordinates.regularRadius line 461
  20. lemma OAI.ThreeManifold.RiemannianCoordinates.regularRadius_hasDerivAt line 464
  21. lemma OAI.ThreeManifold.RiemannianCoordinates.exponential_radial_bound line 483
  22. theorem OAI.ThreeManifold.PathContinuation.ncp_exponential_lift_compact_bounds line 504
  23. lemma OAI.ThreeManifold.RiemannianCoordinates.contDiff_lift_of_localHomeomorph line 584
  24. theorem OAI.ThreeManifold.RiemannianCoordinates.npc_exponential_path_lift line 605
  25. lemma OAI.ThreeManifold.localHomeomorph_discrete_fiber line 641
  26. theorem OAI.ThreeManifold.evenlyCovered_of_radial_lifts line 650
  27. lemma OAI.ThreeManifold.RiemannianCoordinates.smooth_radial_neighborhood line 735
  28. lemma OAI.ThreeManifold.RiemannianCoordinates.covering_of_global_smooth_lifts line 781
  29. theorem OAI.ThreeManifold.RiemannianCoordinates.npc_exponential_isCoveringMap line 808
  30. theorem OAI.ThreeManifold.RiemannianCoordinates.ncp_exponential_path_lift line 825
  31. theorem OAI.ThreeManifold.RiemannianCoordinates.ncp_exponential_isCoveringMap line 852
  32. def OAI.ThreeManifold.RiemannianCoordinates.closedCurvePath line 861
  33. theorem OAI.ThreeManifold.RiemannianCoordinates.closedGeodesic_essential line 867
  34. lemma OAI.ThreeManifold.RiemannianCoordinates.LocalMetricIsometry.velocity_map_ne_zero line 904
  35. lemma OAI.ThreeManifold.CompactMetric.universal_fiber_velocity line 918
  36. lemma OAI.ThreeManifold.CompactMetric.core_fiber_velocity line 942
  37. def OAI.ThreeManifold.CompactMetric.lowPoint line 947
  38. lemma OAI.ThreeManifold.CompactMetric.lowPoint_height line 948
  39. lemma OAI.ThreeManifold.CompactMetric.lowPoint_core line 953
  40. def OAI.ThreeManifold.CompactMetric.pieceFiber line 956
  41. lemma OAI.ThreeManifold.CompactMetric.pieceFiber_smooth line 958
  42. lemma OAI.ThreeManifold.CompactMetric.whole_fiber_geodesic line 968
  43. lemma OAI.ThreeManifold.CompactMetric.piece_fiber_geodesic line 977
  44. lemma OAI.ThreeManifold.CompactMetric.piece_fiber_velocity line 986
  45. lemma OAI.ThreeManifold.CompactMetric.compact_fiber_geodesic line 999
  46. lemma OAI.ThreeManifold.CompactMetric.compact_fiber_velocity line 1002