OAI/Geometry/EinsteinFour/CoordinateSecondBianchi.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Specialization of the second Bianchi algebra to the actual smooth Christoffel symbols, with all four curvature slots differentiated.

  1. theorem OAI.PositiveEinsteinFour.Geometry.matrixPartial_sub line 16
  2. theorem OAI.PositiveEinsteinFour.Geometry.product_entries_differentiable line 24
  3. theorem OAI.PositiveEinsteinFour.Geometry.connectionMatrix_partial_contDiffAt line 35
  4. theorem OAI.PositiveEinsteinFour.Geometry.coordinateCurvatureMatrix_eq_algebra line 42
  5. theorem OAI.PositiveEinsteinFour.Geometry.coordinateCurvatureMatrix_contDiffAt line 48
  6. theorem OAI.PositiveEinsteinFour.Geometry.matrixPartial_coordinateCurvature line 64
  7. def OAI.PositiveEinsteinFour.Geometry.coordinateCovariantCurvatureDerivative line 99
  8. theorem OAI.PositiveEinsteinFour.Geometry.coordinateCovariantCurvatureDerivative_eq_algebra line 107
  9. theorem OAI.PositiveEinsteinFour.Geometry.coordinate_second_bianchi line 122
  10. theorem OAI.PositiveEinsteinFour.Geometry.coordinate_second_bianchi_at_center line 136