OAI/Geometry/EinsteinFour/HighestActionCoordinates.lean

GitHub source file

136 declarations, 0 contain sorry, 0 declared as axioms

Exact coordinate action of the three total plus rotations.

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

    Source documentation

    Simultaneous plus rotation of both derivative slots and the matrix slots.

    def totalPlus (s : Fin 3) (X : Hessian) : Hessian := fun i j a b =>
…
  2. def OAI.PositiveEinsteinFour.HighestHessian.plusCoordinates line 21

    Source documentation

    The same action in the twenty-one actual free coordinates.

    def plusCoordinates (s : Fin 3) (c : Fin 21 → ℝ) : Fin 21 → ℝ :=
…
  3. theorem OAI.PositiveEinsteinFour.HighestHessian.plusCoordinates_0_0 line 88
  4. theorem OAI.PositiveEinsteinFour.HighestHessian.plusCoordinates_0_1 line 91
  5. theorem OAI.PositiveEinsteinFour.HighestHessian.plusCoordinates_0_2 line 94
  6. theorem OAI.PositiveEinsteinFour.HighestHessian.plusCoordinates_0_3 line 97
  7. theorem OAI.PositiveEinsteinFour.HighestHessian.plusCoordinates_0_4 line 100
  8. theorem OAI.PositiveEinsteinFour.HighestHessian.plusCoordinates_0_5 line 103
  9. theorem OAI.PositiveEinsteinFour.HighestHessian.plusCoordinates_0_6 line 106
  10. theorem OAI.PositiveEinsteinFour.HighestHessian.plusCoordinates_0_7 line 109
  11. theorem OAI.PositiveEinsteinFour.HighestHessian.plusCoordinates_0_8 line 112
  12. theorem OAI.PositiveEinsteinFour.HighestHessian.plusCoordinates_0_9 line 115
  13. theorem OAI.PositiveEinsteinFour.HighestHessian.plusCoordinates_0_10 line 118
  14. theorem OAI.PositiveEinsteinFour.HighestHessian.plusCoordinates_0_11 line 121
  15. theorem OAI.PositiveEinsteinFour.HighestHessian.plusCoordinates_0_12 line 124
  16. theorem OAI.PositiveEinsteinFour.HighestHessian.plusCoordinates_0_13 line 127
  17. theorem OAI.PositiveEinsteinFour.HighestHessian.plusCoordinates_0_14 line 130
  18. theorem OAI.PositiveEinsteinFour.HighestHessian.plusCoordinates_0_15 line 133
  19. theorem OAI.PositiveEinsteinFour.HighestHessian.plusCoordinates_0_16 line 136
  20. theorem OAI.PositiveEinsteinFour.HighestHessian.plusCoordinates_0_17 line 139
  21. theorem OAI.PositiveEinsteinFour.HighestHessian.plusCoordinates_0_18 line 142
  22. theorem OAI.PositiveEinsteinFour.HighestHessian.plusCoordinates_0_19 line 145
  23. theorem OAI.PositiveEinsteinFour.HighestHessian.plusCoordinates_0_20 line 148
  24. theorem OAI.PositiveEinsteinFour.HighestHessian.plusCoordinates_1_0 line 151
  25. theorem OAI.PositiveEinsteinFour.HighestHessian.plusCoordinates_1_1 line 154
  26. theorem OAI.PositiveEinsteinFour.HighestHessian.plusCoordinates_1_2 line 157
  27. theorem OAI.PositiveEinsteinFour.HighestHessian.plusCoordinates_1_3 line 160
  28. theorem OAI.PositiveEinsteinFour.HighestHessian.plusCoordinates_1_4 line 163
  29. theorem OAI.PositiveEinsteinFour.HighestHessian.plusCoordinates_1_5 line 166
  30. theorem OAI.PositiveEinsteinFour.HighestHessian.plusCoordinates_1_6 line 169
  31. theorem OAI.PositiveEinsteinFour.HighestHessian.plusCoordinates_1_7 line 172
  32. theorem OAI.PositiveEinsteinFour.HighestHessian.plusCoordinates_1_8 line 175
  33. theorem OAI.PositiveEinsteinFour.HighestHessian.plusCoordinates_1_9 line 178
  34. theorem OAI.PositiveEinsteinFour.HighestHessian.plusCoordinates_1_10 line 181
  35. theorem OAI.PositiveEinsteinFour.HighestHessian.plusCoordinates_1_11 line 184
  36. theorem OAI.PositiveEinsteinFour.HighestHessian.plusCoordinates_1_12 line 187
  37. theorem OAI.PositiveEinsteinFour.HighestHessian.plusCoordinates_1_13 line 190
  38. theorem OAI.PositiveEinsteinFour.HighestHessian.plusCoordinates_1_14 line 193
  39. theorem OAI.PositiveEinsteinFour.HighestHessian.plusCoordinates_1_15 line 196
  40. theorem OAI.PositiveEinsteinFour.HighestHessian.plusCoordinates_1_16 line 199
  41. theorem OAI.PositiveEinsteinFour.HighestHessian.plusCoordinates_1_17 line 202
  42. theorem OAI.PositiveEinsteinFour.HighestHessian.plusCoordinates_1_18 line 205
  43. theorem OAI.PositiveEinsteinFour.HighestHessian.plusCoordinates_1_19 line 208
  44. theorem OAI.PositiveEinsteinFour.HighestHessian.plusCoordinates_1_20 line 211
  45. theorem OAI.PositiveEinsteinFour.HighestHessian.plusCoordinates_2_0 line 214
  46. theorem OAI.PositiveEinsteinFour.HighestHessian.plusCoordinates_2_1 line 217
  47. theorem OAI.PositiveEinsteinFour.HighestHessian.plusCoordinates_2_2 line 220
  48. theorem OAI.PositiveEinsteinFour.HighestHessian.plusCoordinates_2_3 line 223
  49. theorem OAI.PositiveEinsteinFour.HighestHessian.plusCoordinates_2_4 line 226
  50. theorem OAI.PositiveEinsteinFour.HighestHessian.plusCoordinates_2_5 line 229
  51. theorem OAI.PositiveEinsteinFour.HighestHessian.plusCoordinates_2_6 line 232
  52. theorem OAI.PositiveEinsteinFour.HighestHessian.plusCoordinates_2_7 line 235
  53. theorem OAI.PositiveEinsteinFour.HighestHessian.plusCoordinates_2_8 line 238
  54. theorem OAI.PositiveEinsteinFour.HighestHessian.plusCoordinates_2_9 line 241
  55. theorem OAI.PositiveEinsteinFour.HighestHessian.plusCoordinates_2_10 line 244
  56. theorem OAI.PositiveEinsteinFour.HighestHessian.plusCoordinates_2_11 line 247
  57. theorem OAI.PositiveEinsteinFour.HighestHessian.plusCoordinates_2_12 line 250
  58. theorem OAI.PositiveEinsteinFour.HighestHessian.plusCoordinates_2_13 line 253
  59. theorem OAI.PositiveEinsteinFour.HighestHessian.plusCoordinates_2_14 line 256
  60. theorem OAI.PositiveEinsteinFour.HighestHessian.plusCoordinates_2_15 line 259
  61. theorem OAI.PositiveEinsteinFour.HighestHessian.plusCoordinates_2_16 line 262
  62. theorem OAI.PositiveEinsteinFour.HighestHessian.plusCoordinates_2_17 line 265
  63. theorem OAI.PositiveEinsteinFour.HighestHessian.plusCoordinates_2_18 line 268
  64. theorem OAI.PositiveEinsteinFour.HighestHessian.plusCoordinates_2_19 line 271
  65. theorem OAI.PositiveEinsteinFour.HighestHessian.plusCoordinates_2_20 line 274
  66. theorem OAI.PositiveEinsteinFour.HighestHessian.totalPlus_entry_0_0_0 line 277
  67. theorem OAI.PositiveEinsteinFour.HighestHessian.totalPlus_entry_0_0_1 line 284
  68. theorem OAI.PositiveEinsteinFour.HighestHessian.totalPlus_entry_0_0_2 line 291
  69. theorem OAI.PositiveEinsteinFour.HighestHessian.totalPlus_entry_0_0_3 line 298
  70. theorem OAI.PositiveEinsteinFour.HighestHessian.totalPlus_entry_0_1_0 line 305
  71. theorem OAI.PositiveEinsteinFour.HighestHessian.totalPlus_entry_0_1_1 line 312
  72. theorem OAI.PositiveEinsteinFour.HighestHessian.totalPlus_entry_0_1_2 line 319
  73. theorem OAI.PositiveEinsteinFour.HighestHessian.totalPlus_entry_0_1_3 line 326
  74. theorem OAI.PositiveEinsteinFour.HighestHessian.totalPlus_entry_0_2_0 line 333
  75. theorem OAI.PositiveEinsteinFour.HighestHessian.totalPlus_entry_0_2_1 line 340
  76. theorem OAI.PositiveEinsteinFour.HighestHessian.totalPlus_entry_0_2_2 line 347
  77. theorem OAI.PositiveEinsteinFour.HighestHessian.totalPlus_entry_0_2_3 line 354
  78. theorem OAI.PositiveEinsteinFour.HighestHessian.totalPlus_entry_0_3_0 line 361
  79. theorem OAI.PositiveEinsteinFour.HighestHessian.totalPlus_entry_0_3_1 line 368
  80. theorem OAI.PositiveEinsteinFour.HighestHessian.totalPlus_entry_0_3_2 line 375
  81. theorem OAI.PositiveEinsteinFour.HighestHessian.totalPlus_entry_0_3_3 line 382
  82. theorem OAI.PositiveEinsteinFour.HighestHessian.totalPlus_entry_1_0_0 line 389
  83. theorem OAI.PositiveEinsteinFour.HighestHessian.totalPlus_entry_1_0_1 line 396
  84. theorem OAI.PositiveEinsteinFour.HighestHessian.totalPlus_entry_1_0_2 line 403
  85. theorem OAI.PositiveEinsteinFour.HighestHessian.totalPlus_entry_1_0_3 line 410
  86. theorem OAI.PositiveEinsteinFour.HighestHessian.totalPlus_entry_1_1_0 line 417
  87. theorem OAI.PositiveEinsteinFour.HighestHessian.totalPlus_entry_1_1_1 line 424
  88. theorem OAI.PositiveEinsteinFour.HighestHessian.totalPlus_entry_1_1_2 line 431
  89. theorem OAI.PositiveEinsteinFour.HighestHessian.totalPlus_entry_1_1_3 line 438
  90. theorem OAI.PositiveEinsteinFour.HighestHessian.totalPlus_entry_1_2_0 line 445
  91. theorem OAI.PositiveEinsteinFour.HighestHessian.totalPlus_entry_1_2_1 line 452
  92. theorem OAI.PositiveEinsteinFour.HighestHessian.totalPlus_entry_1_2_2 line 459
  93. theorem OAI.PositiveEinsteinFour.HighestHessian.totalPlus_entry_1_2_3 line 466
  94. theorem OAI.PositiveEinsteinFour.HighestHessian.totalPlus_entry_1_3_0 line 473
  95. theorem OAI.PositiveEinsteinFour.HighestHessian.totalPlus_entry_1_3_1 line 480
  96. theorem OAI.PositiveEinsteinFour.HighestHessian.totalPlus_entry_1_3_2 line 487
  97. theorem OAI.PositiveEinsteinFour.HighestHessian.totalPlus_entry_1_3_3 line 494
  98. theorem OAI.PositiveEinsteinFour.HighestHessian.totalPlus_entry_2_0_0 line 501
  99. theorem OAI.PositiveEinsteinFour.HighestHessian.totalPlus_entry_2_0_1 line 508
  100. theorem OAI.PositiveEinsteinFour.HighestHessian.totalPlus_entry_2_0_2 line 515
  101. theorem OAI.PositiveEinsteinFour.HighestHessian.totalPlus_entry_2_0_3 line 522
  102. theorem OAI.PositiveEinsteinFour.HighestHessian.totalPlus_entry_2_1_0 line 529
  103. theorem OAI.PositiveEinsteinFour.HighestHessian.totalPlus_entry_2_1_1 line 536
  104. theorem OAI.PositiveEinsteinFour.HighestHessian.totalPlus_entry_2_1_2 line 543
  105. theorem OAI.PositiveEinsteinFour.HighestHessian.totalPlus_entry_2_1_3 line 550
  106. theorem OAI.PositiveEinsteinFour.HighestHessian.totalPlus_entry_2_2_0 line 557
  107. theorem OAI.PositiveEinsteinFour.HighestHessian.totalPlus_entry_2_2_1 line 564
  108. theorem OAI.PositiveEinsteinFour.HighestHessian.totalPlus_entry_2_2_2 line 571
  109. theorem OAI.PositiveEinsteinFour.HighestHessian.totalPlus_entry_2_2_3 line 578
  110. theorem OAI.PositiveEinsteinFour.HighestHessian.totalPlus_entry_2_3_0 line 585
  111. theorem OAI.PositiveEinsteinFour.HighestHessian.totalPlus_entry_2_3_1 line 592
  112. theorem OAI.PositiveEinsteinFour.HighestHessian.totalPlus_entry_2_3_2 line 599
  113. theorem OAI.PositiveEinsteinFour.HighestHessian.totalPlus_entry_2_3_3 line 606
  114. theorem OAI.PositiveEinsteinFour.HighestHessian.totalPlus_highest line 614

    Source documentation

    The total plus rotation preserves the explicit constrained space.

    theorem totalPlus_highest (s : Fin 3) (c : Fin 21 → ℝ) :
    totalPlus s (highest c) = highest (plusCoordinates s c) := by
