OAI/Geometry/Relativity/CKS/NonroundFrame.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.CKSFrame.I line 9
  2. abbrev OAI.CKSFrame.A line 10
  3. structure OAI.CKSFrame.ConnectionData line 12
  4. def OAI.CKSFrame.chi line 20
  5. def OAI.CKSFrame.leafConnection line 23
  6. def OAI.CKSFrame.connection line 26
  7. lemma OAI.CKSFrame.connection_metric line 31
  8. lemma OAI.CKSFrame.connection_normal line 35
  9. def OAI.CKSFrame.curvature line 39
  10. def OAI.CKSFrame.scalarCurvature line 45
  11. def OAI.CKSFrame.leafCurvature line 48
  12. def OAI.CKSFrame.leafScalar line 54
  13. def OAI.CKSFrame.mean line 57
  14. def OAI.CKSFrame.normalMean line 59
  15. def OAI.CKSFrame.chiNormSq line 61
  16. def OAI.CKSFrame.accelNormSq line 63
  17. def OAI.CKSFrame.accelDiv line 65
  18. lemma OAI.CKSFrame.leafScalar_formula line 68
  19. lemma OAI.CKSFrame.scalarCurvature_formula line 73