OAI/Geometry/EinsteinFour/HighestConstraints.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

Extraction of the exact scalar equations from an actual Hessian.

  1. theorem OAI.PositiveEinsteinFour.HighestHessian.coordinate_constraint_0 line 14
  2. theorem OAI.PositiveEinsteinFour.HighestHessian.coordinate_constraint_1 line 23
  3. theorem OAI.PositiveEinsteinFour.HighestHessian.coordinate_constraint_2 line 32
  4. theorem OAI.PositiveEinsteinFour.HighestHessian.coordinate_constraint_3 line 41
  5. theorem OAI.PositiveEinsteinFour.HighestHessian.coordinate_constraint_4 line 50
  6. theorem OAI.PositiveEinsteinFour.HighestHessian.coordinate_constraint_5 line 59
  7. theorem OAI.PositiveEinsteinFour.HighestHessian.coordinate_constraint_6 line 67
  8. theorem OAI.PositiveEinsteinFour.HighestHessian.coordinate_constraint_7 line 75
  9. theorem OAI.PositiveEinsteinFour.HighestHessian.coordinate_constraint_8 line 83
  10. theorem OAI.PositiveEinsteinFour.HighestHessian.coordinate_constraint_9 line 91
  11. theorem OAI.PositiveEinsteinFour.HighestHessian.coordinate_constraint_10 line 99
  12. theorem OAI.PositiveEinsteinFour.HighestHessian.coordinate_constraint_11 line 107
  13. theorem OAI.PositiveEinsteinFour.HighestHessian.coordinate_constraint_12 line 115
  14. theorem OAI.PositiveEinsteinFour.HighestHessian.coordinate_constraint_17 line 123
  15. theorem OAI.PositiveEinsteinFour.HighestHessian.coordinate_constraint_18 line 131
  16. theorem OAI.PositiveEinsteinFour.HighestHessian.coordinate_constraint_19 line 139
  17. theorem OAI.PositiveEinsteinFour.HighestHessian.coordinate_constraint_20 line 147
  18. theorem OAI.PositiveEinsteinFour.HighestHessian.coordinate_constraint_21 line 155
  19. theorem OAI.PositiveEinsteinFour.HighestHessian.coordinate_constraint_22 line 163
  20. theorem OAI.PositiveEinsteinFour.HighestHessian.coordinate_constraint_23 line 171
  21. theorem OAI.PositiveEinsteinFour.HighestHessian.coordinate_constraint_24 line 179
  22. theorem OAI.PositiveEinsteinFour.HighestHessian.coordinate_constraint_29 line 187
  23. theorem OAI.PositiveEinsteinFour.HighestHessian.coordinate_constraint_30 line 195
  24. theorem OAI.PositiveEinsteinFour.HighestHessian.coordinate_constraint_31 line 203
  25. theorem OAI.PositiveEinsteinFour.HighestHessian.coordinate_constraint_32 line 211
  26. theorem OAI.PositiveEinsteinFour.HighestHessian.coordinate_constraint_33 line 219
  27. theorem OAI.PositiveEinsteinFour.HighestHessian.coordinate_constraint_34 line 227
  28. theorem OAI.PositiveEinsteinFour.HighestHessian.coordinate_constraint_35 line 235
  29. theorem OAI.PositiveEinsteinFour.HighestHessian.coordinate_constraint_36 line 243
  30. theorem OAI.PositiveEinsteinFour.HighestHessian.equations_of_constraints line 252

    Source documentation

    The geometric tensor constraints imply the displayed independent system.

    theorem equations_of_constraints (c : Fin 50 → ℝ)
    (ht : hessianTrace (raw c) = 0)
    (hb : ∀ i r, divergence (raw c) i r = 0) : Equations c where
…

    Mentions: OAI.PositiveEinsteinFour.HighestHessian.raw, OAI.PositiveEinsteinFour.HighestHessian.divergence, OAI.PositiveEinsteinFour.HighestHessian.Equations