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.

Sphere Laplacian diagonal domain

Statement

Assume the Axiom of Countable Choice (The Axiom of Countable Choice ( ${A C}_{ω}$ )). Fix a real parameter $ℏ > 0$ . Let $(Y_{l m})_{l \geq 0, - l \leq m \leq l}$ be the complete orthonormal family of $L^{2} (S^{2}, σ)$ constructed in Associated Legendre function normalization and Sphere ONB, and let $H : = span {Y_{l m} : - l \leq m \leq l, l \in N}$ be its algebraic (finite) span. Define operators $A$ and $L_{z}$ on $L^{2} (S^{2}, σ)$ by the diagonal lemma Diagonal adjoint and graph-core lemma:

$D (A) : = {F : \sum_{l, m} l^{2} (l + 1)^{2} ∣ ⟨ F, Y_{l m} ⟩ ∣^{2} < \infty}, A F : = \sum_{l, m} l (l + 1) ⟨ F, Y_{l m} ⟩ Y_{l m},$ $D (L_{z}) : = {F : \sum_{l, m} m^{2} ∣ ⟨ F, Y_{l m} ⟩ ∣^{2} < \infty}, L_{z} F : = \sum_{l, m} ℏ m ⟨ F, Y_{l m} ⟩ Y_{l m},$

the sums being in the Hilbert-space norm (Hilbert space, Orthonormal families, complete orthonormal systems and Hilbert bases). Finally, for $F$ in the finite span $H$ , use the canonical continuous representatives ${\tilde{Y}}_{l m}$ from Associated Legendre function normalization: set $\tilde{F} : = \sum_{l, m} ⟨ F, Y_{l m} ⟩ {\tilde{Y}}_{l m}$ , a finite sum uniquely determined by the orthonormal coefficients. The same convention applies to $A F, L_{z} F \in H$ . On the chart $Φ (θ, φ) = (\sin θ \cos φ, \sin θ \sin φ, \cos θ)$ with $(θ, φ) \in (0, π) \times (0, 2 π)$ , write $F (θ, φ) : = \tilde{F} (Φ (θ, φ))$ and put

$(S F) (θ, φ) : = - \frac{1}{\sin θ} \partial_{θ} (\sin θ \partial_{θ} F) (θ, φ) - \frac{1}{\sin^{2} θ} \partial_{φ}^{2} F (θ, φ), (D F) (θ, φ) : = - i ℏ \partial_{φ} F (θ, φ),$

where the partial derivatives are those of Directional derivatives and partial derivatives of a map $U \subseteq R^{m} \to R^{n}$ . Then:

(a) $A$ and $L_{z}$ are self-adjoint operators on $L^{2} (S^{2}, σ)$ with the displayed domains; on $Y_{l m}$ they act by $A Y_{l m} = l (l + 1) Y_{l m}$ and $L_{z} Y_{l m} = ℏ m Y_{l m}$ (Symmetric, self-adjoint and essentially self-adjoint operators); $A$ is nonnegative, $⟨ A F, F ⟩ \geq 0$ , and $A 1 = 0$ ;

(b) $H$ is a core of $A$ and of $L_{z}$ : the finite truncations $F_{N} : = \sum_{l \leq N} \sum_{m} ⟨ F, Y_{l m} ⟩ Y_{l m}$ of an element $F$ of $D (A)$ satisfy $F_{N} \to F$ and $A F_{N} \to A F$ in $L^{2}$ , and analogously with $L_{z}$ ;

(c) for every $F \in H$ and every chart point with $\sin θ \neq 0$ , $S F (θ, φ) = (A F) (θ, φ), D F (θ, φ) = (L_{z} F) (θ, φ);$

