OAI/Analysis/MatrixSigning/Complexity/PolynomialStencil.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. instance OAI.CurrentKS.Realization.poly_fiP line 18
2. instance OAI.CurrentKS.Realization.poly_fiI line 19
3. instance OAI.CurrentKS.Realization.poly_fiBasis line 20
4. instance OAI.CurrentKS.Realization.poly_fdS line 21
5. instance OAI.CurrentKS.Realization.poly_fdP line 22
6. instance OAI.CurrentKS.Realization.poly_fdI line 23
7. instance OAI.CurrentKS.Realization.poly_fdJ line 24
8. instance OAI.CurrentKS.Realization.poly_fdBasisI line 25
9. instance OAI.CurrentKS.Realization.poly_fdBasisJ line 26
10. lemma OAI.CurrentKS.Realization.runsPoly_stencilAt line 28
11. lemma OAI.CurrentKS.Realization.runsPoly_stencilGradientEntry line 45
12. lemma OAI.CurrentKS.Realization.runsPoly_stencilGradient line 56
13. lemma OAI.CurrentKS.Realization.runsPoly_stencilHessianEntry line 65
14. lemma OAI.CurrentKS.Realization.runsPoly_stencilHessianRow line 105
15. lemma OAI.CurrentKS.Realization.runsPoly_stencilHessian line 113