ExampleConstruction: AI-generatedVerification: AI-adaptedPipeline-generated

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.

Analytic and nonsmooth data have geometric and algebraic Chebyshev coefficient decay

Example

For a continuous $f$ on $[- 1, 1]$ , define its Chebyshev coefficients by $a_{0} (f) = \frac{1}{π} \int_{0}^{π} f (\cos θ) d θ, a_{n} (f) = \frac{2}{π} \int_{0}^{π} f (\cos θ) \cos (n θ) d θ (n \geq 1) .$ For the analytic function $f_{a} (x) = 1 / (2 - x)$ , these coefficients are $a_{0} = 1 / \sqrt{3}$ and $a_{n} = 2 (2 - \sqrt{3})^{n} / \sqrt{3}$ for $n \geq 1$ , a geometric decay. For the nonsmooth function $f_{s} (x) = ∣ x ∣$ , they are $a_{0} = 2 / π$ , $a_{2 m} = 4 (- 1)^{m - 1} / (π (4 m^{2} - 1))$ for $m \geq 1$ , and $a_{2 m + 1} = 0$ ; the nonzero coefficients decay algebraically like $m^{- 2}$ .

Facts & Assumptions

Given: The coefficient convention above and the two functions $f_{a}$ and $f_{s}$ .

[F1]

Chebyshev polynomials of the first and second kinds by their three-term recurrences and $T_{n} (\cos θ) = \cos (n θ)$ and $U_{n} (\cos θ) \sin θ = \sin ((n + 1) θ)$ for every $n \in N$ : $T_{n} (\cos θ) = \cos (n θ)$ .

[F2]

Arcsine-weighted inner product on the Chebyshev interval and Chebyshev polynomials are orthogonal for the arcsine weight: $⟨ T_{0}, T_{0} ⟩_{C} = π$ , $⟨ T_{n}, T_{n} ⟩_{C} = π / 2$ for $n \geq 1$ , and distinct modes are orthogonal.

[F3]

For $∣ r ∣ < 1$ the sequence $r^{k}$ is null, and for $∣ r ∣ > 1$ the sequence $∣ r ∣^{k}$ diverges to $+ \infty$ : $q^{m + 1} \to 0$ for a real $q$ with $0 < q < 1$ ; Conjugation is an involutive real-field automorphism, $z \overline{z} = ∣ z ∣^{2}$ , and modulus is definite, multiplicative, and subadditive gives complex modulus multiplicativity and the triangle inequality.

[F4]

Complex differentiability at a point, the complex derivative, holomorphic functions, and entire functions: a complex function is holomorphic on an open set when it is complex differentiable at every point there; $C = R [x] / (x^{2} + 1)$ is a field, every element is uniquely $a + b i$ , and every nonzero element has inverse $(a - b i) / (a^{2} + b^{2})$ supplies the complex field operations.

[F5]

The addition formulas for sine and cosine: $2 \cos u \cos v = \cos (u + v) + \cos (u - v)$ .

[F6]

The derivatives of sine and cosine are cosine and minus sine, The chain rule, in one line from Carathéodory: if $g$ is differentiable at $c$ and $f$ is differentiable at $g (c)$ , then $f \circ g$ is differentiable at $c$ with $(f \circ g)^{'} (c) = f^{'} (g (c)) g^{'} (c)$ , and The second fundamental theorem: if $G$ is differentiable on $[a, b]$ with $G^{'} = f$ and $f$ is integrable, then $\int_{a}^{b} f = G (b) - G (a)$ : cosine has antiderivative $\sin (k θ) / k$ for every nonzero integer $k$ .

[F7]

Quarter-turn values and shifts by pi/2 and pi and Signs, monotonicity intervals, and ranges of sine and cosine: $\sin (k π) = 0$ , $\sin ((2 m + 1) π / 2) = (- 1)^{m}$ , $\cos (k π) = (- 1)^{k}$ , and cosine is nonnegative on $[0, π / 2]$ and nonpositive on $[π / 2, π]$ .

[F8]

$\exp (x + i y) = e^{x} (\cos y + i \sin y)$ , $∣ \exp (x + i y) ∣ = e^{x}$ , and $e^{i π} + 1 = 0$ : $e^{i θ} = \cos θ + i \sin θ$ and $∣ e^{i θ} ∣ = 1$ for real $θ$ .

[F9]

