OAI/Geometry/EinsteinFour/TraceDecomposition.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

The actual local tensor identities imply the highest-Hessian constraints.

  1. theorem OAI.PositiveEinsteinFour.HighestHessian.matrixAction_symmetric line 15
  2. theorem OAI.PositiveEinsteinFour.HighestHessian.matrixAction_traceFree line 23
  3. theorem OAI.PositiveEinsteinFour.HighestHessian.traceComponent_symmetric line 28
  4. theorem OAI.PositiveEinsteinFour.HighestHessian.traceComponent_traceFree line 37
  5. theorem OAI.PositiveEinsteinFour.HighestHessian.divergence_add line 52
  6. theorem OAI.PositiveEinsteinFour.HighestHessian.divergence_smul line 59
  7. theorem OAI.PositiveEinsteinFour.HighestHessian.divergence_sub line 66
  8. theorem OAI.PositiveEinsteinFour.HighestHessian.traceComponent_divergence line 73
  9. theorem OAI.PositiveEinsteinFour.HighestHessian.trace_subtracted_condition line 82

    Source documentation

    No representation-theoretic hypothesis is needed: matrix symmetry, the actual trace equation, Bianchi and the curvature commutator suffice.

    theorem trace_subtracted_condition (X : Hessian) (t : Fin 3 → ℝ)
    (ht : ∑ s, t s = 0)
    (hm : ∀ i j, symmetric (X i j) ∧ traceFree (X i j))
    (htrace : hessianTrace X = diagonalLaplacianBlock t)
    (hbianchi : ∀ i r, divergence X i r = 0)
    (hcomm : ∀ i j a b, X i j a b - X j i a b =
      (1 / 2) * ∑ s, (1 + t s) * quaternionMatrix s i j *
        matrixAction s (Matrix.diagonal t) a b) :
    condition (X - traceComponent (diagonalLaplacianBlock t)) := by
…

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