OAI/Geometry/EinsteinFour/WeylNormal.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Link the normal-tensor calculation to the concrete metric. The classical curvature decomposition is displayed as an explicit local hypothesis here; the angular mean identities themselves are proved, not postulated.

  1. theorem OAI.PositiveEinsteinFour.Geometry.squareNorm_eq_frobenius_norm_sq line 21
  2. def OAI.PositiveEinsteinFour.Geometry.normalCurvature line 30
  3. def OAI.PositiveEinsteinFour.Geometry.normalCurvatureDeviation line 34
  4. theorem OAI.PositiveEinsteinFour.Geometry.normalCurvature_eq_of_decomposition line 38
  5. theorem OAI.PositiveEinsteinFour.Geometry.normalCurvatureDeviation_eq_of_decomposition line 48
  6. theorem OAI.PositiveEinsteinFour.Geometry.normalCurvatureDeviation_mean_square line 57
  7. def OAI.PositiveEinsteinFour.Geometry.normalCurvatureDerivative line 69

    Source documentation

    The derivative field uses the metric's actual covariant derivatives.

    def normalCurvatureDerivative (g : SmoothMetric M) (c : M)
    (e : OrthonormalFrame g c) (q : Directions) : Mat3 :=
…

    Mentions: OAI.PositiveEinsteinFour.Geometry.OrthonormalFrame, OAI.PositiveEinsteinFour.Geometry.Mat3

  8. theorem OAI.PositiveEinsteinFour.Geometry.normalCurvatureDerivative_mean_square line 73
  9. theorem OAI.PositiveEinsteinFour.Geometry.normalCurvatureDeviation_mean_frobenius line 82