MetricMinusGreen.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The opposite curvature block acting on the plus Weyl gradient.

def OAI.PositiveEinsteinFour.Geometry.frameMinusCoefficient line 17
def OAI.PositiveEinsteinFour.Geometry.frameMinusCoefficientDerivative line 21

theorem OAI.PositiveEinsteinFour.Geometry.weighted_metric_minus_curvature_green line 29

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_minus_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 (frameMinusCoefficient g p))
    (hDA : ∀ p, Continuous (frameMinusCoefficientDerivative 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, frameMinusCoefficientDerivative g ((i, k), (j, l)) e) = 0)
    (hskew : ∀ i k j l e, frameMinusCoefficient g ((k, i), (j, l)) e =
…

Mentions: OAI.PositiveEinsteinFour.Geometry.FrameBundle, OAI.PositiveEinsteinFour.Geometry.FrameFlow, OAI.PositiveEinsteinFour.Geometry.frameMinusCoefficient, OAI.PositiveEinsteinFour.Geometry.frameMinusCoefficientDerivative, OAI.PositiveEinsteinFour.Geometry.frameGradientSlice, OAI.PositiveEinsteinFour.Geometry.frameHessianSlice, OAI.PositiveEinsteinFour.Geometry.frameThirdSlice