OAI/Analysis/MatrixSigning/Complexity/PolynomialCoordinates.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

1. instance OAI.CurrentKS.Realization.poly_natLT line 24
2. instance OAI.CurrentKS.Realization.poly_scaleMatrix line 25
3. instance OAI.CurrentKS.Realization.poly_negateMatrix line 28
4. instance OAI.CurrentKS.Realization.poly_zeroMatrix line 29
5. instance OAI.CurrentKS.Realization.poly_reEntry line 30
6. instance OAI.CurrentKS.Realization.poly_imEntry line 31
7. instance OAI.CurrentKS.Realization.poly_squareTabulate line 32
8. instance OAI.CurrentKS.Realization.poly_realDecode line 35
9. instance OAI.CurrentKS.Realization.poly_singletonList line 36
10. instance OAI.CurrentKS.Realization.poly_replicateList line 37
11. instance OAI.CurrentKS.Realization.poly_blockScalar line 38
12. instance OAI.CurrentKS.Realization.poly_withLevel line 39
13. instance OAI.CurrentKS.Realization.poly_matrixSub line 40
14. instance OAI.CurrentKS.Realization.poly_zeroRect line 45
15. instance OAI.CurrentKS.Realization.poly_blockDiagonal line 46
16. instance OAI.CurrentKS.Realization.poly_basisVector line 47
17. instance OAI.CurrentKS.Realization.poly_pencilFromEval line 48
18. instance OAI.CurrentKS.Realization.poly_vdD line 60
19. instance OAI.CurrentKS.Realization.poly_vdRest line 61
20. instance OAI.CurrentKS.Realization.poly_vdAtoms line 62
21. instance OAI.CurrentKS.Realization.poly_vdParams line 63
22. instance OAI.CurrentKS.Realization.poly_vdX line 64
23. instance OAI.CurrentKS.Realization.poly_vdTheta line 65
24. instance OAI.CurrentKS.Realization.poly_vdEps line 66
25. instance OAI.CurrentKS.Realization.poly_realDimension line 67
26. instance OAI.CurrentKS.Realization.poly_valueDimension line 68
27. instance OAI.CurrentKS.Realization.poly_coordinateIndexRealizes line 69
28. instance OAI.CurrentKS.Realization.poly_coordinateEntry line 70
29. instance OAI.CurrentKS.Realization.poly_coordinates line 71
30. instance OAI.CurrentKS.Realization.poly_matrixVariable line 72