WeylDerivative.lean`

13 declarations, 0 contain sorry, 0 declared as axioms

Coordinate covariant derivatives of the actual curvature tensor. The scalar-curvature contribution is subtracted in the Ricci=3g normalization. The definitions retain all tensor slots until after differentiation.

abbrev OAI.PositiveEinsteinFour.Geometry.CovariantCoordinates line 19
def OAI.PositiveEinsteinFour.Geometry.curvatureCoordinates line 22
Source documentation
Coordinate components of <R(e_a,e_b)e_c,e_d>.
```
def curvatureCoordinates (g : SmoothMetric M) (c : M) (z : FourSpace) :
    CovariantCoordinates 4 := fun a =>
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.CovariantCoordinates
def OAI.PositiveEinsteinFour.Geometry.unitCurvatureCoordinates line 28
Source documentation
The curvature-one algebraic tensor in arbitrary coordinates.
```
def unitCurvatureCoordinates (g : SmoothMetric M) (c : M) (z : FourSpace) :
    CovariantCoordinates 4 := fun a =>
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.CovariantCoordinates
def OAI.PositiveEinsteinFour.Geometry.normalizedWeylCoordinates line 35
Source documentation
For Ricci=3g this is exactly the Weyl four-tensor. Defining its coordinate field first ensures that derivatives are taken before choosing eigenframes.
```
def normalizedWeylCoordinates (g : SmoothMetric M) (c : M) (z : FourSpace) :
    CovariantCoordinates 4 := curvatureCoordinates g c z - unitCurvatureCoordinates g c z
```
Mentions: OAI.PositiveEinsteinFour.Geometry.CovariantCoordinates, OAI.PositiveEinsteinFour.Geometry.curvatureCoordinates, OAI.PositiveEinsteinFour.Geometry.unitCurvatureCoordinates
def OAI.PositiveEinsteinFour.Geometry.covariantDerivative line 40
Source documentation
The induced Levi-Civita derivative on covariant coordinate tensors. The leading slot records the direction of differentiation.
```
def covariantDerivative {n : ℕ} (g : SmoothMetric M) (c : M)
    (T : FourSpace → CovariantCoordinates n) (z : FourSpace) :
    CovariantCoordinates (n + 1) := fun a =>
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.CovariantCoordinates
def OAI.PositiveEinsteinFour.Geometry.frameTensor line 49
Source documentation
Pull back every covariant slot by a single actual orthonormal frame.
```
def frameTensor {n : ℕ} (A : Mat4) (T : CovariantCoordinates n) :
    CovariantCoordinates n := fun a =>
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.Mat4, OAI.PositiveEinsteinFour.Geometry.CovariantCoordinates
def OAI.PositiveEinsteinFour.Geometry.blockCoordinates line 54
Source documentation
The two-form contraction for a tensor with no derivative slots.
```
def blockCoordinates (T : CovariantCoordinates 4) (Q : Fin 3 → Mat4) : Mat3 :=
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.CovariantCoordinates, OAI.PositiveEinsteinFour.Geometry.Mat4, OAI.PositiveEinsteinFour.Geometry.Mat3
def OAI.PositiveEinsteinFour.Geometry.gradientBlock line 58
Source documentation
A fixed derivative direction in the covariant derivative of curvature.
```
def gradientBlock (T : CovariantCoordinates 5) (Q : Fin 3 → Mat4)
    (i : Fin 4) : Mat3 :=
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.CovariantCoordinates, OAI.PositiveEinsteinFour.Geometry.Mat4, OAI.PositiveEinsteinFour.Geometry.Mat3
def OAI.PositiveEinsteinFour.Geometry.hessianBlock line 63
Source documentation
Both derivative directions in the covariant Hessian of curvature.
```
def hessianBlock (T : CovariantCoordinates 6) (Q : Fin 3 → Mat4)
    (i j : Fin 4) : Mat3 :=
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.CovariantCoordinates, OAI.PositiveEinsteinFour.Geometry.Mat4, OAI.PositiveEinsteinFour.Geometry.Mat3
def OAI.PositiveEinsteinFour.Geometry.plusWeylGradient line 68
Source documentation
The actual plus-block covariant gradient in an orthonormal frame.
```
def plusWeylGradient (g : SmoothMetric M) (c : M) (e : OrthonormalFrame g c)
    (i : Fin 4) : Mat3 :=
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.OrthonormalFrame, OAI.PositiveEinsteinFour.Geometry.Mat3
def OAI.PositiveEinsteinFour.Geometry.plusWeylHessian line 75
Source documentation
The actual plus-block covariant Hessian, before any trace decomposition.
```
def plusWeylHessian (g : SmoothMetric M) (c : M) (e : OrthonormalFrame g c)
    (i j : Fin 4) : Mat3 :=
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.OrthonormalFrame, OAI.PositiveEinsteinFour.Geometry.Mat3
def OAI.PositiveEinsteinFour.Geometry.minusWeylGradient line 83
Source documentation
The opposite block is differentiated in the same actual coordinate connection, before the orthonormal frame and Hodge basis are applied.
```
def minusWeylGradient (g : SmoothMetric M) (c : M) (e : OrthonormalFrame g c)
    (i : Fin 4) : Mat3 :=
…
```
Mentions: OAI.PositiveEinsteinFour.Geometry.OrthonormalFrame, OAI.PositiveEinsteinFour.Geometry.Mat3
def OAI.PositiveEinsteinFour.Geometry.minusWeylHessian line 89