OAI/Analysis/MatrixSigning/Complexity/NaturalPolynomial.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

1. inductive OAI.KS.W23.NaturalPolynomial line 9
2. instance OAI.KS.W23.NaturalPolynomial.(instance at line 18) line 18
3. instance OAI.KS.W23.NaturalPolynomial.(instance at line 19) line 19
4. instance OAI.KS.W23.NaturalPolynomial.(instance at line 20) line 20
5. instance OAI.KS.W23.NaturalPolynomial.(instance at line 21) line 21
6. def OAI.KS.W23.NaturalPolynomial.eval line 23
7. def OAI.KS.W23.NaturalPolynomial.degree line 30
8. def OAI.KS.W23.NaturalPolynomial.coefficient line 37
9. theorem OAI.KS.W23.NaturalPolynomial.eval_constant line 39
10. theorem OAI.KS.W23.NaturalPolynomial.eval_variable line 40
11. theorem OAI.KS.W23.NaturalPolynomial.eval_add line 41
12. theorem OAI.KS.W23.NaturalPolynomial.eval_mul line 43
13. theorem OAI.KS.W23.NaturalPolynomial.eval_power line 45
14. theorem OAI.KS.W23.NaturalPolynomial.eval_numeral line 47
15. theorem OAI.KS.W23.NaturalPolynomial.eval_mono line 49
16. theorem OAI.KS.W23.NaturalPolynomial.eval_le_coefficient_mul_pow line 58
17. theorem OAI.KS.W23.NaturalPolynomial.eval_le_input_polynomial line 77
18. theorem OAI.KS.W23.NaturalPolynomial.eval_le_of_size_bound line 81