OAI/Geometry/EinsteinFour/WeightedConnectionCurvature.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The curvature of the pulled-back connection one-form. The symmetric second derivative of the coordinate change cancels in the alternating sum.

  1. theorem OAI.PositiveEinsteinFour.Geometry.matrixPartial_smul line 15
  2. theorem OAI.PositiveEinsteinFour.Geometry.matrixPartial_sum_four line 25
  3. def OAI.PositiveEinsteinFour.Geometry.weightedConnectionDerivative line 35
  4. theorem OAI.PositiveEinsteinFour.Geometry.weightedConnection_mul line 39
  5. theorem OAI.PositiveEinsteinFour.Geometry.weightedConnection_curvature line 51