MetricHessian.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

The weighted rough-Laplacian identity for the metric's actual Weyl gradient. Differentiation takes place in the coordinate connection before the parallel frame is applied. The integration identity follows from frame-flow invariance, rather than an assumed Hessian integral formula.

abbrev OAI.PositiveEinsteinFour.Geometry.GradientVector line 20
def OAI.PositiveEinsteinFour.Geometry.gradientVector line 22
theorem OAI.PositiveEinsteinFour.Geometry.gradientVector_norm_sq line 25
theorem OAI.PositiveEinsteinFour.Geometry.gradientVector_hessian_norm line 31
def OAI.PositiveEinsteinFour.Geometry.plusWeylThirdDerivative line 42
Source documentation
Three successive covariant derivatives, retaining all derivative slots.
```
def plusWeylThirdDerivative (g : SmoothMetric M) (c : M)
    (e : OrthonormalFrame g c) (i j k : Fin 4) : Mat3 :=
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.OrthonormalFrame, OAI.PositiveEinsteinFour.Geometry.Mat3
def OAI.PositiveEinsteinFour.Geometry.frameGradientVector line 51
def OAI.PositiveEinsteinFour.Geometry.frameHessianVector line 54
def OAI.PositiveEinsteinFour.Geometry.frameThirdVector line 57
def OAI.PositiveEinsteinFour.Geometry.frameGradientLaplacian line 61
Source documentation
The actual rough Laplacian of the Weyl gradient, in the same frame.
```
def frameGradientLaplacian (g : SmoothMetric M) (e : FrameBundle g) : GradientVector :=
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.FrameBundle, OAI.PositiveEinsteinFour.Geometry.GradientVector

theorem OAI.PositiveEinsteinFour.Geometry.weighted_metric_hessian_green line 67

Source documentation

Weighted integration by parts for the actual covariant Hessian. The classical parallel-frame differentiation identities and measure-preserving flows are explicit; no new weighted estimate is a hypothesis.

theorem weighted_metric_hessian_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, ℝ))
    (hZ : Continuous (frameGradientVector g))
    (hX : ∀ i, Continuous (frameHessianVector g i))
    (hXX : ∀ i, Continuous (frameThirdVector g i i))
    (hm : ∀ i t e, HasDerivAt (fun s => m ((φ i).map s e))
      (dm i ((φ i).map t e)) t)
    (hZd : ∀ i t e, HasDerivAt (fun s => frameGradientVector g ((φ i).map s e))
      (frameHessianVector g i ((φ i).map t e)) t)
…

Mentions: OAI.PositiveEinsteinFour.Geometry.FrameBundle, OAI.PositiveEinsteinFour.Geometry.FrameFlow, OAI.PositiveEinsteinFour.Geometry.frameGradientVector, OAI.PositiveEinsteinFour.Geometry.frameHessianVector, OAI.PositiveEinsteinFour.Geometry.frameThirdVector