MetricMatrixGreen.lean`

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The varying-coefficient Green identity for the actual Weyl matrix slot.

def OAI.PositiveEinsteinFour.Geometry.frameWeylMatrix line 21
def OAI.PositiveEinsteinFour.Geometry.frameWeylGradientMatrix line 24
def OAI.PositiveEinsteinFour.Geometry.frameWeylHessianMatrix line 27
theorem OAI.PositiveEinsteinFour.Geometry.weighted_metric_matrix_slot_green line 33
Source documentation
The first-derivative and Laplacian corrections in the nonparallel matrix-slot term follow from differentiating the actual Weyl coefficient. No derivative of a chosen eigenframe occurs.
```
theorem weighted_metric_matrix_slot_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, ℝ))
    (hT : Continuous (frameWeylMatrix g))
    (hDT : ∀ i, Continuous (frameWeylGradientMatrix g i))
    (hDDT : ∀ i, Continuous (frameWeylHessianMatrix g i i))
    (hZ : Continuous (frameGradientVector g))
    (hX : ∀ i, Continuous (frameHessianVector g i))
    (hXX : ∀ i, Continuous (frameThirdVector g i i))
    (hDsym : ∀ i e, symmetric (frameWeylGradientMatrix g i e))
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.FrameBundle, OAI.PositiveEinsteinFour.Geometry.FrameFlow, OAI.PositiveEinsteinFour.Geometry.frameWeylMatrix, OAI.PositiveEinsteinFour.Geometry.frameWeylGradientMatrix, OAI.PositiveEinsteinFour.Geometry.frameWeylHessianMatrix, OAI.PositiveEinsteinFour.Geometry.frameGradientVector, OAI.PositiveEinsteinFour.Geometry.frameHessianVector, OAI.PositiveEinsteinFour.Geometry.frameThirdVector