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.

Associated Legendre function normalization

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 for $l \in N$ and $0 \leq m \leq l$ define the function $w_{l m} : (- 1, 1) \to R$ by

$w_{l m} (t) : = (- 1)^{m} (1 - t^{2})^{m / 2} \frac{d^{m}}{d t^{m}} P_{l} (t),$

where $(1 - t^{2})^{1 / 2} > 0$ denotes the nonnegative square root. Let $σ$ be the polar surface measure on $S^{2}$ and let the angle coordinates be $Φ (θ, φ) = (\sin θ \cos φ, \sin θ \sin φ, \cos θ)$ (Sphere integrals in angle coordinates, The polar surface set function on the unit sphere). The image of $Φ$ is $S^{2} ∖ C$ , where $C : = {(x, 0, z) \in S^{2} : x \geq 0}$ ; $C$ is closed and $σ (C) = 0$ by applying the integral identity of Sphere integrals in angle coordinates to its indicator. For $l \geq m \geq 0$ , define the representative ${\tilde{Y}}_{l m} : S^{2} \to C$ on $S^{2} ∖ C$ by ${\tilde{Y}}_{l m} (Φ (θ, φ)) : = b_{l m} w_{l m} (\cos θ) \frac{e^{i m φ}}{\sqrt{2 π}},$ and on the cut $C$ by ${\tilde{Y}}_{l m} (\sin θ, 0, \cos θ) : = b_{l m} w_{l m} (\cos θ) / \sqrt{2 π} (0 \leq θ \leq π) .$ The limits at $φ = 0$ and $2 π$ agree because $m$ is an integer, and the endpoint values of $w_{l m}$ from (a) give the limits at the poles; hence ${\tilde{Y}}_{l m}$ is continuous. For $1 \leq m \leq l$ set ${\tilde{Y}}_{l, - m} : = (- 1)^{m} \overline{{\tilde{Y}}_{l m}}$ , and write $Y_{l m}$ for the class of ${\tilde{Y}}_{l m}$ in $L^{2} (S^{2}, σ; C)$ . Then:

