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.

Weighted angular completeness

Statement

Assume the Axiom of Countable Choice (The Axiom of Countable Choice ( ${A C}_{ω}$ )). Let $P_{l}$ be the Legendre polynomials of Legendre Rodrigues equation and $w_{l m}$ the associated functions of Associated Legendre function normalization, and let $L^{2} = L^{2} ((- 1, 1), d t; C)$ with inner product linear in the first argument (The space $L^{p} (μ)$ as the quotient by null functions, Complex Lp classes and Euclidean test-function conventions). Then, for each fixed $m \in N$ :

(a) for every $l \geq m$ the polynomial $P_{l}^{(m)}$ has degree $l - m$ and nonzero leading coefficient, and for every $d \in N$ the polynomials $P_{m}^{(m)}, P_{m + 1}^{(m)}, \dots, P_{m + d}^{(m)}$ form a basis of the space of polynomial functions of degree at most $d$ on $[- 1, 1]$ ;

(b) the family $(w_{l m})_{l \geq m}$ has dense linear span in $L^{2}$ : if $f \in L^{2}$ satisfies $\int_{- 1}^{1} f (t) w_{l m} (t) d t = 0$ for every $l \geq m$ , then $f = 0$ almost everywhere; consequently the orthogonal family $(w_{l m})_{l \geq m}$ is complete in $L^{2}$ and its normalization $(w_{l m} / ∥ w_{l m} ∥_{2})_{l \geq m}$ is a Hilbert basis of $L^{2}$ , so every $f \in L^{2}$ has $f = \sum_{l \geq m} (\int_{- 1}^{1} f w_{l m} d t) ∥ w_{l m} ∥_{2}^{- 2} w_{l m}$ with the finite-subset-net convergence of Orthonormal families, complete orthonormal systems and Hilbert bases;

(c) for every fixed $m$ the orthogonal projection of $L^{2}$ onto the one-dimensional span of $w_{m m}$ is $f \mapsto ∥ w_{m m} ∥_{2}^{- 2} (\int_{- 1}^{1} f w_{m m} d t) w_{m m}$ , and $w_{m m} (t) = (- 1)^{m} \frac{(2 m)!}{2^{m} m!} (1 - t^{2})^{m / 2}$ .

Facts & Assumptions

Given: $m \in N$ ; the Legendre polynomials $P_{l}$ ; the functions $w_{l m}$ ; the complex Hilbert space $L^{2} ((- 1, 1), d t)$ .

[F1]

