LemmaStatement: Literature-sourcedProof: AI-generatedPipeline-generatedprecheck passjudge 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.

Chebyshev bounds and endpoint derivatives used by stabilized Runge–Kutta methods

Statement

Let $T_{n}$ and $U_{n}$ be the real evaluation functions of the Chebyshev polynomials defined by Chebyshev polynomials of the first and second kinds by their three-term recurrences. For every natural $n$ ,

$∣ T_{n} (x) ∣ \leq 1, ∣ U_{n} (x) ∣ \leq n + 1 (- 1 \leq x \leq 1),$

and for $n \geq 1$ , $∣ T_{n} (x) ∣ > 1$ whenever $∣ x ∣ > 1$ . Also,

$T_{n} (1) = 1, T_{n} (- 1) = (- 1)^{n}, U_{n} (1) = n + 1, U_{n} (- 1) = (- 1)^{n} (n + 1) .$

For every natural $n \geq 1$ , $T_{n}$ has degree $n$ and leading coefficient $2^{n - 1}$ , while $U_{n}$ has degree $n$ and leading coefficient $2^{n}$ . This degree and leading-coefficient assertion is exactly the content of Degrees and leading coefficients of the Chebyshev polynomials; that item does not assert an extremum bound.

The evaluation functions are twice differentiable at $1$ , with

