/-
Copyright 2025 The Formal Conjectures Authors.
Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at
https://www.apache.org/licenses/LICENSE-2.0
Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.
-/
import FormalConjecturesUtilMean value problem
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
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
namespace MeanValueProblem
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)|$.
@[category research open, AMS 12]
lemma mean_value_problem (p : Polynomial ℂ) (hp : 2 ≤ p.degree) (z : ℂ) (K : ℝ):
∃ c : ℂ, p.derivative.eval c = 0 ∧
‖p.eval z - p.eval c‖ / ‖z - c‖ ≤ ‖p.derivative.eval z‖ := p:Polynomial ℂhp:2 ≤ p.degreez:ℂ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)‖
All goals completed! 🐙
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)|$.
@[category research solved, AMS 12]
lemma mean_value_problem_leq_4 (p : Polynomial ℂ) (hp : 2 ≤ p.degree) (z : ℂ) (K : ℝ):
∃ c : ℂ, p.derivative.eval c = 0 ∧
‖p.eval z - p.eval c‖ / ‖z - c‖ ≤ 4 *‖p.derivative.eval z‖ := p:Polynomial ℂhp:2 ≤ p.degreez:ℂ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)‖
All goals completed! 🐙
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)|$
@[category research solved, AMS 12]
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‖ := p:Polynomial ℂhp:2 ≤ p.natDegreeh:∀ (x : ℂ), p.IsRoot x → x.im = 0z:ℂ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)‖
All goals completed! 🐙
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)|$.
@[category research solved, AMS 12]
lemma 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 : ℂ, p.derivative.eval c = 0 ∧
‖p.eval z - p.eval c‖ / ‖z - c‖ ≤ (p.natDegree - 1)/ p.natDegree * ‖p.derivative.eval z‖ := p:Polynomial ℂhp:2 ≤ p.natDegreeh:∀ (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)‖
All goals completed! 🐙
end MeanValueProblem