(d) for every $l$ the orthogonal projection $P_{l}$ of $L^{2} (S^{2}, σ)$ onto the $(2 l + 1)$ -dimensional span of $Y_{l, - l}, \dots, Y_{l l}$ , defined by $P_{l} F : = \sum_{m = - l}^{l} ⟨ F, Y_{l m} ⟩ Y_{l m}$ (the unique vector in that span with orthogonal residual), reduces both $A$ and $L_{z}$ , i.e. $P_{l} A \subseteq A P_{l}$ and $P_{l} L_{z} \subseteq L_{z} P_{l}$ ; consequently $A$ and $L_{z}$ commute on the finite span $H$ , and for every $F \in D (A)$ with $\sum_{l, m} (l (l + 1) ℏ m)^{2} ∣ ⟨ F, Y_{l m} ⟩ ∣^{2} < \infty$ one has $A L_{z} F = L_{z} A F = \sum_{l, m} l (l + 1) ℏ m ⟨ F, Y_{l m} ⟩ Y_{l m}$ . Writing $c_{l m} = ⟨ F, Y_{l m} ⟩$ and $λ_{l} = l (l + 1)$ , the maximal product domains are $D (A L_{z}) = {F \in L^{2} : \sum_{l, m} (λ_{l} ℏ m)^{2} ∣ c_{l m} ∣^{2} < \infty}$ and $D (L_{z} A) = D (A) \cap D (A L_{z})$ . Thus this is exactly the common domain $D (A L_{z}) \cap D (L_{z} A) = D (L_{z} A)$ , while the two maximal product domains need not coincide. The product-weight condition alone does not imply $F \in D (A)$ : the vector with coefficients $c_{l 0} = 1 / l$ for $l \geq 1$ and all other coefficients zero belongs to $L^{2}$ , has zero product weight, but does not belong to $D (A)$ . The product-weight condition is not automatic for all $F \in D (A) \cap D (L_{z})$ .

The differential expression $S$ is evaluated only away from the poles, where the coordinate formulas are defined; no claim is made about a maximal differential operator on all of $S^{2}$ .

Facts & Assumptions

Given: the complete orthonormal family $(Y_{l m})$ ; the finite span $H$ ; the diagonal operators $A, L_{z}$ ; the differential expressions $S, D$ ; the canonical representatives ${\tilde{Y}}_{l m} = b_{l m} w_{l m} (\cos θ) e^{i m φ} / \sqrt{2 π}$ for $m \geq 0$ , with ${\tilde{Y}}_{l, - m} = (- 1)^{m} \overline{{\tilde{Y}}_{l m}}$ for $m > 0$ , and their finite coefficient sums $\tilde{F}$ .

[F1]

Diagonal lemma: for a complete orthonormal family $(e_{j})$ and real eigenvalues $λ_{j}$ the diagonal operator $S$ with $S e_{j} = λ_{j} e_{j}$ and $D (S) = {x : \sum_{j} λ_{j}^{2} ∣ ⟨ x, e_{j} ⟩ ∣^{2} < \infty}$ is self-adjoint and is the unique self-adjoint extension of its finite span; the finite span is a core, the finite truncations converge in the graph norm, and $⟨ S x, x ⟩ = \sum_{j} λ_{j} ∣ ⟨ x, e_{j} ⟩ ∣^{2}$ (Diagonal adjoint and graph-core lemma).

[F2]

$(Y_{l m})$ is a complete orthonormal family of $L^{2} (S^{2}, σ)$ (Sphere ONB).

[F3]

$w_{l m}$ is continuous on $[- 1, 1]$ , differentiable on $(- 1, 1)$ , and 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}$ (Associated Legendre function normalization (a)).

[F4]

${\tilde{Y}}_{l m} (Φ (θ, φ)) = b_{l m} w_{l m} (\cos θ) e^{i m φ} / \sqrt{2 π}$ for $m \geq 0$ and ${\tilde{Y}}_{l, - m} = (- 1)^{m} \overline{{\tilde{Y}}_{l m}}$ ; their $L^{2}$ classes are $Y_{l m}$ (Associated Legendre function normalization (c)).

[F5]

