OAI/Geometry/EinsteinFour/MetricCurvatureGreen.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Derivative-slot integration for the actual metric Weyl Hessian. The coefficient and its derivative are both the concrete quaternion curvature block. The only differential premises are parallel differentiation and the classical divergence and skew identities.

  1. abbrev OAI.PositiveEinsteinFour.Geometry.MatrixVector line 18
  2. def OAI.PositiveEinsteinFour.Geometry.matrixVector line 20
  3. theorem OAI.PositiveEinsteinFour.Geometry.inner_matrixVector line 22
  4. def OAI.PositiveEinsteinFour.Geometry.frameGradientSlice line 35
  5. def OAI.PositiveEinsteinFour.Geometry.frameHessianSlice line 38
  6. def OAI.PositiveEinsteinFour.Geometry.frameThirdSlice line 41
  7. def OAI.PositiveEinsteinFour.Geometry.framePlusCoefficient line 44
  8. def OAI.PositiveEinsteinFour.Geometry.framePlusCoefficientDerivative line 48
  9. theorem OAI.PositiveEinsteinFour.Geometry.weighted_metric_curvature_green line 56

    Source documentation

    The derivative-slot Green formula on the actual metric tensors. The third derivatives retain their order; the half factor is proved by skewing the first two slots, before any Ricci substitution.

    theorem weighted_metric_curvature_green
    (g : SmoothMetric M) {μ : Measure (FrameBundle g)}
    [CompactSpace (FrameBundle g)] [IsFiniteMeasure μ]
    (φ : Fin 4 → FrameFlow g μ)
    (m : C(FrameBundle g, ℝ)) (dm : Fin 4 → C(FrameBundle g, ℝ))
    (hA : ∀ p, Continuous (framePlusCoefficient g p))
    (hDA : ∀ p, Continuous (framePlusCoefficientDerivative g p))
    (hZ : ∀ j, Continuous (frameGradientSlice g j))
    (hX : ∀ i j, Continuous (frameHessianSlice g i j))
    (hD : ∀ i k j, Continuous (frameThirdSlice g i k j))
    (hdiv : ∀ i j l e, (∑ k, framePlusCoefficientDerivative g ((i, k), (j, l)) e) = 0)
    (hskew : ∀ i k j l e, framePlusCoefficient g ((k, i), (j, l)) e =
…

    Mentions: OAI.PositiveEinsteinFour.Geometry.FrameBundle, OAI.PositiveEinsteinFour.Geometry.FrameFlow, OAI.PositiveEinsteinFour.Geometry.framePlusCoefficient, OAI.PositiveEinsteinFour.Geometry.framePlusCoefficientDerivative, OAI.PositiveEinsteinFour.Geometry.frameGradientSlice, OAI.PositiveEinsteinFour.Geometry.frameHessianSlice, OAI.PositiveEinsteinFour.Geometry.frameThirdSlice