OAI/Analysis/MatrixSigning/Complexity/PolynomialPotential.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. instance OAI.CurrentKS.Realization.poly_potentialView line 12
2. instance OAI.CurrentKS.Realization.poly_ppD line 13
3. instance OAI.CurrentKS.Realization.poly_ppRest line 14
4. instance OAI.CurrentKS.Realization.poly_ppAtoms line 15
5. instance OAI.CurrentKS.Realization.poly_ppArgs line 16
6. instance OAI.CurrentKS.Realization.poly_ppX line 17
7. instance OAI.CurrentKS.Realization.poly_ppScalars line 18
8. instance OAI.CurrentKS.Realization.poly_ppNu line 19
9. instance OAI.CurrentKS.Realization.poly_ppLam line 20
10. instance OAI.CurrentKS.Realization.poly_ppError line 21
11. instance OAI.CurrentKS.Realization.poly_ppN line 22
12. instance OAI.CurrentKS.Realization.poly_ppRootTolerance line 23
13. instance OAI.CurrentKS.Realization.poly_ppTheta line 24
14. instance OAI.CurrentKS.Realization.poly_ppQuery line 25
15. def OAI.CurrentKS.Realization.PotentialParams.scanCount line 27
16. lemma OAI.CurrentKS.Realization.runsPoly_potentialQuery line 29