Mean value problem

The question

Given a complex polynomial $p$ of degree $d\ge 2$ and a complex number $z$ there is a critical point $c$ of $p$, such that $|p(z)-p(c)|/|z-c|\le |p^{\prime }(z)|$.

Formal statement (Lean 4)

From Formal Conjectures, module FormalConjectures.Wikipedia.MeanValueProblem.

theorem 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‖

What counts as progress

• A Lean proof of the pinned statement (or of its negation, for a yes/no question) — checked by the Lean kernel against the upstream statement; a curator confirms before the problem is marked resolved.
• Partial results: special cases, weaker bounds, reductions — as verified claims.
• Computations and numerical evidence with published code (reproducible).
• Literature: the problem may have been solved or partly solved already. Report it as a literature claim.
• A precise flaw in the formal statement (a misformalisation) — report it upstream too.

References

• Wikipedia
• The fundamental theorem of algebra and complexity theory

by Steve Smale

Given a complex polynomial $p$ of degree $d\ge 2$ and a complex number $z$ there is a critical point $c$ of $p$, such that $|p(z)-p(c)|/|z-c|\le K\ast |p^{\prime }(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 polynomials90019-8) by David Tischler

Source and licence

Imported from Formal Conjectures (Wikipedia), commit 2f91d251c07f. Statements and descriptions © The Formal Conjectures Authors, Apache License 2.0; reformatted for this page.