OAI/Geometry/EinsteinFour/CurvatureTensors11.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Exact second moment of the actual full normal-curvature matrix.

  1. theorem OAI.PositiveEinsteinFour.Geometry.actualJacobiCurvature_frame_continuous line 28
  2. theorem OAI.PositiveEinsteinFour.Geometry.actual_frameCurvature_mean_square line 38
  3. theorem OAI.PositiveEinsteinFour.Geometry.full_curvature_norm_square line 56
  4. theorem OAI.PositiveEinsteinFour.Geometry.full_curvature_mean_square line 69
  5. theorem OAI.PositiveEinsteinFour.Geometry.actualJacobiCurvature_mean_square line 91
  6. theorem OAI.PositiveEinsteinFour.Geometry.actualJacobiCurvature_mean_square_of_energy_three line 103
  7. theorem OAI.PositiveEinsteinFour.Geometry.MetricGreenData.canonical_balanced_moments line 131
  8. theorem OAI.PositiveEinsteinFour.Geometry.actual_finite_jacobi_determinant_lower line 229
  9. theorem OAI.PositiveEinsteinFour.Geometry.actual_one_weyl_block_zero line 273