MetricBianchi.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

The actual Weyl gradient, with its derivative index treated as a tangent vector. These changes of coordinate retain every component: neither the Bianchi equation nor a differential estimate is built into the definition.

def OAI.PositiveEinsteinFour.Geometry.gradientTensor line 18
Source documentation
Reorder the derivative slot of a symmetric matrix gradient.
```
def gradientTensor (Z : Gradient) : Tensor where
…
```
theorem OAI.PositiveEinsteinFour.Geometry.gradientTensor_matrix line 22
theorem OAI.PositiveEinsteinFour.Geometry.gradientTensor_traceFree line 29
def OAI.PositiveEinsteinFour.Geometry.gradientDivergence line 35
Source documentation
This is the coordinate divergence of the matrix gradient.
```
def gradientDivergence (Z : Gradient) (r : Fin 3) (i : Fin 4) : ℝ :=
…
```
theorem OAI.PositiveEinsteinFour.Geometry.gradientTensor_divergence line 38
theorem OAI.PositiveEinsteinFour.Geometry.gradientTensor_bianchi line 50
theorem OAI.PositiveEinsteinFour.Geometry.gradientTensor_squaredNorm line 57
Source documentation
The tensor norm is precisely the ordinary covariant-gradient norm.
```
theorem gradientTensor_squaredNorm (Z : Gradient) (hs : ∀ i, symmetric (Z i)) :
    (gradientTensor Z).squaredNorm = gradientSquareNorm Z := by
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.gradientTensor
def OAI.PositiveEinsteinFour.Geometry.plusGradientTensor line 73
Source documentation
The concrete tensor to which the finite Bianchi estimates apply.
```
def plusGradientTensor (g : SmoothMetric M) (c : M) (e : OrthonormalFrame g c) :
    Tensor := gradientTensor (plusWeylGradient g c e)
```
Mentions: OAI.PositiveEinsteinFour.Geometry.OrthonormalFrame, OAI.PositiveEinsteinFour.Geometry.gradientTensor, OAI.PositiveEinsteinFour.Geometry.plusWeylGradient
theorem OAI.PositiveEinsteinFour.Geometry.plusGradientTensor_squaredNorm line 76
theorem OAI.PositiveEinsteinFour.Geometry.plusGradientTensor_refined_kato line 85
Source documentation
Refined Kato for the actual gradient after its classical differential Bianchi equation has been supplied. The eigenframe's normalized spectral shape is explicit; no scalar gradient estimate is a hypothesis.
```
theorem plusGradientTensor_refined_kato (g : SmoothMetric M) (c : M)
    (e : OrthonormalFrame g c) (S : Shape)
    (hs : ∀ i, symmetric (plusWeylGradient g c e i))
    (ht : ∀ i, traceFree (plusWeylGradient g c e i))
    (hb : ∀ r i, gradientDivergence (plusWeylGradient g c e) r i = 0) :
    (5 / 3) * ‖radialCoordinate S (plusGradientTensor g c e)‖ ^ 2 ≤
      gradientSquareNorm (plusWeylGradient g c e) / 6 := by
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.OrthonormalFrame, OAI.PositiveEinsteinFour.Geometry.plusWeylGradient, OAI.PositiveEinsteinFour.Geometry.gradientDivergence, OAI.PositiveEinsteinFour.Geometry.plusGradientTensor