OAI/Geometry/EinsteinFour/ChartMetricTransition.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The actual metric pullback matrix in a chart. The tangent coordinates at the image point use its own centered chart, so this congruence is the zeroth-order part of the curvature coordinate-change calculation.

  1. def OAI.PositiveEinsteinFour.Geometry.chartInverseMatrix line 19
  2. theorem OAI.PositiveEinsteinFour.Geometry.metricInChart_eq_center_congruence line 23
  3. def OAI.PositiveEinsteinFour.Geometry.chartTransition line 35
  4. def OAI.PositiveEinsteinFour.Geometry.chartTransitionMatrix line 38
  5. theorem OAI.PositiveEinsteinFour.Geometry.chartTransition_contDiffAt line 41
  6. theorem OAI.PositiveEinsteinFour.Geometry.chartTransition_fderiv line 51
  7. theorem OAI.PositiveEinsteinFour.Geometry.metricInChart_transition line 66