LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6.1-sol)audited 2026-10-02

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

The Chebyshev constant is the root limit of monic extremal norms

Statement

Let $K \subseteq C$ be nonempty and compact, with $t_{n} (K)$ and $cheb (K)$ as in Chebyshev constant of a compact planar set. Then

$t_{m + n} (K) \leq t_{m} (K) t_{n} (K) (m, n \geq 1),$

and consequently the sequence of nonnegative $n$ -th roots converges with

$\lim_{n \to \infty} t_{n} (K)^{1 / n} = \inf_{n \geq 1} t_{n} (K)^{1 / n} = cheb (K) .$

No choice principle is used.

Facts & Assumptions

Given: a nonempty compact $K \subseteq C$ , the quantities $t_{n} (K)$ and $cheb (K)$ of Chebyshev constant of a compact planar set, and the standing convention that all polynomials are monic of the stated degree when said so.

[F1]

By definition $t_{n} (K) = \inf {∥ p ∥_{K} : p monic of degree n}$ , with $∥ p ∥_{K} = \sup_{z \in K} ∣ p (z) ∣$ and $0 \leq t_{n} (K) < \infty$ ; and $cheb (K) = \inf_{n \geq 1} t_{n} (K)^{1 / n}$ (Chebyshev constant of a compact planar set).

[F2]

Over the integral domain $C$ , a product of nonzero polynomials has $\deg (f g) = \deg f + \deg g$ and leading coefficient the product of the leading coefficients; hence a product of monic polynomials is monic of the summed degree (Over an integral domain, degrees add under multiplication of nonzero polynomials).

[F3]

$∣ z w ∣ = ∣ z ∣ ∣ w ∣$ for all $z, w \in C$ , and $∣ z ∣ \geq 0$ (Conjugation is an involutive real-field automorphism, $z \overline{z} = ∣ z ∣^{2}$ , and modulus is definite, multiplicative, and subadditive).

[F4]

If $S \subseteq R$ is nonempty and bounded below and $ℓ$ is a lower bound of $S$ , then $ℓ = \inf S$ exactly when for every $ε > 0$ there is $s \in S$ with $s < ℓ + ε$ (Epsilon characterisation of the infimum).

[F5]

For $a \geq 0$ and $n \geq 1$ the nonnegative $n$ -th root $a^{1 / n}$ is the unique $s \geq 0$ with $s^{n} = a$ ; for $x, y \geq 0$ one has $(x y)^{1 / n} = x^{1 / n} y^{1 / n}$ , and for $0 \leq x \leq y$ one has $x^{1 / n} \leq y^{1 / n}$ (Existence and uniqueness of $n$ -th roots: a unique $a^{1 / n} \geq 0$ with $(a^{1 / n})^{n} = a$ ).

[F6]

On $[0, \infty)$ the map $x \mapsto x^{n}$ is strictly increasing for $n \geq 1$ (Monotonicity of $x \mapsto x^{n}$ and of $n \mapsto a^{n}$ ).

[F7]

A nonempty finite set of real numbers has a maximum and a minimum (Every nonempty finite set of reals has a maximum and a minimum, Maximum and minimum of a set).

[F8]

$lim sup$ and $lim inf$ of a real sequence are elements of $\overline{R}$ ; a sequence converges to $L \in R$ if and only if ${lim inf}_{k} x_{k} = {lim sup}_{k} x_{k} = L$ (Limit superior and limit inferior of a real sequence as $\inf_{n} \sup_{k \geq n} x_{k}$ and $\sup_{n} \inf_{k \geq n} x_{k}$ in $\overline{R}$ , A real sequence converges to $L \in R$ iff $lim inf x_{k} = lim sup x_{k} = L$ , and diverges to $\pm \infty$ iff both equal $\pm \infty$ ).

[F9]

If $x_{k} \leq y_{k}$ eventually, then ${lim sup}_{k} x_{k} \leq {lim sup}_{k} y_{k}$ and ${lim inf}_{k} x_{k} \leq {lim inf}_{k} y_{k}$ in $\overline{R}$ (If $x_{k} \leq y_{k}$ eventually then $lim sup x_{k} \leq lim sup y_{k}$ and $lim inf x_{k} \leq lim inf y_{k}$ ).

[F10]

For $c > 0$ , $c^{1 / n} \to 1$ as $n \to \infty$ (For every $a > 0$ , $a^{1 / n} \to 1$ ).

Proof

technique · direct

1.1F1F2F3F4algebra

Fix $m, n \geq 1$ and $ε > 0$ . Since $t_{m} (K)$ and $t_{n} (K)$ are finite lower bounds of their respective nonempty sets by [F1], [F4] supplies a monic polynomial $p$ of degree $m$ with $∥ p ∥_{K} < t_{m} (K) + ε$ and a monic polynomial $q$ of degree $n$ with $∥ q ∥_{K} < t_{n} (K) + ε$ . By [F2] the product $p q$ is monic of degree $m + n$ , and by [F3] one has $∣ p (z) q (z) ∣ = ∣ p (z) ∣ ∣ q (z) ∣ \leq ∥ p ∥_{K} ∥ q ∥_{K}$ for every $z \in K$ , so $∥ p q ∥_{K} \leq ∥ p ∥_{K} ∥ q ∥_{K} < (t_{m} (K) + ε) (t_{n} (K) + ε)$ . As $t_{m + n} (K)$ is a lower bound for the norms of all monic degree- $(m + n)$ polynomials ([F1]), $t_{m + n} (K) < (t_{m} (K) + ε) (t_{n} (K) + ε)$ for every $ε > 0$ ; letting $ε ↓ 0$ gives $t_{m + n} (K) \leq t_{m} (K) t_{n} (K)$ .

