OAI/Analysis/MatrixSigning/Optimization/NegativeDirection.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CurrentKS.RationalRoot.negativeDirection line 17
2. lemma OAI.CurrentKS.RationalRoot.quadratic_scale line 20
3. theorem OAI.CurrentKS.RationalRoot.negativeDirection_spec line 29
4. def OAI.CurrentKS.RationalRoot.nearest line 54
5. def OAI.CurrentKS.RationalRoot.roundMesh line 57
6. lemma OAI.CurrentKS.RationalRoot.nearest_error line 60
7. lemma OAI.CurrentKS.RationalRoot.roundMesh_coord_error line 72
8. lemma OAI.CurrentKS.RationalRoot.norm_le_sum_abs line 80
9. lemma OAI.CurrentKS.RationalRoot.roundMesh_error line 87
10. lemma OAI.CurrentKS.RationalRoot.realVector_scale line 98
11. theorem OAI.CurrentKS.RationalRoot.curvature_rounding line 104