TraceHessian.lean`

39 declarations, 0 contain sorry, 0 declared as axioms

The prescribed trace component of the Bianchi Hessian

The arrays are real tensors. The lift is the explicit formula for the restricted trace adjoint in Section 5; its Bianchi constraint, trace and squared norm follow by direct calculation in the fixed quaternion frame.

abbrev OAI.PositiveEinsteinFour.TraceHessian.Mat line 19
abbrev OAI.PositiveEinsteinFour.TraceHessian.Hessian line 20
def OAI.PositiveEinsteinFour.TraceHessian.symmetric line 22
def OAI.PositiveEinsteinFour.TraceHessian.traceFree line 24
def OAI.PositiveEinsteinFour.TraceHessian.ofCoordinates line 26
theorem OAI.PositiveEinsteinFour.TraceHessian.coordinates_eq line 29
def OAI.PositiveEinsteinFour.TraceHessian.quaternionMatrix line 40
Source documentation
Matrix coefficients of the same quaternion triple used for gradients.
```
def quaternionMatrix (s : Fin 3) : Matrix (Fin 4) (Fin 4) ℝ :=
…
```
theorem OAI.PositiveEinsteinFour.TraceHessian.quaternionMatrix_apply line 45
def OAI.PositiveEinsteinFour.TraceHessian.rotation line 51
Source documentation
Speed-two rotations on the self-dual matrix indices.
```
def rotation (s : Fin 3) : Mat :=
…
```
Mentions: OAI.PositiveEinsteinFour.TraceHessian.Mat
def OAI.PositiveEinsteinFour.TraceHessian.matrixAction line 56
theorem OAI.PositiveEinsteinFour.TraceHessian.matrixAction_coordinates_zero line 59
theorem OAI.PositiveEinsteinFour.TraceHessian.matrixAction_coordinates_one line 66
theorem OAI.PositiveEinsteinFour.TraceHessian.matrixAction_coordinates_two line 73
def OAI.PositiveEinsteinFour.TraceHessian.matrixNormSq line 80
theorem OAI.PositiveEinsteinFour.TraceHessian.matrixAction_casimir line 83
Source documentation
The spin-two Casimir, computed on the actual symmetric trace-free matrix.
```
theorem matrixAction_casimir (M : Mat) (hs : symmetric M) (ht : traceFree M) :
    (∑ a, ∑ b, ∑ s, matrixAction s M a b ^ 2) = 24 * matrixNormSq M := by
…
```
Mentions: OAI.PositiveEinsteinFour.TraceHessian.Mat, OAI.PositiveEinsteinFour.TraceHessian.symmetric, OAI.PositiveEinsteinFour.TraceHessian.traceFree, OAI.PositiveEinsteinFour.TraceHessian.matrixAction, OAI.PositiveEinsteinFour.TraceHessian.matrixNormSq
def OAI.PositiveEinsteinFour.TraceHessian.traceLift line 91
Source documentation
The explicit trace lift 3/5 δij S + 1/10 Σ I_s,ij Σ_s S.
```
def traceLift (M : Mat) : Hessian := fun i j a b =>
…
```
Mentions: OAI.PositiveEinsteinFour.TraceHessian.Mat, OAI.PositiveEinsteinFour.TraceHessian.Hessian
def OAI.PositiveEinsteinFour.TraceHessian.hessianTrace line 95
def OAI.PositiveEinsteinFour.TraceHessian.hessianNormSq line 98
Source documentation
Entry-first order is a permutation of the usual Frobenius sum.
```
def hessianNormSq (X : Hessian) : ℝ := ∑ a, ∑ b, ∑ i, ∑ j, X i j a b ^ 2
```
Mentions: OAI.PositiveEinsteinFour.TraceHessian.Hessian
theorem OAI.PositiveEinsteinFour.TraceHessian.quaternionMatrix_diagonal line 100
theorem OAI.PositiveEinsteinFour.TraceHessian.trace_traceLift line 105
Source documentation
Trace followed by its lift gives exactly 12/5 Id.
```
theorem trace_traceLift (M : Mat) : hessianTrace (traceLift M) = (12 / 5 : ℝ) • M := by
…
```
Mentions: OAI.PositiveEinsteinFour.TraceHessian.Mat, OAI.PositiveEinsteinFour.TraceHessian.hessianTrace, OAI.PositiveEinsteinFour.TraceHessian.traceLift
theorem OAI.PositiveEinsteinFour.TraceHessian.quaternion_square_sum line 110
theorem OAI.PositiveEinsteinFour.TraceHessian.traceLift_norm line 119
Source documentation
The norm of the explicit restricted trace lift.
```
theorem traceLift_norm (M : Mat) (hs : symmetric M) (ht : traceFree M) :
    hessianNormSq (traceLift M) = (12 / 5) * matrixNormSq M := by
