OAI/Analysis/SymmetricDomains/PolynomialSignSetRoot.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Release061.SignElimination.finite_polynomial_sign_sampler line 38
2. lemma OAI.Release061.SignElimination.support_eq_of_coeff_sign_eq line 59
3. lemma OAI.Release061.SignElimination.degree_data_of_coeff_sign_eq line 68
4. lemma OAI.Release061.SignElimination.coeff_sign_ext_of_bound line 76
5. lemma OAI.Release061.SignElimination.degree_stratum_signSet line 86
6. lemma OAI.Release061.SignElimination.zero_stratum_signSet line 97
7. theorem OAI.Release061.SignElimination.polynomialSignSet_query_bounded line 107
8. def OAI.Release061.SignElimination.RationalPolynomialOn line 131
9. lemma OAI.Release061.SignElimination.RationalPolynomialOn.mono line 136
10. lemma OAI.Release061.SignElimination.RationalPolynomialOn.congr line 138
11. lemma OAI.Release061.SignElimination.RationalPolynomialOn.const line 140
12. lemma OAI.Release061.SignElimination.RationalPolynomialOn.add line 141
13. lemma OAI.Release061.SignElimination.RationalPolynomialOn.neg line 145
14. lemma OAI.Release061.SignElimination.RationalPolynomialOn.sub line 148
15. lemma OAI.Release061.SignElimination.RationalPolynomialOn.mul line 151
16. lemma OAI.Release061.SignElimination.RationalPolynomialOn.pow line 156
17. lemma OAI.Release061.SignElimination.RationalPolynomialOn.prod line 161
18. lemma OAI.Release061.SignElimination.RationalPolynomialOn.derivative line 169
19. lemma OAI.Release061.SignElimination.RationalPolynomialOn.criticalSampler line 173
20. lemma OAI.Release061.SignElimination.degree_lt_bound line 183
21. theorem OAI.Release061.SignElimination.polynomialSignSet_root_signs line 186