Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck pass
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-root and Lobatto interpolation norms have logarithmic upper bounds

Statement

For n≥1, let ΛnR be the operator norm of interpolation at the n+1 roots of Tn+1, and let ΛnL be the operator norm at the n+1 Chebyshev–Lobatto nodes. With the conventions in Best uniform polynomial error and Chebyshev interpolation operators, ΛnR≤Clog⁡(n+1),ΛnL≤Clog⁡(n+1),C:=4+π+4log⁡2. Here log⁡ is the natural logarithm of The natural logarithm as the inverse of the exponential function. For n=0, both one-node operators have norm 1; the logarithmic estimate is stated for n≥1.

Facts & Assumptions

Given: An integer n≥1, θ∈[0,π], and either angular node family.

[F1]

Best uniform polynomial error and Chebyshev interpolation operators defines Inσ, Λnσ, and the equally spaced root and Lobatto angles.

[F2]

Chebyshev cardinal interpolation reproduces polynomials and its norm is the cardinal sum: Λnσ=sup⁡x∈[−1,1]∑j∣ℓj,nσ(x)∣.

[F3]

Trigonometric formulas for Chebyshev cardinal polynomials: for roots, ∣ℓj(cos⁡θ)∣=∣cos⁡((n+1)θ)∣sin⁡θj/((n+1)∣cos⁡θ−cos⁡θj∣); for Lobatto nodes, ∣ℓj(cos⁡θ)∣=cj∣sin⁡θ sin⁡(nθ)∣/(n∣cos⁡θ−cos⁡θj∣), with cj≤1.

[F4]

Sine chord and Lipschitz bounds: sin⁡u≥2u/π for 0≤u≤π/2, and ∣sin⁡u−sin⁡v∣≤∣u−v∣ for all real u,v.

[F5]

The addition formulas for sine and cosine, The subtraction formulas for sine and cosine, Signs, monotonicity intervals, and ranges of sine and cosine, and Quarter-turn values and shifts by pi/2 and pi: the addition/subtraction formulas give cos⁡θ−cos⁡ϕ=−2sin⁡((θ+ϕ)/2)sin⁡((θ−ϕ)/2) and sin⁡(s±t)=sin⁡scos⁡t±cos⁡ssin⁡t; on [0,π], sine is nonnegative, increasing up to π/2, and satisfies sin⁡(π−s)=sin⁡s, while ∣cos⁡u∣≤1 for every real u.

[F7]

The natural logarithm as the inverse of the exponential function: log⁡ is the natural logarithm; The canonical natural ι(n)=n⋅1F of a field and Canonical naturals are positive and strictly increasing: natural indices in real expressions use their canonical images, and positive natural indices have positive real image.

[F8]

Cosine is continuous on [0,π] by The derivatives of sine and cosine are cosine and minus sine and A function differentiable at c is continuous at c. Its endpoint values are cos⁡0=1 and cos⁡π=−1 by Quarter-turn values and shifts by pi/2 and pi, and π>0 by Pi as twice the smallest positive zero of cosine. The intermediate value theorem Intermediate value theorem, by bisection with a canonical left-half rule: a continuous function on [a,b] takes every value between f(a) and f(b) therefore shows that every value in [−1,1] is cos⁡θ for some θ∈[0,π]. Conversely, cosine has range [−1,1] by Signs, monotonicity intervals, and ranges of sine and cosine, so cos⁡([0,π])=[−1,1].

Proof

1.1givenF1choosealgebra

In either angular grid the spacing is h=π/(n+1) for roots and h=π/n for Lobatto nodes. Choose a nearest grid angle θk and put dj=∣θ−θj∣. Then dk≤h/2; if ∣j−k∣=r≥1, the triangle inequality gives dj≥rh−dk≥(r−12)h. At most two indices occur for each r.

2.1givenF4F5step 1.1algebra

For θ≠θj, put s=(θ+θj)/2 and d=θ−θj. Since the two angles lie in [0,π], ∣d∣/2≤min⁡(s,π−s). The addition/subtraction formulas in [F5] give sin⁡θj,sin⁡θ≤sin⁡s+∣sin⁡(d/2)∣; the monotonicity and supplementary identity in [F5] then give ∣sin⁡(d/2)∣≤sin⁡s, so each numerator is at most 2sin⁡s. Those same formulas give ∣cos⁡θ−cos⁡θj∣=2sin⁡ssin⁡(∣d∣/2), and [F4] gives sin⁡(∣d∣/2)≥∣d∣/π. Thus both ratios sin⁡θj/∣cos⁡θ−cos⁡θj∣ and sin⁡θ/∣cos⁡θ−cos⁡θj∣ are at most π/dj.

3.1givenF3F4F5step 1.1step 2.1algebra

For roots, [F3] and step 2.1 give ∣ℓj,nR(cos⁡θ)∣≤π∣cos⁡((n+1)θ)∣/((n+1)dj). At the nearest node k, cos⁡((n+1)θk)=0, and the cosine addition formula plus [F4] gives ∣cos⁡((n+1)θ)∣≤(n+1)dk, so its term is at most π. For other nodes use ∣cos⁡((n+1)θ)∣≤1 and step 1.1; summing over at most two nodes per distance rank yields ∑j∣ℓj,nR(cos⁡θ)∣≤π+2∑r=1n1/(r−12). At a node the cardinal sum is 1.

3.2givenF3F4F5step 1.1step 2.1algebra

For Lobatto nodes, [F3] and step 2.1 give ∣ℓj,nL(cos⁡θ)∣≤πcj∣sin⁡(nθ)∣/(ndj). At the nearest node k, sin⁡(nθk)=0, so [F4] gives ∣sin⁡(nθ)∣≤ndk and its term is at most π because ck≤1. For other nodes use ∣sin⁡(nθ)∣≤1 and step 1.1; summing over at most two nodes per distance rank yields ∑j∣ℓj,nL(cos⁡θ)∣≤π+2∑r=1n1/(r−12). At a node the cardinal sum is 1.

4.1givenF2F6F7F8step 3.1step 3.2algebra∎

Since 1/(r−12)≤2/r, the shifted sum is at most 2Hn, where Hn=∑r=1n1/r. For r≥2, 1/r≤∫r−1rdt/t, so [F6] gives Hn≤1+log⁡n. Positivity of the real image of n is [F7], so these logarithms are defined. The integral formula also gives 0=log⁡1≤log⁡n≤log⁡(n+1) and log⁡2≤log⁡(n+1) by integrating 1/t>0 over [1,n], [n,n+1], and [2,n+1]. Since log⁡2=∫12dt/t>0 and π>0, we have C>0 and 1<Clog⁡2. Thus both sums are at most π+4+4log⁡n≤(4+(π+4)/log⁡2)log⁡(n+1). By [F8], the angular supremum is over exactly [−1,1]; taking it and using [F2] proves both bounds. At n=0, each one-node operator has norm 1 directly.

Depends on

Used by

Dependency tree · two levels

71 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