Return to Revisions

Okay, here goes:

1. Calculate the coefficients $\langle c_j : j\in d\rangle$ of the degree d-1 polynomial f'.
   
   
   
2. Run quantifier elimination over real closed fields on the formulas
   
   $((\displaystyle\bigwedge_{j\in d} ((a \leq x_j) \land (x_j \leq b))) \implies$ $(((((\displaystyle\sum_{j\in n} 1)\cdot (\displaystyle\sum_{j\in d} (c_j \cdot (\displaystyle\prod_{j\in d} x_j))))+1) \leq 0) \lor (1 \leq ((\displaystyle\sum_{j\in n} 1)\cdot (\displaystyle\sum_{j\in d} (c_j \cdot (\displaystyle\prod_{j\in d} x_j))))))$
   
   until the result is $ \; (0 = 0) \; $.
   
   
   
3. $\frac1n$ is now a lower bound for $|f'|$ in the interval $[a,b]$.