OAI/Geometry/Relativity/CKS/CollarRawCurvature.lean
5 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.CKSAngularGeometry.scalarMatrixToJet_subline 11 - lemma
OAI.CKSAngularGeometry.scalarMatrixToJet_normline 13 - lemma
OAI.CKSAngularGeometry.scalarCurvatureJet_smoothline 35 - lemma
OAI.CKSAngularGeometry.rawQ_differenceline 41 - theorem
OAI.CKSAngularGeometry.raw_curvature_uniformline 47