Sine and cosine are differentiable with $\sin^{'} = \cos$ , $\cos^{'} = - \sin$ ; partial derivatives are computed by the usual rules, including the chain rule for $t = \cos θ$ and the product rule (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)$ , 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$ , Directional derivatives and partial derivatives of a map $U \subseteq R^{m} \to R^{n}$ ). The complex exponential has complex derivative itself (The complex exponential is entire and its complex derivative is itself). For $m \neq 0$ , its defining difference quotient along increments $i m h$ gives $\frac{d}{d φ} e^{i m φ} = i m e^{i m φ}$ ; for $m = 0$ this is the constant derivative $0$ . Repeating gives $\frac{d^{2}}{d φ^{2}} e^{i m φ} = - m^{2} e^{i m φ}$ .

[F6]

For a finite orthonormal family $(u_{j})$ in a Hilbert space, set $P x : = \sum_{j} ⟨ x, u_{j} ⟩ u_{j}$ . Its value lies in their span and $⟨ x - P x, u_{j} ⟩ = 0$ for each $j$ , so it is uniquely determined by orthogonal residual. The finite pairings give $P^{2} = P$ and $⟨ P x, y ⟩ = ⟨ x, P y ⟩$ ; also $∥ x ∥^{2} = ∥ P x ∥^{2} + ∥ x - P x ∥^{2}$ , so $∥ P ∥ \leq 1$ . Thus it is the bounded self-adjoint orthogonal projection onto that span; no finite-dimensional ambient hypothesis is needed (Real and complex inner product spaces, with the inner product linear in the first argument, The induced length is a norm).

Proof

1.1F1F2F4algebra

[(a) and (b)] Enumerate the indices by $j = l^{2} + l + m$ , which bijects the block $- l \leq m \leq l$ to $l^{2} \leq j < (l + 1)^{2}$ and all blocks to $N$ . Apply [F1] to this enumeration of the complete orthonormal family $(Y_{l m})$ of [F2] with the real eigenvalues $λ_{l m} = l (l + 1)$ : the resulting operator is exactly $A$ as defined, is self-adjoint, has the displayed domain, satisfies $⟨ A F, F ⟩ = \sum_{l m} l (l + 1) ∣ ⟨ F, Y_{l m} ⟩ ∣^{2} \geq 0$ , and has the finite span $H$ as a core with the stated truncation property; the eigenvalues are nonnegative, so $A 1 = 0$ because $1 = \sqrt{4 π} Y_{00}$ by [F4] (with $P_{0} = 1$ , $b_{00} = 1 / \sqrt{2}$ ), whose eigenvalue is zero. The same application with the real eigenvalues $ℏ m$ , $m \in Z$ (whose square summability domain is the displayed one because $ℏ > 0$ ), gives clause (a) and the second half of (b) for $L_{z}$ .

1.2F3F4F5algebra

