OAI/Geometry/EinsteinFour/HighestMinus.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

The minus Casimir energy and curvature bound on actual highest Hessians.

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

    Source documentation

    The actual total-minus Casimir is spin one.

    theorem totalMinus_casimir (c : Fin 21 → ℝ) :
    totalMinus 0 (totalMinus 0 (highest c)) +
      totalMinus 1 (totalMinus 1 (highest c)) +
      totalMinus 2 (totalMinus 2 (highest c)) = (-8 : ℝ) • highest c := by
…

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

  2. def OAI.PositiveEinsteinFour.HighestHessian.minusKernel line 22
  3. theorem OAI.PositiveEinsteinFour.HighestHessian.rightQuaternion_skew line 28
  4. theorem OAI.PositiveEinsteinFour.HighestHessian.minusKernel_skew line 32
  5. theorem OAI.PositiveEinsteinFour.HighestHessian.totalMinus_coordinates line 42
  6. theorem OAI.PositiveEinsteinFour.HighestHessian.totalMinus_skew line 49
  7. theorem OAI.PositiveEinsteinFour.HighestHessian.totalMinus_energy line 57
  8. theorem OAI.PositiveEinsteinFour.HighestHessian.minus_energy_bound line 71

    Source documentation

    The minus curvature bound has exactly the coefficient needed by P.

    theorem minus_energy_bound (c : Fin 21 → ℝ) (u : Fin 3 → ℝ) (y : ℝ)
    (hu : ∀ s, -y ≤ u s) :
    -(u 0 * hessianNormSq (totalMinus 0 (highest c)) +
      u 1 * hessianNormSq (totalMinus 1 (highest c)) +
      u 2 * hessianNormSq (totalMinus 2 (highest c))) / 4 ≤
      2 * y * hessianNormSq (highest c) := by
…

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

  9. theorem OAI.PositiveEinsteinFour.HighestHessian.totalMinus_energy_of_condition line 88

    Source documentation

    The minus energy identity applies to every actual constrained Hessian.

    theorem totalMinus_energy_of_condition (X : Hessian) (hX : condition X) :
    hessianNormSq (totalMinus 0 X) + hessianNormSq (totalMinus 1 X) +
      hessianNormSq (totalMinus 2 X) = 8 * hessianNormSq X := by
…

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

  10. theorem OAI.PositiveEinsteinFour.HighestHessian.minus_energy_bound_of_condition line 94