2.1step 1.1F1F4F5

Set $u_{n} : = t_{n} (K)$ for $n \geq 1$ and $L : = cheb (K)$ . Then $u_{n} \geq 0$ and $u_{m + n} \leq u_{m} u_{n}$ by step 1.1, and $L = \inf_{n \geq 1} u_{n}^{1 / n}$ by [F1]; in particular $L \geq 0$ and $L \leq u_{n}^{1 / n}$ for every $n$ . If $u_{k} = 0$ for some $k \geq 1$ , then iterating the submultiplicative inequality of step 1.1 in the form $u_{n} \leq u_{k} u_{n - k}$ for $n > k$ gives $u_{n} = 0$ for every $n \geq k$ , so $u_{n}^{1 / n} = 0$ for all $n \geq k$ by [F5], the root sequence converges to $0$ , and $L = \inf_{n \geq 1} u_{n}^{1 / n} = 0$ because $L \geq 0$ and $0 = u_{k}^{1 / k}$ belongs to the set; in this first case $\lim_{n} t_{n} (K)^{1 / n} = L = cheb (K)$ .

2.2step 1.1F5F6F7algebra

Suppose now that $u_{n} > 0$ for every $n \geq 1$ , and fix $k \geq 1$ . Put $a : = u_{k}^{1 / k} > 0$ , $B : = \max {1, a^{- k}} \geq 1$ and $C : = \max {1, u_{1}, \dots, u_{k - 1}} > 0$ ; both maxima exist by [F7] (for $k = 1$ the set whose maximum defines $C$ is ${1}$ ). Write an arbitrary $n \geq k$ as $n = q k + r$ with integers $q \geq 1$ and $0 \leq r < k$ . Iterating $u_{j + ℓ} \leq u_{j} u_{ℓ}$ of step 1.1 gives $u_{n} \leq u_{k}^{q} {\tilde{u}}_{r}$ , where ${\tilde{u}}_{r} : = 1$ for $r = 0$ and ${\tilde{u}}_{r} : = u_{r}$ for $1 \leq r < k$ ; hence $u_{n} \leq u_{k}^{q} C = a^{k q} C$ because ${\tilde{u}}_{r} \leq C$ . Since $r < k$ one has $a^{- r} \leq B$ : for $a \geq 1$ this is $a^{- r} \leq 1 \leq B$ , and for $0 < a < 1$ the inequality $- r \geq - (k - 1)$ gives $a^{- r} \leq a^{- (k - 1)} \leq a^{- k} \leq B$ . Therefore $a^{k q} C \leq a^{k q} a^{r} B C = a^{n} B C$ , since $1 \leq a^{r} B$ is the same inequality, and consequently $u_{n}^{1 / n} \leq a (B C)^{1 / n}$ for every $n \geq k$ by [F5] and [F6].

3.1step 2.1step 2.2F1F4F8F9F10

In the situation of step 2.2, apply [F9] to the eventual inequality just obtained and use that $n \mapsto a (B C)^{1 / n}$ converges to $a$ by [F10] and [F8]; hence ${lim sup}_{n} u_{n}^{1 / n} \leq a = u_{k}^{1 / k}$ . Since $k \geq 1$ was arbitrary and $L = \inf_{k} u_{k}^{1 / k}$ ([F1]), given $ε > 0$ the characterization [F4] of the infimum supplies $k$ with $u_{k}^{1 / k} < L + ε$ , so ${lim sup}_{n} u_{n}^{1 / n} \leq L + ε$ for every $ε > 0$ , that is, ${lim sup}_{n} u_{n}^{1 / n} \leq L$ . On the other hand $L$ is a lower bound of the root sequence by step 2.1, so ${lim inf}_{n} u_{n}^{1 / n} \geq L$ (Limit superior and limit inferior of a real sequence as $\inf_{n} \sup_{k \geq n} x_{k}$ and $\sup_{n} \inf_{k \geq n} x_{k}$ in $\overline{R}$ ); hence ${lim inf}_{n} u_{n}^{1 / n} = {lim sup}_{n} u_{n}^{1 / n} = L$ , which by [F8] is convergence of $(u_{n}^{1 / n})$ to $L$ . In this second case therefore $\lim_{n} t_{n} (K)^{1 / n} = cheb (K)$ as well.

4.1step 1.1step 2.1step 3.1F1∎

The two cases of steps 2.1 and 3.1 are exhaustive (either some $u_{k} = 0$ or $u_{n} > 0$ for all $n$ ), and in both the root sequence converges to $L = cheb (K)$ ; combining with the submultiplicativity proved in step 1.1 gives $t_{m + n} (K) \leq t_{m} (K) t_{n} (K)$ for all $m, n \geq 1$ and $\lim_{n \to \infty} t_{n} (K)^{1 / n} = \inf_{n \geq 1} t_{n} (K)^{1 / n} = cheb (K)$ .

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

70 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

E. B. Saff, Logarithmic Potential Theory with Applications to Approximation Theory, §1 (standard reference, not scraped)