TheoremStatement: AI-adaptedProof: 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.

Legendre weighted projection has its spectral-Sobolev rate

Statement

Let $s \geq 0$ , $N \geq 0$ , and $u = \sum_{n \geq 0} c_{n} P_{n} \in H_{L}^{s}$ from Legendre weighted spectral-Sobolev scale and projection. Then

∥ u - Π_{N} u ∥_{L_{L}^{2}} \leq (1 + (N + 1) (N + 2))^{- s / 2} ∥ u ∥_{H_{L}^{s}} .

Facts & Assumptions

Given: A real $s \geq 0$ , an integer $N \geq 0$ , and a coefficient sequence in $H_{L}^{s}$ .

[F1]

Legendre weighted spectral-Sobolev scale and projection: $Π_{N} u = \sum_{n = 0}^{N} c_{n} P_{n}$ and the $H_{L}^{s}$ coefficient weight is $(1 + n (n + 1))^{s} 2 / (2 n + 1)$ ; its spectral factor is nondecreasing in $n$ for $s \geq 0$ .

[F2]

Legendre polynomials have explicit norms and weighted derivative orthogonality: $\int_{- 1}^{1} P_{n} P_{m} = 2 δ_{m n} / (2 n + 1)$ .

Proof

1.1F1F2algebra

For a finite Legendre sum, [F1] gives $u - Π_{N} u = \sum_{n > N} c_{n} P_{n}$ . Orthogonality [F2] therefore gives $∥ u - Π_{N} u ∥_{L_{L}^{2}}^{2} = \sum_{n > N} \frac{2}{2 n + 1} ∣ c_{n} ∣^{2} .$ For every $n > N$ , $1 + n (n + 1) \geq 1 + (N + 1) (N + 2)$ ; multiplying each term by the inverse weight gives the stated squared bound for finite sums.

2.1F1step 1.1algebra∎

Finite sums are dense in the completion defining $H_{L}^{s}$ . The truncation $Π_{N}$ is contractive in both the coefficient norm and the $s = 0$ norm, so the finite-sum inequality passes to the limit along any Cauchy sequence of finite sums. Taking square roots proves the claimed estimate for every $u \in H_{L}^{s}$ .

Depends on

Used by

Integrated Legendre projection gives an explicit p-rate in H1 Theorem

Dependency tree · two levels

13 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, Ch. 3 (standard reference, not scraped)
Lloyd N. Trefethen, Finite Difference and Spectral Methods for Ordinary and Partial Differential Equations, Ch. 8 (standard reference, not scraped)