LemmaStatement: AI-adaptedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6.1-sol)

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.

Outgoing spherical trace and Dirichlet-to-Neumann map

Statement

Assume the Axiom of Choice inherited from the explicitly used trace and weak Dirichlet-solvability suppliers (The Axiom of Choice). Let $k > 0$ and $R > 0$ . Use the sphere-normalised basis $Y_{l m}^{R} (R n) : = R^{- 1} Y_{l m} (n)$ on $S_{R}$ , where $Y_{l m}$ is the complete normalised unit-sphere basis of the spherical-harmonic lemma (Spherical harmonics: orthogonal decomposition, complete basis and addition theorem) and the coefficients $t_{l}$ are those of the outgoing radial-function lemma (Spherical Hankel functions: explicit solutions, constant Wronskian and exact Dirichlet-to-Neumann bounds). The map

$T_{R} f = \sum_{l, m} t_{l} f_{l m} Y_{l m}^{R}, f \in H^{1 / 2} (S_{R}),$

is a bounded linear operator $H^{1 / 2} (S_{R}) \to H^{- 1 / 2} (S_{R})$ with

$Re ⟨ T_{R} f, f ⟩ \leq 0, Im ⟨ T_{R} f, f ⟩ = \sum_{l, m} (Im t_{l}) ∣ f_{l m} ∣^{2} > 0 (f \neq 0) .$

It is precisely the outgoing scalar Helmholtz normal derivative at $r = R$ : for every $f \in H^{1 / 2} (S_{R})$ the function $u (r n) = \sum_{l, m} f_{l m} h_{l} (k r) / h_{l} (k R) R^{- 1} Y_{l m} (n)$ for $r \geq R$ is the unique outgoing finite-local-energy exterior solution with trace $f$ on $S_{R}$ and normal derivative $T_{R} f$ in the weak trace sense; it is smooth away from the sphere, and for smooth $f$ it satisfies the ordinary Sommerfeld condition. No uniform pointwise outgoing condition is asserted for arbitrary rough traces; the outgoing condition there is its modal/weak version. Here finite-local-energy means membership in $H^{1} ({R < ∣ x ∣ < R_{1}})$ for every finite $R_{1} > R$ , with the $H^{1 / 2}$ trace on $S_{R}$ ; no global $H^{1}$ or global $L^{2}$ condition at infinity is imposed. The outgoing modal class consists of the displayed outgoing $h_{l}$ radial factors with no incoming partners; for rough traces this modal class is the definition, rather than a pointwise Sommerfeld assertion. Here the boundary Sobolev spaces are their complex versions (or complexifications of the real trace spaces), $f_{l m} = \int_{S_{R}} f \overline{Y_{l m}^{R}} d σ_{R}$ , and the DtN dual pairing is linear in its first argument and conjugate-linear in its second.

Facts & Assumptions

Given: The Axiom of Choice; $k > 0$ , $R > 0$ ; the unit-sphere harmonics $Y_{l m}$ and their solid homogeneous harmonic extensions; the sphere-normalised basis $Y_{l m}^{R} (R n) = R^{- 1} Y_{l m} (n)$ with $σ_{R}$ the surface measure on $S_{R}$ (Surface integration on compact C1 hypersurfaces); the coefficients $t_{l}$ of Spherical Hankel functions: explicit solutions, constant Wronskian and exact Dirichlet-to-Neumann bounds with $- (l + 1) / R \leq Re t_{l} \leq - 1 / R$ and $0 < Im t_{l} \leq k$ ; and the data $f \in H^{1 / 2} (S_{R})$ .

[F1]

Traces and weak solvability. The trace operator on $W^{1, 2}$ of a bounded $C^{1}$ domain is bounded and onto $H^{1 / 2}$ of the boundary, and for prescribed fractional data there is a unique harmonic $H^{1}$ extension whose trace is the data, with $∥ u ∥_{H^{1}} \leq C ∥ f ∥_{H^{1 / 2}}$ (Weak Dirichlet problem with prescribed fractional Sobolev boundary data, The sharp trace theorem: boundedness and range in the fractional space, The $L^{p}$ trace operator on a bounded $C^{1}$ domain, The Axiom of Choice). Smooth ambient restrictions are dense in $H^{1} (B_{R})$ by Ambient smooth restrictions are dense on bounded C^k domains.

[F2]

