OAI/Geometry/EinsteinFour/HessianCompression.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

Curvature compression on all actual inner-Bianchi Hessian tensors.

  1. def OAI.PositiveEinsteinFour.HighestHessian.rawQuaternion line 18
  2. def OAI.PositiveEinsteinFour.HighestHessian.rawMatrixAt line 21
  3. theorem OAI.PositiveEinsteinFour.HighestHessian.hessianPairing_slices line 23
  4. theorem OAI.PositiveEinsteinFour.HighestHessian.hessianNormSq_slices line 28
  5. theorem OAI.PositiveEinsteinFour.HighestHessian.rawSlice_eq_innerSlice line 36
  6. theorem OAI.PositiveEinsteinFour.HighestHessian.outerAction_rawSlice line 42
  7. theorem OAI.PositiveEinsteinFour.HighestHessian.hessianPairing_outer_inner line 50
  8. theorem OAI.PositiveEinsteinFour.HighestHessian.sum_rotate line 58
  9. theorem OAI.PositiveEinsteinFour.HighestHessian.rawQuaternion_pairing line 68
  10. theorem OAI.PositiveEinsteinFour.HighestHessian.derivativeSlotForm_slices line 81

    Source documentation

    The derivative-slot quadratic form retains arbitrary inner-Bianchi slices.

    theorem derivativeSlotForm_slices (s : Fin 3) (X : Hessian) :
    derivativeSlotForm s X = ∑ i, ∑ k, quaternionMatrix s i k *
      rawPairing (rawQuaternion s (rawSlice X k)) (rawSlice X i) := by
…

    Mentions: OAI.PositiveEinsteinFour.HighestHessian.derivativeSlotForm, OAI.PositiveEinsteinFour.HighestHessian.rawQuaternion, OAI.PositiveEinsteinFour.HighestHessian.rawSlice

  11. theorem OAI.PositiveEinsteinFour.HighestHessian.derivativeSlotForm_inner_cross line 93

    Source documentation

    The skew outer quaternion converts the compressed inner action into the cross term in the total-plus energy. No symmetry of the outer slots is used.

    theorem derivativeSlotForm_inner_cross (s : Fin 3) (X : Hessian)
    (hmatrix : ∀ i j, symmetric (X i j) ∧ traceFree (X i j))
    (hbianchi : ∀ i r, divergence X i r = 0) :
    derivativeSlotForm s X =
      -(1 / 5 : ℝ) * hessianPairing (outerAction s X) (innerAction s X) := by
…

    Mentions: OAI.PositiveEinsteinFour.HighestHessian.divergence, OAI.PositiveEinsteinFour.HighestHessian.derivativeSlotForm, OAI.PositiveEinsteinFour.HighestHessian.outerAction, OAI.PositiveEinsteinFour.HighestHessian.innerAction

  12. theorem OAI.PositiveEinsteinFour.HighestHessian.outerAction_norm line 134
  13. theorem OAI.PositiveEinsteinFour.HighestHessian.matrixSlotForm_slices line 148
  14. theorem OAI.PositiveEinsteinFour.HighestHessian.innerAction_norm line 156

    Source documentation

    The matrix-row energy identity applies independently to every outer slice.

    theorem innerAction_norm (s : Fin 3) (X : Hessian)
    (hmatrix : ∀ i j, symmetric (X i j) ∧ traceFree (X i j))
    (hbianchi : ∀ i r, divergence X i r = 0) :
    hessianNormSq (innerAction s X) + 40 * matrixSlotForm s X =
      25 * hessianNormSq X := by
…

    Mentions: OAI.PositiveEinsteinFour.HighestHessian.divergence, OAI.PositiveEinsteinFour.HighestHessian.innerAction, OAI.PositiveEinsteinFour.HighestHessian.matrixSlotForm

  15. theorem OAI.PositiveEinsteinFour.HighestHessian.hessianNormSq_add line 172
  16. theorem OAI.PositiveEinsteinFour.HighestHessian.curvature_directional_identity line 182

    Source documentation

    The exact directional curvature identity on the whole actual inner-Bianchi tensor space, before restriction to the highest component.

    theorem curvature_directional_identity (s : Fin 3) (X : Hessian)
    (hmatrix : ∀ i j, symmetric (X i j) ∧ traceFree (X i j))
    (hbianchi : ∀ i r, divergence X i r = 0) :
    10 * derivativeSlotForm s X + 40 * matrixSlotForm s X +
      hessianNormSq (totalPlus s X) = 26 * hessianNormSq X := by
