OAI/Geometry/EinsteinFour/ChartCurvatureTransition.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Differentiating the actual Christoffel transformation gives the curvature intertwining equation.

  1. def OAI.PositiveEinsteinFour.Geometry.chartWeightedConnection line 19
  2. theorem OAI.PositiveEinsteinFour.Geometry.chartWeightedConnection_contDiffAt line 24
  3. theorem OAI.PositiveEinsteinFour.Geometry.chartWeightedConnection_partial line 44
  4. theorem OAI.PositiveEinsteinFour.Geometry.chart_connection_intertwining line 78
  5. theorem OAI.PositiveEinsteinFour.Geometry.chart_connection_intertwining_derivative line 91
  6. theorem OAI.PositiveEinsteinFour.Geometry.chart_curvature_intertwining line 138
  7. theorem OAI.PositiveEinsteinFour.Geometry.chartWeightedConnection_curvature line 156
  8. theorem OAI.PositiveEinsteinFour.Geometry.coordinateCurvatureMatrix_transition line 176

    Source documentation

    The actual (1,3)-curvature in two overlapping metric charts.

    theorem coordinateCurvatureMatrix_transition (g : SmoothMetric M) (c d : M)
    (z : FourSpace) (hz : z ∈ (chartAt FourSpace c).target)
    (hx : (chartAt FourSpace c).symm z ∈ (chartAt FourSpace d).source) (i j : Fin 4) :
    coordinateCurvatureMatrix g c i j z = (chartTransitionMatrix c d z)⁻¹ *
      (∑ a, ∑ b, (chartTransitionMatrix c d z a i * chartTransitionMatrix c d z b j) •
        coordinateCurvatureMatrix g d a b (chartTransition c d z)) *
          chartTransitionMatrix c d z := by
…

    Mentions: OAI.PositiveEinsteinFour.Geometry.coordinateCurvatureMatrix, OAI.PositiveEinsteinFour.Geometry.chartTransitionMatrix, OAI.PositiveEinsteinFour.Geometry.chartTransition