[(c) for $A$ ] For $F = Y_{l m}$ with $m \geq 0$ , evaluate its canonical representative; by [F4], $F (θ, φ) = c w (\cos θ) e^{i m φ}$ with $w = w_{l m}$ and $c = b_{l m} / \sqrt{2 π}$ . Computing the partial derivatives with [F5]: $\partial_{φ}^{2} F = - m^{2} F$ and, writing $t = \cos θ$ , $\partial_{θ} F = - c \sin θ w^{'} (t) e^{i m φ}$ , so $\sin θ \partial_{θ} F = - c \sin^{2} θ w^{'} (t) e^{i m φ}$ and $\partial_{θ} (\sin θ \partial_{θ} F) = c (- 2 \sin θ \cos θ w^{'} + \sin^{3} θ w^{''}) e^{i m φ}$ ; dividing by $- \sin θ$ gives $c (2 t w^{'} - (1 - t^{2}) w^{''}) e^{i m φ} = - c ((1 - t^{2}) w^{'})^{'} e^{i m φ}$ , where in the last step $((1 - t^{2}) w^{'})^{'} = - 2 t w^{'} + (1 - t^{2}) w^{''}$ . Also $- \sin^{- 2} θ \partial_{φ}^{2} F = + m^{2} (1 - t^{2})^{- 1} F$ . Adding, $S F = c [- ((1 - t^{2}) w^{'})^{'} + \frac{m^{2}}{1 - t^{2}} w] e^{i m φ}$ , which by [F3] equals $c l (l + 1) w e^{i m φ} = l (l + 1) F = A F$ . For negative indices, $Y_{l, - m} = (- 1)^{m} \overline{Y_{l m}}$ and the real-coefficient differential expression $S$ commutes with conjugation, so the same eigenvalue identity holds. Both sides are linear over finite sums, so the identity extends to all of $H$ .

2.1step 1.2F4F5algebra

[(c) for $L_{z}$ ] With $F = Y_{l m}$ , $\partial_{φ} F = i m F$ , so $D F = - i ℏ (i m) F = ℏ m F = L_{z} F$ by the definition of $L_{z}$ . For negative indices [F4] gives $Y_{l, - m} = (- 1)^{m} \overline{Y_{l m}}$ and $\partial_{φ} Y_{l, - m} = (- 1)^{m} \overline{\partial_{φ} Y_{l m}} = - i m Y_{l, - m}$ , so again $D Y_{l, - m} = ℏ (- m) Y_{l, - m} = L_{z} Y_{l, - m}$ . Extending by linearity to $H$ completes the proof of (c).

3.1step 1.1step 2.1F1F6algebra∎

[(d)] On the basis $A L_{z} Y_{l m} = l (l + 1) ℏ m Y_{l m} = L_{z} A Y_{l m}$ , and both operators are linear, so $A$ and $L_{z}$ commute on the finite span $H$ . For each $l$ , the span $V_{l}$ of $Y_{l, - l}, \dots, Y_{l l}$ consists of eigenvectors of $A$ with eigenvalue $l (l + 1)$ and of $L_{z}$ with eigenvalues $ℏ (- l), \dots, ℏ l$ ; by [F6] the projection is $P_{l} x = \sum_{m} ⟨ x, Y_{l m} ⟩ Y_{l m}$ , and grouping the diagonal expansions by $l$ shows $A P_{l} x = P_{l} A x$ for $x \in D (A)$ and $L_{z} P_{l} x = P_{l} L_{z} x$ for $x \in D (L_{z})$ . Finally, let $F \in D (A)$ satisfy the displayed product-weight condition. Since $∣ m ∣ \leq l$ and $l^{2} \leq l^{2} (l + 1)^{2}$ , $F \in D (L_{z})$ . The product-weight condition gives $L_{z} F \in D (A)$ and $A F \in D (L_{z})$ , so both compositions are defined: $A L_{z} F = \sum_{l, m} l (l + 1) ℏ m c_{l m} Y_{l m}$ with $\sum ∣ l (l + 1) ℏ m ∣^{2} ∣ c_{l m} ∣^{2} < \infty$ by hypothesis, and symmetrically for $L_{z} A F$ , so the two series converge to the same element. For the maximal domains, the product-weight condition implies $F \in D (L_{z})$ , since $λ_{l} \geq 2$ whenever $m \neq 0$ ; it is then exactly the condition $L_{z} F \in D (A)$ . Hence it describes $D (A L_{z})$ alone. The other composition additionally requires $F \in D (A)$ , giving $D (L_{z} A) = D (A) \cap D (A L_{z})$ . The stated $m = 0$ counterexample shows these maximal domains can differ. To verify that the product condition is not automatic on $D (A) \cap D (L_{z})$ , take $c_{l l} = l^{- 3}$ for $l \geq 1$ and every other coefficient zero: the separate domain sums are bounded by constants times $\sum l^{- 2}$ and $\sum l^{- 4}$ , respectively, but the product sum has terms $ℏ^{2} (l + 1)^{2} / l^{2} \geq ℏ^{2}$ and diverges.

Sphere Laplacian diagonal domain

Statement

Facts & Assumptions

Proof

Depends on

Dependency tree · 2 levels

Sources