OAI/Geometry/EinsteinFour/ActualRicciContraction.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Contraction of the actual chart curvature in an orthonormal frame. This is a finite change-of-basis calculation, used to discharge the Ricci positivity needed by constant Einstein normalization.

  1. theorem OAI.PositiveEinsteinFour.Geometry.sum_six_rotate line 16
  2. theorem OAI.PositiveEinsteinFour.Geometry.tensor_trace_basis_change line 48
  3. theorem OAI.PositiveEinsteinFour.Geometry.OrthonormalFrame.inverse_contraction line 93
  4. theorem OAI.PositiveEinsteinFour.Geometry.frameCurvature_ricci line 114
  5. theorem OAI.PositiveEinsteinFour.Geometry.curvatureComponent_first_skew line 129
  6. theorem OAI.PositiveEinsteinFour.Geometry.frameCurvature_first_skew line 135
  7. theorem OAI.PositiveEinsteinFour.Geometry.frameCurvature_first_self line 166