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.
Em Boundary And Spectral Prerequisites
1 · Prerequisites
- Absolute and Conditional Convergence; Rearrangement; Products
- Absolute Continuity and the Sharp Fundamental Theorem of Calculus
- Analyticity of Holomorphic Functions; Liouville and Morera
- Approximation and Compactness in C(K)
- Arc Length and Rectifiable Curves
- Areas of Elementary Plane Figures
- Banach Valued Integration and the Radon Nikodym Property
- Bessel-Potential Completions and Real-Order Sobolev Spaces
- Binary Operations, Monoids, Groups and Subgroups
- Bounded Linear Operators and Quotient Spaces
- Bounded Variation and the Riemann–Stieltjes Integral
- Character Groups and Elementary LCA Duals
- Compact Operators and Riesz Schauder Theory
- Compact Self Adjoint Hilbert Schmidt and Trace Class Operators
- Compactness
- Compactness in Metric Spaces
- Completeness, Completion, and Uniform Continuity
- Complex Differentiability and the Cauchy–Riemann Equations
- Complex Lp Spaces and Test-Function Conventions
- Complex Power Series and Analytic Functions
- Connectedness
- Constant Rank, Submersions, Immersions and Regular Level Sets
- Construction of the Natural Numbers
- Construction of the Real Numbers via Cauchy Sequences
- Construction of the Real Numbers via Dedekind Cuts
- Continuity, IVT, EVT, and Uniform Continuity
- Contour Integration
- Convergence: Nets and Filters
- Convexity
- Cosets, Index and Lagrange's Theorem
- Countability and Uncountability
- Countability Axioms and Cardinal Functions
- Darboux, L'Hôpital, and Taylor's Theorem
- Density Separability and Convolution in Lᵖ
- Determinants of Matrices over a Commutative Ring
- Differentiation of Monotone Functions and the Vitali Covering Theorem
- Distributions Test Functions and Differentiation
- Divisibility, Euclidean Domains, Principal Ideal Domains and Unique Factorisation
- Divisibility, Greatest Common Divisors and Bézout's Identity
- Dual Spaces Adjoint Operators and Annihilators
- Dual Spaces, Bilinear and Quadratic Forms, and Sylvester's Law of Inertia
- Eigenvalues, Eigenvectors and the Characteristic Polynomial
- Em Elementary Mathematical Prerequisites
- Em Expanded Analysis Prerequisites
- Equivalent Forms of Completeness
- Euclidean Surface Measure, Divergence, and Green Identities
- Filters and Ultrafilters
- Finite Counting, Factorials and Binomial Coefficients
- Finite Dimensional Normed Spaces and Riesz Lemma
- Finite Probability and the Probabilistic Method
- Foundations of the Real Numbers for Analysis
- Fourier Multipliers and Sobolev Characterisations
- Fourier Transform Convolution and Approximate Identities
- Fredholm Elliptic Problems and the Elliptic Spectrum
- Fubini and Change of Variables
- Function Space Topologies and the Exponential Law
- Fundamental Solutions Newtonian Potentials and Green Functions
- Fundamental Trigonometric Identities
- Further Trigonometric Identities and Inverse Functions
- Gaussian Elimination, Elementary Matrices and Reduced Row Echelon Form
- Geometric Hahn Banach and Convex Separation
- Goursat's Theorem and Cauchy's Theorem in a Convex Domain
- Group Actions, Orbits, Stabilisers and Cayley's Theorem
- Harmonic Functions and Mean Values in Rn
- Hausdorff via the Diagonal
- Hereditary and Productive Behaviour of the Separation Axioms
- Hilbert Space Geometry and Riesz Representation
- Ideals, Quotient Rings and the Isomorphism Theorems for Rings
- Improper and Parameter-Dependent Multiple Integrals
- Improper Integrals
- Inner Product Spaces, Gram-Schmidt, Projections and Adjoints
- Interior and Boundary Sobolev Elliptic Regularity
- Lax--Milgram and Weak Elliptic Solutions
- Lebesgue Measure on Euclidean Space
- Limits of Real Functions
- limsup, liminf, and Subsequential Limits
- Line Integrals and the Gradient Theorem
- Linear Algebra Methods in Combinatorics
- Linear Independence, Bases and Dimension
- Linear Transformations, Rank-Nullity and Quotient Spaces
- Matrices, the Matrix of a Linear Map, and Change of Basis
- Maximum Principles Harnack and Liouville in Rn
- Measurable Functions and Simple Approximation
- Measures and Their Basic Properties
- Metric Spaces
- Minkowski Theory and Number Field Class Groups
- Mixed Partials, Taylor Formulae, and Extrema
- Modes of Convergence Egorov and Lusin
- Monotone Functions, Discontinuities, and Continuity Sets
- Monotone Sequences, Bolzano-Weierstrass, and Cauchy Completeness
- Normal Subgroups and Quotient Groups
- Normed and Banach Spaces
- Norming and Separation under Hahn–Banach
- Order, Zorn's Lemma, and the Axiom of Choice
- Orthonormal Bases, Parseval and Fourier Series
- Outer Measure and the Caratheodory Extension Theorem
- Partitions of Unity and Paracompactness
- pi: the Equivalent Characterizations
- Picard-Lindelöf and First-Order Ordinary Differential Equations
- Poisson Problems and Interior Harmonic Estimates
- Poisson Summation Sampling and Lattice Duality
- Polynomial Rings, the Division Algorithm and Roots
- Power Series and Real-Analytic Functions
- Product Measures and the Fubini Tonelli Theorems
- Projective Algebraic Sets Projective Morphisms and Cones
- Properties of the Integral and the Working FTC
- Radon Measures and the Riesz Markov Kakutani Theorem
- Rank Theorems and Embedded Submanifolds
- Rees Modules Artin Rees and Hilbert Samuel Theory
- Reflexivity and Eberlein Smulian
- Regular Surfaces and Surface Integrals
- Relations, Functions, and Quotients
- Rellich Kondrachov and Sobolev Compactness
- Rings, Subrings, Integral Domains and Fields
- Rⁿ as a Normed Space; Vector-Valued Functions
- Roots, Rational Powers, and Classical Inequalities
- Schwartz Space and the Plancherel Theorem
- Separation Axioms: the Hierarchy
- Sequences and Limits
- Sequences and Series of Functions; Uniform Convergence
- Series: Convergence and the Nonnegative Tests
- Sigma Algebras and Borel Sets
- Signed and Complex Measures Hahn and Jordan
- Simple Field Extensions and the Construction of the Complex Numbers
- Sine, Cosine, and the Definition of Pi
- Smooth Approximation and Sobolev Extension
- Smooth Manifolds and Smooth Maps
- Smooth Partitions of Unity and Exhaustions
- Smooth Vector Bundles and Sections
- Sobolev Poincare and Morrey Inequalities
- Sobolev Traces and Zero Boundary Values
- Stone–Weierstrass in General
- Subspaces, Products, and Quotients
- Suprema and Infima
- Symmetric Groups, Cycle Decomposition and the Sign Homomorphism
- Tangent Cotangent and the Differential
- Tempered Distributions and the Fourier Transform
- The Analytic Hahn Banach Theorem
- The Ascoli–Arzelà Theorem
- The Baire Principles of Functional Analysis
- The Cantor Set, Baire Category, and Measure Zero in ℝ
- The Complex Exponential and Euler's Formula
- The Derivative and the Mean Value Theorems
- The Determinant of a Linear Operator, Cofactors and Cramer's Rule
- The Divergence Theorem and Classical Stokes
- The Duality of Lᵖ and L^q
- The Exponential Function
- The Fundamental Group of the Circle
- The Fundamental Theorems of Calculus
- The Identity Theorem, the Maximum Principle and the Open Mapping Theorem
- The Inverse and Implicit Function Theorems
- The Inverse Function Theorem Completed
- The Lebesgue and Riemann Integrals Compared
- The Lebesgue Integral and the Convergence Theorems
- The Logarithm and General Powers
- The Lᵖ Spaces Holder Minkowski and Riesz Fischer
- The Maximal Function and Lebesgue Differentiation
- The Radon Nikodym Theorem and Lebesgue Decomposition
- The Real Gamma and Beta Functions
- The Riemann Integral in Rᵐ and Jordan Content
- The Riemann Integral: Definition and Integrability
- The Topology of Euclidean Space
- The Total Derivative in ℝᵐ → ℝⁿ
- The ZFC Axioms and the Basic Set Constructions
- Topological Spaces and Continuity
- Topology of ℝ
- Triangularisation, Generalised Eigenspaces and Jordan Canonical Form
- Uniform Spaces: the Three Definitions
- Vector Spaces, Linear Subspaces, Span and Direct Sums
- Volumes of Elementary Solids and Solids of Revolution
- Weak Derivatives and Sobolev Spaces
- Whitney Embedding Tubular Neighbourhoods and Approximation
2 · Summary
This page supplies the mathematical boundary and spectral toolkit that the
electromagnetism track consumes: the Carleman and unique-continuation
prerequisites of the exterior uniqueness arguments, the exterior spherical
multipole basis and the ball boundary series, the exterior scalar and vector
Helmholtz problems with modal outgoing radiation, the smooth-domain elliptic
boundary-value conclusions with their piecewise-interface variant, and the PEC
cavity and rectangular spectral completeness statements. Everything here
carries domain: mathematics, depends only on mathematical suppliers, and is
used by consuming physical items as a stated mathematical premise; no physical
charge interpretation, field identification or empirical claim is made on this
page, and the physical reading of every quantity stays with the consuming
electromagnetism pages.
Under Countable Choice, the page opens with Three-dimensional radial Carleman inequality with integer weight, a singular-weight estimate in three dimensions: for every integer with the inequality holds for compactly supported smooth functions away from the origin and extends to functions supported in a fixed annulus. Under Countable Choice, Weak unique continuation for bounded potentials in three dimensions then propagates the vanishing of an solution of , with locally essentially bounded, from a nonempty open set to the whole connected domain; no sign, smoothness or decay of the potential is assumed.
Exterior spherical multipole expansion and the ball boundary series develops the exterior multipole expansion of the Newtonian integral of a compactly supported density, including its uniform tail bound, its termwise differentiability, and the ball boundary branch in which the harmonic series is the unique finite--supremum harmonic function with the given boundary data. Uniqueness of the outgoing exterior scalar Helmholtz solution with Dirichlet data and Existence and uniqueness for the exterior vector Helmholtz problem with prescribed tangential trace and outgoing radiation then solve the exterior Helmholtz problems, under their stated Axiom of Choice, positive wavenumber and connected smooth-exterior hypotheses, in the modal outgoing class of the sphere Dirichlet-to-Neumann map: the homogeneous scalar Dirichlet problem has only the zero solution, and for every smooth tangential datum the vector problem with , prescribed tangential trace and the accompanying normal closure relation has exactly one classical solution.
Weak and classical solvability of the elliptic boundary problems with Dirichlet, Neumann and transmission data records the weak and classical solvability, under its stated Axiom of Choice, of the Dirichlet, Neumann and transmission problems for a uniformly positive smooth coefficient on a bounded smooth domain, with the exact trace, the componentwise compatibility and normalisation of the Neumann problem, and the explicit exclusion of edge, junction, reentrant and non-smooth regimes. Finally, Spectral completeness of the declared PEC waveguide and cavity classes states the spectral completeness, under its stated Axiom of Choice, of the declared smooth PEC cavity class, with a complete orthonormal eigenbasis of the curl form, eigenfields and the modal second-order wave expansion with an abstract positive speed, together with the rectangular reflection-parity energy class.
The companion page em-boundary-and-spectral-prerequisites-examples records three explicit mathematical checks of hypotheses and conventions of these results: the incompatible sphere conditions, the piecewise-constant coefficient witness that blocks a global conclusion, and the same witness as a hypothesis boundary for the smooth-domain spectral class.
3 · Logical flowchart
4 · Definitions, postulates, theorems and proofs
Three-dimensional radial Carleman inequality with integer weight
Statement
Assume the Axiom of Countable Choice (), in the exact meaning of The Axiom of Countable Choice (). Let be an integer and put . Write for and let be the Euclidean Laplacian (The Laplacian of a function and of a vector field). Then for every , Moreover, if is compactly supported in an annulus , then the weak second derivatives of exist as locally square integrable functions, denotes their sum in the weak sense (Weak derivative of a locally integrable function, Integer-order Sobolev spaces and their norms), and the same inequality holds for . The weights and are bounded on every fixed compact annulus with , and this boundedness on the support of the function is the only property of the weights used in the density extension below; the weight is unbounded at the origin for every , and the weight is unbounded at the origin for every and equals the constant for . That is why the extension is stated for functions whose support stays away from . The constant is explicit and is not claimed to be sharp.
Facts & Assumptions
Given: The Axiom of Countable Choice (The Axiom of Countable Choice ()); an integer with ; first a function , later a class compactly supported in .
Polar coordinates: for every Borel measurable , , where is the polar surface measure on (Polar coordinates decompose Lebesgue measure into r^{n-1} dr d sigma).
One-dimensional substitution with the absolute derivative: if is and injective with nonvanishing derivative on a neighbourhood of and is continuous on an interval containing , then (In one dimension the compact-Jordan formula is substitution over the unoriented image interval with the absolute derivative).
The Laplacian is (The Laplacian of a function and of a vector field), the divergence and gradient are the coordinate operators of Divergence and curl of a vector field, and for data (Divergence and curl are linear and satisfy the scalar product rules).
Coordinate differentiation of the composites below uses the chain rule for total derivatives and the sum, scalar and product rules (The chain rule for total derivatives: , Sums, scalar multiples, products and quotients: , , , and when ).
Spherical harmonics: the space of homogeneous harmonic polynomials of degree on has dimension , harmonics of distinct degrees are orthogonal in for the unnormalised surface measure of total mass , and the union over of their restrictions to admits a complete orthonormal basis of (Spherical harmonics: orthogonal decomposition, complete basis and addition theorem).
Parseval for a complete orthonormal family: a family is complete if and only if for every , the sum being the supremum of finite subsums (Parseval equivalences for an orthonormal family).
Fourier calculus in the convention: Plancherel's theorem makes the Fourier transform a unitary isometry of , and (Plancherel theorem, Fourier differentiation and multiplication identities on tempered distributions).
Tonelli's theorem: for a nonnegative measurable function on a -finite product space the iterated integrals agree; the counting measure on is -finite (Tonelli's theorem for nonnegative measurable functions on a sigma-finite product).
Between concentric balls there is a smooth bump equal to on with support in (A smooth bump between concentric Euclidean balls).
Under Countable Choice, is dense in in the Sobolev norm (Compactly supported smooth functions are dense in W^{k,p}(R^n)).
Weak Leibniz rule with a smooth factor: for smooth with bounded derivatives through order and , the product belongs to with for every , and the weak derivatives are the almost-everywhere classes of these sums (Weak Leibniz rule with a smooth factor).
Weak derivatives and Sobolev spaces: the weak derivative is defined by the signed test identity, and consists of classes whose weak derivatives of every order at most are classes (Weak derivative of a locally integrable function, Integer-order Sobolev spaces and their norms).
First Green identity on a bounded domain: for real and , under Countable Choice (First Green identity); complex identities follow by real and imaginary parts.
Choice accounting. Countable Choice is used through [L10] (whose density statement carries it) and through [L6] and [L7] (the Parseval and Plancherel suppliers carry it); the coordinate computations, the polar-coordinate identity and the modal summation consume nothing beyond those suppliers.
Proof
Given: The Axiom of Countable Choice, an integer with , and first a smooth compactly supported on .
Change of variables. Assume first . The map is a diffeomorphism of onto ; since is smooth and compactly supported away from the origin, the functions and are smooth and is compactly supported in uniformly in . By [L1] with the substitution , whose derivative is supplied by [L2], the measure becomes ; writing gives because . Hence .
Spherical Laplacian and the polar form of . For let be its degree-zero homogeneous extension to and define for . This is well defined: by the chain rule, for every and every function on , while ; hence , and does not depend on , so the value at defines a function of alone. Define , which is tangent because ; for a smooth tangential field on , define with . For the product rule gives , and ; using [L3] twice and the direct computation , so that , the last step using . In particular, for a harmonic homogeneous polynomial of degree and , the identity with and gives , hence . The same computation applied to a general with , whose gradient splits as into radial and tangential parts, gives the general polar form ; the divergence of a tangential field with is in these coordinates, and .
The conjugated operator. Apply the polar form of step 1.2 to , , whose radial part is . Coordinate differentiation by [L4] gives and , so while . Hence Substituting gives and , so with one has
Modal decomposition. For almost every the function is smooth on , hence in , and by [L5] it expands as in a complete orthonormal basis of degree- spherical harmonics, the coefficients being smooth in . For complex-valued , apply the real harmonic basis expansion to its real and imaginary parts and combine the coefficients; orthogonality then gives the same complex expansion and absolute-square Parseval identity. By step 1.2, each satisfies , and is symmetric for the surface pairing: extend two smooth sphere functions homogeneously with degree zero to the annulus . Their normal derivatives vanish on both boundary spheres. Subtracting the two first Green identities [L13] gives ; using and polar coordinates [L1], the radial factor is , so . Applying this to the real and imaginary parts of and to gives the modal identity without any unproved surface integration formula, so the coefficients of against are exactly ; hence since . Parseval for the complete family at each [L6] and Tonelli's theorem against the counting measure on the index set [L8] give all terms being nonnegative; each is smooth and compactly supported on , and is its second derivative combination, again compactly supported and square integrable.
Fourier multiplier bound, mode by mode. Fix . In the convention of [L7], the distributional Fourier transform of is the bounded continuous function with symbol , and Plancherel gives . Put , and . Then and , so For integers and one has : on the range , nonempty only for , the function is decreasing, so ; at and the values are and ; and on the range one has . Since for every , conclude for all , and therefore
The weighted right-hand side. Combining step 2.1 with the measure identity of step 1.1 gives because ; hence
Summation. Squaring the mode-wise inequality of step 2.3, summing over all and inserting the two identities of step 2.2 and step 3.1 yields which is the asserted inequality after taking square roots. Both sides are finite because is compactly supported in an annulus on which the two weights are bounded.
Density extension to functions supported in an annulus. Now let be compactly supported in , so its weak derivatives through order two exist as locally square integrable functions and is their weak sum [L12]. By [L9] fix with on and , and put ; then is smooth, on , outside , and because on a neighbourhood of . By [L10] choose with in ; then with in , because the weak Leibniz expansion of [L11] through order two bounds by a constant times , and likewise in . Every and every is supported in , as is because weak derivatives of a class supported in are supported there, and on the weights and are bounded by and by (the exponent ). Applying step 4.1 to each and passing to the limit in gives , and the weak derivatives and weak Laplacian of are those named in the statement.
Weak unique continuation for bounded potentials in three dimensions
Statement
Assume the Axiom of Countable Choice (). Let be nonempty, open and connected, let , and let satisfy in the distributional sense: for every , with the classical Laplacian. Here denotes the locally integrable classes on whose weak derivatives of every order at most two exist and are locally square integrable (Weak derivative of a locally integrable function, Integer-order Sobolev spaces and their norms); means that is measurable and that on every compact subset, with the essential supremum of The essential supremum of a measurable function with respect to a measure and the space of The space of essentially bounded measurable functions. If on a nonempty open subset of , then on . No smoothness, sign, symmetry or decay hypothesis on beyond local essential boundedness is used, and no analyticity is assumed.
Facts & Assumptions
Given: The Axiom of Countable Choice (The Axiom of Countable Choice ()); a nonempty open connected ; ; with in the distributional sense; and a nonempty open on which vanishes.
Radial Carleman lemma: for every integer with and every compactly supported in an annulus , the weak Laplacian exists as a locally square integrable function and (Three-dimensional radial Carleman inequality with integer weight).
Bumps: for there is a smooth equal to on with support in (A smooth bump between concentric Euclidean balls).
Weak Leibniz rule: for and , the product is in and for every , the derivatives being the locally integrable weak derivatives (Weak Leibniz rule with a smooth factor).
Weak derivatives are defined by the signed test identity and consists of classes with weak derivatives of order at most two in ; is the corresponding local class (Weak derivative of a locally integrable function, Integer-order Sobolev spaces and their norms).
Essential supremum and : , is the set of measurable with , and if then almost everywhere (The essential supremum of a measurable function with respect to a measure, The space of essentially bounded measurable functions, The essential supremum is attained as the least essential bound).
Connectedness: a separation of a topological space is an ordered pair of nonempty disjoint open sets with union the whole space, and the space is connected when no separation exists; equivalently a connected space has no nonempty proper clopen subset (Separation of a topological space, connected and disconnected spaces, clopen sets, and connected subsets).
is countable and dense in , and the open boxes with rational form a countable basis for the topology of , which coincides with the Euclidean metric topology ( is a countable dense subset of , and rational open boxes form a countable basis, For the product topology on copies of the usual topology of is the metric topology of on , and hence also of and , so as a product and as a metric space are one space, For all norms on are equivalent).
Null sets and almost everywhere: a measurable set is null if its measure is zero, and a property holds almost everywhere if its exceptional set is contained in a null set (Measure-null sets and almost-everywhere statements relative to a measure).
Countable subadditivity: for a sequence of measurable sets, (Finite and countable subadditivity of measures).
Smoothness: mean continuous partial derivatives through order and means for every ( Euclidean maps and diffeomorphisms); in particular a cutoff is , so its classical Laplacian is defined.
Metric topology: is open in a metric space exactly when every has some with the metric ball contained in , and closed means open complement (The metric topology: a set is open when every one of its points has a ball around it inside the set; closed means open complement, Open ball, closed ball and sphere in a metric space).
Choice accounting. Countable Choice is inherited through [L1], which is a supplier carrying that assumption; the weak Leibniz and Sobolev interfaces [L3]–[L4] also carry Countable Choice. The localization, absorption, zero-set and counting arguments below use no further choice principle.
Proof
Given: The Axiom of Countable Choice, a nonempty open connected , , an solution of distributionally, and on a nonempty open .
Localization at a zero point. Fix and choose with and with (both possible by [L11]); translate so that . Choose with on [L2] and set . Since and is smooth with compact support in , the weak Leibniz rule [L3] through order two shows that , extended by zero, lies in with weak Laplacian the square integrable function ; the hypothesis that holds distributionally says exactly that the distribution is the regular distribution of the locally integrable function , so testing this identity against for arbitrary gives , and is so its classical Laplacian is defined [L10]. Thus as classes with , and is supported in the annulus because , hence , on . Finally almost everywhere on , so is compactly supported in the annulus .
Carleman estimate with the potential split. Let be the essential supremum of over with respect to Lebesgue measure [L5]; it is finite because is compactly contained in and , and by [L5] one has almost everywhere on . Applying [L1] to with parameter , , and using together with on the support of , one has and therefore .
Absorption and the inner-ball bound. For every integer the factor satisfies , so absorbing the first term in the estimate of step 2.1 gives ; since is supported in where (the exponent ), this yields . For every one has almost everywhere on (because on ) and there, so .
Limit and local propagation. For fixed the bound of step 3.1 tends to as the integer , because is fixed by the localization of step 1.1, and ; hence almost everywhere on for every . Since is the countable union of the positive-radius balls , , and a countable union of null sets is null by [L8] and [L9], it follows that almost everywhere on . Restated without the translation: if has a neighbourhood on which vanishes almost everywhere and satisfies , then almost everywhere on .
The zero set is open in and carries no mass. Let . Then is open and nonempty (it contains ), and almost everywhere on : for each point of some open zero neighbourhood exists by the definition of , and [L7] supplies a rational box contained in it and containing that point. Consider the entire subfamily of the fixed countable rational-box basis consisting of boxes on which almost everywhere. Its union equals : every is an open zero neighbourhood, and every point of lies in such a box. For a fixed measurable representative, each exceptional set is null; the union over this countable subfamily is null by [L8] and [L9]. Thus almost everywhere on , without selecting a box or radius simultaneously for an uncountable family of points.
is open. Let and choose with : [L11] gives with , and , so qualifies. If some existed, then ; every satisfies , so , and step 4.1 would give almost everywhere on ; since , the point lies in that ball, so would have a neighbourhood on which vanishes almost everywhere, contradicting . Hence , and is open.
Conclusion. The sets and are disjoint, open, and their union is , and is nonempty; since is connected [L6], no separation of exists, so and . By step 5.1, almost everywhere on , which is the class statement on .
Exterior spherical multipole expansion and the ball boundary series
Statement
Assume Countable Choice (), with the exact meaning of The Axiom of Countable Choice (). Let and let vanish outside . Use the complete orthonormal basis of real spherical harmonics on with unnormalised surface measure of total mass and the addition theorem of Spherical harmonics: orthogonal decomposition, complete basis and addition theorem, and the Legendre generating kernel and its compact remainder bound from Legendre polynomials from a convergent zonal kernel: generating function and exterior expansion. Write , , . Then:
(a) Exterior multipole expansion. For every with , the series converging absolutely and uniformly on for every , with tail after degree bounded by ; for every fixed , the degree- term is the angular projection of onto the degree- harmonics. This function is continuous and bounded by , so it is in ; no sphere trace or property of the volume density is asserted. The degree-zero and degree-one terms are the Coulomb and dipole terms with the explicit remainder bound of Monopole-dipole expansion with an explicit remainder for compactly supported densities (, , for ).
(b) Termwise differentiation. On every compact with the series may be differentiated termwise to every order, the differentiated series converging uniformly on ; in particular the potential is on .
(c) Ball boundary branch. For with coefficients the series converges in as and, with all derivatives, uniformly on each closed ball of radius , is harmonic on the open unit ball, and is the unique harmonic function there with a finite and boundary limit ; for continuous it equals the Poisson integral of and extends continuously to the closed ball with boundary values .
This is a statement about the Newtonian integral of a compactly supported density and about harmonic functions; no physical charge distribution or electrostatic interpretation is asserted. In every coefficient integral the factor is defined at by its homogeneous polynomial extension: zero for and the constant degree-zero harmonic for . This is a finite assignment, and changing its value at that null singleton changes no integral.
Facts & Assumptions
Given: Countable Choice; ; a density vanishing outside ; the complete orthonormal basis of real spherical harmonics with unnormalised surface measure of total mass ; and the notation , , , with the Euclidean inner product of The Euclidean inner product on .
Legendre kernel and its consequences: is a real polynomial with on , , ; for ; for , with the remainder after degree bounded by uniformly on ; the coefficient terms , extended at by and for , are smooth and harmonic on , and on an observation compact set disjoint from every fixed spatial derivative series converges uniformly (Legendre polynomials from a convergent zonal kernel: generating function and exterior expansion).
Spherical harmonics and addition: the real homogeneous harmonic polynomials of degree on (every occurring monomial has total degree , the zero polynomial is included, and ) restricted to form a -dimensional space, distinct degrees are orthogonal for , the union admits the complete orthonormal basis , and ; in particular (Spherical harmonics: orthogonal decomposition, complete basis and addition theorem).
The ball boundary branch: for with coefficients , the series , , and all its derivatives converge uniformly on every closed smaller ball, is harmonic, in as , is the unique harmonic function with and boundary limit , and for continuous it equals with continuous extension to the closed ball (Ball Poisson series: interior convergence, boundary data and the Poisson kernel).
Coulomb–dipole splitting: with and , for , with (Monopole-dipole expansion with an explicit remainder for compactly supported densities).
Cauchy–Schwarz: (Cauchy-Schwarz inequality for ).
Monotonicity and scalar rules for nonnegative integrals: pointwise implies , and for (Monotonicity and nonnegative homogeneity of the nonnegative integral).
Orthonormal families and orthonormal bases: an orthonormal family has , and a complete orthonormal system has closed linear span the whole Hilbert space (Orthonormal families, complete orthonormal systems and Hilbert bases).
Interior derivative estimates for harmonic functions: on a ball of radius contained in the harmonicity domain, , so derivatives on a compact set are controlled by the supremum on a slightly larger compact set (Interior derivative estimates for harmonic functions).
Newton–Leibniz with interior derivative: a continuous function with continuous coordinate derivative on an interval differs from a primitive of by a constant; applied along coordinate segments this identifies uniform derivative limits with derivatives of the limit (Newton–Leibniz needs only continuity on , differentiability on , and a Riemann-integrable extension of the interior derivative).
Smoothness: maps have continuous partial derivatives through order , and means for every ( Euclidean maps and diffeomorphisms).
Choice accounting. Countable Choice is assumed in the Statement and is carried by the spherical-harmonic and ball-series suppliers [L2]–[L3]; the measure-theoretic integrations and the differentiation argument introduce no further choice.
Proof
Given: Countable Choice, , supported in , the orthonormal spherical-harmonic basis and the Legendre kernel.
Zonal expansion with uniform tail. Fix with and let . By [L1] the kernel expansion converges absolutely and uniformly for (the term at being read by the stated homogeneous extension), and its remainder after degree is bounded by ; multiplying by the density and integrating, the uniform bound gives , so , the zonal series converging absolutely and, for every , uniformly on with the stated tail bound .
Ball boundary branch. Part (c) of the Statement is exactly [L3]: the series and all its derivatives converge uniformly on each closed smaller ball, is harmonic, in , uniqueness holds in the class with finite radial supremum, and for continuous the Poisson representation and the continuous extension to the closed ball hold.
Spherical form, absolute convergence and the degree tail. For the addition theorem [L2] gives . For each put , a finite integral because is bounded on and ; then by [L2] and [L5], and by the monotonicity rule [L6] applied to the absolute values, so the degree- contribution of the spherical series is bounded in modulus by and the series converges absolutely, with degree tail after bounded by . Substituting the addition theorem degree by degree into step 1.1 gives, for every , the equality of the truncated zonal and spherical sums, and both truncations converge to the same limit by step 1.1 and this bound; this proves the expansion of part (a) and its uniform convergence on .
The degree- term is the angular projection. Fix and put . Then for every , and is continuous: for and , the reverse triangle inequality gives , while both denominators are at least ; hence , proving continuity directly. Hence with . By step 2.1 the spherical series for converges uniformly on the compact sphere , so the pairing with each basis element may be taken termwise and by the orthonormality of the basis [L7]; this is precisely the stated angular projection.
Coulomb and dipole identification. Summing the degree- spherical term over and using the addition theorem in reverse gives , the zonal degree term computed in step 1.1, and it is the degree- term of the spherical series of step 2.1. Since and [L1], the degrees and contribute and ; the remaining tail is , and for the explicit remainder bound of [L4] applies to it, so the degree-zero and degree-one terms are the Coulomb and dipole terms of the Statement.
Termwise differentiation. Each degree term is , with the full weighted coefficient of [L1]. For fixed , its polynomial extension in is smooth jointly for , including , and harmonic in by [L1]. On a compact observation neighbourhood times its spatial derivatives are uniformly continuous and bounded. By [L9] along coordinate segments, for each such derivative its difference quotient converges uniformly in to ; integrating the error bounds it by times that uniform error. Induction therefore gives , continuous by the same uniform bounds, and . For a nonempty compact in choose nested compact neighbourhoods and a fixed such that for every . The harmonic partial sums converge uniformly on by step 2.1. Hence [L8] applied to gives for every multi-index . The derivative limits are uniform and continuous on . Apply [L9] to on short coordinate segments in and pass to the uniform limits in the integral identity; this identifies the limit of with the corresponding derivative of the limit of . Induction proves termwise differentiation to every order on , with smooth in the sense of [L10]. The empty compact case is vacuous.
Assembly. Part (a) is steps 1.1, 2.1, 3.1 and 3.2 (expansion, uniform tail, angular projection and Coulomb–dipole identification); part (b) is step 3.3; part (c) is step 1.2; the statement about the value at is the finite-assignment convention recorded in the Statement, which leaves every integral unchanged because a singleton is null. This proves all three parts.
Uniqueness of the outgoing exterior scalar Helmholtz solution with Dirichlet data
Statement
Assume the Axiom of Choice inherited from the modal DtN/trace suppliers, covering the Countable Choice used by the local UCP supplier. Let be a bounded open set with boundary (Bounded C^k domains and boundary charts) whose exterior is connected, let , and let with . Suppose is on , solves on with the Euclidean Laplacian (The Laplacian of a function and of a vector field), vanishes on , and is outgoing in the class of Outgoing spherical trace and Dirichlet-to-Neumann map: its trace lies in and its normal derivative on is in the weak trace sense of that lemma. Then on . No decay rate, asymptotic expansion or pointwise Sommerfeld formula beyond the stated outgoing class is assumed.
Facts & Assumptions
Given: The Axiom of Choice (The Axiom of Choice); a bounded obstacle with connected exterior ; ; with ; and a solution of on , vanishing on , outgoing in the modal class of the sphere DtN lemma, with trace and normal derivative .
First Green identity on a bounded domain: for real and , (First Green identity).
The Laplacian is (The Laplacian of a function and of a vector field).
Bounded domains have the local graph property, so is a bounded domain whose boundary is the disjoint union of the smooth pieces and (Bounded C^k domains and boundary charts).
Sphere DtN lemma: for the map is bounded with and for ; the function , , is the unique outgoing finite-local-energy exterior solution with trace on and normal derivative in the weak trace sense (Outgoing spherical trace and Dirichlet-to-Neumann map).
Bounded-potential unique continuation: for nonempty open connected , and with distributionally, vanishing of on a nonempty open subset of forces on (Weak unique continuation for bounded potentials in three dimensions).
Choice accounting. The Axiom of Choice is assumed in the Statement and is carried by the DtN/trace supplier [L4]; the local unique-continuation supplier [L5] carries Countable Choice, which AC supplies. The Green-identity, positivity and propagation steps below introduce no further choice.
Proof
Given: The data and solution of the Given paragraph above.
Green's identity on the truncated exterior and vanishing of the imaginary boundary pairing. The truncated region is a bounded open set whose boundary is the disjoint union of and , with the outward normal of equal to the outer normal of and to the inward normal of [L3]. Write with real smooth . Applying [L1] to and and adding gives , because and . For the imaginary part, apply [L1] to and and subtract: the volume integrand is , and the boundary integrand is . Thus the FULL complex identity is . The inner boundary contributes zero because on , so . Since on in the weak trace sense of [L4] and , the last identity is the vanishing of the imaginary part of the dual pairing, .
The boundary trace vanishes. By [L4] the imaginary pairing of the DtN operator is with every coefficient . Since the left side is zero by step 1.1 and every term of the sum is nonnegative, every coefficient vanishes, so ; consequently also and, by the trace identity of [L4], .
Vanishing on the exterior of the large sphere. Restricted to , the field is an outgoing finite-local-energy solution of the Helmholtz equation with trace on and normal derivative : is on the closed region , hence in every , and its trace and weak normal derivative on are the ones named in the statement. By the uniqueness clause of [L4] there is exactly one such solution, namely the outgoing series with coefficients ; hence on . The set is a nonempty open subset of because is bounded, so vanishes on the nonempty open set .
Unique continuation on . The real and imaginary parts of are on , hence in , and satisfy on because ; the coefficient lies in and is nonempty, open and connected. By step 3.1 each of them vanishes on the nonempty open subset , so [L5] applied to and on gives on , that is, on , as asserted.
Existence and uniqueness for the exterior vector Helmholtz problem with prescribed tangential trace and outgoing radiation
Statement
Assume the Axiom of Choice, as used by the variational, Sobolev and compact-spectral suppliers and by the Fredholm alternative (The Axiom of Choice). Let be a bounded open set with boundary (Bounded C^k domains and boundary charts) whose exterior is connected, let , and let with . Write and let be the outward unit normal field of , so that on the field points into ; extend to a smooth normal collar by , so , using The Euclidean tubular neighbourhood theorem; put and, for a field on , .
For smooth in boundary charts and satisfying , put where is any smooth extension of to a neighbourhood of ; the expression is independent of the extension and equals the surface divergence of with respect to the Euclidean surface measure of . Write for the Euclidean Laplacian (The Laplacian of a function and of a vector field), acting componentwise, and for a vector field on write with the scalar Dirichlet-to-Neumann map of Outgoing spherical trace and Dirichlet-to-Neumann map.
Then there is exactly one field with which is outgoing on the sphere in the modal sense of that lemma: its trace lies in and the normal derivative of on equals componentwise in the weak trace sense of the sphere DtN lemma. With these data the normal boundary values of on satisfy the closure relation as an identity of functions on . No scalar Dirichlet condition is imposed on the three Cartesian components of , and no decay rate, asymptotic expansion or pointwise Sommerfeld formula beyond the stated modal outgoing class is assumed.
Facts & Assumptions
Given: The Axiom of Choice (The Axiom of Choice); a bounded obstacle with connected exterior ; ; with ; the truncated annulus with outward unit normal and ; a smooth -valued tangential field on ; the conventions of the fields , , explained in the Statement, and the notation , of Integer-order Sobolev spaces and their norms.
Sphere Dirichlet-to-Neumann lemma: for the map is bounded with and for ; for every the outgoing series , , is the unique outgoing finite-local-energy exterior solution with trace on and normal derivative in the weak trace sense; it is smooth away from the sphere, and for smooth it satisfies the ordinary Sommerfeld condition (Outgoing spherical trace and Dirichlet-to-Neumann map).
Exterior scalar uniqueness: if has bounded boundary, is connected, , solves on , vanishes on and is outgoing in the class of [L1], then on (Uniqueness of the outgoing exterior scalar Helmholtz solution with Dirichlet data).
Weak prescribed-trace Dirichlet existence: under the adopted Axiom of Choice, for a bounded domain , a measurable symmetric real matrix field satisfying for a.e. and every , with , and , there is exactly one with trace solving for all , with (Weak Dirichlet problem with prescribed fractional Sobolev boundary data).
Smooth-domain elliptic regularity: under the adopted Axiom of Choice, on a bounded domain with a smooth real symmetric matrix field satisfying the uniform bounds of [L3] and smooth on the closure, the weak solution with smooth Dirichlet data is on the closure and satisfies the classical equation and boundary values (Classical smoothness of weak Poisson solutions on smooth domains and across smooth interfaces).
Bounded-potential unique continuation: for nonempty open connected , and with distributionally, vanishing of on a nonempty open subset of forces on (Weak unique continuation for bounded potentials in three dimensions).
Interior regularity: if is a local weak solution of with , then (Interior regularity for divergence-form equations).
Interior regularity: if is a local weak solution of with , , then (Interior elliptic regularity).
Riesz representation: every bounded linear functional on a real or complex Hilbert space is represented by a unique vector (Riesz representation for Hilbert spaces).
Fredholm alternative: for a compact operator on a Banach space, is injective if and only if it is surjective, and in that case it is boundedly invertible (Fredholm alternative for identity minus compact).
Trace operator: on a bounded domain the trace is bounded and equals classical restriction on continuous Sobolev functions (The trace operator on a bounded domain).
Sobolev-Gauss-Green formula: for a bounded domain , and every , (The Gauss-Green integration-by-parts formula with Sobolev traces).
Half-space strip trace estimate: for smooth with compact support in the closed half-space and one has for a.e. and every (The half-space trace estimate and the half-space trace operator).
Extension theorem for bounded smooth domains: every bounded domain is a -extension domain (Bounded C^k domains admit integer-order Sobolev extension).
Subcritical Sobolev compactness: for a bounded extension domain and , every sequence bounded in has a subsequence converging in (The Rellich--Kondrachov theorem for on bounded extension domains).
Sequential compact-embedding criterion: under Countable and Dependent Choice, holds if and only if every bounded sequence in has a subsequence converging in (Compactly embedded normed spaces).
In ZF the Axiom of Choice implies the Axiom of Dependent Choice and the Axiom of Countable Choice (AC implies DC implies countable choice).
Difference quotients are (Difference quotients on a shrunken domain). Discrete integration by parts and shifted product rules hold on common localized domains, with no boundary remainder for tangential quotients on a half-space (Difference-quotient calculus: integration by parts, product rule, commutation). The increment estimate holds when the used segments stay in the enlarged domain, including tangential half-space directions (The difference-quotient characterisation of for ). Smooth cutoff commutators obey The cutoff difference-quotient commutator estimate.
Higher-order Sobolev embedding: on a bounded extension domain, membership with yields a representative on the closure, compatibly for different (Higher-order Sobolev embedding).
Cauchy-Schwarz: , and for , (Cauchy-Schwarz inequality for ).
Clairaut-Schwarz: mixed partial derivatives of a function commute (Clairaut--Schwarz theorem for continuous second partial derivatives).
Fractional trace and Sobolev completeness: on a bounded domain, is bounded (The sharp trace theorem: boundedness and range in the fractional space); the Sobolev space is complete (Integer-order Sobolev spaces are Banach), and with its integral inner product is a Hilbert space. Both assumptions are covered by the adopted Axiom of Choice.
Smooth ambient extension: if every derivative of a function has a continuous extension to the closure of a bounded smooth domain, the explicit extension operator, applied to a time-independent input, supplies one smooth ambient extension with all those boundary derivatives (A fixed smooth-domain extension that preserves smooth parameters).
The explicit outgoing solve the radial Helmholtz equation and do not vanish on positive real arguments (Spherical Hankel functions: explicit solutions, constant Wronskian and exact Dirichlet-to-Neumann bounds).
Homogeneous harmonic polynomials of degree restrict to the finite degree- spherical harmonic space with the complete orthonormal bases of Spherical harmonics: orthogonal decomposition, complete basis and addition theorem.
Under the stated Choice, the compact smooth boundary has a normal tubular neighbourhood whose normal-addition map is a diffeomorphism (The Euclidean tubular neighbourhood theorem); the normal extended constantly along its fibres has .
Choice accounting. The Axiom of Choice is assumed in the Statement. It supplies the Fredholm alternative [L9], the tensor/frame and Sobolev suppliers' own choice assumptions, and through [L16] the Countable and Dependent Choice used by the sequential compactness criterion [L15] and by the trace and difference-quotient interfaces of [L10], [L12] and [L17]. No other choice principle is used, and no choice is made in the explicit finite constructions below.
Proof
Given: The data and conventions of the Given paragraph above; in particular the truncated annulus , its outward unit normal , the coefficient on , and the smooth tangential field on .
The test space and the variational form. Define , the tangential part being taken with respect to the trace of on the smooth boundary component ; by the boundedness of the trace operator [L10] applied componentwise, is a closed subspace of the complex Hilbert space of [L21], hence complete. Define the sesquilinear form , where and uses the scalar DtN pairing of [L1] on the components. Then : the first two terms are bounded by Cauchy-Schwarz [L19]; the boundary term is bounded by by [L10]; and the last by the boundedness of [L1] combined with the exact fractional trace bound [L21] for functions on the smooth sphere .
Collar trace inequality on the inner boundary. For every there is such that every satisfies . Indeed, cover by finitely many flattening charts of the smooth boundary (Bounded C^k domains and boundary charts) and let be a smooth cutoff, equal to near and supported in the resulting collar. On the collar, in normal coordinates with proportional to the distance to , the strip estimate [L12] with , divided by and integrated over with the bounded chart Jacobians, gives for every smooth ; choosing so small that , expanding and absorbing the cutoff terms into yields the claim for smooth , and both sides are continuous in the norm (boundary term by [L10]), while products of global approximations with a fixed cutoff are dense in the classes supported in the collar by Compactly supported smooth functions are dense in W^{k,p}(R^n) and [L13]; the inequality therefore extends to all .
Smooth componentwise lift of the tangential datum. For let be the Cartesian components of and extend them by zero to , obtaining smooth functions . The domain is bounded and smooth, and is real symmetric with . Thus [L3] with , applied separately to the real and imaginary parts, there is a unique with trace and for all ; by [L4] with and the smooth Dirichlet data , each is on , is harmonic on , and . Hence is on , satisfies componentwise, and , and is tangential on .
Coercivity of the shifted form. With , where is the constant of step 1.2 for , one has for every , with . Indeed ; the last term is nonnegative by of [L1] applied componentwise to ; and the boundary term obeys by step 1.2 and [L19].
The shifted form is boundedly invertible. By the Riesz representation theorem [L8], applied to the bounded conjugate-linear functional on the complete space , the shifted form is represented by a bounded linear operator with and for constants (step 2.1 and step 1.1). Choose and put . For , by expanding the square and using [L19]; hence for every the iteration is a strict contraction of the complete space , so . The geometric tail estimate makes Cauchy; completeness supplies its limit , continuity gives and , and the same contraction inequality makes the fixed point unique. If then , so ; thus is boundedly invertible with .
The kernel of the form is trivial. Let satisfy for every . Taking and imaginary parts in step 2.1 gives , where ; by [L1] the imaginary pairing equals with , so every coefficient vanishes, on , and consequently . For every supported away from the identity has no inner-boundary contribution and reads ; in particular every , whose restriction to is an admissible test vanishing near , satisfies , and taking compactly supported in the interior of gives weakly on . Define on and on ; assign any value on the null sphere , so defines an class, and its only interface is the sphere , across which the full trace of the field is . For the Sobolev-Gauss-Green formula [L11] on the bounded domain , applied componentwise with and , gives ; the boundary term over vanishes because is compactly supported in , and the term over vanishes because there; hence , so the distributional gradient of is the field , , and the weak identity above gives . By [L6] each real and imaginary part of each component of lies in and satisfies distributionally; is nonempty, open and connected and on the nonempty open set , so [L5] gives on , in particular on .
Compactness of the pairing and the Fredholm reduction. Use the Riesz identification fixed in step 3.1 and let be the represented pairing, . A conjugate-linear functional in is represented here by applying [L8] to its complex conjugate and then conjugating the pairing, so this identification is linear in . The inclusion is continuous and is a bounded -extension domain [L13], so by [L14] with every bounded sequence in has an -convergent subsequence; by [L16] the Countable and Dependent Choice assumptions of the sequential criterion [L15] are available, so the inclusion is compact, and so is its restriction , hence also the composition of that restriction with the bounded represented pairing . Therefore is compact, and the operator represented by satisfies ; by the Fredholm alternative [L9] the operator is boundedly invertible as soon as its kernel is trivial, and its kernel consists exactly of the with for all .
Bounded invertibility of . By step 3.2 the kernel of is trivial, so the Fredholm alternative [L9] makes it boundedly invertible; hence and the form are boundedly invertible: for every bounded conjugate-linear functional on there is exactly one with for all , and .
The weak solution with prescribed tangential trace. Define on the functional . Both summands are bounded in : the first by step 1.1, the second because and is trace-continuous into by [L10], applied in the boundary charts. By step 5.1 there is exactly one with for all ; set . Then on because and is tangential there, and testing the defining identity with compactly supported in the interior of gives weakly on . Moreover, for every supported away from one has , so the same integration-by-parts computation as in step 3.2 shows that the normal trace of on equals in the weak trace sense, where .
Gluing across the artificial sphere and smoothness on the open set . Let be the outgoing series of [L1] built from the trace , defined on ; by [L1] it is a finite-local-energy solution there with normal derivative , and it is smooth away from the sphere. Define on and on . The two pieces have the same trace on ; applying the Sobolev-Gauss-Green formula [L11] on and on the exterior annulus (with the outward normals and on ) and adding, the two interface pairings cancel, so with weak gradient the two-sided gradient. For every test the weak equations on both sides then give : on this is the weak identity of step 6.1, on the exterior it is the weak Helmholtz equation satisfied by the outgoing series, and the interface terms have cancelled. Since for every as soon as , repeated application of the interior gain-two estimate [L7] starting from gives for every , hence a representative satisfying the classical Helmholtz equation on .
Homogeneous tangential traces before boundary localization. Put , with the smooth harmonic lift of step 1.3; by step 6.1, , so its tangential trace on is zero. Fix a smooth normal collar chart with coordinates , in , and a smooth orthonormal frame extended constantly along its normal lines. Write ; thus on the flat boundary. The weak identity for is . Since , integrating the smooth lift term by parts in a chart away from gives the smooth volume datum and normal boundary datum (the trace is zero and ). Transporting and localizing this identity by a cutoff gives, for every compactly localized test with on the flat boundary, The principal matrix is smooth, uniformly positive and scalar in , since ; is smooth and possibly signed; ; plus smooth lift/cutoff terms belongs to ; and times the localized cutoff is smooth. Tests are admissible: their first two components have zero trace, so odd reflection of those components and even reflection of the third, followed by parity-preserving mollification and cutoff, approximate them in ; pulling back the smooth frame and chart and extending by zero produces fields in . The difference-quotient tests below therefore act on , whose first two traces actually vanish, rather than on with its prescribed nonzero traces.
Tangential second derivatives and recovery of the normal derivatives. Let be a tangential direction, put and test the system of step 7.2 with on a nested pair of half-boxes; this test has on and compact support, so it is admissible. The discrete integration by parts of [L17] and the shifted product rule give a principal term bounded below by with the ellipticity constant of , while all remaining terms involve , , , , or the transferred quotients of , and are bounded by using [L17], the increment estimate , and [L19]. On the Robin term gives ; the trace estimate of step 1.2 (with the flattened ) absorbs the first term for either sign of , and bounded , the trace bound for and [L19] bound the second; the smooth datum contributes , bounded by and absorbed in the same way. Choosing the finitely many small gives uniformly in , hence every tangential second derivative of lies in after the limit argument in which the bounded functional is represented in by [L8]. From the interior equation one then recovers , whose right side is now and whose coefficient satisfies ; so all second derivatives of lie in on the smaller half-box, and a finite cover of the compact boundary gives up to and hence , since is smooth.
Higher-order bootstrap and the classical boundary conclusion. Suppose on the larger half-box for some ; the data of the local system then satisfy , each divergence datum and the lift-adjusted boundary datum is smooth because all coefficients are smooth. For a tangential multi-index of order put ; differentiating the system of step 7.2 by keeps the principal matrix and the Robin coefficient , and replaces the data by , and built from , and the finitely many commutator terms with , all known by the induction hypothesis; the tangential traces of are again zero in the first two components and free in the third, and localized tests for are admissible by the test approximation of step 7.2; the differentiated Robin commutators contain traces of tangential derivatives of of order at most , their tangential derivatives of one further order have traces because the corresponding interior derivatives of order at most belong to ; trace continuity and smooth approximation therefore place those commutators in by [L10]. Applying step 8.1 to gains two further tangential or mixed derivatives, and differentiating the normal-recovery equation of step 8.1 and inducting on the number of normal derivatives recovers the remaining ones; nested half-boxes and a finite boundary cover give on each smaller patch for every , with constants depending on the data, , the chart and the fixed nested covers. By the Sobolev embedding [L18] on a rounded bounded smooth subdomain of the chart that agrees with near the smaller patch and lies inside the larger half-box (hence an extension domain by [L13]) each class with has a representative on the closed patch, compatible for different ; hence , and therefore , has all derivatives continuous up to ; combining with the smooth gluing at , [L22] on the bounded annulus supplies one smooth ambient representative near its closure, and the classical integration by parts in the local frame (equivalently [L11] with classical traces) turns for admissible inner-collar tests into the boundary identities and on .
The divergence constraint. Let on . By step 9.1 and step 7.1, once the two-sided solution is matched at ; the mixed partials commute [L20], so on . On the exact boundary identity holds in the classical sense with the chosen normal extension, and its first two terms sum to by step 9.1 while the third equals ; hence on . To check outgoingness without assuming it for derivatives, let be the homogeneous harmonic polynomial of a single angular mode and set . Product differentiation gives and , so is harmonic of degree , while is harmonic of degree (zero when ), as in [L24]. Direct differentiation of the finite polynomial formula [L23] gives for and for . The Cartesian derivative therefore is for ; for only the first term occurs, since and . Expand these two harmonic polynomials in the finite bases of their degrees [L24]. The all-derivative convergence of [L1] justifies differentiation and angular projection on every annulus strictly outside ; a fixed output degree receives terms only from the two adjacent input degrees, so each radial coefficient of is a multiple of its outgoing , with no incoming partner. Since is smooth across , its coefficients and radial derivatives extend continuously to ; nonvanishing of [L23] identifies those coefficients with the outgoing series for and gives . Thus belongs to the exact outgoing class of [L1]. The exterior scalar uniqueness lemma [L2] applies to on the connected and gives on , that is, the divergence constraint.
Uniqueness of the classical problem. Let both satisfy the conditions of the Statement. Their difference is on , solves componentwise on , has and on , and is outgoing on . Then with , and the integration by parts of step 3.2 and step 6.1 shows that for every : the volume terms reproduce the Helmholtz equation, the inner boundary term cancels against on through the exact identity of step 10.1, and the outer term cancels because by outgoingness. By step 3.2, on ; its trace on is zero, so [L1] gives outside that sphere as well, hence on .
Assembly and choice accounting. Existence is step 6.1 together with the regularity and gluing of steps 7.1, 8.1 and 9.1: the constructed has the prescribed tangential trace, satisfies on , is on and outgoing on in the stated weak trace sense, and satisfies the closure relation of step 9.1; its divergence vanishes by step 10.1. Uniqueness is step 11.1. The only choice principle used is the Axiom of Choice assumed in the Statement: it supplies the Fredholm alternative, and through [L16] the Countable and Dependent Choice invoked by the compactness, trace and difference-quotient interfaces [L15], [L10], [L12], [L17]; the lift, the coercive inversion and the boundary bootstrap make only finitely many explicit selections. This proves all assertions.
Weak and classical solvability of the elliptic boundary problems with Dirichlet, Neumann and transmission data
Statement
Assume the Axiom of Choice and Countable Choice as declared by the weak-solvability and regularity lemmas below (The Axiom of Choice, The Axiom of Countable Choice ()). Let be a bounded domain in the local graph sense of Bounded C^k domains and boundary charts, let be uniformly positive, that is for all and and some , and let be smooth on . The Euclidean inner product is that of The Euclidean inner product on ; at a boundary point with outward unit normal the outward conormal vector is and the outward conormal derivative is . Here is the space of real symmetric matrices, is the Sobolev space of Integer-order Sobolev spaces and their norms, is the closure of (Zero-boundary Sobolev space as a norm closure), and is the bounded onto trace of The sharp trace theorem: boundedness and range in the fractional space, with the fractional boundary space defined in [L1]. Then:
(a) Dirichlet. For every there is exactly one weak solution with trace of for all ; it depends continuously on the data, , has a representative on , and satisfies the classical equations in and .
(b) Neumann. Let be a smooth outward conormal datum satisfying on every connected component of . Then there is a weak solution of for all ; it is unique up to a separately chosen additive constant on each component, and imposing on every component gives a unique normalised solution which is on each closed component and satisfies the classical equations in and . In particular on a connected domain the compatibility is , with a single additive constant.
(c) Transmission. Let there be finitely many pairwise disjoint closed smooth interfaces strictly inside , let be piecewise smooth on the closures of the resulting pieces and uniformly positive in the above sense, let be piecewise smooth on the closed pieces and let be a smooth sheet charge on the union of the interfaces; the weak right-hand side is , together with in the Neumann case. Prescribe either the smooth outer Dirichlet datum of (a), or the smooth outer Neumann datum of (b) with the componentwise compatibility condition for every component . With outer Dirichlet data the globally solution is unique; with outer Neumann data it exists exactly when that compatibility holds and is then unique modulo componentwise additive constants, the zero componentwise means making it unique; the equal one-sided traces and regularity on each closed side hold in either case, and the flux jump is in the sign convention of Weak Neumann and transmission existence with interface charges, where is a chosen unit normal on the interface and is the difference from the -positive side to the other.
Edge and junction points, reentrant corners, coefficient loss of regularity and general piecewise classical regularity beyond finitely many disjoint smooth interfaces are excluded. The existence content of all three parts is that of the two weak solvability lemmas; this theorem states the combined existence-and-regularity conclusions on the declared domains and adds no existence assertion beyond them.
Facts & Assumptions
Given: The Axiom of Choice and Countable Choice (The Axiom of Choice, The Axiom of Countable Choice ()); a bounded domain with the graph property of Bounded C^k domains and boundary charts; a uniformly positive coefficient , smooth on the closure in parts (a)–(b) and piecewise smooth on the closed pieces with finitely many disjoint closed smooth interfaces in part (c); a smooth bulk datum (piecewise smooth in (c)); a smooth sheet charge in (c); smooth boundary data ; the conventions , outward conormal vector , outward conormal derivative , and the trace and spaces , of Integer-order Sobolev spaces and their norms and the trace operator.
Weak prescribed-trace Dirichlet existence: for a bounded domain , uniformly elliptic measurable , and , there is exactly one with trace solving for all , and (Weak Dirichlet problem with prescribed fractional Sobolev boundary data).
Smooth-domain elliptic regularity: on a bounded domain, with smooth uniformly positive and smooth on the closure, the weak solution of with smooth Dirichlet data, or with smooth compatible Neumann flux data, is on the closure and satisfies the classical equation and boundary data; for finitely many disjoint closed smooth interfaces strictly inside with piecewise smooth positive , piecewise smooth and smooth sheet charge , the weak solution is smooth on each closed side (Classical smoothness of weak Poisson solutions on smooth domains and across smooth interfaces).
Weak Neumann and transmission existence: with on for and , a weak Neumann solution for all exists if and only if , and is then unique up to an additive constant, the normalisation making it unique; on finitely many components compatibility and normalisation are imposed separately on each component; for finitely many disjoint smooth stationary interfaces with piecewise smooth uniformly elliptic , bulk and prescribed sheet charge defining a bounded trace functional on , the same argument gives weak Dirichlet or compatible Neumann existence for the transmission problem, the globally potential has identical one-sided traces, and where the solution is classically smooth on each side integration by parts gives the jump (Weak Neumann and transmission existence with interface charges).
Divergence theorem for bounded piecewise domains: for a bounded domain with the specified finite piecewise presentation and a field on the closures of the pieces, the integral of the divergence equals the sum of the outward fluxes over the faces, counted once off the seam sets (Divergence for finite piecewise C1 presentations).
First Green identity: for a bounded domain and , , (First Green identity).
Specified-lift variational solver: on a bounded open domain with measurable symmetric uniformly positive coefficient, for a specified and a bounded functional there is exactly one with for all (Weak Dirichlet existence for a prescribed lift and uniformly elliptic coefficient).
is the closure of (Zero-boundary Sobolev space as a norm closure), and on the smooth bounded domain the trace is bounded and onto under AC (The sharp trace theorem: boundedness and range in the fractional space).
Choice accounting. The Axiom of Choice and its Countable Choice consequence are those assumed explicitly by the two weak-solvability lemmas [L1] and [L3] and by the regularity lemma [L2]; the classical upgrades, the divergence theorem [L4] and the Green identity [L5] introduce no further choice, and the assembly steps select nothing.
Proof
Given: The domain, coefficients, data and conventions of the Given paragraph above, with the smooth Dirichlet datum , the smooth compatible outward conormal datum , or the transmission configuration of the Statement.
The Dirichlet branch: existence, uniqueness, exact trace, continuous dependence. Let and . By [L1] with the uniformly elliptic smooth coefficient there is exactly one with trace and for all , and ; this gives the existence, uniqueness, exact prescribed trace and continuous dependence asserted in (a).
The Neumann branch. Let and put ; since is bounded and is bounded into , is a bounded linear functional on of the form required by [L3] with density represented by the smooth function . Testing the weak identity with the constant on a component gives , so the componentwise compatibility is necessary; it is also the hypothesis of the Statement. By [L3] there is then a weak solution, unique up to one additive constant per component, and the normalisation makes it unique; on each connected component the upgrade part of [L2] applies with the smooth datum and gives local classical solutions satisfying and , the different choices of the additive constant changing nothing in the equation. On a connected this is , that is .
Transmission: weak existence, unique traces and the conditional jump. In the configuration of part (c), let , a bounded functional on because is smooth on the compact interface union and is bounded into of that finite union. For outer Dirichlet data, obtain an exact boundary lift from [L1] applied with coefficient and zero bulk datum (this is only a lift, not the transmission solution). Restrict the bounded functional to and apply [L6] with the actual piecewise coefficient; it gives the unique transmission solution in with the prescribed outer trace. For outer Neumann data, the weak Neumann part of [L3] applies directly to the bounded functional including the sheet and outer flux terms; hence a globally weak solution exists, is unique for outer Dirichlet data, and for outer Neumann data exists exactly when vanishes on the constants of every component, that is when the stated compatibility holds, and is then unique modulo componentwise constants, the zero componentwise means fixing it. By the transmission part of [L3] the globally potential has identical one-sided traces, and wherever it is classically smooth on each side, integration by parts gives the jump in the stated sign convention.
Classical upgrade of the Dirichlet branch. The solution of step 1.1 is the weak solution of in with the smooth Dirichlet datum : for compactly supported test fields the weak identity is exactly the distributional equation , where the divergence is that of a field once the classical upgrade below identifies as such, and the boundary values are the prescribed ones by trace uniqueness. Applying the Dirichlet part of [L2] with the smooth and smooth yields the representative on satisfying the classical equation and boundary values.
Transmission: one-sided classical regularity and the unconditional jump. The weak solution of step 1.3 is the weak solution of the transmission problem for the piecewise smooth positive , piecewise smooth and smooth sheet charge of the Statement, with either the smooth outer Dirichlet datum or the smooth compatible outer Neumann datum. By the interface part of [L2] it is on each closed side; in particular it is classically smooth on each side of every interface, so the conditional jump identity of step 1.3 applies and the flux jump holds unconditionally in the stated class. The equal one-sided traces are those of step 1.3, and on each closed side the classical equation holds because the weak identity tested against compactly supported fields localized in the interior of a side is the distributional equation there. The interface integration by parts underlying the jump is the divergence theorem [L4] applied to the field on the two pieces and the Green identity [L5]; the smooth chain and product rules of Sums, scalar multiples, products and quotients: , , , and when and The chain rule for total derivatives: are the calculus conventions used in transporting the equation to the closed pieces, and the Euclidean pairings are those of The Euclidean inner product on .
Assembly and exclusions. Part (a) is steps 1.1 and 2.1, part (b) is step 1.2, and part (c) is steps 1.3 and 2.2, with the definitions of the conormal vector and derivative fixed in the Statement. Nothing beyond the declared smooth-domain, finite-interface regime is asserted: no edge or junction point, no reentrant corner, no coefficient loss of regularity and no general piecewise classical regularity is claimed, and no existence assertion is used beyond the two weak solvability lemmas [L1] and [L3]. The choice assumptions are exactly those recorded in the Choice accounting paragraph, and the finite interface and component collections are handled by the explicit finite sums above. This proves all three parts.
Spectral completeness of the declared PEC waveguide and cavity classes
Statement
Assume the Axiom of Choice (The Axiom of Choice). Let be a bounded domain in the local graph sense of Bounded C^k domains and boundary charts, with outward Euclidean unit normal field on . Restate the class conventions of Spectral completeness of the curl form in a smooth PEC cavity: is the real Hilbert space of square integrable vector fields with the inner product induced by the Euclidean inner product of The Euclidean inner product on , and are the graph spaces with norms and , the curl and divergence being taken in the distributional sense; is the graph-norm closure in of the fields that are smooth on a neighbourhood of and satisfy pointwise on ; and , . This is the explicit weak perfect-electric-conductor class of that item, not an identification with every maximal tangential-trace realisation.
Then:
(a) Smooth PEC cavity. The curl form on has a complete orthonormal eigenbasis with nonnegative eigenvalues of finite multiplicity, with whenever is infinite dimensional and with the finite-dimensional zero eigenspace retained. Each eigenfield satisfies for every ; the eigen-equation holds distributionally together with the PEC trace; and has a representative on for which , and hold classically on , where and is extended constant along collar normal lines. For every explicitly chosen positive mathematical speed and every pair of data , , the associated second-order wave has coefficients solving with and , in the modal class of that item: its displacement lies in and its velocity in , finite modal sums converge in and on every compact time interval , and the finitely many modes are . The speed is a positive abstract mathematical parameter and has no physical dependency. The scalar auxiliary Dirichlet resolvent used inside the recorded cavity argument has, for every , a unique solution of , with smooth zero-boundary approximants converging in and whose gradients converge in the PEC graph norm, by The L-two Dirichlet resolvent and smooth zero-boundary test density. For smooth this solution is smooth on the closure by the same smooth-boundary bootstrap; no classical regularity for a general datum is asserted. Smooth unshifted scalar boundary problems have the classical upgrade of Weak and classical solvability of the elliptic boundary problems with Dirichlet, Neumann and transmission data with .
(b) Rectangular reflection-parity class. Let with and let be constants. In the reflection boundary class of Rectangular PEC reflection class: Fourier completeness, weak solutions and energy conservation (real fields on the torus whose components carry the parities of that item and whose distributional divergences vanish), the finite separated Fourier modes are dense at every time, and every initial datum of the class has a unique weak solution of , in the class, along which is constant.
No completeness is asserted in lossy, open-ended or non-smooth classes, and the constant-Ohmic and open-longitudinal branches are homed separately as physical items on the guide page; they are not mathematical premises or dependencies of this statement.
Facts & Assumptions
Given: The Axiom of Choice; a bounded domain with outward unit normal ; the graph spaces , and the class , subspace and space of the Statement; a positive speed and data , ; positive constants , , for part (b).
Smooth PEC cavity spectral closure (Spectral completeness of the curl form in a smooth PEC cavity): for a bounded domain , with the graph-norm closure in of the smooth-on-closure fields with , and , the curl form on has a complete orthonormal eigenbasis with nonnegative eigenvalues of finite multiplicity tending to infinity whenever is infinite dimensional, the zero eigenspace is finite dimensional and retained; each eigenfield satisfies the full graph-class variational identity for every and the distributional eigen-equation with the PEC trace; and for every explicitly chosen mathematical speed and all , the associated second-order wave has coefficients , displacement in , velocity in , finite modal sums converging in and on every compact time interval , and affine modes . The speed is an abstract positive mathematical parameter.
Eigenfield boundary regularity (Smooth boundary regularity of PEC cavity eigenfields in the declared graph completion): if with as in [L1], weakly and satisfies for every , then for every integer and has a representative on the closure for which , , and hold classically, with and the normal extended constant along collar normal lines; zero eigenvalues and disconnected domains are included.
Scalar elliptic boundary existence (Weak and classical solvability of the elliptic boundary problems with Dirichlet, Neumann and transmission data): for a bounded domain, uniformly positive smooth coefficient and smooth right-hand side on the closure, the weak Dirichlet problem with smooth boundary data and the weak compatible Neumann problem each have exactly one solution modulo the stated normalisation, which is on the closure and satisfies the classical equation and boundary values; the existence content is that of the weak solvability lemmas and edge, junction and non-smooth regimes are excluded.
Rectangular PEC energy completeness (Rectangular PEC reflection class: Fourier completeness, weak solutions and energy conservation): for with and constants , in the reflection boundary class with distributional the finite separated Fourier modes are dense and the class is -complete, every initial datum has a unique weak solution of , in the class, and the energy is constant along it; the item assumes Countable Choice and supplies neither trace regularity for arbitrary fields nor completeness in lossy, open or non-rectangular guides.
Choice principles: the Axiom of Choice states that every family of nonempty sets has a choice function (The Axiom of Choice); it implies the Axiom of Dependent Choice and the Axiom of Countable Choice (AC implies DC implies countable choice), the latter meaning that every sequence of nonempty sets has a choice function (The Axiom of Countable Choice ()).
Conventions: a map is on the closure when it is the restriction of a smooth map on a neighbourhood of the closure ( Euclidean maps and diffeomorphisms); the Euclidean inner product is that of The Euclidean inner product on ; and the classical product, sum and chain rules used to read the differentiated identities of [L2] are those of Sums, scalar multiples, products and quotients: , , , and when and The chain rule for total derivatives: .
Exact scalar auxiliary resolvent and density (The L-two Dirichlet resolvent and smooth zero-boundary test density): for every there is a unique with , , and smooth zero-boundary approximants converge in , with their gradients converging in the PEC curl/div graph norm. No classical smoothness is asserted for a general .
Choice accounting. The Axiom of Choice is assumed in the Statement. It is used by [L1]–[L3], whose statements declare it, and it supplies through [L5] the Countable Choice assumed by the rectangular supplier [L4]. No further choice principle is used, and the wrapper introduces no selection.
Proof
Given: The Axiom of Choice, the bounded domain , the classes , , and the data of the Statement.
The definitions agree and the cavity conclusions apply. The class , the subspace and the space of the Statement are exactly those of [L1] for the same domain : the same graph-norm closure of the same smooth fields on the closure with , the same divergence-free subspace and the same closed span, and the Axiom of Choice assumed in the Statement is the choice assumption of [L1], whose meaning is fixed by [L5]. Hence all conclusions of [L1] hold in the present setting: the curl form on has a complete orthonormal eigenbasis with nonnegative eigenvalues of finite multiplicity and whenever is infinite dimensional, the zero eigenspace is finite dimensional and retained, each eigenfield satisfies the full variational identity and the distributional eigen-equation with the PEC trace, and the modal wave expansion with the chosen positive speed has the stated initial coefficients, the stated continuities on compact intervals and affine zero modes.
Rectangular class. [L4] states exactly the assertions of part (b) for the reflection boundary class with constants : density of the finite separated Fourier modes at every time, unique weak solutions of the two equations in the class for every initial datum, and constancy of . Its Countable Choice hypothesis is available in the present setting: the Statement assumes the Axiom of Choice, and the implication to Countable Choice is the choice supplier [L5].
Smooth eigenfields. Fix . By step 1.1, , weakly and the full variational identity holds for with ; hence the hypotheses of [L2] are satisfied and for every integer with a representative on , for which the classical relations , , and hold, with and extended constant along collar normal lines; the Euclidean pairing and the reading of the differentiated identities are those of [L6]. In particular the zero eigenvalues are included and no eigenfield is discarded.
Exact scalar auxiliary boundary problem. The actual divergence-preservation argument in [L1] sets and uses with . Its existence and the admissible smooth zero-boundary approximation of are exactly [L7], so the full graph-class identity can be passed to this rough-data test without assuming that is smooth. If is smooth, the boundary quotient argument recorded in [L7] and the smooth-domain bootstrap behind [L3] apply with the additional zeroth-order term : tangential differentiation creates only lower-order derivatives of , which are already controlled at each induction stage, and normal recovery uses the positive coefficient of as before. Starting from the solution, induction gives every , hence the smooth representative on the closure; the unchanged lower-order term requires no new boundary data. Independently, [L3] supplies the classical upgrade for smooth unshifted Poisson Dirichlet or compatible Neumann problems with . The vector eigenfield upgrade is still supplied by [L2], and no smoothness of the actual rough auxiliary datum is used in spectral closure.
Assembly, exclusions and choice accounting. Part (a) is steps 1.1, 2.1 and 2.2: step 1.1 transfers the spectral completeness, multiplicity, growth, zero-mode retention, full- identity, distributional eigen-equation and modal wave expansion from [L1]; step 2.1 upgrades every eigenfield to a field on the closure satisfying the classical PEC relations, including the zero eigenvalues; and step 2.2 records the exact rough-data resolvent and graph-density prerequisite [L7], its smooth-data bootstrap, and the separate smooth unshifted scalar upgrade [L3]. Part (b) is step 1.2, which is [L4] verbatim in the present notation. Nothing outside the declared classes is asserted: no lossy, open-ended or non-smooth spectral completeness, no identification with every maximal tangential-trace realisation, and no physical reading of the abstract speed ; the constant-Ohmic and open-longitudinal branches are homed on the guide page as separate physical items and are not used here. The Axiom of Choice is used only through [L1]–[L3] and, through its Countable Choice consequence [L5], through [L4]; no other choice principle and no choice of data beyond the explicit open set occurs. This proves all assertions.
5 · Examples, experiments and counterexamples
None yet.
Sources
- D. Tataru, Carleman estimates, unique continuation and applications (Northwestern University, 1998 monograph draft), Chapter 3.6: Theorem 3.50 with Remark 3.51 and Corollary 3.6.1 (singular-weight estimates for the Laplacian) and Theorem 3.52 (strong unique continuation)
- S. Dyatlov, Lecture notes for 18.155: Plancherel (Definition 11.22, Theorem 11.29) and the Fourier differentiation identities (Section 12.1)
- Blair Davey, Quantitative unique continuation for Schrödinger operators (arXiv:1903.04021), PDF page 1
- D. Tataru, Carleman estimates, unique continuation and applications (Northwestern University monograph, 1998)
- J. K. Hunter, Notes on Partial Differential Equations (UC Davis)
- NIST Digital Library of Mathematical Functions, §14.30 Spherical and Spheroidal Harmonics
- S. Axler, P. Bourdon, W. Ramey, Harmonic Function Theory, 2nd ed. (Springer GTM 137), author-hosted full text, Chapter 5 (harmonic polynomials, spherical harmonics and zonal harmonics) and Chapter 1 (Poisson kernel for the ball)
- A. Moiola, Scattering of time-harmonic acoustic waves (University of Pavia lecture notes, 2022)
- TU Dortmund, Lecture notes: The Rellich Lemma on the Helmholtz equation
- TU Dortmund, Lecture Notes: The Rellich Lemma on the Helmholtz equation
- D. Tataru, Carleman estimates, unique continuation and applications (Northwestern University, 1998 monograph draft)
- P. Arbenz, R. Geus, S. Adam, On Solving Maxwell Eigenvalue Problems for Accelerating Cavities (ICAP 2000)