OAI/Analysis/MatrixSigning/Complexity/PolynomialCurvature.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

1. instance OAI.CurrentKS.Realization.poly_vectorNeg line 16
2. instance OAI.CurrentKS.Realization.poly_squareSum line 17
3. instance OAI.CurrentKS.Realization.poly_vectorDivide line 18
4. instance OAI.CurrentKS.Realization.poly_initialScale line 19
5. instance OAI.CurrentKS.Realization.poly_normalizeVector line 20
6. instance OAI.CurrentKS.Realization.poly_intCeil line 21
7. instance OAI.CurrentKS.Realization.poly_nearest line 22
8. instance OAI.CurrentKS.Realization.poly_nearestMesh line 23
9. instance OAI.CurrentKS.Realization.poly_roundMesh line 24
10. instance OAI.CurrentKS.Realization.poly_curvatureView line 25
11. instance OAI.CurrentKS.Realization.poly_cuN line 26
12. instance OAI.CurrentKS.Realization.poly_cuRest line 27
13. instance OAI.CurrentKS.Realization.poly_cuH line 28
14. instance OAI.CurrentKS.Realization.poly_cuScalars line 29
15. instance OAI.CurrentKS.Realization.poly_cuA line 30
16. instance OAI.CurrentKS.Realization.poly_cuMore line 31
17. instance OAI.CurrentKS.Realization.poly_cuM line 32
18. instance OAI.CurrentKS.Realization.poly_cuLast line 33
19. instance OAI.CurrentKS.Realization.poly_cuS line 34
20. instance OAI.CurrentKS.Realization.poly_cuRho line 35
21. instance OAI.CurrentKS.Realization.poly_cuShift line 36
22. instance OAI.CurrentKS.Realization.poly_computedCurvature line 37
23. instance OAI.CurrentKS.Realization.poly_updateVector line 38
24. instance OAI.CurrentKS.Realization.poly_endpointEntry line 39
25. instance OAI.CurrentKS.Realization.poly_endpointCandidates line 40
26. instance OAI.CurrentKS.Realization.poly_freezeScalar line 41
27. instance OAI.CurrentKS.Realization.poly_freezeVector line 42