OAI/Combinatorics/Progressions/Polynomial/RealPolynomialEvaluationMass.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos3.realPolynomialMass line 16
2. theorem OAI.Erdos3.realPolynomialMass_nonneg line 19
3. theorem OAI.Erdos3.realPolynomialMass_zero line 22
4. theorem OAI.Erdos3.realPolynomialMass_monomial line 25
5. theorem OAI.Erdos3.realPolynomialMass_C line 30
6. theorem OAI.Erdos3.realPolynomialMass_X line 34
7. theorem OAI.Erdos3.realPolynomialMass_one line 38
8. theorem OAI.Erdos3.realPolynomialMass_eq_sum_of_support_subset line 41
9. theorem OAI.Erdos3.realPolynomialMass_coeff_le line 49
10. theorem OAI.Erdos3.realPolynomialMass_add_le line 57
11. theorem OAI.Erdos3.realPolynomialMass_sum_le line 69
12. theorem OAI.Erdos3.realPolynomialMass_mul_le line 88
13. theorem OAI.Erdos3.realPolynomialMass_prod_le line 108
14. theorem OAI.Erdos3.realPolynomialMass_pow_le line 118
15. theorem OAI.Erdos3.realPolynomialMass_C_mul_le line 127
16. theorem OAI.Erdos3.polynomialFunctional_expansion line 142
17. theorem OAI.Erdos3.polynomialFunctional_map_expansion line 153
18. theorem OAI.Erdos3.polynomialFunctional_le_mass line 164
19. theorem OAI.Erdos3.polynomialFunctional_homogeneous_le_mass line 178
20. theorem OAI.Erdos3.realPolynomialMass_substitution_le line 196
21. theorem OAI.Erdos3.polynomial_substitution_totalDegree_le line 223
22. theorem OAI.Erdos3.realPolynomialMass_rename_le line 240
23. def OAI.Erdos3.polynomialMonomial line 260
24. theorem OAI.Erdos3.polynomialMonomial_eval line 264
25. theorem OAI.Erdos3.polynomialMonomial_mass_le line 270
26. theorem OAI.Erdos3.polynomialMonomial_totalDegree_le line 284
27. theorem OAI.Erdos3.realPolynomialMass_smul line 307
28. theorem OAI.Erdos3.realPolynomialMass_pderiv line 315
29. theorem OAI.Erdos3.polynomialDerivation_eq_sum line 332
30. theorem OAI.Erdos3.realPolynomialMass_derivation line 342
31. theorem OAI.Erdos3.abs_aeval_le_mass_box line 374