Spherical harmonics and ball expansion. The $Y_{l m}$ form a complete orthonormal basis of $L^{2} (S^{2})$ , with solid homogeneous harmonic extensions; the ball Poisson series has interior convergence with all derivatives, $L^{2}$ boundary limits and uniqueness (Spherical harmonics: orthogonal decomposition, complete basis and addition theorem, Ball Poisson series: interior convergence, boundary data and the Poisson kernel). Real $L^{2}$ (and its complexification) is a Hilbert space with the integral pairing ( $L^{2}$ with the integral pairing is a Hilbert space).

[F3]

First Green identity and Dirichlet energy. For $C^{2}$ functions, $\int_{Ω} ∣ \nabla u ∣^{2} = - \int_{Ω} u Δ u + \int_{\partial Ω} u \partial_{ν} u$ on a bounded $C^{1}$ domain (First Green identity); the Laplacian is the Euclidean one (The Laplacian of a $C^{2}$ function and of a $C^{2}$ vector field).

[F4]

Hankel functions. The explicit finite-polynomial functions $h_{l}$ solve the radial Helmholtz equation, never vanish for positive real arguments, obey $Im (\overline{h_{l}} h_{l}^{'}) = z^{- 2}$ , and have $- (l + 1) / r \leq Re (k h_{l}^{'} (k r) / h_{l} (k r)) \leq - 1 / r$ and $0 < Im (k h_{l}^{'} (k r) / h_{l} (k r)) \leq k$ (Spherical Hankel functions: explicit solutions, constant Wronskian and exact Dirichlet-to-Neumann bounds). In particular $F_{l} (z) : = z^{2} ∣ h_{l} (z) ∣^{2}$ is nonincreasing, because its logarithmic derivative is $2 / z + 2 Re (h_{l}^{'} / h_{l}) \leq 0$ .

[F5]

Bounds. Cauchy-Schwarz for $L^{2}$ (Cauchy-Schwarz inequality for $L^{2}$ ), dominated convergence (Dominated convergence) and the algebra of derivatives (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$ ).

[F6]

Harmonic derivative estimate. Under Countable Choice, for a harmonic $v$ and $B_{ρ} (x) ⋐ Ω$ , $∣ D^{α} v (x) ∣ \leq C_{3, α} ρ^{- 3 - ∣ α ∣} \int_{B_{ρ} (x)} ∣ v ∣$ (Interior derivative estimates for harmonic functions). The smooth modal branch of Exact Helmholtz boundary representation with actual traces gives uniform $r^{- 1}$ amplitude and the ordinary uniform Sommerfeld residual for smooth angular traces, using the same explicit outgoing radial factors.

Proof

technique · direct

1.1givenF1F2F3F6algebra

For finite harmonic data the harmonic ball extension $v (r n) = \sum (r / R)^{l} f_{l m} R^{- 1} Y_{l m} (n)$ has, by [F3] and the orthonormality of the solid harmonics, Dirichlet energy $\int_{B_{R}} ∣ \nabla v ∣^{2} = \sum_{l, m} (l / R) ∣ f_{l m} ∣^{2}$ and $L^{2}$ norm $\sum_{l, m} R ∣ f_{l m} ∣^{2} / (2 l + 3)$ ; hence its $H^{1}$ norm squared is $\sum_{l, m} ∣ f_{l m} ∣^{2} (l / R + R / (2 l + 3))$ , comparable to $\sum_{l, m} (l + 1) ∣ f_{l m} ∣^{2}$ ; the sharp trace bound of [F1] gives $∥ f ∥_{H^{1 / 2}} \leq C ∥ v ∥_{H^{1}}$ , and the weak harmonic-solver bound gives the reverse inequality $∥ v ∥_{H^{1}} \leq C ∥ f ∥_{H^{1 / 2}}$ , since this finite harmonic polynomial is the unique weak solution with that trace. To extend the norm equivalence, smooth data are dense in $H^{1 / 2}$ : lift an arbitrary datum by [F1], approximate its lift in $H^{1}$ by the smooth restrictions of [F1], and apply the bounded sharp trace. For a smooth sphere datum $g$ , the rotation-generator integration-by-parts calculation in [F6] gives $∣ g_{l m} ∣ \leq ∥ Λ^{p} g ∥_{2} [l (l + 1)]^{- p}$ for $l \geq 1$ and any $p$ , with $Λ Y_{l m} = - l (l + 1) Y_{l m}$ . Hence its harmonic partial sums have Cauchy ball extensions in $H^{1}$ by the finite energy formula just computed. Their traces converge in $H^{1 / 2}$ by the sharp trace, and in $L^{2}$ to $g$ by completeness [F2], so the trace limit is $g$ . Thus finite harmonic data are dense in $H^{1 / 2}$ . The two equivalent norms on finite data consequently have the same completion; weighted coefficient convergence and $L^{2}$ completeness identify that completion with $\sum_{l, m} (l + 1) ∣ f_{l m} ∣^{2} < \infty$ for the actual coefficients of $f$ . This proves the claimed norm equivalence for every $f \in H^{1 / 2} (S_{R})$ .

