OAI/Geometry/EinsteinFour/HighestCondition.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The displayed highest coordinates satisfy every original tensor constraint.

  1. theorem OAI.PositiveEinsteinFour.HighestHessian.highest_derivative_symmetric line 15

    Source documentation

    Symmetry is built into the two derivative slots of the coordinate array.

    theorem highest_derivative_symmetric (c : Fin 21 → ℝ) (i j : Fin 4) :
    highest c i j = highest c j i := by
…

    Mentions: OAI.PositiveEinsteinFour.HighestHessian.highest

  2. theorem OAI.PositiveEinsteinFour.HighestHessian.highest_matrix_symmetric line 19
  3. theorem OAI.PositiveEinsteinFour.HighestHessian.highest_matrix_traceFree line 25
  4. theorem OAI.PositiveEinsteinFour.HighestHessian.highest_trace line 31
  5. theorem OAI.PositiveEinsteinFour.HighestHessian.highest_divergence line 38
  6. theorem OAI.PositiveEinsteinFour.HighestHessian.highest_condition line 47

    Source documentation

    The concrete constrained-space description in both directions.

    theorem highest_condition (c : Fin 21 → ℝ) : condition (highest c) := by
…

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

  7. theorem OAI.PositiveEinsteinFour.HighestHessian.condition_iff_exists_highest line 52