TraceSubtraction.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Exact subtraction of the prescribed trace from the weighted square.

theorem OAI.PositiveEinsteinFour.HighestHessian.traceComponent_pairing_hessian line 18

Source documentation

The restricted trace adjoint pairs with any actual inner-Bianchi array, including an unsymmetrized weight derivative.

theorem traceComponent_pairing_hessian (M : Mat) (hs : symmetric M) (ht : traceFree M)
    (X : Hessian) (hmatrix : ∀ i j, symmetric (X i j) ∧ traceFree (X i j))
    (hbianchi : ∀ i r, divergence X i r = 0) :
    hessianPairing (traceComponent M) X =
      (5 / 12 : ℝ) * matrixPairing M (hessianTrace X) := by
…

Mentions: OAI.PositiveEinsteinFour.HighestHessian.divergence

theorem OAI.PositiveEinsteinFour.HighestHessian.weightTensor_matrix_bianchi line 42
Source documentation
The weight derivative keeps the genuine inner Bianchi constraints.
```
theorem weightTensor_matrix_bianchi (a : Vec) (Z : Tensor)
    (hz : Z.traceFree) (hb : Z.bianchi) :
    (∀ i j, symmetric (weightTensor a Z i j) ∧ traceFree (weightTensor a Z i j)) ∧
      (∀ i r, divergence (weightTensor a Z) i r = 0) := by
…
```
Mentions: OAI.PositiveEinsteinFour.HighestHessian.weightTensor, OAI.PositiveEinsteinFour.HighestHessian.divergence
theorem OAI.PositiveEinsteinFour.HighestHessian.weightTensor_trace line 70
Source documentation
Trace of the unsymmetrized weight tensor is contraction with its real outer derivative vector.
```
theorem weightTensor_trace (a : Vec) (Z : Tensor) :
    hessianTrace (weightTensor a Z) = fun b c => inner ℝ a (Z.matrix b c) := by
…
```
Mentions: OAI.PositiveEinsteinFour.HighestHessian.weightTensor
def OAI.PositiveEinsteinFour.HighestHessian.traceCurvatureBlock line 77
theorem OAI.PositiveEinsteinFour.HighestHessian.traceCurvatureBlock_symmetric line 80
theorem OAI.PositiveEinsteinFour.HighestHessian.traceCurvatureBlock_traceFree line 93

theorem OAI.PositiveEinsteinFour.HighestHessian.traceComponent_curvaturePairing line 103

Source documentation

The curvature action of the trace component pairs through the actual Hessian trace, with the full skew part retained.

theorem traceComponent_curvaturePairing (t u : Fin 3 → ℝ) (ht : ∑ s, t s = 0)
    (M : Mat) (hsM : symmetric M) (htM : traceFree M)
    (X : Hessian) (hmatrix : ∀ i j, symmetric (X i j) ∧ traceFree (X i j))
    (hbianchi : ∀ i r, divergence X i r = 0) :
    curvaturePairing t u (traceComponent M) X =
      (5 / 12 : ℝ) * matrixPairing (traceCurvatureBlock t M) (hessianTrace X) := by
…

Mentions: OAI.PositiveEinsteinFour.HighestHessian.divergence, OAI.PositiveEinsteinFour.HighestHessian.curvaturePairing, OAI.PositiveEinsteinFour.HighestHessian.traceCurvatureBlock

theorem OAI.PositiveEinsteinFour.HighestHessian.prescribed_trace_curvaturePairing line 115

Source documentation

The mixed trace pairing equals its self pairing when the trace is prescribed.

theorem prescribed_trace_curvaturePairing (t u : Fin 3 → ℝ) (ht : ∑ s, t s = 0)
    (M : Mat) (hsM : symmetric M) (htM : traceFree M)
    (X : Hessian) (hmatrix : ∀ i j, symmetric (X i j) ∧ traceFree (X i j))
    (hbianchi : ∀ i r, divergence X i r = 0) (htrace : hessianTrace X = M) :
    curvaturePairing t u X (traceComponent M) =
      curvaturePairing t u (traceComponent M) (traceComponent M) := by
…

Mentions: OAI.PositiveEinsteinFour.HighestHessian.divergence, OAI.PositiveEinsteinFour.HighestHessian.curvaturePairing

theorem OAI.PositiveEinsteinFour.HighestHessian.weighted_trace_subtraction line 130

Source documentation

Both trace subtractions in the weighted Hessian square are exact. In particular, the mixed term uses the full unsymmetrized weight tensor.

theorem weighted_trace_subtraction (t u : Fin 3 → ℝ) (ht : ∑ s, t s = 0)
    (M : Mat) (hsM : symmetric M) (htM : traceFree M)
    (X L : Hessian) (hmatrix : ∀ i j, symmetric (X i j) ∧ traceFree (X i j))
    (hbianchi : ∀ i r, divergence X i r = 0) (htrace : hessianTrace X = M) (m : ℝ) :
    m * curvaturePairing t u (X - traceComponent M) (X - traceComponent M) +
        curvaturePairing t u (X - traceComponent M) L =
      m * curvaturePairing t u X X + curvaturePairing t u X L -
        m * curvaturePairing t u (traceComponent M) (traceComponent M) -
          curvaturePairing t u (traceComponent M) L := by
…

Mentions: OAI.PositiveEinsteinFour.HighestHessian.divergence, OAI.PositiveEinsteinFour.HighestHessian.curvaturePairing