…

    Mentions: OAI.PositiveEinsteinFour.HighestHessian.totalPlus, OAI.PositiveEinsteinFour.HighestHessian.highest, OAI.PositiveEinsteinFour.HighestHessian.plusCoordinates

  115. theorem OAI.PositiveEinsteinFour.HighestHessian.coordinate_casimir_0 line 667
  116. theorem OAI.PositiveEinsteinFour.HighestHessian.coordinate_casimir_1 line 673
  117. theorem OAI.PositiveEinsteinFour.HighestHessian.coordinate_casimir_2 line 679
  118. theorem OAI.PositiveEinsteinFour.HighestHessian.coordinate_casimir_3 line 685
  119. theorem OAI.PositiveEinsteinFour.HighestHessian.coordinate_casimir_4 line 691
  120. theorem OAI.PositiveEinsteinFour.HighestHessian.coordinate_casimir_5 line 697
  121. theorem OAI.PositiveEinsteinFour.HighestHessian.coordinate_casimir_6 line 703
  122. theorem OAI.PositiveEinsteinFour.HighestHessian.coordinate_casimir_7 line 709
  123. theorem OAI.PositiveEinsteinFour.HighestHessian.coordinate_casimir_8 line 715
  124. theorem OAI.PositiveEinsteinFour.HighestHessian.coordinate_casimir_9 line 721
  125. theorem OAI.PositiveEinsteinFour.HighestHessian.coordinate_casimir_10 line 727
  126. theorem OAI.PositiveEinsteinFour.HighestHessian.coordinate_casimir_11 line 733
  127. theorem OAI.PositiveEinsteinFour.HighestHessian.coordinate_casimir_12 line 739
  128. theorem OAI.PositiveEinsteinFour.HighestHessian.coordinate_casimir_13 line 745
  129. theorem OAI.PositiveEinsteinFour.HighestHessian.coordinate_casimir_14 line 751
  130. theorem OAI.PositiveEinsteinFour.HighestHessian.coordinate_casimir_15 line 757
  131. theorem OAI.PositiveEinsteinFour.HighestHessian.coordinate_casimir_16 line 763
  132. theorem OAI.PositiveEinsteinFour.HighestHessian.coordinate_casimir_17 line 769
  133. theorem OAI.PositiveEinsteinFour.HighestHessian.coordinate_casimir_18 line 775
  134. theorem OAI.PositiveEinsteinFour.HighestHessian.coordinate_casimir_19 line 781
  135. theorem OAI.PositiveEinsteinFour.HighestHessian.coordinate_casimir_20 line 787
  136. theorem OAI.PositiveEinsteinFour.HighestHessian.coordinate_casimir line 794

    Source documentation

    The spin-three Casimir is proved on the actual coordinate action.

    theorem coordinate_casimir (c : Fin 21 → ℝ) :
    plusCoordinates 0 (plusCoordinates 0 c) +
      plusCoordinates 1 (plusCoordinates 1 c) +
      plusCoordinates 2 (plusCoordinates 2 c) = (-48 : ℝ) • c := by
…

    Mentions: OAI.PositiveEinsteinFour.HighestHessian.plusCoordinates