OAI/Geometry/EinsteinFour/ChartConnectionTransition.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The connection coordinate change is derived from the actual metric pullback, using metric compatibility and zero torsion.

  1. def OAI.PositiveEinsteinFour.Geometry.pulledChartConnection line 18
  2. theorem OAI.PositiveEinsteinFour.Geometry.chartTransitionMatrix_det_ne_zero line 25
  3. theorem OAI.PositiveEinsteinFour.Geometry.chartTransitionMatrix_contDiffAt line 34
  4. theorem OAI.PositiveEinsteinFour.Geometry.matrixPartial_transition_target_metric line 41
  5. theorem OAI.PositiveEinsteinFour.Geometry.pulledChartConnection_metric line 64
  6. theorem OAI.PositiveEinsteinFour.Geometry.pulledChartConnection_torsion line 105
  7. theorem OAI.PositiveEinsteinFour.Geometry.christoffel_transition line 119