OAI/Geometry/EinsteinFour/TraceAction.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The precise curvature action on the prescribed trace component.

  1. theorem OAI.PositiveEinsteinFour.TraceHessian.traceLift_add line 15
  2. theorem OAI.PositiveEinsteinFour.TraceHessian.traceLift_smul line 22
  3. theorem OAI.PositiveEinsteinFour.TraceHessian.traceLift_sub line 28
  4. theorem OAI.PositiveEinsteinFour.TraceHessian.traceLift_weighted_sum line 32
  5. theorem OAI.PositiveEinsteinFour.TraceHessian.pairing_weighted_sum line 36
  6. theorem OAI.PositiveEinsteinFour.TraceHessian.traceLift_curvatureAction line 43

    Source documentation

    The trace adjoint intertwines the total plus action and kills the minus action, so its curvature action is exactly 4 - B_F(t).

    theorem traceLift_curvatureAction (t u : Fin 3 → ℝ) (ht : ∑ s, t s = 0)
    (M : Mat) (hs : symmetric M) (hm : traceFree M) (Y : Hessian) :
    curvaturePairing t u (traceLift M) Y =
      hessianPairing (traceLift ((4 : ℝ) • M - diagonalCurvatureAction t M)) Y := by
…

    Mentions: OAI.PositiveEinsteinFour.TraceHessian.Mat, OAI.PositiveEinsteinFour.TraceHessian.symmetric, OAI.PositiveEinsteinFour.TraceHessian.traceFree, OAI.PositiveEinsteinFour.TraceHessian.Hessian, OAI.PositiveEinsteinFour.TraceHessian.traceLift, OAI.PositiveEinsteinFour.TraceHessian.hessianPairing

  7. theorem OAI.PositiveEinsteinFour.TraceHessian.traceComponent_curvatureAction line 76

    Source documentation

    The normalization 5/12 commutes with the exact trace curvature action.

    theorem traceComponent_curvatureAction (t u : Fin 3 → ℝ) (ht : ∑ s, t s = 0)
    (M : Mat) (hs : symmetric M) (hm : traceFree M) (Y : Hessian) :
    curvaturePairing t u (traceComponent M) Y =
      hessianPairing (traceComponent ((4 : ℝ) • M - diagonalCurvatureAction t M)) Y := by
…

    Mentions: OAI.PositiveEinsteinFour.TraceHessian.Mat, OAI.PositiveEinsteinFour.TraceHessian.symmetric, OAI.PositiveEinsteinFour.TraceHessian.traceFree, OAI.PositiveEinsteinFour.TraceHessian.Hessian, OAI.PositiveEinsteinFour.TraceHessian.traceComponent, OAI.PositiveEinsteinFour.TraceHessian.hessianPairing