OAI/Geometry/EinsteinFour/GeodesicJacobiSecondVariationAlgebra.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

Finite metric algebra for the second variation of energy.

  1. def OAI.PositiveEinsteinFour.Geometry.jacobiMetricPair line 14
  2. theorem OAI.PositiveEinsteinFour.Geometry.jacobiMetricPair_symm line 17
  3. theorem OAI.PositiveEinsteinFour.Geometry.jacobiMetricPair_add_left line 21
  4. theorem OAI.PositiveEinsteinFour.Geometry.jacobiMetricPair_add_right line 25
  5. theorem OAI.PositiveEinsteinFour.Geometry.jacobiMetricPair_smul_right line 29
  6. theorem OAI.PositiveEinsteinFour.Geometry.jacobiMetricPair_neg_left line 33
  7. theorem OAI.PositiveEinsteinFour.Geometry.jacobiMetricPair_matrix_add line 37
  8. theorem OAI.PositiveEinsteinFour.Geometry.jacobiMetricPair_left_product line 41
  9. theorem OAI.PositiveEinsteinFour.Geometry.jacobiMetricPair_right_product line 46
  10. def OAI.PositiveEinsteinFour.Geometry.jacobiMetricRate line 50
  11. def OAI.PositiveEinsteinFour.Geometry.jacobiMetricSecondRate line 52
  12. theorem OAI.PositiveEinsteinFour.Geometry.jacobiMetricRate_pair line 55
  13. theorem OAI.PositiveEinsteinFour.Geometry.jacobiMetricRate_symm line 61
  14. theorem OAI.PositiveEinsteinFour.Geometry.jacobiMetricSecondRate_pair_self line 67
  15. def OAI.PositiveEinsteinFour.Geometry.coordinateEnergySecondDensity line 82
  16. theorem OAI.PositiveEinsteinFour.Geometry.coordinateEnergySecondDensity_expansion line 86
  17. theorem OAI.PositiveEinsteinFour.Geometry.jacobiMetricPair_skew line 97
  18. theorem OAI.PositiveEinsteinFour.Geometry.jacobiSecondVariation_vector_identity line 110

    Source documentation

    The vector terms left after adding the boundary derivative to the curvature term collapse by torsion freedom and its derivative.

    theorem jacobiSecondVariation_vector_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 y : JacobiCoordinateVector) :
    jacobiCurvature Γ D y v *ᵥ y +
        jacobiConnection Γ v *ᵥ (jacobiConnection Γ y *ᵥ y) +
        jacobiConnectionDerivative D v y *ᵥ y =
      jacobiConnectionDerivative D y y *ᵥ v +
        jacobiConnection Γ y *ᵥ (jacobiConnection Γ y *ᵥ v) := by
…

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

  19. def OAI.PositiveEinsteinFour.Geometry.coordinateIndexDensity line 126
  20. def OAI.PositiveEinsteinFour.Geometry.coordinateEnergyBoundaryRate line 132
  21. theorem OAI.PositiveEinsteinFour.Geometry.coordinateEnergySecondDensity_eq_index_add_boundary line 140

    Source documentation

    The full pointwise second-variation identity.

    theorem coordinateEnergySecondDensity_eq_index_add_boundary
    (G : Mat4) (Γ : Fin 4 → Mat4) (D : Fin 4 → Fin 4 → Mat4)
    (hG : G.IsSymm) (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 y w : JacobiCoordinateVector)
    (hK : (jacobiCurvature Γ D y v)ᵀ * G + G * jacobiCurvature Γ D y v = 0) :
    coordinateEnergySecondDensity G (jacobiMetricRate G (jacobiConnection Γ y))
        (jacobiMetricSecondRate G (jacobiConnection Γ y) (jacobiConnectionDerivative D y y)) v w =
      coordinateIndexDensity G Γ D v y w + coordinateEnergyBoundaryRate G Γ D v y w := by
…

    Mentions: OAI.PositiveEinsteinFour.Geometry.Mat4, OAI.PositiveEinsteinFour.Geometry.JacobiCoordinateVector, OAI.PositiveEinsteinFour.Geometry.jacobiCurvature, OAI.PositiveEinsteinFour.Geometry.coordinateEnergySecondDensity, OAI.PositiveEinsteinFour.Geometry.jacobiMetricRate, OAI.PositiveEinsteinFour.Geometry.jacobiConnection, OAI.PositiveEinsteinFour.Geometry.jacobiMetricSecondRate, OAI.PositiveEinsteinFour.Geometry.jacobiConnectionDerivative, OAI.PositiveEinsteinFour.Geometry.coordinateIndexDensity, OAI.PositiveEinsteinFour.Geometry.coordinateEnergyBoundaryRate