$P_{l}$ is a polynomial of degree $l$ with nonzero leading coefficient $a_{l} = \frac{(2 l)!}{2^{l} (l!)^{2}}$ (Legendre Rodrigues equation). Iterating the monomial derivative rule (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 factorial recursion (The factorial $n!$ and the falling factorial $n^{\underline{k}}$ , defined by recursion in $N$ ) gives, for $l \geq m$ , leading term $a_{l} l! / (l - m)! t^{l - m}$ in $P_{l}^{(m)}$ ; lower-degree terms either vanish or have smaller degree. Thus its degree is $l - m$ , and $P_{m}^{(m)} = a_{m} m!$ .

[F2]

$w_{l m} = (- 1)^{m} (1 - t^{2})^{m / 2} P_{l}^{(m)}$ is continuous on $[- 1, 1]$ , the family $(w_{l m})_{l \geq m}$ is orthogonal in $L^{2}$ , and $∥ w_{l m} ∥_{2}^{2} = \int_{- 1}^{1} w_{l m}^{2} d t \in (0, \infty)$ (Associated Legendre function normalization).

[F3]

The real polynomial functions are uniformly dense in the real continuous functions on $[- 1, 1]$ : for every continuous $g : [- 1, 1] \to R$ and every $ε > 0$ there is a polynomial $p$ with $\sup_{[- 1, 1]} ∣ g - p ∣ < ε$ (Real Stone–Weierstrass theorem for compact Hausdorff spaces).

[F4]

Under Countable Choice, for every bounded interval $(a, b)$ the complex continuous functions on $[a, b]$ are dense in complex $L^{p} ((a, b))$ for $1 \leq p < + \infty$ , in particular in $L^{2}$ (Continuous functions are dense in $L^{p}$ of finite tori and of bounded intervals (2)). For continuous $g$ , integrating $∣ g (t) ∣^{2} \leq ∥ g ∥_{\infty}^{2}$ over $(a, b)$ gives $∥ g ∥_{2}^{2} \leq (b - a) ∥ g ∥_{\infty}^{2}$ , hence $∥ g ∥_{2} \leq \sqrt{b - a} ∥ g ∥_{\infty}$ by the defining $L^{2}$ norm (The space $L^{p} (μ)$ as the quotient by null functions, Complex Lp classes and Euclidean test-function conventions).

[F5]

$∥ f g ∥_{1} \leq ∥ f ∥_{2} ∥ g ∥_{2}$ and $∣ \int f \overline{g} ∣ \leq ∥ f ∥_{2} ∥ g ∥_{2}$ in $L^{2}$ (Cauchy-Schwarz inequality for $L^{2}$ , Complex Lp classes and Euclidean test-function conventions).

[F6]

For a family that is orthonormal and complete in a Hilbert space, the expansion, Parseval identity and coefficient formulas hold with finite-subset-net convergence (Orthonormal families, complete orthonormal systems and Hilbert bases, Parseval equivalences for an orthonormal family).

Proof

1.1F1algebra

[(a)] By [F1], $P_{l}^{(m)}$ has degree $l - m$ and nonzero leading coefficient for each $l \geq m$ . Hence in the ordered list $P_{m}^{(m)}, P_{m + 1}^{(m)}, \dots, P_{m + d}^{(m)}$ the $j$ -th polynomial has degree $j$ , $0 \leq j \leq d$ : the leading-degree matrix is triangular with nonzero diagonal, so the polynomials are linearly independent; they are $d + 1$ vectors in the $(d + 1)$ -dimensional space of polynomials of degree at most $d$ , hence a basis.

2.1step 1.1F2algebra

[(b), first reduction] Let $f \in L^{2}$ satisfy $\int_{- 1}^{1} f w_{l m} d t = 0$ for all $l \geq m$ , and put $g (t) : = f (t) (1 - t^{2})^{m / 2}$ . Since $t \mapsto (1 - t^{2})^{m / 2}$ is continuous and bounded on $[- 1, 1]$ , $g \in L^{2}$ and $∥ g ∥_{2} \leq ∥ f ∥_{2}$ ; moreover for every $l \geq m$ , $\int_{- 1}^{1} g P_{l}^{(m)} d t = (- 1)^{m} \int_{- 1}^{1} f w_{l m} d t = 0$ by [F2]. By step 1.1, every polynomial $q$ of degree at most $d$ is a linear combination of $P_{m}^{(m)}, \dots, P_{m + d}^{(m)}$ , so $\int_{- 1}^{1} g q d t = 0$ for every polynomial $q$ .

3.1step 2.1F3F4F5algebra

[(b), density step] Polynomials are dense in $L^{2} ((- 1, 1))$ : given $φ \in L^{2}$ and $ε > 0$ , [F4] supplies a continuous $h$ on $[- 1, 1]$ with $∥ φ - h ∥_{2} < ε / 2$ , and apply [F3] separately to the real and imaginary parts of $h$ , obtaining real polynomials $p_{1}, p_{2}$ whose respective uniform errors are below $ε / (4 \sqrt{2})$ , and put $p = p_{1} + i p_{2}$ ; then $\sup_{[- 1, 1]} ∣ h - p ∣ < ε / (2 \sqrt{2})$ , so $∥ h - p ∥_{2} < ε / 2$ by [F4] (applied to the interval length $2$ ), whence $∥ φ - p ∥_{2} < ε$ . Applying this to the complex-valued $g$ componentwise (real and imaginary parts) gives polynomials $q_{j}$ with $∥ g - q_{j} ∥_{2} \to 0$ ; since $\int g q = 0$ for all polynomials, Cauchy–Schwarz [F5] gives $∥ g ∥_{2}^{2} = \int g \overline{g} = \lim_{j} \int g \overline{q_{j}} = 0$ , so $g = 0$ almost everywhere. On $(- 1, 1)$ the factor $(1 - t^{2})^{m / 2}$ is strictly positive, so $f = g / (1 - t^{2})^{m / 2} = 0$ almost everywhere.

4.1step 3.1F2F6algebra

[(b), completeness and expansion] By [F2] the family $(w_{l m})_{l \geq m}$ is orthogonal with all norms nonzero, so $(w_{l m} / ∥ w_{l m} ∥_{2})_{l \geq m}$ is orthonormal; if a vector of $L^{2}$ is orthogonal to the whole family, it is orthogonal to every $w_{l m}$ and vanishes by step 3.1, so the orthonormal family is complete in the sense of [F6]; the expansion, normalization and coefficient formulas follow from [F6].

5.1step 4.1F1F2F5algebra∎

[(c)] The orthogonal projection onto the span of a unit vector $u$ is $x \mapsto ⟨ x, u ⟩ u$ , and for an unnormalized nonzero vector $w$ it is $x \mapsto ∥ w ∥_{2}^{- 2} ⟨ x, w ⟩ w$ ; with $w = w_{m m}$ and the inner product linear in the first argument this is the displayed formula. Indeed its value lies in the span of $w$ , and its residual has zero inner product with $w$ , uniquely determining the orthogonal projection; Cauchy–Schwarz bounds its norm by $∥ x ∥_{2}$ . The explicit value of $w_{m m}$ follows from $P_{m}^{(m)} = \frac{(2 m)!}{2^{m} m!}$ (the leading coefficient of $P_{m}$ times $m!$ ) inserted into the definition of $w_{l m}$ .

Weighted angular completeness

Statement

Facts & Assumptions

Proof

Depends on

Dependency tree · 2 levels

Sources