FormalConjectures.Wikipedia.MeanValueProblem

FormalConjectures
Wikipedia
MeanValueProblem

/-
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.
-/
module

public import FormalConjecturesUtil

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 at a point $z$ if the normalised polynomial $p(X + z) - p(z)$ has only real roots, or if all its nonzero roots have the same norm. Critical points and values of complex polynomials by David Tischler

@[expose] public sectionnamespace 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‖ := byp: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)‖
  sorryAll 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‖ := byp: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)‖
  sorryAll goals completed! 🐙

The following tighter bound depending on the degree $d$ of the polynomial $p$ has been shown by Tischler. Let $z$ be a complex number such that the normalised polynomial $p(X + z) - p(z)$ has only real roots, i.e. every $x$ with $p(x) = p(z)$ satisfies $\operatorname{Im} x = \operatorname{Im} z$. Then there is a critical point $c$ of $p$ such that $|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) (z : ℂ)
    (h : ∀ x : ℂ, p.eval x = p.eval z → x.im = z.im) (K : ℝ) :
    ∃ c : ℂ, p.derivative.eval c = 0 ∧
      ‖p.eval z - p.eval c‖ / ‖z - c‖ ≤ (p.natDegree - 1)/ p.natDegree * ‖p.derivative.eval z‖ := byp:Polynomial ℂhp:2 ≤ p.natDegreez:ℂh:∀ (x : ℂ), Polynomial.eval x p = Polynomial.eval z p → x.im = z.imK:ℝ⊢ ∃ 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)‖
  sorryAll goals completed! 🐙

The following tighter bound depending on the degree $d$ of the polynomial $p$ has been shown by Tischler. Let $z$ be a complex number such that all nonzero roots of the normalised polynomial $p(X + z) - p(z)$ have the same norm, i.e. all $x \ne z$ with $p(x) = p(z)$ have the same distance to $z$. Then there is a critical point $c$ of $p$ such that $|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) (z : ℂ)
    (h : ∀ x y : ℂ, p.eval x = p.eval z → p.eval y = p.eval z → x ≠ z → y ≠ z →
      ‖x - z‖ = ‖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‖ := byp:Polynomial ℂhp:2 ≤ p.natDegreez:ℂh:∀ (x y : ℂ),
  Polynomial.eval x p = Polynomial.eval z p →
    Polynomial.eval y p = Polynomial.eval z p → x ≠ z → y ≠ z → ‖x - z‖ = ‖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)‖
  sorryAll goals completed! 🐙

end MeanValueProblem