OAI/Geometry/ConjugatePoints/Basic.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.ThreeManifold.E3 line 15

   Also declared: ComparatorChallenges/ConjugatePoints.lean:11 (same declaration text).

2. abbrev OAI.ThreeManifold.I3 line 16

   Also declared: ComparatorChallenges/ConjugatePoints.lean:12 (same declaration text).

3. def OAI.ThreeManifold.OrientedAtlas line 20

   Also declared: ComparatorChallenges/ConjugatePoints.lean:16 (same declaration text).

4. abbrev OAI.ThreeManifold.SmoothMetric line 27

   Also declared: ComparatorChallenges/ConjugatePoints.lean:23 (same declaration text).

5. def OAI.ThreeManifold.basisVector line 31

   Also declared: ComparatorChallenges/ConjugatePoints.lean:27 (same declaration text).

6. def OAI.ThreeManifold.metricMatrix line 33

   Also declared: ComparatorChallenges/ConjugatePoints.lean:29 (same declaration text).

7. def OAI.ThreeManifold.coordPartial line 39

   Also declared: ComparatorChallenges/ConjugatePoints.lean:35 (same declaration text).

8. def OAI.ThreeManifold.christoffel line 42

   Also declared: ComparatorChallenges/ConjugatePoints.lean:38 (same declaration text).

9. def OAI.ThreeManifold.connectionTerm line 49

   Also declared: ComparatorChallenges/ConjugatePoints.lean:45 (same declaration text).

10. def OAI.ThreeManifold.curvatureCoefficient line 53

    Also declared: ComparatorChallenges/ConjugatePoints.lean:49 (same declaration text).

11. def OAI.ThreeManifold.curvatureTerm line 60

    Also declared: ComparatorChallenges/ConjugatePoints.lean:56 (same declaration text).

12. def OAI.ThreeManifold.NonpositiveSectionalCurvature line 65

    Also declared: ComparatorChallenges/ConjugatePoints.lean:61 (same declaration text).

13. def OAI.ThreeManifold.alongDerivative line 71

    Also declared: ComparatorChallenges/ConjugatePoints.lean:67 (same declaration text).

14. def OAI.ThreeManifold.IsGeodesicOn line 75

    Also declared: ComparatorChallenges/ConjugatePoints.lean:71 (same declaration text).

15. def OAI.ThreeManifold.fieldCoordinates line 81

    Also declared: ComparatorChallenges/ConjugatePoints.lean:77 (same declaration text).

16. def OAI.ThreeManifold.IsJacobiFieldOn line 85

    Also declared: ComparatorChallenges/ConjugatePoints.lean:81 (same declaration text).

17. def OAI.ThreeManifold.NoConjugatePoints line 95

    Also declared: ComparatorChallenges/ConjugatePoints.lean:91 (same declaration text).

18. def OAI.ThreeManifold.MainStatement line 101

    Also declared: ComparatorChallenges/ConjugatePoints.lean:97 (same declaration text).