2.1step 1.1givenF4F5algebra

Define $T_{R} f = \sum_{l, m} t_{l} f_{l m} Y_{l m}^{R}$ and pair it with $f^{'} \in H^{1 / 2} (S_{R})$ by $⟨ T_{R} f, f^{'} ⟩ = \sum_{l, m} t_{l} f_{l m} \overline{f_{l m}^{'}}$ ; the bounds $∣ t_{l} ∣ \leq (l + 1) / R + k$ of [F4] and Cauchy-Schwarz [F5] give $∣ ⟨ T_{R} f, f^{'} ⟩ ∣ \leq C (R, k) ∥ f ∥_{H^{1 / 2}} ∥ f^{'} ∥_{H^{1 / 2}}$ with the weight $(l + 1)$ supplied by step 1.1, so $T_{R}$ is a bounded operator into $H^{- 1 / 2} (S_{R})$ .

2.2step 1.1givenF2F4F5F6algebra

Exterior realisation and convergence away from the sphere. For $l \geq 1$ , establish the needed positive-coefficient identity locally from the explicit formula of [F4]. Put $y = z h_{l}$ and $L = l (l + 1)$ , so $y^{''} + (1 - L z^{- 2}) y = 0$ and $F_{l} = ∣ y ∣^{2}$ . Product differentiation gives $F_{l}^{'''} + 4 (1 - L z^{- 2}) F_{l}^{'} + 4 L z^{- 3} F_{l} = 0$ . The displayed finite polynomial formula for $h_{l}$ shows that $F_{l}$ is an even polynomial in $z^{- 1}$ (the odd cross terms cancel in conjugate pairs), with constant term $a_{0} = 1$ . Substitution of $F_{l} = \sum_{j = 0}^{l} a_{j} z^{- 2 j}$ gives $a_{j + 1} = (2 j + 1) [L - j (j + 1)] a_{j} / [2 (j + 1)]$ , so $a_{j} = (2 j)! (l + j)! / [2^{2 j} (j!)^{2} (l - j)!] > 0$ for $0 \leq j \leq l$ . Thus the coefficients satisfy $a_{j - 1} / a_{j} = 2 j / [(2 j - 1) (l + j) (l - j + 1)] \leq 2 / [l (l - j + 1)]$ . Thus $a_{l - d} / a_{l} \leq (2 / l)^{d} / d!$ and $a_{l} z^{- 2 l} \leq F_{l} (z) \leq a_{l} z^{- 2 l} \exp (2 z^{2} / l)$ . For $R + δ \leq r \leq R_{1}$ this gives $∣ h_{l} (k r) / h_{l} (k R) ∣ \leq (R / r)^{l + 1} \exp (k^{2} R_{1}^{2} / l)$ , a geometric bound in $l$ . The logarithmic-derivative bound $∣ k h_{l}^{'} (k r) / h_{l} (k r) ∣ \leq (l + 1) / r + k$ , followed by induction in the radial ODE, bounds each fixed radial derivative by that geometric factor times a polynomial in $l$ on the same annulus. For angular derivatives, write the solid harmonic as $P_{l m} (x) = ∣ x ∣^{l} Y_{l m} (x / ∣ x ∣)$ . The addition diagonal gives $∥ Y_{l m} ∥_{\infty} \leq \sqrt{(2 l + 1) / (4 π)}$ ; on a ball of radius $1 / [2 (l + 1)]$ about a unit vector, $∣ P_{l m} ∣ \leq (1 + 1 / [2 (l + 1)])^{l} \sqrt{(2 l + 1) / (4 π)} \leq e^{1 / 2} \sqrt{(2 l + 1) / (4 π)}$ . Applying [F6] to this harmonic polynomial gives $∣ D^{α} P_{l m} ∣ \leq C_{α} (l + 1)^{∣ α ∣ + 1 / 2}$ on $S^{2}$ . Chain rules in any fixed finite sphere atlas therefore give polynomial bounds for all fixed angular derivatives of $Y_{l m}$ . Combining these bounds with $\sum_{l, m} (l + 1) ∣ f_{l m} ∣^{2} < \infty$ from step 1.1 proves absolute uniform convergence of the series defining $u$ and of every fixed derivative on the closed annulus, by Cauchy-Schwarz against a geometric sequence. Termwise differentiation is justified by the coordinate FTC and uniform convergence of the derivative series. The radial ODE and angular harmonic identity give $(Δ + k^{2}) u = 0$ there.

3.1step 2.1givenF4F2algebra

Signs: $Re ⟨ T_{R} f, f ⟩ = \sum Re (t_{l}) ∣ f_{l m} ∣^{2} \leq 0$ and $Im ⟨ T_{R} f, f ⟩ = \sum (Im t_{l}) ∣ f_{l m} ∣^{2} > 0$ for $f \neq 0$ , by $- (l + 1) / R \leq Re t_{l} \leq - 1 / R$ and $0 < Im t_{l}$ of [F4] together with the completeness of the basis (a nonzero $f$ has some nonzero coefficient).

3.2step 1.1step 2.1step 2.2F1F2F3F4F5algebra

Finite local energy, trace and normal derivative. Let $u_{N}$ be a finite harmonic sum. Orthogonality and $∣ h_{l} (k r) / h_{l} (k R) ∣ \leq R / r$ give $∥ u_{N} ∥_{L^{2} (R < ∣ x ∣ < R_{1})}^{2} \leq (R_{1} - R) \sum_{l, m} ∣ f_{l m} ∣^{2}$ . Apply the complex Green identity (obtained by applying [F3] to both real parts and both mixed real/imaginary pairs) on the annulus. The outer boundary real term is nonpositive since the radial logarithmic derivative at $R_{1}$ has negative real part. The inner outward normal is $- e_{r}$ , so the inner real term is $- \sum Re t_{l} ∣ f_{l m} ∣^{2} \leq \sum (l + 1) ∣ f_{l m} ∣^{2} / R$ . Consequently $∥ \nabla u_{N} ∥_{2}^{2} \leq k^{2} (R_{1} - R) \sum ∣ f_{l m} ∣^{2} + R^{- 1} \sum (l + 1) ∣ f_{l m} ∣^{2}$ . The same estimate for differences of finite sums proves convergence in $H^{1}$ on every finite annulus, to the smooth interior limit of step 2.2. Boundedness of the trace operator [F1] and step 1.1 identify the inner trace as $f$ . The finite sums have increasing-radial derivative $T_{R} f_{N}$ on $S_{R}$ ; the Green pairing against any $H^{1}$ test passes to the limit by the $H^{1}$ convergence and the bounded pairing in step 2.1, identifying the increasing-radial weak normal derivative as $T_{R} f$ . Thus the claimed finite-local-energy and weak-trace assertions hold for every $f$ .

4.1step 2.2step 3.2F4F2algebra

Uniqueness: in the outgoing modal class defined in the Statement every degree- $l$ radial coefficient is an $h_{l} (k r)$ multiple. Since $h_{l} (k R) \neq 0$ by [F4], the prescribed trace fixes that multiple to $f_{l m} / h_{l} (k R)$ in the sphere-normalised basis; harmonic completeness [F2] then fixes the function on every exterior sphere, and the l=0 mode $e^{i k r} / r$ shows why no global $L^{2}$ or $H^{1}$ condition at infinity is imposed (its global energy integrals diverge).

5.1step 1.1step 3.1step 3.2F1F5F6algebra∎

For complex boundary data apply the real prescribed-trace and harmonic solver of [F1] to the real and imaginary parts and combine; the squared boundary norm is the sum of the two real energy norms and the pairing is linear-conjugate-linear as stated, For smooth $f$ , the smooth modal branch of [F6], with angular coefficients $f_{l m} / R$ and sphere radius $R$ , gives the ordinary uniform Sommerfeld condition for exactly this series. This completes the identification of $T_{R}$ with the outgoing DtN map and its properties.

Outgoing spherical trace and Dirichlet-to-Neumann map

Statement

Facts & Assumptions

Proof

Depends on

Dependency tree · 2 levels

Sources