OAI/Analysis/HyperbolicCones/DeformationRoots.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Paper256.intervalPolynomial_eval line 11
2. theorem OAI.Paper256.intervalPolynomial_isRoot_iff line 16
3. theorem OAI.Paper256.deformedPolynomial_root_set line 29
4. theorem OAI.Paper256.deformedPolynomial_roots_compact line 40
5. theorem OAI.Paper256.intervalPolynomial_derivative_eval line 46
6. theorem OAI.Paper256.intervalPolynomial_roots_simple line 52
7. theorem OAI.Paper256.deformedPolynomial_roots_simple line 59
8. theorem OAI.Paper256.intervalPolynomial_radial_aeval line 68
9. theorem OAI.Paper256.intervalPolynomial_real_zero line 73
10. theorem OAI.Paper256.deformedPolynomial_real_zero line 101