OAI/Geometry/EinsteinFour/JacobiCurvatureCap.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Positivity of the curvature perturbation below the scalar conjugate threshold. The cap three follows from positivity and trace three.

  1. theorem OAI.PositiveEinsteinFour.Jacobi.three_sub_posSemidef line 11
  2. theorem OAI.PositiveEinsteinFour.Jacobi.scalarLift_quadratic line 38
  3. theorem OAI.PositiveEinsteinFour.Jacobi.scalarLift_posDef line 47
  4. theorem OAI.PositiveEinsteinFour.Jacobi.scalarLift_sub_three line 63
  5. theorem OAI.PositiveEinsteinFour.Jacobi.symmetricCurvatureKernel_one_sub_posDef line 72