Zeros of polynomials
Location, counting and multiplicity of the zeros of polynomials: real-rootedness, stability, interlacing, root bounds and Sturm sequences.
- L1 norm and root bounds for polynomials
- Parity-change bound on real zeros
- Real-rooted polynomials
- Interlacing families of polynomials
- Stable polynomials
- Sturm's theorem
- Taylor expansion and double roots
TheoremAuerbach's problem on zero sets of real polynomials#●ready to prove
MathlibExt.Algebra.Polynomial.ScottishBook148Wanted.auerbachPolynomialZeroSetSeparatesIffFactorsSignDefinite
Let P be a nonzero real polynomial in n variables. Its zero set does
not cut (separate) Euclidean space, i.e. the complement of the zero set is
connected, if and only if every irreducible factor of P over the reals is
always nonnegative or always nonpositive (as a function). The complement of
a real algebraic hypersurface is semialgebraic, so connectedness of the
complement is equivalent to the path-connectedness used by Rojas.
theorem_wanted auerbachPolynomialZeroSetSeparatesIffFactorsSignDefinite :
∀ (n : ℕ) (P : MvPolynomial (Fin n) ℝ), P ≠ 0 →
IsConnected {x : Fin n → ℝ | (MvPolynomial.eval x) P ≠ 0} ↔
∀ Q : MvPolynomial (Fin n) ℝ, Irreducible Q → Q ∣ P →
(∀ x : Fin n → ℝ, 0 ≤ (MvPolynomial.eval x) Q) ∨
∀ x : Fin n → ℝ, (MvPolynomial.eval x) Q ≤ 0
Sources
Sources
- H. Auerbach, Problem 148 of the Scottish Book; both necessity and sufficiency proved by J. M. Rojas, "About Herman Auerbach's problem on factors of real polynomials with connected zero set complement", 2015 (see the commentary in Mauldin (ed.), The Scottish Book, 2nd ed., 2015).
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.