The subtraction formulas for sine and cosine: $\cos (u - v) = \cos u \cos v + \sin u \sin v$ .

[F10]

Parity and the Pythagorean identity for sine and cosine: $\sin^{2} θ + \cos^{2} θ = 1$ .

[F11]

The derivative $f^{'} (c) = \lim_{x \to c} \frac{f (x) - f (c)}{x - c}$ of $f : A \to R$ at a point $c \in A$ that is a limit point of $A$ , and differentiability on a set: differentiability at a point is the existence of the two-sided difference-quotient limit.

[F12]

A continuous function on $[a, b]$ is Riemann integrable, by Heine-Cantor and Riemann's criterion and Integrable functions on $[a, b]$ form a set closed under sums and scalar multiples, and $\int_{a}^{b} (λ f + μ g) = λ \int_{a}^{b} f + μ \int_{a}^{b} g$ : continuous functions on a compact interval are Riemann integrable, and finite linear combinations may be integrated termwise.

[F13]

Uniformly close integrable functions have integrals differing by at most the interval length times their uniform error: integrable functions uniformly within $η$ on $[0, π]$ have integrals differing by at most $π η$ .

[F14]

A function differentiable at $c$ is continuous at $c$ makes sine and cosine continuous; A composite of continuous functions is continuous, with no side hypothesis of the kind the composition of limits needs and Sums, scalar multiples, products, absolute values, maxima, minima and quotients with nonvanishing denominator of continuous functions are continuous, as are constants, the identity and every polynomial function preserve continuity under the compositions, finite sums, products, and the nonvanishing denominator in this example. The absolute-value clause of Sums, scalar multiples, products, absolute values, maxima, minima and quotients with nonvanishing denominator of continuous functions are continuous, as are constants, the identity and every polynomial function makes $f_{s} (x) = ∣ x ∣$ continuous. Hence all coefficient integrands are continuous and [F12] makes them integrable.

[F15]

A real-analytic function on an open subset of $R$ is locally represented by a convergent real power series: a real function on an open set is real analytic if near each point it agrees with a convergent real power series centered at that point.

Proof

1.1givenF3F4F11F15algebra

The set $Ω = {z \in C : ∣ z ∣ < 3 / 2}$ is an open neighborhood of $[- 1, 1]$ and omits $2$ . For $z, z_{0} \in Ω$ with $z \neq z_{0}$ , $\frac{f_{a} (z) - f_{a} (z_{0})}{z - z_{0}} = \frac{1}{(2 - z) (2 - z_{0})} ⟶ \frac{1}{(2 - z_{0})^{2}} (z \to z_{0}) .$ Thus [F4] makes $f_{a}$ holomorphic on a neighborhood of the interval. To verify analyticity in the power-series sense as well, fix a real $c < 2$ and put $t = (x - c) / (2 - c)$ for $∣ x - c ∣ < (2 - c) / 2$ . Finite geometric summation gives $\frac{1}{2 - x} = \sum_{k = 0}^{M} \frac{(x - c)^{k}}{(2 - c)^{k + 1}} + \frac{t^{M + 1}}{(2 - c) (1 - t)}$ . Since $∣ t ∣ < 1 / 2$ , the remainder has absolute value at most $2^{- M} / (2 - c)$ , tending to zero by [F3]. The series therefore represents $f_{a}$ on a neighborhood of every $c < 2$ , establishing real analyticity on $(- \infty, 2)$ by [F15], in particular near $[- 1, 1]$ .

1.2givenF6F7F9F11F14algebra

The function $f_{s} (x) = ∣ x ∣$ is continuous by [F14] and is not differentiable at $0$ : for $h > 0$ its difference quotient is $1$ , while for $h < 0$ it is $- 1$ , so the two-sided limit in [F11] does not exist. By [F7], $∣ \cos θ ∣ = \cos θ$ on $[0, π / 2]$ and $∣ \cos θ ∣ = - \cos θ$ on $[π / 2, π]$ . The subtraction identity [F9] gives $\cos (n (π - θ)) = (- 1)^{n} \cos (n θ)$ , so reflection makes each odd coefficient integral its own negative. Therefore $a_{0} (f_{s}) = \frac{1}{π} \int_{0}^{π} ∣ \cos θ ∣ d θ = \frac{2}{π} .$ For odd $n$ , that reflection makes $a_{n} (f_{s}) = 0$ .

1.3F3F4F5F8F14algebrainduction

Put $q = 2 - \sqrt{3}$ . Then $0 < q < 1$ , $q^{- 1} = 2 + \sqrt{3}$ , $q + q^{- 1} = 4$ , and $1 - q^{2} = 2 \sqrt{3} q$ . By [F8], $z = q e^{i θ}$ has modulus $q$ . For $m \geq 1$ , put $S_{m} (z) = \sum_{n = 1}^{m} z^{n}$ . Multiplying the finite sum by $1 - z$ cancels consecutive terms and gives $(1 - z) S_{m} = z - z^{m + 1}$ . The triangle inequality in [F3] gives $∣ 1 - z ∣ \geq 1 - q > 0$ , so $∣ S_{m} (z) - \frac{z}{1 - z} ∣ = \frac{∣ z ∣^{m + 1}}{∣ 1 - z ∣} \leq \frac{q^{m + 1}}{1 - q} .$ Induction using the addition formulas in [F5] and Euler's identity in [F8] gives $z^{n} = q^{n} (\cos (n θ) + i \sin (n θ))$ . Thus $C_{m} (θ) : = 1 + 2 \sum_{n = 1}^{m} q^{n} \cos (n θ)$ , a continuous function by [F14], differs from $1 + 2 Re (z / (1 - z))$ by at most $2 q^{m + 1} / (1 - q)$ , uniformly for $θ \in [0, π]$ .

2.1F1F3F4F8F10F14step 1.3algebra

Multiplying numerator and denominator by $1 - q \cos θ + i q \sin θ$ and using [F10] gives $Re \frac{z}{1 - z} = \frac{q \cos θ - q^{2}}{1 - 2 q \cos θ + q^{2}} .$ Hence $1 + 2 Re \frac{z}{1 - z} = \frac{1 - q^{2}}{1 - 2 q \cos θ + q^{2}} = \frac{\sqrt{3}}{2 - \cos θ},$ because the denominator equals $2 q (2 - \cos θ)$ . By step 1.3, the continuous functions $C_{m} / \sqrt{3}$ satisfy $\sup_{0 \leq θ \leq π} ∣ \frac{C_{m} (θ)}{\sqrt{3}} - f_{a} (\cos θ) ∣ \leq η_{m} : = \frac{2 q^{m + 1}}{\sqrt{3} (1 - q)} ⟶ 0$ by [F3]. This also establishes the claimed convergent Chebyshev expansion through [F1].

3.1F1F2F7F12F13F14step 2.1algebra

Fix a coefficient index $n \geq 0$ . By [F14], the functions $f_{a} (\cos θ)$ , $C_{m} / \sqrt{3}$ , and their products with $\cos (n θ)$ are continuous; [F12] makes them integrable. Since $∣ \cos (n θ) ∣ \leq 1$ by [F7], [F13] bounds the corresponding coefficient differences by $η_{m}$ for index zero and by $2 η_{m}$ for positive indices. For every $m \geq n$ , finite integration and orthogonality [F2] give the coefficients of $C_{m} / \sqrt{3}$ as $1 / \sqrt{3}$ at zero and $2 q^{n} / \sqrt{3}$ at each $1 \leq n \leq m$ . Letting $m \to \infty$ therefore yields exactly the asserted coefficients of $f_{a}$ ; no interchange of an unbounded infinite sum and integral is assumed.

4.1givenF5F6F7algebra∎

For $m \geq 1$ , symmetry about $π / 2$ and [F5] give $\int_{0}^{π} ∣ \cos θ ∣ \cos (2 m θ) d θ = 2 \int_{0}^{π / 2} \cos θ \cos (2 m θ) d θ = \frac{2 (- 1)^{m - 1}}{4 m^{2} - 1},$ where the last equality follows by integrating $\frac{1}{2} [\cos ((2 m + 1) θ) + \cos ((2 m - 1) θ)]$ using [F6]–[F7]. Multiplying by $2 / π$ gives $a_{2 m} (f_{s}) = 4 (- 1)^{m - 1} / (π (4 m^{2} - 1))$ . This coefficient magnitude is asymptotic to $1 / (π m^{2})$ .

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

117 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

Jie Shen and Tao Tang, Spectral and High-Order Methods with Applications, §1.8 (standard reference, not scraped)
Lloyd N. Trefethen, Finite Difference and Spectral Methods for Ordinary and Partial Differential Equations, Ch. 8 (standard reference, not scraped)