OAI/Geometry/EinsteinFour/TensorPairing.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

Skew matrix actions on the actual four tensor slots.

  1. theorem OAI.PositiveEinsteinFour.TraceHessian.skew_matrix_pairing line 14

    Source documentation

    The usual reindexing proof for a real skew-adjoint matrix.

    theorem skew_matrix_pairing {ι : Type*} [Fintype ι]
    (A : ι → ι → ℝ) (hA : ∀ i j, A i j = -A j i) (x y : ι → ℝ) :
    (∑ i, (∑ j, A i j * x j) * y i) =
      -(∑ i, x i * (∑ j, A i j * y j)) := by
…
  2. abbrev OAI.PositiveEinsteinFour.TraceHessian.TensorIndex line 31
  3. def OAI.PositiveEinsteinFour.TraceHessian.tensorCoordinates line 33
  4. theorem OAI.PositiveEinsteinFour.TraceHessian.tensorCoordinates_pairing line 36
  5. def OAI.PositiveEinsteinFour.TraceHessian.plusKernel line 61

    Source documentation

    The Kronecker sum of the four actual infinitesimal rotation actions.

    def plusKernel (s : Fin 3) (p q : TensorIndex) : ℝ :=
…

    Mentions: OAI.PositiveEinsteinFour.TraceHessian.TensorIndex

  6. theorem OAI.PositiveEinsteinFour.TraceHessian.quaternionMatrix_skew line 71
  7. theorem OAI.PositiveEinsteinFour.TraceHessian.rotation_skew line 75
  8. theorem OAI.PositiveEinsteinFour.TraceHessian.plusKernel_skew line 79
  9. theorem OAI.PositiveEinsteinFour.TraceHessian.matrixAction_row_sum line 92
  10. theorem OAI.PositiveEinsteinFour.TraceHessian.hessianPairing_add_left line 104
  11. theorem OAI.PositiveEinsteinFour.TraceHessian.hessianPairing_smul_left line 109
  12. def OAI.PositiveEinsteinFour.TraceHessian.matrixPairing line 115

    Source documentation

    Matrix-slot Frobenius pairing.

    def matrixPairing (M N : Mat) : ℝ := ∑ a, ∑ b, M a b * N a b

    Mentions: OAI.PositiveEinsteinFour.TraceHessian.Mat

  13. theorem OAI.PositiveEinsteinFour.TraceHessian.matrixPairing_coordinates line 117
  14. theorem OAI.PositiveEinsteinFour.TraceHessian.matrixNormSq_coordinates line 124
  15. theorem OAI.PositiveEinsteinFour.TraceHessian.hessianPairing_derivative_order line 130
  16. theorem OAI.PositiveEinsteinFour.TraceHessian.hessianNormSq_derivative_order line 135