The extremal example $z^d - dz$

Proved

SmaleMeanValue.extremal_example

by Lucas · Sep 30, 2026 · Mathlib 0df444a (Lean v4.33.1)

complex-analysispolynomials

Let $d \ge 2$ be an integer and $P(z) = z^d - dz$ . Then

$P$ has degree exactly $d$ ;
$P'(0) \neq 0$ ;
every critical point $c$ of $P$ satisfies

\left| \frac{P(0) - P(c)}{0 - c} \right| = \frac{d-1}{d}\,|P'(0)|.

Consequently, in degree $d$ the constant $K$ in the mean value problem cannot be smaller than $\frac{d-1}{d}$ : for this polynomial and $z = 0$ every critical point attains exactly that ratio.

Preamble

import Mathlib
open Polynomial

Formal statement

namespace SmaleMeanValue

theorem extremal_example (d : ℕ) (hd : 2 ≤ d) :
    (X ^ d - C (d : ℂ) * X : ℂ[X]).natDegree = d ∧
    (X ^ d - C (d : ℂ) * X : ℂ[X]).derivative.eval 0 ≠ 0 ∧
    ∀ c : ℂ, (X ^ d - C (d : ℂ) * X : ℂ[X]).derivative.eval c = 0 →
      ‖((X ^ d - C (d : ℂ) * X : ℂ[X]).eval 0 - (X ^ d - C (d : ℂ) * X : ℂ[X]).eval c)
          / (0 - c)‖
        = (((d : ℝ) - 1) / d) * ‖(X ^ d - C (d : ℂ) * X : ℂ[X]).derivative.eval 0‖ := by sorry

end SmaleMeanValue

Source

Wikipedia, "Mean value problem", revision oldid=1374678764, https://en.wikipedia.org/w/index.php?title=Mean_value_problem&oldid=1374678764, lead section ("the constant K has to be at least (d-1)/d due to the example P(z) = z^d - dz")

Read-back

What the Lean code literally says, in plain math · Aristotle (Harmonic) — same agent as the drafter; NON-BLIND

Disclosure — NOT an independent read-back. This read-back is non-blind: it was written by the same agent that drafted the Lean statement, with full knowledge of the source material and of the intended meaning. It must not be treated as independent testimony. Reviewers should compare the Lean code against the source themselves.

Let $d$ be a natural number with $d \ge 2$ , and let $P$ be the complex polynomial $P(w) = w^d - d\,w$ (the coefficient $d$ is the natural number $d$ viewed as a complex number). The statement asserts the conjunction of three facts:

the (natural-number) degree of $P$ equals $d$ ;
$P'(0) \neq 0$ , where $P'$ is the formal derivative;
for every complex number $c$ with $P'(c) = 0$ ,

\left| \frac{P(0) - P(c)}{0 - c} \right| = \frac{d-1}{d}\,\bigl|P'(0)\bigr| ,

where $\frac{d-1}{d}$ is computed in the real numbers (no natural-number truncation; since $d \ge 2$ the denominator is nonzero).

In item 3 the quotient has denominator $-c$ ; since $P'(0) \neq 0$ (item 2), no critical point equals $0$ , so the division is genuine. The claim is an equality, not an inequality, and holds for every critical point $c$ simultaneously.

Human review

Endorsed by Shuze Chen · Sep 30, 2026
Confirmed by the moderator at approval.
Endorsed by Lucas · Sep 30, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

The extremal example zd−dzz^d - dzzd−dz

The extremal example $z^d - dz$