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 ONB

Statement

Assume the Axiom of Countable Choice (The Axiom of Countable Choice ( ${A C}_{ω}$ )). Let $σ$ be the polar surface measure on $S^{2}$ (The polar surface set function on the unit sphere) and let $(Y_{l m})_{l \geq 0, - l \leq m \leq l}$ be the functions of Associated Legendre function normalization (The complex exponential by its power series). Then $(Y_{l m})$ is a complete orthonormal family of the complex Hilbert space $L^{2} (S^{2}, σ)$ (Orthonormal families, complete orthonormal systems and Hilbert bases, The space $L^{p} (μ)$ as the quotient by null functions): the family is orthonormal, and if $F \in L^{2} (S^{2}, σ)$ satisfies $\int_{S^{2}} F \overline{Y_{l m}} d σ = 0$ for all $l \geq 0$ and $- l \leq m \leq l$ , then $F = 0$ almost everywhere. Consequently every $F$ has the expansion $F = \sum_{l = 0}^{\infty} \sum_{m = - l}^{l} ⟨ F, Y_{l m} ⟩ Y_{l m}, ∥ F ∥^{2} = \sum_{l, m} ∣ ⟨ F, Y_{l m} ⟩ ∣^{2},$ with $⟨ F, Y_{l m} ⟩ = \int_{S^{2}} F \overline{Y_{l m}} d σ$ and finite-subset-net convergence (Parseval equivalences for an orthonormal family).

Facts & Assumptions

Given: the measure $σ$ on $S^{2}$ ; the functions $Y_{l m} = b_{l m} w_{l ∣ m ∣} (\cos θ) e^{i m φ} / \sqrt{2 π}$ with the convention $Y_{l, - m} = (- 1)^{m} \overline{Y_{l m}}$ ; a function $F \in L^{2} (S^{2}, σ)$ .

[F1]

Orthonormality of the family $(Y_{l m})$ in $L^{2} (S^{2}, σ)$ (Associated Legendre function normalization (d)).

[F2]

Angle coordinates: $\int_{S^{2}} G d σ = \int_{(0, π) \times (0, 2 π)} G (Φ (θ, φ)) \sin θ d (θ, φ)$ for $G \in L^{1}$ , with $Φ (θ, φ) = (\sin θ \cos φ, \sin θ \sin φ, \cos θ)$ (Sphere integrals in angle coordinates).

[F3]

Weighted completeness: for each $k \in N$ , if $h \in L^{2} ((- 1, 1), d t)$ satisfies $\int_{- 1}^{1} h (t) w_{l k} (t) d t = 0$ for all $l \geq k$ , then $h = 0$ a.e. (Weighted angular completeness (b)).

[F4]

The normalized characters $e_{k} (φ) = e^{i k φ} / \sqrt{2 π}$ , $k \in Z$ , are orthonormal in $L^{2} ((0, 2 π), d φ)$ , and their linear span is dense: trigonometric polynomials are uniformly dense in the continuous periodic functions (Trigonometric polynomials are uniformly dense in continuous functions on the torus), and continuous functions on $[0, 2 π]$ with equal endpoint values are dense in $L^{2} ((0, 2 π))$ (Continuous functions are dense in $L^{p}$ of finite tori and of bounded intervals, The trigonometric characters are orthonormal in $L^{2}$ of the torus); hence if $h \in L^{2} ((0, 2 π))$ has $\int_{0}^{2 π} h (φ) e^{- i k φ} d φ = 0$ for every $k \in Z$ , then $h = 0$ a.e.

[F5]

Tonelli's and Fubini's theorems identify the rectangle integral in [F2] with iterated integrals, for nonnegative and for $L^{1}$ integrands (Tonelli's theorem for nonnegative measurable functions on a sigma-finite product, Fubini's theorem for L^1 functions on a sigma-finite product).

[F6]

