OAI/Geometry/EinsteinFour/OrthonormalFrame.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Existence of the concrete orthonormal frames used for the curvature blocks. This is obtained from the actual positive metric matrix.

  1. theorem OAI.PositiveEinsteinFour.Geometry.chartMetric_apply line 19
  2. theorem OAI.PositiveEinsteinFour.Geometry.sum_coordinateVector line 30
  3. theorem OAI.PositiveEinsteinFour.Geometry.chartMetric_pairing line 35
  4. theorem OAI.PositiveEinsteinFour.Geometry.chartMetric_posDef line 59
  5. def OAI.PositiveEinsteinFour.Geometry.canonicalFrame line 75

    Source documentation

    A fixed, canonical choice from the positive square root of the inverse metric. No choice of curvature eigenvectors is needed for this frame.

    def canonicalFrame (g : SmoothMetric M) (c : M) : OrthonormalFrame g c where
…

    Mentions: OAI.PositiveEinsteinFour.Geometry.OrthonormalFrame

  6. instance OAI.PositiveEinsteinFour.Geometry.(instance at line 85) line 85