OAI/Analysis/MatrixSigning/Optimization/ShiftedHessian.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CurrentKS.RationalRoot.shiftedHessian line 15
2. def OAI.CurrentKS.RationalRoot.realQuadratic line 18
3. lemma OAI.CurrentKS.RationalRoot.shiftedHessian_symm line 22
4. lemma OAI.CurrentKS.RationalRoot.realQuadratic_cast line 26
5. lemma OAI.CurrentKS.RationalRoot.realQuadratic_shift line 31
6. def OAI.CurrentKS.RationalRoot.computedCurvature line 44
7. lemma OAI.CurrentKS.RationalRoot.curvature_parameters line 48
8. theorem OAI.CurrentKS.RationalRoot.computedCurvature_spec line 57