OAI/Geometry/EinsteinFour/HighestSquare.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

The weighted positive square on the actual highest-Hessian arrays.

  1. theorem OAI.PositiveEinsteinFour.HighestHessian.tensorCoordinates_add line 14
  2. theorem OAI.PositiveEinsteinFour.HighestHessian.tensorCoordinates_smul line 17
  3. theorem OAI.PositiveEinsteinFour.HighestHessian.totalPlus_add line 20
  4. theorem OAI.PositiveEinsteinFour.HighestHessian.totalPlus_smul line 29
  5. theorem OAI.PositiveEinsteinFour.HighestHessian.totalMinus_add line 37
  6. theorem OAI.PositiveEinsteinFour.HighestHessian.totalMinus_smul line 46
  7. def OAI.PositiveEinsteinFour.HighestHessian.curvaturePairing line 55

    Source documentation

    The symmetric form of the concrete curvature operator.

    def curvaturePairing (t u : Fin 3 → ℝ) (X Y : Hessian) : ℝ :=
…
  8. theorem OAI.PositiveEinsteinFour.HighestHessian.curvaturePairing_self line 60
  9. theorem OAI.PositiveEinsteinFour.HighestHessian.curvaturePairing_comm line 64
  10. theorem OAI.PositiveEinsteinFour.HighestHessian.curvaturePairing_add_left line 68
  11. theorem OAI.PositiveEinsteinFour.HighestHessian.curvaturePairing_smul_left line 75
  12. theorem OAI.PositiveEinsteinFour.HighestHessian.curvaturePairing_add_right line 82
  13. theorem OAI.PositiveEinsteinFour.HighestHessian.curvaturePairing_smul_right line 88
  14. theorem OAI.PositiveEinsteinFour.HighestHessian.weighted_curvature_square_identity line 94

    Source documentation

    The exact weighted-square expansion, before any geometric integration.

    theorem weighted_curvature_square_identity (t u : Fin 3 → ℝ) (X Y : Hessian)
    (m : ℝ) (hm : m ≠ 0) :
    (m / 6) * curvaturePairing t u (X + (1 / (2 * m)) • Y)
      (X + (1 / (2 * m)) • Y) =
    (m / 6) * curvaturePairing t u X X + curvaturePairing t u X Y / 6 +
      curvaturePairing t u Y Y / (24 * m) := by
…

    Mentions: OAI.PositiveEinsteinFour.HighestHessian.curvaturePairing

  15. theorem OAI.PositiveEinsteinFour.HighestHessian.weighted_curvature_square_nonneg line 109

    Source documentation

    Positivity of the actual highest-Hessian operator gives the weighted square used in the Hessian argument.

    theorem weighted_curvature_square_nonneg (c d : Fin 21 → ℝ)
    (t u : Fin 3 → ℝ) (x y m : ℝ) (hm : 0 < m)
    (ht : ∀ s, -x ≤ t s) (hu : ∀ s, -y ≤ u s) (hxy : x + y ≤ 2) :
    0 ≤ (m / 6) * curvaturePairing t u (highest c) (highest c) +
      curvaturePairing t u (highest c) (highest d) / 6 +
      curvaturePairing t u (highest d) (highest d) / (24 * m) := by
…

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

  16. theorem OAI.PositiveEinsteinFour.HighestHessian.weighted_curvature_square_nonneg_of_condition line 123

    Source documentation

    The weighted square in intrinsic tensor form, with only the concrete highest-Hessian constraints as hypotheses.

    theorem weighted_curvature_square_nonneg_of_condition (X Y : Hessian)
    (hX : condition X) (hY : condition Y) (t u : Fin 3 → ℝ)
    (x y m : ℝ) (hm : 0 < m) (ht : ∀ s, -x ≤ t s)
    (hu : ∀ s, -y ≤ u s) (hxy : x + y ≤ 2) :
    0 ≤ (m / 6) * curvaturePairing t u X X + curvaturePairing t u X Y / 6 +
      curvaturePairing t u Y Y / (24 * m) := by
…

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