If $\int_{S^{2}} ∣ F ∣^{2} d σ < \infty$ , then by [F2] and [F5] the iterated integral $\int_{0}^{π} \int_{0}^{2 π} ∣ F (Φ (θ, φ)) ∣^{2} \sin θ d φ d θ$ is finite, so for almost every $θ$ the function $φ \mapsto F (Φ (θ, φ))$ lies in $L^{2} ((0, 2 π))$ (The space $L^{p} (μ)$ as the quotient by null functions, Complex Lp classes and Euclidean test-function conventions).

[F7]

$∣ \int g \overline{h} ∣ \leq ∥ g ∥_{2} ∥ h ∥_{2}$ and vanishing of all pairings against a dense family forces vanishing (Cauchy-Schwarz inequality for $L^{2}$ ).

Proof

1.1givenF2F3F5F6F7algebra

[Completeness: Fourier coefficients along the circles] Suppose $F \in L^{2} (S^{2}, σ)$ is orthogonal to every $Y_{l m}$ , and for $k \in Z$ and $θ \in (0, π)$ define $G_{k} (θ) : = \frac{1}{\sqrt{2 π}} \int_{0}^{2 π} F (Φ (θ, φ)) e^{- i k φ} d φ$ ; by [F6] and Cauchy–Schwarz [F7] each $G_{k}$ is defined for almost every $θ$ , and $\int_{0}^{π} ∣ G_{k} (θ) ∣^{2} \sin θ d θ \leq \int_{0}^{π} \int_{0}^{2 π} ∣ F (Φ (θ, φ)) ∣^{2} d φ \sin θ d θ < \infty$ , so $G_{k} \in L^{2} (\sin θ d θ)$ and, after the reparametrisation $t = \cos θ$ , $G_{k} \in L^{2} ((- 1, 1), d t)$ . For $l \geq k \geq 0$ , [F2] and [F5] compute $⟨ F, Y_{l k} ⟩ = b_{l k} \int_{0}^{π} G_{k} (θ) w_{l k} (\cos θ) \sin θ d θ = b_{l k} \int_{- 1}^{1} G_{k} (t) w_{l k} (t) d t$ ; hence $\int_{- 1}^{1} G_{k} (t) w_{l k} (t) d t = 0$ for every $l \geq k$ , and by [F3] $G_{k} = 0$ almost everywhere for every $k \geq 0$ . For $k < 0$ write $m : = - k > 0$ ; the convention gives $\overline{Y_{l, - m}} = (- 1)^{m} Y_{l m}$ , so orthogonality of $F$ to $Y_{l, - m}$ gives $0 = (- 1)^{m} \int_{S^{2}} F Y_{l m} d σ$ , whose rectangle form is $b_{l m} \int_{0}^{π} G_{- m} (θ) w_{l m} (\cos θ) \sin θ d θ$ with $0 \leq m \leq l$ ; by [F3] again, $G_{- m} = G_{k} = 0$ almost everywhere. So all circle Fourier coefficients of $F$ vanish for almost every $θ$ .

2.1step 1.1F2F4F6algebra

[Completeness: vanishing on the spheres] By [F4] applied to the $L^{2} ((0, 2 π))$ -function $φ \mapsto F (Φ (θ, φ))$ , which exists for almost every $θ$ by [F6] and has all Fourier coefficients zero by step 1.1, one has $F (Φ (θ, φ)) = 0$ for almost every $φ$ and almost every $θ$ ; hence $F \circ Φ = 0$ almost everywhere on the rectangle, and by [F2] (which for the nonnegative function $∣ F ∣$ identifies $\int_{S^{2}} ∣ F ∣ d σ$ with the rectangle integral) $F = 0$ almost everywhere on $S^{2}$ .

3.1step 2.1F1F7algebra∎

[The expansion] By [F1] the family is orthonormal, and by steps 1.1 and 2.1 it is complete; the expansion, Parseval identity and coefficient formula are the Hilbert-basis statements of Orthonormal families, complete orthonormal systems and Hilbert bases and Parseval equivalences for an orthonormal family, with finite-subset-net convergence.

Sphere ONB

Statement

Facts & Assumptions

Proof

Depends on

Dependency tree · 2 levels

Sources