OAI/Geometry/EinsteinFour/MatrixSlotLaplacian.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Pair the raw Ricci-commuted gradient with the varying matrix-slot operator. The final square is the energy of the orthogonal compression.

  1. theorem OAI.PositiveEinsteinFour.Geometry.matrixSlotOperator_compression_pairing line 16
  2. theorem OAI.PositiveEinsteinFour.Geometry.matrixSlotOperator_ricci_pairing line 28

    Source documentation

    The matrix-slot pairing uses the uncompressed differential equation; the coefficient 20 and compressed squared norm are consequences.

    theorem matrixSlotOperator_ricci_pairing (S : Shape) (v : ℝ)
    (p k l : Vec) (L : Tensor) (hLz : L.traceFree) (hLb : L.bianchi)
    (hL : L.matrix = ricciGradient (fun s => v * S.s s) (parameters S p k l)) :
    inner ℝ (matrixSlotOperator (Matrix.diagonal (fun s => v * S.s s))
      (tensorGradientVector (parameters S p k l))) (tensorGradientVector L) =
        13 * (6 * curvatureBilinear S v (parameters S p k l) (parameters S p k l)) -
          20 * (curvatureAction S v p k l).squaredNorm := by
…

    Mentions: OAI.PositiveEinsteinFour.Geometry.matrixSlotOperator, OAI.PositiveEinsteinFour.Geometry.tensorGradientVector