OAI/Geometry/EinsteinFour/GeodesicJacobiAlgebra.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.PositiveEinsteinFour.Geometry.JacobiCoordinateVector line 16
2. def OAI.PositiveEinsteinFour.Geometry.jacobiConnection line 18
3. def OAI.PositiveEinsteinFour.Geometry.jacobiConnectionDerivative line 21
4. def OAI.PositiveEinsteinFour.Geometry.jacobiCurvature line 24
5. theorem OAI.PositiveEinsteinFour.Geometry.weighted_matrix_swap line 28
6. theorem OAI.PositiveEinsteinFour.Geometry.jacobiConnection_mul line 38
7. theorem OAI.PositiveEinsteinFour.Geometry.jacobiCurvature_eq line 51
8. theorem OAI.PositiveEinsteinFour.Geometry.jacobiConnection_mulVec_comm line 63
9. theorem OAI.PositiveEinsteinFour.Geometry.jacobiConnectionDerivative_mulVec_comm line 77
10. theorem OAI.PositiveEinsteinFour.Geometry.linearized_geodesic_curvature_identity line 99

    Source documentation

    The coordinate variation equation implies the covariant Jacobi equation. Only torsion freedom and its differentiated identity enter.

    theorem linearized_geodesic_curvature_identity
        (Γ : Fin 4 → Mat4) (D : Fin 4 → Fin 4 → Mat4)
        (hΓ : ∀ a i j, Γ i a j = Γ j a i)
        (hD : ∀ r a i j, D r i a j = D r j a i)
        (v a y w b : JacobiCoordinateVector)
        (ha : a = -(jacobiConnection Γ v *ᵥ v))
        (hb : b = -(jacobiConnectionDerivative D y v *ᵥ v) -
          jacobiConnection Γ w *ᵥ v - jacobiConnection Γ v *ᵥ w) :
        b + jacobiConnectionDerivative D v v *ᵥ y + jacobiConnection Γ a *ᵥ y +
          (2 : ℝ) • (jacobiConnection Γ v *ᵥ w) +
          jacobiConnection Γ v *ᵥ (jacobiConnection Γ v *ᵥ y) +
          jacobiCurvature Γ D y v *ᵥ v = 0 := by
    …

    Mentions: OAI.PositiveEinsteinFour.Geometry.Mat4, OAI.PositiveEinsteinFour.Geometry.JacobiCoordinateVector, OAI.PositiveEinsteinFour.Geometry.jacobiConnection, OAI.PositiveEinsteinFour.Geometry.jacobiConnectionDerivative, OAI.PositiveEinsteinFour.Geometry.jacobiCurvature

11. theorem OAI.PositiveEinsteinFour.Geometry.actual_jacobiConnection_comm line 124
12. theorem OAI.PositiveEinsteinFour.Geometry.actual_jacobiCurvature_eq line 130
13. theorem OAI.PositiveEinsteinFour.Geometry.actual_linearized_geodesic_curvature_identity line 136