OAI/Geometry/EinsteinFour/CurvatureForm.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The actual coordinate curvature is a four-linear form. This supplies the multilinearity used to change normal frames without an independent curvature-transformation assumption.

  1. def OAI.PositiveEinsteinFour.Geometry.fourIndicesEquiv line 20
  2. theorem OAI.PositiveEinsteinFour.Geometry.sum_four_indices line 26

    Distinct definitions of this name: OAI/Geometry/EinsteinFour/WeylEstimates03.lean:5373 (different declaration text). Qualify references as OAI.PositiveEinsteinFour.Geometry.sum_four_indices@path.

  3. theorem OAI.PositiveEinsteinFour.Geometry.multilinear_combinations line 33
  4. def OAI.PositiveEinsteinFour.Geometry.curvatureForm line 59
  5. theorem OAI.PositiveEinsteinFour.Geometry.frameCurvature_eq_form line 85
  6. theorem OAI.PositiveEinsteinFour.Geometry.OrthonormalFrame.turn_vector line 90
  7. theorem OAI.PositiveEinsteinFour.Geometry.frameCurvature_turn line 96
  8. theorem OAI.PositiveEinsteinFour.Geometry.frameCurvatureField_turn line 113