Crane (2007): $K < 4 - 2.263/\sqrt d$ for $d \ge 8$

Open

SmaleMeanValue.crane_bound

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

complex-analysispolynomials

Let $d \ge 8$ . There is a real constant

K < 4 - \frac{2.263}{\sqrt d}

such that for every complex polynomial $P$ of degree exactly $d$ and every $z \in \mathbb C$ with $P'(z) \neq 0$ there is a critical point $c$ of $P$ with

\left| \frac{P(z) - P(c)}{z - c} \right| \le K\,|P'(z)|.

Equivalently, the best constant in degree $d$ is strictly smaller than $4 - 2.263/\sqrt d$ .

Preamble

import Mathlib
open Polynomial

Formal statement

namespace SmaleMeanValue

theorem crane_bound (d : ℕ) (hd : 8 ≤ d) :
    ∃ K : ℝ, K < 4 - 2.263 / Real.sqrt d ∧
      ∀ P : ℂ[X], P.natDegree = d → ∀ z : ℂ, P.derivative.eval z ≠ 0 →
        ∃ c : ℂ, P.derivative.eval c = 0 ∧
          ‖(P.eval z - P.eval c) / (z - c)‖ ≤ K * ‖P.derivative.eval z‖ := 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, section "Partial results" ("Edward Crane showed that K < 4 - 2.263/sqrt(d) for d >= 8"); Crane, Bull. LMS 39(5) (2007), 781–791, https://doi.org/10.1112/blms/bdm063

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 8$ . The statement asserts that there exists a real number $K$ with

K < 4 - \frac{2.263}{\sqrt d}

(the real square root of $d$ ; $2.263$ is the exact decimal $2263/1000$ ) such that the following holds for every complex polynomial $P$ whose (natural-number) degree is exactly $d$ and every complex number $z$ with $P'(z) \neq 0$ ( $P'$ the formal derivative): there exists $c \in \mathbb C$ with $P'(c) = 0$ and

\left| \frac{P(z) - P(c)}{z - c} \right| \le K\,|P'(z)| .

The constant $K$ may depend on $d$ but not on $P$ or $z$ . The bound on $K$ is strict. Since $P'(z) \neq 0 = P'(c)$ , $c \neq z$ , so the quotient involves no division by zero.

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

Crane (2007): K<4−2.263/dK < 4 - 2.263/\sqrt dK<4−2.263/d​ for d≥8d \ge 8d≥8

Crane (2007): $K < 4 - 2.263/\sqrt d$ for $d \ge 8$