Mean value problem

Reference:

• Wikipedia
• The fundamental theorem of algebra and complexity theory by Steve Smale

Given a complex polynomial $p$ of degree $d ≥ 2$ and a complex number $z$ there is a critical point $c$ of $p$, such that $|p(z)-p(c)|/|z-c| ≤ K* |p'(z)|$ for $K=1$.

The conjecture has been proven for:

• K = 4 The fundamental theorem of algebra and complexity theory by Steve Smale
• K = (d-1)/d if $p$ has real roots or all the roots of $p$ have the same norm. Critical points and values of complex polynomials by David Tischler

theorem mean_value_problem (p : Polynomial ℂ) (hp : 2 ≤ p.degree) (z : ℂ) (K : ℝ) : ∃ (c : ℂ), Polynomial.eval c (Polynomial.derivative p) = 0 ∧ ‖Polynomial.eval z p - Polynomial.eval c p‖ / ‖z - c‖ ≤ ‖Polynomial.eval z (Polynomial.derivative p)‖

Given a complex polynomial $p$ of degree $d ≥ 2$ and a complex number $z$ there is a critical point $c$ of $p$, such that $|p(z)-p(c)|/|z-c| ≤ |p'(z)|$.

theorem mean_value_problem_leq_4 (p : Polynomial ℂ) (hp : 2 ≤ p.degree) (z : ℂ) (K : ℝ) : ∃ (c : ℂ), Polynomial.eval c (Polynomial.derivative p) = 0 ∧ ‖Polynomial.eval z p - Polynomial.eval c p‖ / ‖z - c‖ ≤ 4 * ‖Polynomial.eval z (Polynomial.derivative p)‖

The following weaker version of the mean value problem has been proven. Given a complex polynomial $p$ of degree $d ≥ 2$ and a complex number $z$ there a critical point $c$ of $p$, such that $|p(z)-p(c)|/|z-c| ≤ 4|p'(z)|$.

theorem mean_value_problem_of_real_roots (p : Polynomial ℂ) (hp : 2 ≤ p.natDegree) (h : ∀ (x : ℂ), p.IsRoot x → x.im = 0) (z : ℂ) (K : ℝ) : ∃ (c : ℂ), Polynomial.eval c (Polynomial.derivative p) = 0 ∧ ‖Polynomial.eval z p - Polynomial.eval c p‖ / ‖z - c‖ ≤ (↑p.natDegree - 1) / ↑p.natDegree * ‖Polynomial.eval z (Polynomial.derivative p)‖

The following tighter bound depending on the degree $d$ of the polynomial $p$, in the case of $p$ only having real roots has been shown by Tischler. $|p(z)-p(c)|/|z-c| \le (d-1)/d \cdot |p'(z)|$

theorem mean_value_problem_of_roots_same_norm (p : Polynomial ℂ) (hp : 2 ≤ p.natDegree) (h : ∀ (x y : ℂ), p.IsRoot x ∧ p.IsRoot y → ‖x‖ = ‖y‖) (z : ℂ) (K : ℝ) : ∃ (c : ℂ), Polynomial.eval c (Polynomial.derivative p) = 0 ∧ ‖Polynomial.eval z p - Polynomial.eval c p‖ / ‖z - c‖ ≤ (↑p.natDegree - 1) / ↑p.natDegree * ‖Polynomial.eval z (Polynomial.derivative p)‖

The following tighter bound depending on the degree $d$ of the polynomial $p$, in the case of $p$ all roots having the same norm has been shown by Tischler. $|p(z) - p(c)|/|z-c| \le (d-1)/d \cdot |p'(z)|$.