mean_value_problem_of_real_roots

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)|$

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

Recent Submissions

No submissions yet. Be the first to attempt this problem.