OAI/Geometry/EinsteinFour/FourDeterminantDerivative.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Determinant differentiation in the four-dimensional coordinates used for the metric volume density. The proof uses the alternating determinant and its row-replacement formula, without a matrix inverse.

  1. def OAI.PositiveEinsteinFour.Geometry.determinantForm line 24
  2. def OAI.PositiveEinsteinFour.Geometry.determinantDifferential line 29
  3. theorem OAI.PositiveEinsteinFour.Geometry.determinantDifferential_apply line 33
  4. theorem OAI.PositiveEinsteinFour.Geometry.hasDerivAt_det_of_components line 43
  5. theorem OAI.PositiveEinsteinFour.Geometry.determinantDifferential_left line 52
  6. theorem OAI.PositiveEinsteinFour.Geometry.determinantDifferential_transpose line 61
  7. theorem OAI.PositiveEinsteinFour.Geometry.determinantDifferential_right line 73
  8. theorem OAI.PositiveEinsteinFour.Geometry.determinantDifferential_congruence line 80

    Source documentation

    The determinant of a metric Gram matrix has twice the connection trace as its logarithmic derivative.

    theorem determinantDifferential_congruence (G C : Matrix (Fin 4) (Fin 4) ℝ) :
    determinantDifferential G (Cᵀ * G + G * C) = 2 * C.trace * G.det := by
…

    Mentions: OAI.PositiveEinsteinFour.Geometry.determinantDifferential