TraceAdjoint.lean`

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

The explicit trace lift is the actual adjoint on the Bianchi subspace.

def OAI.PositiveEinsteinFour.TraceHessian.referenceShape line 14
def OAI.PositiveEinsteinFour.TraceHessian.liftSlicePairing line 21
Source documentation
Pairing of one outer-derivative slice of the lift with an actual Bianchi matrix of four-vectors.
```
def liftSlicePairing (M : Mat) (i : Fin 4) (Z : Tensor) : ℝ :=
…
```
Mentions: OAI.PositiveEinsteinFour.TraceHessian.Mat
def OAI.PositiveEinsteinFour.TraceHessian.derivativePairing line 25
Source documentation
Pairing with the corresponding derivative component of the gradient.
```
def derivativePairing (M : Mat) (i : Fin 4) (Z : Tensor) : ℝ :=
…
```
Mentions: OAI.PositiveEinsteinFour.TraceHessian.Mat
theorem OAI.PositiveEinsteinFour.TraceHessian.traceLift_adjoint_parameters_0 line 28
theorem OAI.PositiveEinsteinFour.TraceHessian.traceLift_adjoint_parameters_1 line 37
theorem OAI.PositiveEinsteinFour.TraceHessian.traceLift_adjoint_parameters_2 line 46
theorem OAI.PositiveEinsteinFour.TraceHessian.traceLift_adjoint_parameters_3 line 55
theorem OAI.PositiveEinsteinFour.TraceHessian.traceLift_adjoint_parameters line 64
theorem OAI.PositiveEinsteinFour.TraceHessian.traceLift_adjoint_slice line 76
Source documentation
The adjoint identity holds for every actual symmetric trace-free Bianchi gradient; no projection identity is a premise.
```
theorem traceLift_adjoint_slice (M : Mat) (hs : symmetric M) (ht : traceFree M)
    (Z : Tensor) (hz : Z.traceFree) (hb : Z.bianchi) (i : Fin 4) :
    liftSlicePairing M i Z = derivativePairing M i Z := by
…
```
Mentions: OAI.PositiveEinsteinFour.TraceHessian.Mat, OAI.PositiveEinsteinFour.TraceHessian.symmetric, OAI.PositiveEinsteinFour.TraceHessian.traceFree, OAI.PositiveEinsteinFour.TraceHessian.liftSlicePairing, OAI.PositiveEinsteinFour.TraceHessian.derivativePairing
def OAI.PositiveEinsteinFour.TraceHessian.slicesTrace line 83
Source documentation
Trace of the two derivative slots, for a family of Bianchi gradients.
```
def slicesTrace (Z : Fin 4 → Tensor) : Mat := fun a b => ∑ i, (Z i).matrix a b i
```
Mentions: OAI.PositiveEinsteinFour.TraceHessian.Mat
theorem OAI.PositiveEinsteinFour.TraceHessian.traceLift_adjoint line 86
Source documentation
The global finite-dimensional adjoint identity for the restricted trace.
```
theorem traceLift_adjoint (M : Mat) (hs : symmetric M) (ht : traceFree M)
    (Z : Fin 4 → Tensor) (hz : ∀ i, (Z i).traceFree) (hb : ∀ i, (Z i).bianchi) :
    (∑ i, liftSlicePairing M i (Z i)) = ∑ a, ∑ b, M a b * slicesTrace Z a b := by
…
```
Mentions: OAI.PositiveEinsteinFour.TraceHessian.Mat, OAI.PositiveEinsteinFour.TraceHessian.symmetric, OAI.PositiveEinsteinFour.TraceHessian.traceFree, OAI.PositiveEinsteinFour.TraceHessian.liftSlicePairing, OAI.PositiveEinsteinFour.TraceHessian.slicesTrace
def OAI.PositiveEinsteinFour.TraceHessian.slicesHessian line 96
Source documentation
The actual four-index array associated to differentiated Bianchi tensors.
```
def slicesHessian (Z : Fin 4 → Tensor) : Hessian :=
…
```
Mentions: OAI.PositiveEinsteinFour.TraceHessian.Hessian
def OAI.PositiveEinsteinFour.TraceHessian.hessianPairing line 100
Source documentation
Frobenius pairing on all four tensor slots.
```
def hessianPairing (X Y : Hessian) : ℝ :=
…
```
Mentions: OAI.PositiveEinsteinFour.TraceHessian.Hessian
theorem OAI.PositiveEinsteinFour.TraceHessian.hessianPairing_self line 103
theorem OAI.PositiveEinsteinFour.TraceHessian.hessianPairing_comm line 107
theorem OAI.PositiveEinsteinFour.TraceHessian.hessianNormSq_sub line 111
theorem OAI.PositiveEinsteinFour.TraceHessian.traceComponent_pairing line 123
Source documentation
The trace component pairs with an arbitrary constrained Hessian only through its trace. This includes the prescribed skew part of the Hessian.
```
theorem traceComponent_pairing (M : Mat) (hs : symmetric M) (ht : traceFree M)
    (Z : Fin 4 → Tensor) (hz : ∀ i, (Z i).traceFree) (hb : ∀ i, (Z i).bianchi) :
    hessianPairing (traceComponent M) (slicesHessian Z) =
      (5 / 12 : ℝ) * ∑ a, ∑ b, M a b * slicesTrace Z a b := by
…
```
Mentions: OAI.PositiveEinsteinFour.TraceHessian.Mat, OAI.PositiveEinsteinFour.TraceHessian.symmetric, OAI.PositiveEinsteinFour.TraceHessian.traceFree, OAI.PositiveEinsteinFour.TraceHessian.hessianPairing, OAI.PositiveEinsteinFour.TraceHessian.traceComponent, OAI.PositiveEinsteinFour.TraceHessian.slicesHessian, OAI.PositiveEinsteinFour.TraceHessian.slicesTrace
theorem OAI.PositiveEinsteinFour.TraceHessian.traceComponent_subtraction line 138
Source documentation
Exact subtraction of the whole prescribed trace component.
```
theorem traceComponent_subtraction (M : Mat) (hs : symmetric M) (ht : traceFree M)
    (Z : Fin 4 → Tensor) (hz : ∀ i, (Z i).traceFree) (hb : ∀ i, (Z i).bianchi)
    (htrace : slicesTrace Z = M) :
    hessianNormSq (slicesHessian Z - traceComponent M) =
      hessianNormSq (slicesHessian Z) - (5 / 12) * matrixNormSq M := by
…
```
Mentions: OAI.PositiveEinsteinFour.TraceHessian.Mat, OAI.PositiveEinsteinFour.TraceHessian.symmetric, OAI.PositiveEinsteinFour.TraceHessian.traceFree, OAI.PositiveEinsteinFour.TraceHessian.slicesTrace, OAI.PositiveEinsteinFour.TraceHessian.hessianNormSq, OAI.PositiveEinsteinFour.TraceHessian.slicesHessian, OAI.PositiveEinsteinFour.TraceHessian.traceComponent, OAI.PositiveEinsteinFour.TraceHessian.matrixNormSq