OAI/Geometry/EinsteinFour/CoordinateMetricCompatibility.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The metric-compatibility identity for the actual Christoffel formula. This algebraic step needs only invertibility of the chart metric.

  1. theorem OAI.PositiveEinsteinFour.Geometry.matrix_lower_inverse line 18
  2. theorem OAI.PositiveEinsteinFour.Geometry.lowered_christoffel line 26
  3. theorem OAI.PositiveEinsteinFour.Geometry.christoffel_metric_compatibility line 34
  4. theorem OAI.PositiveEinsteinFour.Geometry.christoffel_metric_compatibility_at_center line 45
  5. theorem OAI.PositiveEinsteinFour.Geometry.curvature_matrix_skew_of_metric_differentials line 55

    Source documentation

    Differentiating metric compatibility in two coordinate directions leaves exactly the skew-adjointness equation for their curvature commutator.

    theorem curvature_matrix_skew_of_metric_differentials (G A B C D : Mat4)
    (hmixed :
      Cᵀ * G + Bᵀ * (Aᵀ * G + G * A) + (Aᵀ * G + G * A) * B + G * C =
      Dᵀ * G + Aᵀ * (Bᵀ * G + G * B) + (Bᵀ * G + G * B) * A + G * D) :
    (C - D + A * B - B * A)ᵀ * G + G * (C - D + A * B - B * A) = 0 := by
…

    Mentions: OAI.PositiveEinsteinFour.Geometry.Mat4