OAI/Geometry/EinsteinFour/HighestHessian.lean

GitHub source file

66 declarations, 0 contain sorry, 0 declared as axioms

Every actual highest Hessian has the twenty-one displayed coordinates.

  1. theorem OAI.PositiveEinsteinFour.HighestHessian.entry_reconstruction_0 line 14
  2. theorem OAI.PositiveEinsteinFour.HighestHessian.entry_reconstruction_1 line 25
  3. theorem OAI.PositiveEinsteinFour.HighestHessian.entry_reconstruction_2 line 36
  4. theorem OAI.PositiveEinsteinFour.HighestHessian.entry_reconstruction_3 line 47
  5. theorem OAI.PositiveEinsteinFour.HighestHessian.entry_reconstruction_4 line 58
  6. theorem OAI.PositiveEinsteinFour.HighestHessian.entry_reconstruction_5 line 67
  7. theorem OAI.PositiveEinsteinFour.HighestHessian.entry_reconstruction_6 line 76
  8. theorem OAI.PositiveEinsteinFour.HighestHessian.entry_reconstruction_7 line 85
  9. theorem OAI.PositiveEinsteinFour.HighestHessian.entry_reconstruction_8 line 92
  10. theorem OAI.PositiveEinsteinFour.HighestHessian.entry_reconstruction_9 line 99
  11. theorem OAI.PositiveEinsteinFour.HighestHessian.raw_reconstruction line 107

    Source documentation

    The actual trace and Bianchi constraints determine every nonfree entry.

    theorem raw_reconstruction (c : Fin 50 → ℝ)
    (ht : hessianTrace (raw c) = 0)
    (hb : ∀ i r, divergence (raw c) i r = 0) :
    raw c = highest (freeCoordinates c) := by
…

    Mentions: OAI.PositiveEinsteinFour.HighestHessian.raw, OAI.PositiveEinsteinFour.HighestHessian.divergence, OAI.PositiveEinsteinFour.HighestHessian.highest, OAI.PositiveEinsteinFour.HighestHessian.freeCoordinates

  12. def OAI.PositiveEinsteinFour.HighestHessian.coordinates line 127

    Source documentation

    Extract the fifty independent entries of a derivative-symmetric tensor.

    def coordinates (X : Hessian) : Fin 50 → ℝ :=
