Tischler (1989): optimal constant when all roots have the same modulus

Open

SmaleMeanValue.tischler_equal_modulus_roots

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

complex-analysispolynomials

Let $P$ be a complex polynomial of degree $d \ge 2$ all of whose roots have the same absolute value, and let $z \in \mathbb C$ with $P'(z) \neq 0$ . Then there is a critical point $c$ of $P$ with

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

This is the second class of polynomials for which Tischler established the optimal form of Smale's conjecture.

Formalization Note The source states the hypothesis as "all roots of $P$ have the same norm"; it is formalized literally, as equality of the absolute values of all roots, with $z$ an arbitrary non-critical point.

Preamble

import Mathlib
open Polynomial

Formal statement

namespace SmaleMeanValue

theorem tischler_equal_modulus_roots (P : ℂ[X]) (hP : 2 ≤ P.natDegree)
    (hnorm : ∀ r ∈ P.roots, ∀ s ∈ P.roots, ‖r‖ = ‖s‖) (z : ℂ)
    (hz : P.derivative.eval z ≠ 0) :
    ∃ c : ℂ, P.derivative.eval c = 0 ∧
      ‖(P.eval z - P.eval c) / (z - c)‖ ≤
        (((P.natDegree : ℝ) - 1) / P.natDegree) * ‖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" (Tischler 1989, all roots of the same norm); Tischler, J. Complexity 5(4) (1989), 438–456, https://doi.org/10.1016/0885-064X(89)90019-8

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 $P$ be any polynomial with complex coefficients, and write $d$ for its degree (the natural-number degree; for the zero polynomial this would be $0$ , but here it is excluded because $d \ge 2$ is assumed). Write $P'$ for the formal derivative of $P$ and $P(w)$ for evaluation at $w \in \mathbb C$ . Assume that any two roots $r, s$ of $P$ in $\mathbb C$ (from the multiset of roots) satisfy $|r| = |s|$ , i.e. all roots of $P$ lie on one circle centred at the origin $0$ (not at $z$ ). The common radius may be $0$ , in which case $P = a\,w^d$ for some $a \neq 0$ . Let $z$ be any complex number such that $P'(z) \neq 0$ . The statement asserts that there exists $c \in \mathbb C$ with $P'(c) = 0$ and

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

where $\frac{d-1}{d}$ is computed in the real numbers from $d$ . Here $c$ ranges over all complex numbers; the condition $P'(c) = 0$ says that $c$ is a critical point of $P$ . Because $P'(z) \neq 0$ and $P'(c) = 0$ , necessarily $c \neq z$ , so the denominator $z - c$ is never zero and no division-by-zero convention is involved. The absolute values are the usual modulus on $\mathbb C$ .

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