$T_{n}^{'} (1) = n^{2}, T_{n}^{''} (1) = \frac{n^{2} (n^{2} - 1)}{3} .$

Here each natural number in a real formula denotes its canonical real image (The canonical natural $ι (n) = n \cdot 1_{F}$ of a field), and powers use Integer powers $a^{m}$ .

Facts & Assumptions

Given: A natural number $n$ , the Chebyshev polynomial recurrences, and a real $x \in [- 1, 1]$ when an interval bound is used.

[F1]

Chebyshev polynomials of the first and second kinds by their three-term recurrences: $T_{0} = 1$ , $T_{1} = X$ , $T_{n + 2} = 2 X T_{n + 1} - T_{n}$ ; $U_{0} = 1$ , $U_{1} = 2 X$ , and $U_{n + 2} = 2 X U_{n + 1} - U_{n}$ .

[F2]

$T_{n} (\cos θ) = \cos (n θ)$ and $U_{n} (\cos θ) \sin θ = \sin ((n + 1) θ)$ for every $n \in N$ : for real $θ$ , $T_{n} (\cos θ) = \cos (n θ)$ and $U_{n} (\cos θ) \sin θ = \sin ((n + 1) θ)$ .

[F3]

Signs, monotonicity intervals, and ranges of sine and cosine and Parity and the Pythagorean identity for sine and cosine: every $x \in [- 1, 1]$ is $\cos θ$ for some real $θ$ , and $∣ \sin θ ∣, ∣ \cos θ ∣ \leq 1$ for every real $θ$ .

[F4]

The zero sets of sine and cosine and the least positive common period 2 pi and Quarter-turn values and shifts by pi/2 and pi: if $\sin θ = 0$ , then $θ = m π$ for an integer $m$ , and the cosine shift identities give $\cos θ \in {- 1, 1}$ .

[F5]

The addition formulas for sine and cosine and The triangle inequality: $\sin ((m + 1) θ) = \sin (m θ) \cos θ + \cos (m θ) \sin θ$ , and $∣ a + b ∣ \leq ∣ a ∣ + ∣ b ∣$ .

[F6]

Degrees and leading coefficients of the Chebyshev polynomials: for $n \geq 1$ , $T_{n}$ has degree $n$ and leading coefficient $2^{n - 1}$ , and $U_{n}$ has degree $n$ and leading coefficient $2^{n}$ . This fact supplies degree only, not an extremum estimate.

[F7]

Higher derivatives and the classes $C^{k}$ and $C^{\infty}$ , Evaluation and roots of a polynomial in a commutative target ring, For a natural $n \geq 1$ the function $x \mapsto x^{n}$ is differentiable everywhere with derivative $ι (n) x^{n - 1}$ ; for $n = 0$ it is the constant $1$ , with derivative $0$ ; for a natural $n \geq 1$ the function $x \mapsto x^{- n}$ is differentiable at every $x \neq 0$ with derivative $- ι (n) x^{- n - 1}$ ; consequently every polynomial function is differentiable at every real, with the derivative computed term by term, and Sums, scalar multiples, products and quotients: $(f + g)^{'} (c) = f^{'} (c) + g^{'} (c)$ , $(α f)^{'} (c) = α f^{'} (c)$ , $(f g)^{'} (c) = f^{'} (c) g (c) + f (c) g^{'} (c)$ , and $(f / g)^{'} (c) = (f^{'} (c) g (c) - f (c) g^{'} (c)) / g (c)^{2}$ when $g (c) \neq 0$ : iterated real derivatives are defined recursively; polynomial evaluation gives the functions $T_{n} (x)$ ; $X^{'} = 1$ , $1^{'} = 0$ , and sums and products of differentiable functions obey their derivative rules.

[F8]

The principle of mathematical induction: a property true at $0$ and inherited by successors holds for every natural number.

Proof

1.1F1F8inductionalgebra

The recurrences [F1] give $T_{n} (1) = 1$ and $T_{n} (- 1) = (- 1)^{n}$ by induction from $T_{0}, T_{1}$ : the successor substitution is $2 (- 1) (- 1)^{n + 1} - (- 1)^{n} = (- 1)^{n + 2}$ . They give $U_{n} (1) = n + 1$ and $U_{n} (- 1) = (- 1)^{n} (n + 1)$ , since the bases hold at $n = 0, 1$ and the successor substitutions are $2 (n + 2) - (n + 1) = n + 3$ and $- 2 (- 1)^{n + 1} (n + 2) - (- 1)^{n} (n + 1) = (- 1)^{n + 2} (n + 3)$ .

1.2F3F5F8baseihinductionalgebra

Fix $θ \in R$ . For $m = 0$ , $∣ \sin ((m + 1) θ) ∣ \leq (m + 1) ∣ \sin θ ∣$ is equality. If it holds at $m$ , then [F5] and [F3] give $∣ \sin ((m + 2) θ) ∣ \leq ∣ \sin ((m + 1) θ) ∣ ∣ \cos θ ∣ + ∣ \cos ((m + 1) θ) ∣ ∣ \sin θ ∣ \leq (m + 2) ∣ \sin θ ∣$ . Induction [F8] proves this inequality for every natural $m$ .

1.3F1F8inductionalgebra

For $x > 1$ , induction in the recurrence [F1] gives $T_{1} (x) > T_{0} (x) = 1$ and, whenever $T_{n + 1} (x) > T_{n} (x) \geq 1$ , $T_{n + 2} (x) - T_{n + 1} (x) = (2 x - 1) T_{n + 1} (x) - T_{n} (x) \geq 2 (x - 1) T_{n + 1} (x) > 0.$ Thus $T_{n} (x) > 1$ for every $n \geq 1$ . The recurrence also gives $T_{n} (- x) = (- 1)^{n} T_{n} (x)$ : the identity holds at $n = 0, 1$ , and if it holds at $n, n + 1$ , then $T_{n + 2} (- x) = 2 (- x) (- 1)^{n + 1} T_{n + 1} (x) - (- 1)^{n} T_{n} (x) = (- 1)^{n + 2} (2 x T_{n + 1} (x) - T_{n} (x)) = (- 1)^{n + 2} T_{n + 2} (x)$ . Applying the positive case to $- x > 1$ proves $∣ T_{n} (x) ∣ > 1$ when $x < - 1$ .

1.4F1F7F8baseihinduction

Each $T_{n}$ is twice differentiable as a real polynomial evaluation function: $T_{0}, T_{1}$ are, and if $T_{n}, T_{n + 1}$ are twice differentiable, [F1] and [F7] make $T_{n + 2} = 2 X T_{n + 1} - T_{n}$ twice differentiable. Thus the derivative recurrences below are defined for every $n$ .

2.1F2F3F4step 1.1step 1.2choosealgebra

Let $x \in [- 1, 1]$ and choose $θ$ with $x = \cos θ$ by [F3]. If $\sin θ \neq 0$ , [F2] and step 1.2 give $∣ U_{n} (x) ∣ = ∣ \sin ((n + 1) θ) ∣ / ∣ \sin θ ∣ \leq n + 1$ . If $\sin θ = 0$ , [F4] gives $x = \cos θ \in {- 1, 1}$ , so step 1.1 gives the same bound. Also [F2] and [F3] give $∣ T_{n} (x) ∣ = ∣ \cos (n θ) ∣ \leq 1$ .

2.2F1F7F8step 1.1step 1.4inductionalgebra

Put $p_{n} : = T_{n}^{'} (1)$ . Differentiating [F1] once by [F7] and using $T_{n} (1) = 1$ gives $p_{0} = 0$ , $p_{1} = 1$ , and $p_{n + 2} = 2 + 2 p_{n + 1} - p_{n}$ . The values $p_{n} = n^{2}$ satisfy the bases and recurrence because $2 + 2 (n + 1)^{2} - n^{2} = (n + 2)^{2}$ ; induction gives $T_{n}^{'} (1) = n^{2}$ .

3.1F1F6baseinductionalgebrastep 2.1

To supply the consecutive base indices needed by the recurrence, [F1] gives $T_{0} = U_{0} = 1$ , each of degree $0$ and leading coefficient $1$ , and $T_{1} = X$ , $U_{1} = 2 X$ , of degree $1$ and leading coefficients $1$ and $2$ . The recurrence at index $0$ gives $T_{2} = 2 X^{2} - 1$ and $U_{2} = 4 X^{2} - 1$ , of degree $2$ and leading coefficients $2$ and $4$ . Thus the formulas in [F6] hold at indices $1$ and $2$ . Now suppose they hold at indices $n$ and $n + 1$ for some $n \geq 1$ . In $T_{n + 2} = 2 X T_{n + 1} - T_{n}$ , the first term has degree $n + 2$ and leading coefficient $2 \cdot 2^{n} = 2^{n + 1}$ , while the subtracted term has degree $n$ ; hence no leading-term cancellation occurs. In $U_{n + 2} = 2 X U_{n + 1} - U_{n}$ , the first term has degree $n + 2$ and leading coefficient $2 \cdot 2^{n + 1} = 2^{n + 2}$ , while the subtracted term has degree $n$ . Induction starting with indices $1$ and $2$ gives the formulas for every index $n \geq 1$ , agreeing with [F6]. No extremum claim is taken from that source item; the interval inequalities in the Statement were proved in step 2.1.

4.1F1F7F8step 1.4step 2.2inductiondischarge-inductionalgebra∎

Put $q_{n} : = T_{n}^{''} (1)$ . Differentiating [F1] twice by [F7] gives $q_{0} = q_{1} = 0$ and $q_{n + 2} = 4 p_{n + 1} + 2 q_{n + 1} - q_{n}$ . The values $q_{n} = n^{2} (n^{2} - 1) / 3$ satisfy the bases and, using step 2.2, the recurrence since $4 (n + 1)^{2} + \frac{2 (n + 1)^{2} ((n + 1)^{2} - 1) - n^{2} (n^{2} - 1)}{3} = \frac{(n + 2)^{2} ((n + 2)^{2} - 1)}{3} .$ Induction proves the stated second-derivative formula.

Depends on

Used by

Dependency tree · two levels

56 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

B.P. Sommeijer, L.F. Shampine, and J.G. Verwer, RKC: An explicit solver for parabolic PDEs, Section 2 (standard reference, not scraped)
Ibrahim Almuslimani and Gilles Vilmart, Explicit Stabilized Integrators for Stiff Optimal Control Problems, Section 2.2 (standard reference, not scraped)