OAI/Geometry/EinsteinFour/HighestCoordinates.lean

GitHub source file

81 declarations, 0 contain sorry, 0 declared as axioms

The undetermined Hessian in concrete quaternion coordinates.

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

    Source documentation

    A symmetric derivative array from its ten matrix entries.

    def symmetricArray (m : Fin 10 → Mat) : Hessian :=
…
  2. def OAI.PositiveEinsteinFour.HighestHessian.rawEntries line 20

    Source documentation

    All fifty coordinates before imposing derivative trace and Bianchi.

    def rawEntries (c : Fin 50 → ℝ) : Fin 10 → Mat :=
…
  3. def OAI.PositiveEinsteinFour.HighestHessian.raw line 33
  4. theorem OAI.PositiveEinsteinFour.HighestHessian.rawEntries_0 line 35
  5. theorem OAI.PositiveEinsteinFour.HighestHessian.rawEntries_1 line 38
  6. theorem OAI.PositiveEinsteinFour.HighestHessian.rawEntries_2 line 41
  7. theorem OAI.PositiveEinsteinFour.HighestHessian.rawEntries_3 line 44
  8. theorem OAI.PositiveEinsteinFour.HighestHessian.rawEntries_4 line 47
  9. theorem OAI.PositiveEinsteinFour.HighestHessian.rawEntries_5 line 50
  10. theorem OAI.PositiveEinsteinFour.HighestHessian.rawEntries_6 line 53
  11. theorem OAI.PositiveEinsteinFour.HighestHessian.rawEntries_7 line 56
  12. theorem OAI.PositiveEinsteinFour.HighestHessian.rawEntries_8 line 59
  13. theorem OAI.PositiveEinsteinFour.HighestHessian.rawEntries_9 line 62
  14. theorem OAI.PositiveEinsteinFour.HighestHessian.raw_0_0 line 66
  15. theorem OAI.PositiveEinsteinFour.HighestHessian.raw_0_1 line 69
  16. theorem OAI.PositiveEinsteinFour.HighestHessian.raw_0_2 line 72
  17. theorem OAI.PositiveEinsteinFour.HighestHessian.raw_0_3 line 75
  18. theorem OAI.PositiveEinsteinFour.HighestHessian.raw_1_0 line 78
  19. theorem OAI.PositiveEinsteinFour.HighestHessian.raw_1_1 line 81
  20. theorem OAI.PositiveEinsteinFour.HighestHessian.raw_1_2 line 84
  21. theorem OAI.PositiveEinsteinFour.HighestHessian.raw_1_3 line 87
  22. theorem OAI.PositiveEinsteinFour.HighestHessian.raw_2_0 line 90
  23. theorem OAI.PositiveEinsteinFour.HighestHessian.raw_2_1 line 93
  24. theorem OAI.PositiveEinsteinFour.HighestHessian.raw_2_2 line 96
  25. theorem OAI.PositiveEinsteinFour.HighestHessian.raw_2_3 line 99
  26. theorem OAI.PositiveEinsteinFour.HighestHessian.raw_3_0 line 102
  27. theorem OAI.PositiveEinsteinFour.HighestHessian.raw_3_1 line 105
  28. theorem OAI.PositiveEinsteinFour.HighestHessian.raw_3_2 line 108
  29. theorem OAI.PositiveEinsteinFour.HighestHessian.raw_3_3 line 111
  30. def OAI.PositiveEinsteinFour.HighestHessian.entries line 116

    Source documentation

    The twenty-one free coordinates after the actual tensor constraints.

    def entries (c : Fin 21 → ℝ) : Fin 10 → Mat :=
