OAI/Geometry/EinsteinFour/CurvatureMetricSkew.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

Differentiated metric compatibility gives skew-adjointness of actual coordinate curvature, and hence the last-slot symmetry of frame curvature.

  1. def OAI.PositiveEinsteinFour.Geometry.matrixPartial line 19
  2. def OAI.PositiveEinsteinFour.Geometry.connectionMatrix line 22
  3. theorem OAI.PositiveEinsteinFour.Geometry.partial_mul line 25
  4. theorem OAI.PositiveEinsteinFour.Geometry.matrixPartial_add line 33
  5. theorem OAI.PositiveEinsteinFour.Geometry.matrixPartial_mul line 41
  6. theorem OAI.PositiveEinsteinFour.Geometry.matrixPartial_transpose line 56
  7. theorem OAI.PositiveEinsteinFour.Geometry.matrixPartial_congr line 59
  8. theorem OAI.PositiveEinsteinFour.Geometry.matrixPartial_comm line 66
  9. theorem OAI.PositiveEinsteinFour.Geometry.matrixPartial_metric line 82
  10. theorem OAI.PositiveEinsteinFour.Geometry.matrix_mul_differentiable line 99
  11. theorem OAI.PositiveEinsteinFour.Geometry.matrixPartial_metric_second line 107
  12. def OAI.PositiveEinsteinFour.Geometry.coordinateCurvatureMatrix line 140
  13. theorem OAI.PositiveEinsteinFour.Geometry.coordinateCurvatureMatrix_apply line 147
  14. theorem OAI.PositiveEinsteinFour.Geometry.coordinateCurvatureMatrix_skew line 154
  15. theorem OAI.PositiveEinsteinFour.Geometry.lowered_curvature_last_skew line 168
  16. theorem OAI.PositiveEinsteinFour.Geometry.lowered_curvature_last_skew_at_center line 189