OAI/Geometry/EinsteinFour/AngularCurvature.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

The normal Jacobi form of the actual quaternion curvature decomposition.

  1. abbrev OAI.PositiveEinsteinFour.Angular.CurvatureArray line 13
  2. def OAI.PositiveEinsteinFour.Angular.normalVector line 15
  3. def OAI.PositiveEinsteinFour.Angular.twoFormNormal line 18
  4. theorem OAI.PositiveEinsteinFour.Angular.twoFormNormal_plus line 21
  5. theorem OAI.PositiveEinsteinFour.Angular.twoFormNormal_minus line 30
  6. def OAI.PositiveEinsteinFour.Angular.normalEvaluation line 39

    Source documentation

    Evaluate <R(I_i q,q)q,I_j q> as a linear functional on four-tensors.

    def normalEvaluation (q : Directions) (i j : Fin 3) : CurvatureArray →ₗ[ℝ] ℝ where
…

    Mentions: OAI.PositiveEinsteinFour.Angular.Directions, OAI.PositiveEinsteinFour.Angular.CurvatureArray

  7. def OAI.PositiveEinsteinFour.Angular.twoFormProduct line 46
  8. theorem OAI.PositiveEinsteinFour.Angular.normalEvaluation_product line 48
  9. def OAI.PositiveEinsteinFour.Angular.blockTensor line 76
  10. theorem OAI.PositiveEinsteinFour.Angular.normalEvaluation_blockTensor line 79
  11. def OAI.PositiveEinsteinFour.Angular.einsteinCurvatureTensor line 87

    Source documentation

    Ric=3g removes the off-diagonal curvature blocks.

    def einsteinCurvatureTensor (T U : Mat3) : CurvatureArray :=
…

    Mentions: OAI.PositiveEinsteinFour.Angular.Mat3, OAI.PositiveEinsteinFour.Angular.CurvatureArray

  12. theorem OAI.PositiveEinsteinFour.Angular.normalEvaluation_einstein line 91

    Source documentation

    Curvature decomposition gives the normal matrix used by the Jacobi ODE.

    theorem normalEvaluation_einstein (T U : Mat3) (q : Directions) (i j : Fin 3) :
    normalEvaluation q i j (einsteinCurvatureTensor T U) =
      (1 + normalDeviation T U q) i j := by
…

    Mentions: OAI.PositiveEinsteinFour.Angular.Mat3, OAI.PositiveEinsteinFour.Angular.Directions, OAI.PositiveEinsteinFour.Angular.normalEvaluation, OAI.PositiveEinsteinFour.Angular.einsteinCurvatureTensor, OAI.PositiveEinsteinFour.Angular.normalDeviation