…
  31. def OAI.PositiveEinsteinFour.HighestHessian.highest line 129
  32. theorem OAI.PositiveEinsteinFour.HighestHessian.entries_0 line 131
  33. theorem OAI.PositiveEinsteinFour.HighestHessian.entries_1 line 134
  34. theorem OAI.PositiveEinsteinFour.HighestHessian.entries_2 line 137
  35. theorem OAI.PositiveEinsteinFour.HighestHessian.entries_3 line 140
  36. theorem OAI.PositiveEinsteinFour.HighestHessian.entries_4 line 143
  37. theorem OAI.PositiveEinsteinFour.HighestHessian.entries_5 line 146
  38. theorem OAI.PositiveEinsteinFour.HighestHessian.entries_6 line 149
  39. theorem OAI.PositiveEinsteinFour.HighestHessian.entries_7 line 152
  40. theorem OAI.PositiveEinsteinFour.HighestHessian.entries_8 line 155
  41. theorem OAI.PositiveEinsteinFour.HighestHessian.entries_9 line 158
  42. theorem OAI.PositiveEinsteinFour.HighestHessian.highest_0_0 line 161
  43. theorem OAI.PositiveEinsteinFour.HighestHessian.highest_0_1 line 164
  44. theorem OAI.PositiveEinsteinFour.HighestHessian.highest_0_2 line 167
  45. theorem OAI.PositiveEinsteinFour.HighestHessian.highest_0_3 line 170
  46. theorem OAI.PositiveEinsteinFour.HighestHessian.highest_1_0 line 173
  47. theorem OAI.PositiveEinsteinFour.HighestHessian.highest_1_1 line 176
  48. theorem OAI.PositiveEinsteinFour.HighestHessian.highest_1_2 line 179
  49. theorem OAI.PositiveEinsteinFour.HighestHessian.highest_1_3 line 182
  50. theorem OAI.PositiveEinsteinFour.HighestHessian.highest_2_0 line 185
  51. theorem OAI.PositiveEinsteinFour.HighestHessian.highest_2_1 line 188
  52. theorem OAI.PositiveEinsteinFour.HighestHessian.highest_2_2 line 191
  53. theorem OAI.PositiveEinsteinFour.HighestHessian.highest_2_3 line 194
  54. theorem OAI.PositiveEinsteinFour.HighestHessian.highest_3_0 line 197
  55. theorem OAI.PositiveEinsteinFour.HighestHessian.highest_3_1 line 200
  56. theorem OAI.PositiveEinsteinFour.HighestHessian.highest_3_2 line 203
  57. theorem OAI.PositiveEinsteinFour.HighestHessian.highest_3_3 line 206
  58. def OAI.PositiveEinsteinFour.HighestHessian.freeCoordinates line 210
  59. theorem OAI.PositiveEinsteinFour.HighestHessian.freeCoordinates_0 line 214
  60. theorem OAI.PositiveEinsteinFour.HighestHessian.freeCoordinates_1 line 217
  61. theorem OAI.PositiveEinsteinFour.HighestHessian.freeCoordinates_2 line 220
  62. theorem OAI.PositiveEinsteinFour.HighestHessian.freeCoordinates_3 line 223
  63. theorem OAI.PositiveEinsteinFour.HighestHessian.freeCoordinates_4 line 226
  64. theorem OAI.PositiveEinsteinFour.HighestHessian.freeCoordinates_5 line 229
  65. theorem OAI.PositiveEinsteinFour.HighestHessian.freeCoordinates_6 line 232
  66. theorem OAI.PositiveEinsteinFour.HighestHessian.freeCoordinates_7 line 235
  67. theorem OAI.PositiveEinsteinFour.HighestHessian.freeCoordinates_8 line 238
  68. theorem OAI.PositiveEinsteinFour.HighestHessian.freeCoordinates_9 line 241
  69. theorem OAI.PositiveEinsteinFour.HighestHessian.freeCoordinates_10 line 244
  70. theorem OAI.PositiveEinsteinFour.HighestHessian.freeCoordinates_11 line 247
  71. theorem OAI.PositiveEinsteinFour.HighestHessian.freeCoordinates_12 line 250
  72. theorem OAI.PositiveEinsteinFour.HighestHessian.freeCoordinates_13 line 253
  73. theorem OAI.PositiveEinsteinFour.HighestHessian.freeCoordinates_14 line 256
  74. theorem OAI.PositiveEinsteinFour.HighestHessian.freeCoordinates_15 line 259
  75. theorem OAI.PositiveEinsteinFour.HighestHessian.freeCoordinates_16 line 262
  76. theorem OAI.PositiveEinsteinFour.HighestHessian.freeCoordinates_17 line 265
  77. theorem OAI.PositiveEinsteinFour.HighestHessian.freeCoordinates_18 line 268
  78. theorem OAI.PositiveEinsteinFour.HighestHessian.freeCoordinates_19 line 271
  79. theorem OAI.PositiveEinsteinFour.HighestHessian.freeCoordinates_20 line 274
  80. def OAI.PositiveEinsteinFour.HighestHessian.divergence line 279

    Source documentation

    Bianchi is imposed on each fixed outer derivative, using the original quaternion action on the inner derivative and matrix slots.

    def divergence (X : Hessian) (i : Fin 4) (r : Fin 3) : Vec :=
…
  81. def OAI.PositiveEinsteinFour.HighestHessian.condition line 284

    Source documentation

    The highest Hessian tensor is symmetric in its derivatives, has zero trace, and satisfies the differentiated Bianchi equation.

    def condition (X : Hessian) : Prop :=
…