OAI/Geometry/EinsteinFour/CurvatureCoordinateSmoothness.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Local regularity of the actual curvature and its coordinate covariant derivatives, on the nonsingular part of a metric chart.

  1. theorem OAI.PositiveEinsteinFour.Geometry.curvatureComponent_contDiffAt line 19
  2. theorem OAI.PositiveEinsteinFour.Geometry.curvatureCoordinates_contDiffAt line 33
  3. theorem OAI.PositiveEinsteinFour.Geometry.unitCurvatureCoordinates_contDiffAt line 43
  4. theorem OAI.PositiveEinsteinFour.Geometry.normalizedWeylCoordinates_contDiffAt line 50
  5. theorem OAI.PositiveEinsteinFour.Geometry.covariantDerivative_contDiffAt line 57
  6. theorem OAI.PositiveEinsteinFour.Geometry.covariantDerivative_sub line 73

    Source documentation

    Linearity is proved for differentiable coordinate tensors, so it also applies to the actual curvature fields on a metric chart.

    theorem covariantDerivative_sub (g : SmoothMetric M) (c : M) (z : FourSpace)
    {n : ℕ} (S T : FourSpace → CovariantCoordinates n)
    (hS : ∀ a, DifferentiableAt ℝ (fun w => S w a) z)
    (hT : ∀ a, DifferentiableAt ℝ (fun w => T w a) z) :
    covariantDerivative g c (fun w => S w - T w) z =
      covariantDerivative g c S z - covariantDerivative g c T z := by
…

    Mentions: OAI.PositiveEinsteinFour.Geometry.CovariantCoordinates, OAI.PositiveEinsteinFour.Geometry.covariantDerivative

  7. theorem OAI.PositiveEinsteinFour.Geometry.covariantDerivative_congr line 90