…
  13. theorem OAI.PositiveEinsteinFour.HighestHessian.coordinates_0 line 131
  14. theorem OAI.PositiveEinsteinFour.HighestHessian.coordinates_1 line 134
  15. theorem OAI.PositiveEinsteinFour.HighestHessian.coordinates_2 line 137
  16. theorem OAI.PositiveEinsteinFour.HighestHessian.coordinates_3 line 140
  17. theorem OAI.PositiveEinsteinFour.HighestHessian.coordinates_4 line 143
  18. theorem OAI.PositiveEinsteinFour.HighestHessian.coordinates_5 line 146
  19. theorem OAI.PositiveEinsteinFour.HighestHessian.coordinates_6 line 149
  20. theorem OAI.PositiveEinsteinFour.HighestHessian.coordinates_7 line 152
  21. theorem OAI.PositiveEinsteinFour.HighestHessian.coordinates_8 line 155
  22. theorem OAI.PositiveEinsteinFour.HighestHessian.coordinates_9 line 158
  23. theorem OAI.PositiveEinsteinFour.HighestHessian.coordinates_10 line 161
  24. theorem OAI.PositiveEinsteinFour.HighestHessian.coordinates_11 line 164
  25. theorem OAI.PositiveEinsteinFour.HighestHessian.coordinates_12 line 167
  26. theorem OAI.PositiveEinsteinFour.HighestHessian.coordinates_13 line 170
  27. theorem OAI.PositiveEinsteinFour.HighestHessian.coordinates_14 line 173
  28. theorem OAI.PositiveEinsteinFour.HighestHessian.coordinates_15 line 176
  29. theorem OAI.PositiveEinsteinFour.HighestHessian.coordinates_16 line 179
  30. theorem OAI.PositiveEinsteinFour.HighestHessian.coordinates_17 line 182
  31. theorem OAI.PositiveEinsteinFour.HighestHessian.coordinates_18 line 185
  32. theorem OAI.PositiveEinsteinFour.HighestHessian.coordinates_19 line 188
  33. theorem OAI.PositiveEinsteinFour.HighestHessian.coordinates_20 line 191
  34. theorem OAI.PositiveEinsteinFour.HighestHessian.coordinates_21 line 194
  35. theorem OAI.PositiveEinsteinFour.HighestHessian.coordinates_22 line 197
  36. theorem OAI.PositiveEinsteinFour.HighestHessian.coordinates_23 line 200
  37. theorem OAI.PositiveEinsteinFour.HighestHessian.coordinates_24 line 203
  38. theorem OAI.PositiveEinsteinFour.HighestHessian.coordinates_25 line 206
  39. theorem OAI.PositiveEinsteinFour.HighestHessian.coordinates_26 line 209
  40. theorem OAI.PositiveEinsteinFour.HighestHessian.coordinates_27 line 212
  41. theorem OAI.PositiveEinsteinFour.HighestHessian.coordinates_28 line 215
  42. theorem OAI.PositiveEinsteinFour.HighestHessian.coordinates_29 line 218
  43. theorem OAI.PositiveEinsteinFour.HighestHessian.coordinates_30 line 221
  44. theorem OAI.PositiveEinsteinFour.HighestHessian.coordinates_31 line 224
  45. theorem OAI.PositiveEinsteinFour.HighestHessian.coordinates_32 line 227
  46. theorem OAI.PositiveEinsteinFour.HighestHessian.coordinates_33 line 230
  47. theorem OAI.PositiveEinsteinFour.HighestHessian.coordinates_34 line 233
  48. theorem OAI.PositiveEinsteinFour.HighestHessian.coordinates_35 line 236
  49. theorem OAI.PositiveEinsteinFour.HighestHessian.coordinates_36 line 239
  50. theorem OAI.PositiveEinsteinFour.HighestHessian.coordinates_37 line 242
  51. theorem OAI.PositiveEinsteinFour.HighestHessian.coordinates_38 line 245
  52. theorem OAI.PositiveEinsteinFour.HighestHessian.coordinates_39 line 248
  53. theorem OAI.PositiveEinsteinFour.HighestHessian.coordinates_40 line 251
  54. theorem OAI.PositiveEinsteinFour.HighestHessian.coordinates_41 line 254
  55. theorem OAI.PositiveEinsteinFour.HighestHessian.coordinates_42 line 257
  56. theorem OAI.PositiveEinsteinFour.HighestHessian.coordinates_43 line 260
  57. theorem OAI.PositiveEinsteinFour.HighestHessian.coordinates_44 line 263
  58. theorem OAI.PositiveEinsteinFour.HighestHessian.coordinates_45 line 266
  59. theorem OAI.PositiveEinsteinFour.HighestHessian.coordinates_46 line 269
  60. theorem OAI.PositiveEinsteinFour.HighestHessian.coordinates_47 line 272
  61. theorem OAI.PositiveEinsteinFour.HighestHessian.coordinates_48 line 275
  62. theorem OAI.PositiveEinsteinFour.HighestHessian.coordinates_49 line 278
  63. theorem OAI.PositiveEinsteinFour.HighestHessian.raw_coordinates line 281
  64. theorem OAI.PositiveEinsteinFour.HighestHessian.exists_highest line 306

    Source documentation

    Every actual highest Hessian has the displayed twenty-one coordinates. Only derivative symmetry, matrix symmetry/trace, and Bianchi are used.

    theorem exists_highest (X : Hessian) (hX : condition X) :
    ∃ c : Fin 21 → ℝ, highest c = X := by
…

    Mentions: OAI.PositiveEinsteinFour.HighestHessian.condition, OAI.PositiveEinsteinFour.HighestHessian.highest

  65. theorem OAI.PositiveEinsteinFour.HighestHessian.freeCoordinates_coordinates_highest line 317

    Source documentation

    The displayed parameters are independent: extraction recovers each of the twenty-one free entries.

    theorem freeCoordinates_coordinates_highest (c : Fin 21 → ℝ) :
    freeCoordinates (coordinates (highest c)) = c := by
…

    Mentions: OAI.PositiveEinsteinFour.HighestHessian.freeCoordinates, OAI.PositiveEinsteinFour.HighestHessian.coordinates, OAI.PositiveEinsteinFour.HighestHessian.highest

  66. theorem OAI.PositiveEinsteinFour.HighestHessian.highest_injective line 323

    Source documentation

    The concrete parameter map has no hidden quotient or redundancy.

    theorem highest_injective : Function.Injective highest := by
…

    Mentions: OAI.PositiveEinsteinFour.HighestHessian.highest