OAI/Geometry/EinsteinFour/BianchiSlices.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Actual gradient slices of a four-slot Hessian.

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

    Source documentation

    A fixed outer derivative, retaining its actual tangent-vector entries.

    def innerSlice (X : Hessian) (i : Fin 4) : Tensor where
…
  2. theorem OAI.PositiveEinsteinFour.HighestHessian.innerSlice_matrix line 19
  3. theorem OAI.PositiveEinsteinFour.HighestHessian.innerSlice_traceFree line 26
  4. theorem OAI.PositiveEinsteinFour.HighestHessian.innerSlice_bianchi line 31
  5. theorem OAI.PositiveEinsteinFour.HighestHessian.innerSlice_of_condition line 40

    Source documentation

    The concrete highest-Hessian constraints give genuine Bianchi slices.

    theorem innerSlice_of_condition (X : Hessian) (hX : condition X) (i : Fin 4) :
    (innerSlice X i).traceFree ∧ (innerSlice X i).bianchi := by
…

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