OAI/Geometry/EinsteinFour/HighestMinusCoordinates.lean

GitHub source file

137 declarations, 0 contain sorry, 0 declared as axioms

Exact coordinate action of the three total minus rotations.

  1. def OAI.PositiveEinsteinFour.HighestHessian.rightQuaternion line 15

    Source documentation

    Right quaternion multiplication, commuting with the fixed left frame.

    def rightQuaternion (s : Fin 3) : Matrix (Fin 4) (Fin 4) ℝ :=
…
  2. def OAI.PositiveEinsteinFour.HighestHessian.totalMinus line 20
  3. def OAI.PositiveEinsteinFour.HighestHessian.minusCoordinates line 24
  4. theorem OAI.PositiveEinsteinFour.HighestHessian.minusCoordinates_0_0 line 91
  5. theorem OAI.PositiveEinsteinFour.HighestHessian.minusCoordinates_0_1 line 94
  6. theorem OAI.PositiveEinsteinFour.HighestHessian.minusCoordinates_0_2 line 97
  7. theorem OAI.PositiveEinsteinFour.HighestHessian.minusCoordinates_0_3 line 100
  8. theorem OAI.PositiveEinsteinFour.HighestHessian.minusCoordinates_0_4 line 103
  9. theorem OAI.PositiveEinsteinFour.HighestHessian.minusCoordinates_0_5 line 106
  10. theorem OAI.PositiveEinsteinFour.HighestHessian.minusCoordinates_0_6 line 109
  11. theorem OAI.PositiveEinsteinFour.HighestHessian.minusCoordinates_0_7 line 112
  12. theorem OAI.PositiveEinsteinFour.HighestHessian.minusCoordinates_0_8 line 115
  13. theorem OAI.PositiveEinsteinFour.HighestHessian.minusCoordinates_0_9 line 118
  14. theorem OAI.PositiveEinsteinFour.HighestHessian.minusCoordinates_0_10 line 121
  15. theorem OAI.PositiveEinsteinFour.HighestHessian.minusCoordinates_0_11 line 124
  16. theorem OAI.PositiveEinsteinFour.HighestHessian.minusCoordinates_0_12 line 127
  17. theorem OAI.PositiveEinsteinFour.HighestHessian.minusCoordinates_0_13 line 130
  18. theorem OAI.PositiveEinsteinFour.HighestHessian.minusCoordinates_0_14 line 133
  19. theorem OAI.PositiveEinsteinFour.HighestHessian.minusCoordinates_0_15 line 136
  20. theorem OAI.PositiveEinsteinFour.HighestHessian.minusCoordinates_0_16 line 139
  21. theorem OAI.PositiveEinsteinFour.HighestHessian.minusCoordinates_0_17 line 142
  22. theorem OAI.PositiveEinsteinFour.HighestHessian.minusCoordinates_0_18 line 145
  23. theorem OAI.PositiveEinsteinFour.HighestHessian.minusCoordinates_0_19 line 148
  24. theorem OAI.PositiveEinsteinFour.HighestHessian.minusCoordinates_0_20 line 151
  25. theorem OAI.PositiveEinsteinFour.HighestHessian.minusCoordinates_1_0 line 154
  26. theorem OAI.PositiveEinsteinFour.HighestHessian.minusCoordinates_1_1 line 157
  27. theorem OAI.PositiveEinsteinFour.HighestHessian.minusCoordinates_1_2 line 160
  28. theorem OAI.PositiveEinsteinFour.HighestHessian.minusCoordinates_1_3 line 163
  29. theorem OAI.PositiveEinsteinFour.HighestHessian.minusCoordinates_1_4 line 166
  30. theorem OAI.PositiveEinsteinFour.HighestHessian.minusCoordinates_1_5 line 169
  31. theorem OAI.PositiveEinsteinFour.HighestHessian.minusCoordinates_1_6 line 172
  32. theorem OAI.PositiveEinsteinFour.HighestHessian.minusCoordinates_1_7 line 175
  33. theorem OAI.PositiveEinsteinFour.HighestHessian.minusCoordinates_1_8 line 178
  34. theorem OAI.PositiveEinsteinFour.HighestHessian.minusCoordinates_1_9 line 181
  35. theorem OAI.PositiveEinsteinFour.HighestHessian.minusCoordinates_1_10 line 184
  36. theorem OAI.PositiveEinsteinFour.HighestHessian.minusCoordinates_1_11 line 187
  37. theorem OAI.PositiveEinsteinFour.HighestHessian.minusCoordinates_1_12 line 190
  38. theorem OAI.PositiveEinsteinFour.HighestHessian.minusCoordinates_1_13 line 193
  39. theorem OAI.PositiveEinsteinFour.HighestHessian.minusCoordinates_1_14 line 196
  40. theorem OAI.PositiveEinsteinFour.HighestHessian.minusCoordinates_1_15 line 199
  41. theorem OAI.PositiveEinsteinFour.HighestHessian.minusCoordinates_1_16 line 202
  42. theorem OAI.PositiveEinsteinFour.HighestHessian.minusCoordinates_1_17 line 205
  43. theorem OAI.PositiveEinsteinFour.HighestHessian.minusCoordinates_1_18 line 208
  44. theorem OAI.PositiveEinsteinFour.HighestHessian.minusCoordinates_1_19 line 211
  45. theorem OAI.PositiveEinsteinFour.HighestHessian.minusCoordinates_1_20 line 214
  46. theorem OAI.PositiveEinsteinFour.HighestHessian.minusCoordinates_2_0 line 217
  47. theorem OAI.PositiveEinsteinFour.HighestHessian.minusCoordinates_2_1 line 220
  48. theorem OAI.PositiveEinsteinFour.HighestHessian.minusCoordinates_2_2 line 223
  49. theorem OAI.PositiveEinsteinFour.HighestHessian.minusCoordinates_2_3 line 226
  50. theorem OAI.PositiveEinsteinFour.HighestHessian.minusCoordinates_2_4 line 229
  51. theorem OAI.PositiveEinsteinFour.HighestHessian.minusCoordinates_2_5 line 232
  52. theorem OAI.PositiveEinsteinFour.HighestHessian.minusCoordinates_2_6 line 235
  53. theorem OAI.PositiveEinsteinFour.HighestHessian.minusCoordinates_2_7 line 238
  54. theorem OAI.PositiveEinsteinFour.HighestHessian.minusCoordinates_2_8 line 241
  55. theorem OAI.PositiveEinsteinFour.HighestHessian.minusCoordinates_2_9 line 244
  56. theorem OAI.PositiveEinsteinFour.HighestHessian.minusCoordinates_2_10 line 247
  57. theorem OAI.PositiveEinsteinFour.HighestHessian.minusCoordinates_2_11 line 250
  58. theorem OAI.PositiveEinsteinFour.HighestHessian.minusCoordinates_2_12 line 253
  59. theorem OAI.PositiveEinsteinFour.HighestHessian.minusCoordinates_2_13 line 256
  60. theorem OAI.PositiveEinsteinFour.HighestHessian.minusCoordinates_2_14 line 259
  61. theorem OAI.PositiveEinsteinFour.HighestHessian.minusCoordinates_2_15 line 262
  62. theorem OAI.PositiveEinsteinFour.HighestHessian.minusCoordinates_2_16 line 265
  63. theorem OAI.PositiveEinsteinFour.HighestHessian.minusCoordinates_2_17 line 268
  64. theorem OAI.PositiveEinsteinFour.HighestHessian.minusCoordinates_2_18 line 271
  65. theorem OAI.PositiveEinsteinFour.HighestHessian.minusCoordinates_2_19 line 274
  66. theorem OAI.PositiveEinsteinFour.HighestHessian.minusCoordinates_2_20 line 277
  67. theorem OAI.PositiveEinsteinFour.HighestHessian.totalMinus_entry_0_0_0 line 280
  68. theorem OAI.PositiveEinsteinFour.HighestHessian.totalMinus_entry_0_0_1 line 286
  69. theorem OAI.PositiveEinsteinFour.HighestHessian.totalMinus_entry_0_0_2 line 292
  70. theorem OAI.PositiveEinsteinFour.HighestHessian.totalMinus_entry_0_0_3 line 298
  71. theorem OAI.PositiveEinsteinFour.HighestHessian.totalMinus_entry_0_1_0 line 304
  72. theorem OAI.PositiveEinsteinFour.HighestHessian.totalMinus_entry_0_1_1 line 310
  73. theorem OAI.PositiveEinsteinFour.HighestHessian.totalMinus_entry_0_1_2 line 316
  74. theorem OAI.PositiveEinsteinFour.HighestHessian.totalMinus_entry_0_1_3 line 322
  75. theorem OAI.PositiveEinsteinFour.HighestHessian.totalMinus_entry_0_2_0 line 328
  76. theorem OAI.PositiveEinsteinFour.HighestHessian.totalMinus_entry_0_2_1 line 334
  77. theorem OAI.PositiveEinsteinFour.HighestHessian.totalMinus_entry_0_2_2 line 340
  78. theorem OAI.PositiveEinsteinFour.HighestHessian.totalMinus_entry_0_2_3 line 346
  79. theorem OAI.PositiveEinsteinFour.HighestHessian.totalMinus_entry_0_3_0 line 352
  80. theorem OAI.PositiveEinsteinFour.HighestHessian.totalMinus_entry_0_3_1 line 358
  81. theorem OAI.PositiveEinsteinFour.HighestHessian.totalMinus_entry_0_3_2 line 364
  82. theorem OAI.PositiveEinsteinFour.HighestHessian.totalMinus_entry_0_3_3 line 371
  83. theorem OAI.PositiveEinsteinFour.HighestHessian.totalMinus_entry_1_0_0 line 377
  84. theorem OAI.PositiveEinsteinFour.HighestHessian.totalMinus_entry_1_0_1 line 383
  85. theorem OAI.PositiveEinsteinFour.HighestHessian.totalMinus_entry_1_0_2 line 389
  86. theorem OAI.PositiveEinsteinFour.HighestHessian.totalMinus_entry_1_0_3 line 395
  87. theorem OAI.PositiveEinsteinFour.HighestHessian.totalMinus_entry_1_1_0 line 401
  88. theorem OAI.PositiveEinsteinFour.HighestHessian.totalMinus_entry_1_1_1 line 407
  89. theorem OAI.PositiveEinsteinFour.HighestHessian.totalMinus_entry_1_1_2 line 413
  90. theorem OAI.PositiveEinsteinFour.HighestHessian.totalMinus_entry_1_1_3 line 419
  91. theorem OAI.PositiveEinsteinFour.HighestHessian.totalMinus_entry_1_2_0 line 425
  92. theorem OAI.PositiveEinsteinFour.HighestHessian.totalMinus_entry_1_2_1 line 431
  93. theorem OAI.PositiveEinsteinFour.HighestHessian.totalMinus_entry_1_2_2 line 437
  94. theorem OAI.PositiveEinsteinFour.HighestHessian.totalMinus_entry_1_2_3 line 443
  95. theorem OAI.PositiveEinsteinFour.HighestHessian.totalMinus_entry_1_3_0 line 449
  96. theorem OAI.PositiveEinsteinFour.HighestHessian.totalMinus_entry_1_3_1 line 455
  97. theorem OAI.PositiveEinsteinFour.HighestHessian.totalMinus_entry_1_3_2 line 461
  98. theorem OAI.PositiveEinsteinFour.HighestHessian.totalMinus_entry_1_3_3 line 467
  99. theorem OAI.PositiveEinsteinFour.HighestHessian.totalMinus_entry_2_0_0 line 473
  100. theorem OAI.PositiveEinsteinFour.HighestHessian.totalMinus_entry_2_0_1 line 479
  101. theorem OAI.PositiveEinsteinFour.HighestHessian.totalMinus_entry_2_0_2 line 485
  102. theorem OAI.PositiveEinsteinFour.HighestHessian.totalMinus_entry_2_0_3 line 491
  103. theorem OAI.PositiveEinsteinFour.HighestHessian.totalMinus_entry_2_1_0 line 497
  104. theorem OAI.PositiveEinsteinFour.HighestHessian.totalMinus_entry_2_1_1 line 503
  105. theorem OAI.PositiveEinsteinFour.HighestHessian.totalMinus_entry_2_1_2 line 509
  106. theorem OAI.PositiveEinsteinFour.HighestHessian.totalMinus_entry_2_1_3 line 515
  107. theorem OAI.PositiveEinsteinFour.HighestHessian.totalMinus_entry_2_2_0 line 521
  108. theorem OAI.PositiveEinsteinFour.HighestHessian.totalMinus_entry_2_2_1 line 527
  109. theorem OAI.PositiveEinsteinFour.HighestHessian.totalMinus_entry_2_2_2 line 533
  110. theorem OAI.PositiveEinsteinFour.HighestHessian.totalMinus_entry_2_2_3 line 539
  111. theorem OAI.PositiveEinsteinFour.HighestHessian.totalMinus_entry_2_3_0 line 545
  112. theorem OAI.PositiveEinsteinFour.HighestHessian.totalMinus_entry_2_3_1 line 551
  113. theorem OAI.PositiveEinsteinFour.HighestHessian.totalMinus_entry_2_3_2 line 557
  114. theorem OAI.PositiveEinsteinFour.HighestHessian.totalMinus_entry_2_3_3 line 563
  115. theorem OAI.PositiveEinsteinFour.HighestHessian.totalMinus_highest line 569
  116. theorem OAI.PositiveEinsteinFour.HighestHessian.minus_coordinate_casimir_0 line 622
  117. theorem OAI.PositiveEinsteinFour.HighestHessian.minus_coordinate_casimir_1 line 628
  118. theorem OAI.PositiveEinsteinFour.HighestHessian.minus_coordinate_casimir_2 line 634
  119. theorem OAI.PositiveEinsteinFour.HighestHessian.minus_coordinate_casimir_3 line 640
  120. theorem OAI.PositiveEinsteinFour.HighestHessian.minus_coordinate_casimir_4 line 646
  121. theorem OAI.PositiveEinsteinFour.HighestHessian.minus_coordinate_casimir_5 line 652
  122. theorem OAI.PositiveEinsteinFour.HighestHessian.minus_coordinate_casimir_6 line 658
  123. theorem OAI.PositiveEinsteinFour.HighestHessian.minus_coordinate_casimir_7 line 664
  124. theorem OAI.PositiveEinsteinFour.HighestHessian.minus_coordinate_casimir_8 line 670
  125. theorem OAI.PositiveEinsteinFour.HighestHessian.minus_coordinate_casimir_9 line 676
  126. theorem OAI.PositiveEinsteinFour.HighestHessian.minus_coordinate_casimir_10 line 682
  127. theorem OAI.PositiveEinsteinFour.HighestHessian.minus_coordinate_casimir_11 line 688
  128. theorem OAI.PositiveEinsteinFour.HighestHessian.minus_coordinate_casimir_12 line 694
  129. theorem OAI.PositiveEinsteinFour.HighestHessian.minus_coordinate_casimir_13 line 700
  130. theorem OAI.PositiveEinsteinFour.HighestHessian.minus_coordinate_casimir_14 line 706
  131. theorem OAI.PositiveEinsteinFour.HighestHessian.minus_coordinate_casimir_15 line 712
  132. theorem OAI.PositiveEinsteinFour.HighestHessian.minus_coordinate_casimir_16 line 718
  133. theorem OAI.PositiveEinsteinFour.HighestHessian.minus_coordinate_casimir_17 line 724
  134. theorem OAI.PositiveEinsteinFour.HighestHessian.minus_coordinate_casimir_18 line 730
  135. theorem OAI.PositiveEinsteinFour.HighestHessian.minus_coordinate_casimir_19 line 736
  136. theorem OAI.PositiveEinsteinFour.HighestHessian.minus_coordinate_casimir_20 line 742
  137. theorem OAI.PositiveEinsteinFour.HighestHessian.minus_coordinate_casimir line 748