LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge pass (gpt-6-luna)

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.

A scaled Chebyshev polynomial suppresses a separated interval

Statement

Let $a > b > c$ be real numbers, let $k \in N$ with $k \geq 0$ , and put

$ξ (x) : = \frac{2 x - b - c}{b - c}, ξ_{a} : = ξ (a) = 1 + \frac{2 (a - b)}{b - c} > 1.$

Define

$p_{k} (x) : = \frac{T_{k} (ξ (x))}{T_{k} (ξ_{a})},$

where $T_{k}$ is the $k$ th Chebyshev polynomial of the first kind from Chebyshev polynomials of the first and second kinds by their three-term recurrences. Then $p_{k}$ is a real polynomial of degree exactly $k$ , $p_{k} (a) = 1$ , and

$\max_{x \in [c, b]} ∣ p_{k} (x) ∣ = \frac{1}{T_{k} (ξ_{a})} .$

Facts & Assumptions

Given: Real numbers $a > b > c$ , an integer $k \geq 0$ , the affine map $ξ$ , the exterior point $ξ_{a}$ , and the polynomial $p_{k}$ in the Statement.

[F1]

Chebyshev polynomials of the first and second kinds by their three-term recurrences: $T_{0} = 1$ , $T_{1} = X$ , and $T_{j + 1} = 2 X T_{j} - T_{j - 1}$ for $j \geq 1$ .

[F2]

Formal real polynomials, evaluation, degree, leading coefficient, and monic polynomials: the degree and leading coefficient of a nonzero formal real polynomial are determined by its highest nonzero coefficient.

[F3]

Square roots exist: a unique $\sqrt{a} \geq 0$ with $(\sqrt{a})^{2} = a$ ; the positives are ${x^{2} : x \neq 0}$ : every nonnegative real has a nonnegative square root.

Proof

1.1givenF1F3inductionalgebra

Fix $t \in [- 1, 1]$ . Since $1 - t^{2} \geq 0$ , choose $s \geq 0$ with $s^{2} = 1 - t^{2}$ by [F3]. Define real sequences by $u_{0} = 1$ , $v_{0} = 0$ , and $u_{j + 1} = t u_{j} - s v_{j}, v_{j + 1} = s u_{j} + t v_{j} .$ Direct expansion gives $u_{j + 1}^{2} + v_{j + 1}^{2} = (t^{2} + s^{2}) (u_{j}^{2} + v_{j}^{2}) = u_{j}^{2} + v_{j}^{2}$ , so induction from $u_{0}^{2} + v_{0}^{2} = 1$ gives $∣ u_{j} ∣ \leq 1$ . Also $u_{j} = t u_{j + 1} + s v_{j + 1}$ , by substituting the recurrences and using $t^{2} + s^{2} = 1$ . Hence $u_{j + 2} + u_{j} = (t u_{j + 1} - s v_{j + 1}) + (t u_{j + 1} + s v_{j + 1}) = 2 t u_{j + 1}$ . Since $u_{0} = 1$ and $u_{1} = t$ , [F1] and induction give $u_{j} = T_{j} (t)$ . Thus $∣ T_{j} (t) ∣ \leq 1$ ; equality holds at $t = 1$ , where $s = 0$ and $u_{j} = 1$ for every $j$ .

1.2givenF1inductionalgebra

For $ξ_{a} > 1$ , recurrence [F1] gives $T_{0} (ξ_{a}) = 1$ and $T_{1} (ξ_{a}) = ξ_{a} > 1$ . If $T_{j} (ξ_{a}) > T_{j - 1} (ξ_{a}) > 0$ , then $T_{j + 1} (ξ_{a}) = 2 ξ_{a} T_{j} (ξ_{a}) - T_{j - 1} (ξ_{a}) > (2 ξ_{a} - 1) T_{j} (ξ_{a}) > T_{j} (ξ_{a}) .$ Induction proves $T_{k} (ξ_{a}) > 0$ , so the normalizing denominator is nonzero.

1.3F1F2inductionalgebra

The recurrence gives $T_{0} = 1$ of degree $0$ and $T_{1} = X$ of degree $1$ with leading coefficient $1$ . If $j \geq 1$ , $T_{j}$ has degree $j$ and leading coefficient $2^{j - 1}$ , and $T_{j - 1}$ has degree $j - 1$ (with $T_{0}$ having degree $0$ when $j = 1$ ), then $2 X T_{j}$ has degree $j + 1$ and leading coefficient $2^{j}$ , while subtracting $T_{j - 1}$ cannot change that highest-degree term. By [F1], induction gives $\deg T_{k} = k$ and leading coefficient $2^{k - 1}$ for every $k \geq 1$ .

2.1givenstep 1.1step 1.2step 1.3algebra∎

The affine map $ξ$ is increasing, has nonzero slope $2 / (b - c)$ , and sends $[c, b]$ onto $[- 1, 1]$ . For $k \geq 1$ , step 1.3 shows that $T_{k} (ξ (x))$ has degree $k$ ; step 1.2 shows division by $T_{k} (ξ_{a}) > 0$ preserves that degree. For $k = 0$ , $p_{0} = 1$ has degree $0$ . Step 1.1 bounds the numerator on $[c, b]$ by $1$ in absolute value and attains $1$ at $x = b$ , since $ξ (b) = 1$ . Since $ξ (a) = ξ_{a}$ , steps 1.2 and 1.3 give $p_{k} (a) = 1$ and prove the maximum formula.

Depends on

Used by

Lanczos largest Ritz values obey a Chebyshev start-angle bound, including degenerate branches Theorem

Dependency tree · two levels

12 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

Yousef Saad, Iterative Methods for Sparse Linear Systems, 2nd ed., §6.11.1, printed pp. 209–210 (standard reference, not scraped)
David Bindel, Matrix Computations (CS 6210), Cornell University, Fall 2012, Lectures 38–39 (standard reference, not scraped)