OAI/Geometry/EinsteinFour/TraceActionIntertwining.lean

GitHub source file

74 declarations, 0 contain sorry, 0 declared as axioms

The trace lift intertwines the actual tensor rotation actions.

  1. theorem OAI.PositiveEinsteinFour.TraceHessian.traceLift_plus_0_0_0 line 14
  2. theorem OAI.PositiveEinsteinFour.TraceHessian.traceLift_plus_0_0_1 line 22
  3. theorem OAI.PositiveEinsteinFour.TraceHessian.traceLift_plus_0_0_2 line 30
  4. theorem OAI.PositiveEinsteinFour.TraceHessian.traceLift_plus_0_0_3 line 38
  5. theorem OAI.PositiveEinsteinFour.TraceHessian.traceLift_plus_0_0 line 46
  6. theorem OAI.PositiveEinsteinFour.TraceHessian.traceLift_plus_0_1_0 line 54
  7. theorem OAI.PositiveEinsteinFour.TraceHessian.traceLift_plus_0_1_1 line 62
  8. theorem OAI.PositiveEinsteinFour.TraceHessian.traceLift_plus_0_1_2 line 70
  9. theorem OAI.PositiveEinsteinFour.TraceHessian.traceLift_plus_0_1_3 line 78
  10. theorem OAI.PositiveEinsteinFour.TraceHessian.traceLift_plus_0_1 line 86
  11. theorem OAI.PositiveEinsteinFour.TraceHessian.traceLift_plus_0_2_0 line 94
  12. theorem OAI.PositiveEinsteinFour.TraceHessian.traceLift_plus_0_2_1 line 102
  13. theorem OAI.PositiveEinsteinFour.TraceHessian.traceLift_plus_0_2_2 line 110
  14. theorem OAI.PositiveEinsteinFour.TraceHessian.traceLift_plus_0_2_3 line 118
  15. theorem OAI.PositiveEinsteinFour.TraceHessian.traceLift_plus_0_2 line 126
  16. theorem OAI.PositiveEinsteinFour.TraceHessian.traceLift_plus_0_3_0 line 134
  17. theorem OAI.PositiveEinsteinFour.TraceHessian.traceLift_plus_0_3_1 line 142
  18. theorem OAI.PositiveEinsteinFour.TraceHessian.traceLift_plus_0_3_2 line 150
  19. theorem OAI.PositiveEinsteinFour.TraceHessian.traceLift_plus_0_3_3 line 158
  20. theorem OAI.PositiveEinsteinFour.TraceHessian.traceLift_plus_0_3 line 166
  21. theorem OAI.PositiveEinsteinFour.TraceHessian.traceLift_plus_1_0_0 line 174
  22. theorem OAI.PositiveEinsteinFour.TraceHessian.traceLift_plus_1_0_1 line 182
  23. theorem OAI.PositiveEinsteinFour.TraceHessian.traceLift_plus_1_0_2 line 190
  24. theorem OAI.PositiveEinsteinFour.TraceHessian.traceLift_plus_1_0_3 line 198
  25. theorem OAI.PositiveEinsteinFour.TraceHessian.traceLift_plus_1_0 line 206
  26. theorem OAI.PositiveEinsteinFour.TraceHessian.traceLift_plus_1_1_0 line 214
  27. theorem OAI.PositiveEinsteinFour.TraceHessian.traceLift_plus_1_1_1 line 222
  28. theorem OAI.PositiveEinsteinFour.TraceHessian.traceLift_plus_1_1_2 line 230
  29. theorem OAI.PositiveEinsteinFour.TraceHessian.traceLift_plus_1_1_3 line 238
  30. theorem OAI.PositiveEinsteinFour.TraceHessian.traceLift_plus_1_1 line 246
  31. theorem OAI.PositiveEinsteinFour.TraceHessian.traceLift_plus_1_2_0 line 254
  32. theorem OAI.PositiveEinsteinFour.TraceHessian.traceLift_plus_1_2_1 line 262
  33. theorem OAI.PositiveEinsteinFour.TraceHessian.traceLift_plus_1_2_2 line 270
  34. theorem OAI.PositiveEinsteinFour.TraceHessian.traceLift_plus_1_2_3 line 278
  35. theorem OAI.PositiveEinsteinFour.TraceHessian.traceLift_plus_1_2 line 286
  36. theorem OAI.PositiveEinsteinFour.TraceHessian.traceLift_plus_1_3_0 line 294
  37. theorem OAI.PositiveEinsteinFour.TraceHessian.traceLift_plus_1_3_1 line 302
  38. theorem OAI.PositiveEinsteinFour.TraceHessian.traceLift_plus_1_3_2 line 310
  39. theorem OAI.PositiveEinsteinFour.TraceHessian.traceLift_plus_1_3_3 line 318
  40. theorem OAI.PositiveEinsteinFour.TraceHessian.traceLift_plus_1_3 line 326
  41. theorem OAI.PositiveEinsteinFour.TraceHessian.traceLift_plus_2_0_0 line 334
  42. theorem OAI.PositiveEinsteinFour.TraceHessian.traceLift_plus_2_0_1 line 342
  43. theorem OAI.PositiveEinsteinFour.TraceHessian.traceLift_plus_2_0_2 line 350
  44. theorem OAI.PositiveEinsteinFour.TraceHessian.traceLift_plus_2_0_3 line 358
  45. theorem OAI.PositiveEinsteinFour.TraceHessian.traceLift_plus_2_0 line 366
  46. theorem OAI.PositiveEinsteinFour.TraceHessian.traceLift_plus_2_1_0 line 374
  47. theorem OAI.PositiveEinsteinFour.TraceHessian.traceLift_plus_2_1_1 line 382
  48. theorem OAI.PositiveEinsteinFour.TraceHessian.traceLift_plus_2_1_2 line 390
  49. theorem OAI.PositiveEinsteinFour.TraceHessian.traceLift_plus_2_1_3 line 398
  50. theorem OAI.PositiveEinsteinFour.TraceHessian.traceLift_plus_2_1 line 406
  51. theorem OAI.PositiveEinsteinFour.TraceHessian.traceLift_plus_2_2_0 line 414
  52. theorem OAI.PositiveEinsteinFour.TraceHessian.traceLift_plus_2_2_1 line 422
  53. theorem OAI.PositiveEinsteinFour.TraceHessian.traceLift_plus_2_2_2 line 430
  54. theorem OAI.PositiveEinsteinFour.TraceHessian.traceLift_plus_2_2_3 line 438
  55. theorem OAI.PositiveEinsteinFour.TraceHessian.traceLift_plus_2_2 line 446
  56. theorem OAI.PositiveEinsteinFour.TraceHessian.traceLift_plus_2_3_0 line 454
  57. theorem OAI.PositiveEinsteinFour.TraceHessian.traceLift_plus_2_3_1 line 462
  58. theorem OAI.PositiveEinsteinFour.TraceHessian.traceLift_plus_2_3_2 line 470
  59. theorem OAI.PositiveEinsteinFour.TraceHessian.traceLift_plus_2_3_3 line 478
  60. theorem OAI.PositiveEinsteinFour.TraceHessian.traceLift_plus_2_3 line 486
  61. theorem OAI.PositiveEinsteinFour.TraceHessian.traceLift_minus_0_0 line 494
  62. theorem OAI.PositiveEinsteinFour.TraceHessian.traceLift_minus_0_1 line 501
  63. theorem OAI.PositiveEinsteinFour.TraceHessian.traceLift_minus_0_2 line 508
  64. theorem OAI.PositiveEinsteinFour.TraceHessian.traceLift_minus_0_3 line 515
  65. theorem OAI.PositiveEinsteinFour.TraceHessian.traceLift_minus_1_0 line 522
  66. theorem OAI.PositiveEinsteinFour.TraceHessian.traceLift_minus_1_1 line 529
  67. theorem OAI.PositiveEinsteinFour.TraceHessian.traceLift_minus_1_2 line 536
  68. theorem OAI.PositiveEinsteinFour.TraceHessian.traceLift_minus_1_3 line 543
  69. theorem OAI.PositiveEinsteinFour.TraceHessian.traceLift_minus_2_0 line 550
  70. theorem OAI.PositiveEinsteinFour.TraceHessian.traceLift_minus_2_1 line 557
  71. theorem OAI.PositiveEinsteinFour.TraceHessian.traceLift_minus_2_2 line 564
  72. theorem OAI.PositiveEinsteinFour.TraceHessian.traceLift_minus_2_3 line 571
  73. theorem OAI.PositiveEinsteinFour.TraceHessian.totalPlus_traceLift line 579

    Source documentation

    The plus tensor action on the explicit restricted trace adjoint.

    theorem totalPlus_traceLift (s : Fin 3) (M : Mat) :
    totalPlus s (traceLift M) = traceLift (matrixAction s M) := by
…

    Mentions: OAI.PositiveEinsteinFour.TraceHessian.Mat, OAI.PositiveEinsteinFour.TraceHessian.traceLift, OAI.PositiveEinsteinFour.TraceHessian.matrixAction

  74. theorem OAI.PositiveEinsteinFour.TraceHessian.totalMinus_traceLift line 597

    Source documentation

    The minus tensor action on the explicit restricted trace adjoint.

    theorem totalMinus_traceLift (s : Fin 3) (M : Mat) :
    totalMinus s (traceLift M) = 0 := by
…

    Mentions: OAI.PositiveEinsteinFour.TraceHessian.Mat, OAI.PositiveEinsteinFour.TraceHessian.traceLift