…

    Mentions: OAI.PositiveEinsteinFour.HighestHessian.divergence, OAI.PositiveEinsteinFour.HighestHessian.derivativeSlotForm, OAI.PositiveEinsteinFour.HighestHessian.matrixSlotForm, OAI.PositiveEinsteinFour.HighestHessian.totalPlus

  17. theorem OAI.PositiveEinsteinFour.HighestHessian.originalPlusCurvatureForm_eq_of_inner_bianchi line 195

    Source documentation

    The plus curvature identity is valid on the entire actual Bianchi gradient bundle, before taking the highest projection.

    theorem originalPlusCurvatureForm_eq_of_inner_bianchi (X : Hessian)
    (hmatrix : ∀ i j, symmetric (X i j) ∧ traceFree (X i j))
    (hbianchi : ∀ i r, divergence X i r = 0)
    (t : Fin 3 → ℝ) (ht : ∑ s, t s = 0) :
    originalPlusCurvatureForm t X = 4 * hessianNormSq X +
      (∑ s, t s * hessianNormSq (totalPlus s X)) / 24 := by
…

    Mentions: OAI.PositiveEinsteinFour.HighestHessian.divergence, OAI.PositiveEinsteinFour.HighestHessian.originalPlusCurvatureForm, OAI.PositiveEinsteinFour.HighestHessian.totalPlus

  18. theorem OAI.PositiveEinsteinFour.HighestHessian.originalCurvatureForm_eq_of_inner_bianchi line 213

    Source documentation

    This equality includes an unsymmetrized weight tensor as soon as its inner gradient satisfies Bianchi. The outer slots need not be symmetric.

    theorem originalCurvatureForm_eq_of_inner_bianchi (X : Hessian)
    (hmatrix : ∀ i j, symmetric (X i j) ∧ traceFree (X i j))
    (hbianchi : ∀ i r, divergence X i r = 0)
    (t u : Fin 3 → ℝ) (ht : ∑ s, t s = 0) (hu : ∑ s, u s = 0) :
    originalCurvatureForm t u X = casimirCurvatureForm t u X := by
…

    Mentions: OAI.PositiveEinsteinFour.HighestHessian.divergence, OAI.PositiveEinsteinFour.HighestHessian.originalCurvatureForm, OAI.PositiveEinsteinFour.HighestHessian.casimirCurvatureForm

  19. theorem OAI.PositiveEinsteinFour.HighestHessian.divergence_add_inner line 224
  20. def OAI.PositiveEinsteinFour.HighestHessian.originalPolarPairing line 234

    Source documentation

    Polarization of the original real quadratic curvature contraction.

    def originalPolarPairing (t u : Fin 3 → ℝ) (X Y : Hessian) : ℝ :=
…
  21. theorem OAI.PositiveEinsteinFour.HighestHessian.casimirCurvatureForm_add line 238
  22. theorem OAI.PositiveEinsteinFour.HighestHessian.originalPolarPairing_eq_of_inner_bianchi line 248

    Source documentation

    The mixed original curvature term agrees with the computed operator on arbitrary two inner-Bianchi tensors, including unsymmetrized weights.

    theorem originalPolarPairing_eq_of_inner_bianchi (X Y : Hessian)
    (hmatrixX : ∀ i j, symmetric (X i j) ∧ traceFree (X i j))
    (hbianchiX : ∀ i r, divergence X i r = 0)
    (hmatrixY : ∀ i j, symmetric (Y i j) ∧ traceFree (Y i j))
    (hbianchiY : ∀ i r, divergence Y i r = 0)
    (t u : Fin 3 → ℝ) (ht : ∑ s, t s = 0) (hu : ∑ s, u s = 0) :
    originalPolarPairing t u X Y = curvaturePairing t u X Y := by
…

    Mentions: OAI.PositiveEinsteinFour.HighestHessian.divergence, OAI.PositiveEinsteinFour.HighestHessian.originalPolarPairing, OAI.PositiveEinsteinFour.HighestHessian.curvaturePairing