…
```
Mentions: OAI.PositiveEinsteinFour.TraceHessian.Mat, OAI.PositiveEinsteinFour.TraceHessian.symmetric, OAI.PositiveEinsteinFour.TraceHessian.traceFree, OAI.PositiveEinsteinFour.TraceHessian.hessianNormSq, OAI.PositiveEinsteinFour.TraceHessian.traceLift, OAI.PositiveEinsteinFour.TraceHessian.matrixNormSq
def OAI.PositiveEinsteinFour.TraceHessian.liftDivergence line 134
Source documentation
The actual Bianchi divergence of an inner-gradient slice of the lift.
```
def liftDivergence (M : Mat) (i : Fin 4) (r : Fin 3) : Vec :=
…
```
Mentions: OAI.PositiveEinsteinFour.TraceHessian.Mat
theorem OAI.PositiveEinsteinFour.TraceHessian.traceLift_bianchi_0_0 line 137
theorem OAI.PositiveEinsteinFour.TraceHessian.traceLift_bianchi_0_1 line 145
theorem OAI.PositiveEinsteinFour.TraceHessian.traceLift_bianchi_0_2 line 153
theorem OAI.PositiveEinsteinFour.TraceHessian.traceLift_bianchi_1_0 line 161
theorem OAI.PositiveEinsteinFour.TraceHessian.traceLift_bianchi_1_1 line 169
theorem OAI.PositiveEinsteinFour.TraceHessian.traceLift_bianchi_1_2 line 177
theorem OAI.PositiveEinsteinFour.TraceHessian.traceLift_bianchi_2_0 line 185
theorem OAI.PositiveEinsteinFour.TraceHessian.traceLift_bianchi_2_1 line 193
theorem OAI.PositiveEinsteinFour.TraceHessian.traceLift_bianchi_2_2 line 201
theorem OAI.PositiveEinsteinFour.TraceHessian.traceLift_bianchi_3_0 line 209
theorem OAI.PositiveEinsteinFour.TraceHessian.traceLift_bianchi_3_1 line 217
theorem OAI.PositiveEinsteinFour.TraceHessian.traceLift_bianchi_3_2 line 225
theorem OAI.PositiveEinsteinFour.TraceHessian.traceLift_bianchi line 234
Source documentation
Every lifted trace belongs to the constrained inner-gradient space.
```
theorem traceLift_bianchi (M : Mat) (hs : symmetric M) (ht : traceFree M)
    (i : Fin 4) (r : Fin 3) : liftDivergence M i r = 0 := by
…
```
Mentions: OAI.PositiveEinsteinFour.TraceHessian.Mat, OAI.PositiveEinsteinFour.TraceHessian.symmetric, OAI.PositiveEinsteinFour.TraceHessian.traceFree, OAI.PositiveEinsteinFour.TraceHessian.liftDivergence
def OAI.PositiveEinsteinFour.TraceHessian.traceComponent line 252
Source documentation
The prescribed trace component of an actual Hessian.
```
def traceComponent (M : Mat) : Hessian := fun i j => (5 / 12 : ℝ) • traceLift M i j
```
Mentions: OAI.PositiveEinsteinFour.TraceHessian.Mat, OAI.PositiveEinsteinFour.TraceHessian.Hessian, OAI.PositiveEinsteinFour.TraceHessian.traceLift
theorem OAI.PositiveEinsteinFour.TraceHessian.trace_traceComponent line 254
theorem OAI.PositiveEinsteinFour.TraceHessian.traceComponent_norm line 262
Source documentation
The exact coefficient subtracted in the weighted Hessian identity.
```
theorem traceComponent_norm (M : Mat) (hs : symmetric M) (ht : traceFree M) :
    hessianNormSq (traceComponent M) = (5 / 12) * matrixNormSq M := by
…
```
Mentions: OAI.PositiveEinsteinFour.TraceHessian.Mat, OAI.PositiveEinsteinFour.TraceHessian.symmetric, OAI.PositiveEinsteinFour.TraceHessian.traceFree, OAI.PositiveEinsteinFour.TraceHessian.hessianNormSq, OAI.PositiveEinsteinFour.TraceHessian.traceComponent, OAI.PositiveEinsteinFour.TraceHessian.matrixNormSq