(a) each $w_{l m}$ extends continuously to $[- 1, 1]$ , with $w_{l m} (\pm 1) = 0$ when $m \geq 1$ , and on $(- 1, 1)$ it satisfies the associated Legendre equation $- ((1 - t^{2}) w_{l m}^{'})^{'} + \frac{m^{2}}{1 - t^{2}} w_{l m} = l (l + 1) w_{l m} (- 1 < t < 1),$ equivalently $(1 - t^{2}) w_{l m}^{''} - 2 t w_{l m}^{'} + [l (l + 1) - \frac{m^{2}}{1 - t^{2}}] w_{l m} = 0$ ;

(b) for fixed $m \geq 0$ the functions $w_{l m}$ , $l \geq m$ , are pairwise orthogonal in $L^{2} ((- 1, 1), d t)$ : $\int_{- 1}^{1} w_{l m} w_{k m} d t = 0$ for $k \neq l$ ; moreover $0 < \int_{- 1}^{1} w_{l m}^{2} d t < + \infty$ ;

(c) with $b_{l m} : = (\int_{- 1}^{1} w_{l m}^{2} d t)^{- 1 / 2} > 0$ and the representatives just defined, one has $∣ Y_{l, - m} ∣ = ∣ Y_{l m} ∣$ and $\overline{Y_{l m}} = (- 1)^{m} Y_{l, - m}$ for all $l$ and all $m$ with $∣ m ∣ \leq l$ ;

(d) the family ${Y_{l m} : l \geq 0, - l \leq m \leq l}$ is orthonormal in $L^{2} (S^{2}, σ; C)$ (Real and complex inner product spaces, with the inner product linear in the first argument, The space $L^{p} (μ)$ as the quotient by null functions): for all $(l, m) \neq (l^{'}, m^{'})$ with $∣ m ∣ \leq l$ , $∣ m^{'} ∣ \leq l^{'}$ , the integral $\int_{S^{2}} Y_{l m} \overline{Y_{l^{'} m^{'}}} d σ$ equals $0$ , and it equals $1$ when $(l, m) = (l^{'}, m^{'})$ ;

(e) $w_{l 0} = P_{l}$ , and $w_{l l} (t) = (- 1)^{l} \frac{(2 l)!}{2^{l} l!} (1 - t^{2})^{l / 2}$ .

The functions $Y_{l m}$ are complex-valued $L^{2}$ -functions on the sphere; no physical interpretation as angular momentum eigenfunctions or spherical harmonics of an atom is asserted.

Facts & Assumptions

Given: the Legendre polynomials $P_{l}$ ; integers $l \geq 0$ , $0 \leq m \leq l$ ; the functions $w_{l m}$ ; the measure $σ$ and the parametrisation $Φ$ ; the constants $b_{l m}$ and functions $Y_{l m}$ .

[F1]

$P_{l}$ satisfies $(1 - t^{2}) P_{l}^{''} - 2 t P_{l}^{'} + l (l + 1) P_{l} = 0$ on $R$ , is a polynomial of degree $l$ , and $P_{l}^{(m)}$ is therefore the polynomial function of a degree- $(l - m)$ polynomial (Legendre Rodrigues equation).

[F2]

The general Leibniz rule and the algebra of derivatives compute the derivatives of products; the chain rule computes derivatives of composites (The general Leibniz rule for the $n$ -th derivative of a product, 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$ , 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)$ ).

[F3]

Sphere integrals in angle coordinates: for Borel $F \geq 0$ , $\int_{S^{2}} F d σ = \int_{(0, π) \times (0, 2 π)} F (Φ (θ, φ)) \sin θ d (θ, φ)$ , and the complex $L^{1}$ version; $σ (S^{2}) = 4 π$ (Sphere integrals in angle coordinates).

[F4]

Characters of the circle: $\int_{0}^{2 π} e^{i k φ} d φ = 2 π$ if $k = 0$ and $= 0$ for every nonzero $k \in Z$ (The trigonometric characters are orthonormal in $L^{2}$ of the torus, The complex exponential by its power series).

[F5]

A continuous real function on the compact interval $[- 1, 1]$ is (Riemann and Lebesgue) integrable; products of continuous functions are continuous, and $\int_{- 1}^{1} g > 0$ for a continuous $g \geq 0$ that is not identically zero (A continuous function on $[a, b]$ is Riemann integrable, by Heine-Cantor and Riemann's criterion, Complex Lp classes and Euclidean test-function conventions).

[F6]

If $G : [a, b] \to R$ is differentiable at every point of $[a, b]$ as a function on $[a, b]$ (with one-sided derivatives at $a, b$ ) and $G^{'}$ is integrable on $[a, b]$ , then $\int_{a}^{b} G^{'} = G (b) - G (a)$ (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)$ ).

[F7]

For $f, g \in L^{2}$ the product $f \overline{g}$ is in $L^{1}$ with $\int ∣ f \overline{g} ∣ \leq ∥ f ∥_{2} ∥ g ∥_{2}$ ; the inner product in $L^{2} (S^{2}, σ; C)$ is linear in the first argument; conjugation satisfies $\overline{z w} = \overline{z} \overline{w}$ and $∣ z ∣^{2} = z \overline{z}$ (Cauchy-Schwarz inequality for $L^{2}$ , Real and complex inner product spaces, with the inner product linear in the first argument, Conjugation is an involutive real-field automorphism, $z \overline{z} = ∣ z ∣^{2}$ , and modulus is definite, multiplicative, and subadditive, Complex Lp classes and Euclidean test-function conventions).

[F8]

For the given $0 \leq m \leq l$ , $d^{m} P_{l} / d t^{m}$ is a polynomial of degree $l - m$ with nonzero leading coefficient, so $w_{l m}$ is not the zero function on $(- 1, 1)$ , because $(1 - t^{2})^{m / 2} > 0$ there (Legendre Rodrigues equation, The factorial $n!$ and the falling factorial $n^{\underline{k}}$ , defined by recursion in $N$ ).

[F9]

If $G : [a, b] \to R$ is continuous on $[a, b]$ and differentiable at every point of $(a, b)$ as a function on $[a, b]$ , the mean value theorem gives a $c \in (a, b)$ with $G (b) - G (a) = G^{'} (c) (b - a)$ (The mean value theorem, as the case $g (x) = x$ of Cauchy's: for $f$ continuous on $[a, b]$ with $a < b$ and differentiable on $(a, b)$ there is $c \in (a, b)$ with $f (b) - f (a) = f^{'} (c) (b - a)$ ).

Proof

1.1F1F2algebra

[Differentiated equation] Let $v : = P_{l}^{(m)}$ . Differentiating the Legendre equation of [F1] $m$ times with the general Leibniz rule [F2] gives, since the third and higher derivatives of $1 - t^{2}$ vanish, $(1 - t^{2}) v^{''} - 2 t (m + 1) v^{'} + [l (l + 1) - m (m + 1)] v = 0$ : the coefficient of $v^{''}$ is $1 - t^{2}$ ; that of $v^{'}$ collects $- 2 t$ from differentiating $1 - t^{2}$ once times the derivative count $(\binom{m}{1})$ and $- 2 t$ from the term $- 2 t P_{l}^{'}$ , total $- 2 t (m + 1)$ ; and that of $v$ collects $(\binom{m}{2}) (- 2) + m (- 2) + l (l + 1) = - m (m - 1) - 2 m + l (l + 1) = l (l + 1) - m (m + 1)$ .

1.2F1F2algebra

[Continuity at the endpoints] For $m = 0$ , $w_{l 0} = P_{l}$ is a polynomial; for $m \geq 1$ , $w_{l m} = (- 1)^{m} (1 - t^{2})^{m / 2} Q (t)$ with $Q = P_{l}^{(m)}$ a polynomial, so $∣ w_{l m} (t) ∣ \leq (1 - t^{2})^{m / 2} \sup_{[- 1, 1]} ∣ Q ∣ \to 0$ as $t \to \pm 1$ , and the function extended by $w_{l m} (\pm 1) : = 0$ is continuous on $[- 1, 1]$ .

2.1step 1.1F2algebra

[Substitution] Put $f (t) : = (1 - t^{2})^{m / 2} > 0$ on $(- 1, 1)$ , so that $w_{l m} = (- 1)^{m} f v$ ; the sign is constant and will be carried along. Put $u : = (- 1)^{m} v$ , so $w = f u$ and $u$ satisfies the same homogeneous equation as $v$ in step 1.1. From $u = f^{- 1} w$ and [F2], $u^{'} = f^{- 1} w^{'} - f^{- 2} f^{'} w$ and $u^{''} = f^{- 1} w^{''} - 2 f^{- 2} f^{'} w^{'} + (2 f^{- 3} (f^{'})^{2} - f^{- 2} f^{''}) w$ . Substituting into step 1.1 and multiplying by $f$ gives $(1 - t^{2}) w^{''} + [- 2 \frac{f^{'}}{f} (1 - t^{2}) - 2 t (m + 1)] w^{'} + [- \frac{f^{''}}{f} (1 - t^{2}) + 2 (\frac{f^{'}}{f})^{2} (1 - t^{2}) + 2 t (m + 1) \frac{f^{'}}{f} - m (m + 1) + l (l + 1)] w = 0$ . Direct differentiation gives $\frac{f^{'}}{f} = - \frac{m t}{1 - t^{2}}$ and therefore $\frac{f^{''}}{f} = (\frac{f^{'}}{f})^{'} + (\frac{f^{'}}{f})^{2} = \frac{- m - m t^{2}}{(1 - t^{2})^{2}} + \frac{m^{2} t^{2}}{(1 - t^{2})^{2}} = \frac{m (- 1 + (m - 1) t^{2})}{(1 - t^{2})^{2}}$ . Hence the coefficient of $w^{'}$ is $2 m t - 2 t (m + 1) = - 2 t$ , and the coefficient of $w$ equals $\frac{m - m (m + 1) t^{2}}{1 - t^{2}} - m (m + 1) + l (l + 1) = l (l + 1) - \frac{m^{2}}{1 - t^{2}}$ , using $\frac{m - m (m + 1) t^{2}}{1 - t^{2}} - m (m + 1) = - \frac{m^{2}}{1 - t^{2}}$ (expand the left side over the common denominator $1 - t^{2}$ ). This is the associated equation.

3.1step 2.1step 1.2F2F5F6F9algebra

[Orthogonality] Fix $m$ and let $k \neq l$ , $k \geq m$ . Multiply the associated equation for $w_{l m}$ by $w_{k m}$ and that for $w_{k m}$ by $w_{l m}$ , subtract, and use $- ((1 - t^{2}) w_{l m}^{'})^{'} w_{k m} + ((1 - t^{2}) w_{k m}^{'})^{'} w_{l m} = - \frac{d}{d t} [(1 - t^{2}) (w_{l m}^{'} w_{k m} - w_{l m} w_{k m}^{'})]$ : $(l (l + 1) - k (k + 1)) w_{l m} w_{k m} = - \frac{d}{d t} G (t)$ with $G (t) : = (1 - t^{2}) (w_{l m}^{'} (t) w_{k m} (t) - w_{l m} (t) w_{k m}^{'} (t))$ on $(- 1, 1)$ . By step 1.2, put $Q_{l} = P_{l}^{(m)}$ and $Q_{k} = P_{k}^{(m)}$ . If $m = 0$ , then both $w$ functions are polynomials and the factor $1 - t^{2}$ gives $G (t) \to 0$ at both endpoints. If $m \geq 1$ , put $f (t) = (1 - t^{2})^{m / 2}$ , so $f^{'} = - m t (1 - t^{2})^{m / 2 - 1}$ and $w_{l m} = (- 1)^{m} f Q_{l}$ , $w_{k m} = (- 1)^{m} f Q_{k}$ ; since $Q_{l}, Q_{k}$ and their derivatives are bounded on $[- 1, 1]$ , each term in $(1 - t^{2}) w_{l m}^{'} w_{k m}$ and $(1 - t^{2}) w_{l m} w_{k m}^{'}$ , after the product rule, is bounded by a constant times $(1 - t^{2})^{m}$ or $(1 - t^{2})^{m + 1}$ , so again $G (t) \to 0$ at both endpoints. Extend $G$ by $G (\pm 1) = 0$ ; these limits make it continuous on $[- 1, 1]$ . The subtracted equations give $G^{'} (t) = q (t) : = - (l (l + 1) - k (k + 1)) w_{l m} (t) w_{k m} (t)$ on $(- 1, 1)$ , and step 1.2 makes $q$ continuous on $[- 1, 1]$ . For each $x \in (- 1, 1)$ , [F9] on $[x, 1]$ gives $(G (1) - G (x)) / (1 - x) = q (ξ_{x})$ for some $ξ_{x} \in (x, 1)$ , so as $x ↑ 1$ this quotient tends to $q (1)$ . On $[- 1, x]$ , [F9] gives $(G (x) - G (- 1)) / (x + 1) = q (η_{x})$ for some $η_{x} \in (- 1, x)$ ; as $x ↓ - 1$ this quotient tends to $q (- 1)$ . Thus $G$ is differentiable at every point of $[- 1, 1]$ with the endpoint convention of [F6], and $G^{'} = q$ is continuous, hence integrable by [F5]. Now [F6] gives $\int_{- 1}^{1} G^{'} = G (1) - G (- 1) = 0$ , so $(l (l + 1) - k (k + 1)) \int_{- 1}^{1} w_{l m} w_{k m} d t = 0$ and, since $l \neq k$ , $\int_{- 1}^{1} w_{l m} w_{k m} d t = 0$ .

3.2step 2.1step 1.2F5F8algebra

[Positivity and finiteness of the norms] By steps 2.1 and 1.2, $w_{l m}^{2}$ is continuous on $[- 1, 1]$ , so its integral is finite and nonnegative by [F5]; it is not zero because $w_{l m}$ is not the zero function on $(- 1, 1)$ : $P_{l}^{(m)}$ is a nonzero polynomial by [F8] and $(1 - t^{2})^{m / 2} > 0$ in the interior, so $w_{l m}$ is nonzero at every point where the polynomial does not vanish, and a continuous nonzero function has positive integral by [F5]. Hence $0 < \int_{- 1}^{1} w_{l m}^{2} d t < + \infty$ and $b_{l m}$ of the Statement is a well-defined positive real.

3.3step 2.1F1F7algebra

[The functions $Y_{l m}$ and their conjugation] The formula in the Statement defines continuous representatives on $S^{2}$ , so each class $Y_{l m}$ belongs to $L^{2} (S^{2}, σ)$ because $σ$ is finite; their chart moduli satisfy $∣ Y_{l m} (Φ (θ, φ)) ∣ = b_{l m} ∣ w_{l m} (\cos θ) ∣ / \sqrt{2 π}$ . By definition $Y_{l, - m} = (- 1)^{m} \overline{Y_{l m}}$ , so $∣ Y_{l, - m} ∣ = ∣ Y_{l m} ∣$ and, conjugating twice, $\overline{Y_{l, - m}} = (- 1)^{m} Y_{l m}$ , which is the displayed identity for every $m \geq 0$ . This establishes (c), and the identities in (e) follow from $P_{l}^{(0)} = P_{l}$ and $P_{l}^{(l)} = \frac{(2 l)!}{2^{l} l!}$ (the leading coefficient of $P_{l}$ times $l!$ , by [F1]).

4.1step 3.1step 3.2step 3.3F3F4F7algebra∎

[Orthonormality] Let $m, m^{'} \geq 0$ . The extensions on $C$ do not affect integrals because $σ (C) = 0$ . Thus [F3] applies to the $L^{1}$ function $Y_{l m} \overline{Y_{l^{'} m^{'}}}$ , whose integral against $σ$ is the inner product; with [F4], this gives $⟨ Y_{l m}, Y_{l^{'} m^{'}} ⟩ = b_{l m} b_{l^{'} m^{'}} \frac{1}{2 π} (\int_{0}^{2 π} e^{i (m - m^{'}) φ} d φ) (\int_{- 1}^{1} w_{l m} (t) w_{l^{'} m^{'}} (t) d t) = δ_{m m^{'}} b_{l m} b_{l^{'} m} \int_{- 1}^{1} w_{l m} w_{l^{'} m} d t$ , which by steps 3.1 and 3.2 equals $0$ for $l \neq l^{'}$ and $1$ for $l = l^{'}$ . For entries with negative lower index, write the inner product as a product of conjugation operations using [F7]: $⟨ Y_{l, - m}, Y_{l^{'}, - m^{'}} ⟩ = (- 1)^{m + m^{'}} ⟨ \overline{Y_{l m}}, \overline{Y_{l^{'} m^{'}}} ⟩ = (- 1)^{m + m^{'}} \overline{⟨ Y_{l m}, Y_{l^{'} m^{'}} ⟩}$ , and $⟨ Y_{l m}, Y_{l^{'}, - m^{'}} ⟩ = (- 1)^{m^{'}} \int_{S^{2}} Y_{l m} Y_{l^{'} m^{'}} d σ$ , whose rectangle form has $φ$ -factor $\int_{0}^{2 π} e^{i (m + m^{'}) φ} d φ$ , vanishing unless $m = m^{'} = 0$ by [F4], in which case it reduces to the already treated case; collecting the cases gives orthonormality for all pairs. This proves (d), and (a), (b) were proved in steps 2.1, 3.1 and 3.2.

Associated Legendre function normalization

Statement

Facts & Assumptions

Proof

Depends on

Dependency tree · 2 levels

Sources