OAI/Geometry/EinsteinFour/FrameCurvature.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The two fields on the actual orthonormal frame bundle that enter the geodesic mean-square argument. They are evaluations of the metric curvature and its covariant derivative, with no independent curvature field.

  1. def OAI.PositiveEinsteinFour.Geometry.firstDirection line 17
  2. theorem OAI.PositiveEinsteinFour.Geometry.firstDirection_apply line 21
  3. theorem OAI.PositiveEinsteinFour.Geometry.firstDirection_normal line 25
  4. def OAI.PositiveEinsteinFour.Geometry.frameCurvatureField line 34
  5. def OAI.PositiveEinsteinFour.Geometry.frameCurvatureDerivative line 37
  6. theorem OAI.PositiveEinsteinFour.Geometry.frameCurvatureField_apply line 40
  7. theorem OAI.PositiveEinsteinFour.Geometry.frameCurvatureDerivative_eq line 50