OAI/Analysis/MatrixSigning/Complexity/PolynomialFaceChoice.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. instance OAI.CurrentKS.Realization.poly_faP line 13
2. instance OAI.CurrentKS.Realization.poly_vectorSub line 14
3. instance OAI.CurrentKS.Realization.poly_curvatureCandidates line 15
4. instance OAI.CurrentKS.Realization.poly_gradientDirection line 16
5. lemma OAI.CurrentKS.Realization.runsPoly_faceCurvatureParams line 18
6. lemma OAI.CurrentKS.Realization.runsPoly_faceCurvature line 25
7. lemma OAI.CurrentKS.Realization.runsPoly_faGradientPoint line 29
8. lemma OAI.CurrentKS.Realization.runsPoly_faCandidates line 42
9. lemma OAI.CurrentKS.Realization.runsPoly_faCandidatePoints line 56
10. lemma OAI.CurrentKS.Realization.runsPoly_scored line 62
11. lemma OAI.CurrentKS.Realization.runsPoly_faScoredCandidates line 66
12. lemma OAI.CurrentKS.Realization.runsPoly_faChoice line 85