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.
Uniform far-zone asymptotics and retarded-time flux limit for compact conserved smooth sources
Statement
Assume Countable Choice (The Axiom of Countable Choice ()), as used by the declared polar/surface and change-of-variables suppliers. Let , , and be constants, let and satisfy (H1) whenever or , and (H2) on . Here and below and are the open and closed Euclidean balls of radius about the origin, and is the unit sphere. On the open exterior define the retarded scalar and vector potentials and the fields , , where , and are the spatial operators of The Jacobian matrix of partial derivatives and the gradient in the scalar-valued case and Divergence and curl of a vector field. The fields are defined on using these ordinary derivatives; the conclusions below use . Every displayed spatial integrand is evaluated on and extended by zero outside it, including at , so no quotient is used. All vector-valued integrals are componentwise scalar Lebesgue integrals.
(a) (Fields as retarded integrals.) On the open set the potentials are of class in , and there where , , and are the partial derivatives in the second variable. Moreover, on , and each component of coincide with the corresponding solution constructed in the wave Cauchy problem of The three-dimensional wave Cauchy problem: Kirchhoff representation, uniqueness, domain of dependence and compact support for zero Cauchy data at and scalar source , respectively .
(b) (Uniform far-zone expansion.) For and put and . Then , and there are constants , depending only on and on the suprema of on , such that for every , and , with ,
(c) (Retarded-time flux limit.) Let and let be the surface measure on (Surface integration on compact C1 hypersurfaces). Then for every , This is a limit at fixed retarded time , not at fixed observation time ; no decay or boundary condition at spatial infinity is assumed beyond the compact spatial support in (H1).
Facts & Assumptions
Given: (The Axiom of Countable Choice ()); constants , , , ; sources , satisfying (H1) and (H2) of the Statement; the retarded potentials and fields of the Statement, with all vector integrals read componentwise. For , , we write , , , , , and , so that ; denote the suprema of on , and the Lebesgue measure of the ball.
A measurable is integrable exactly when , and then the integral is computed from the positive and negative parts or, for complex , as ; denotes the integrable class and is the integral over a measurable set. (Integrable real and complex functions, and their integrals, The class of integrable functions, Integral over a measurable subset)
The integral is linear, , measurable implies , for , and integrable functions that agree almost everywhere have the same integral. (The Lebesgue integral is linear on , The modulus of an integral is bounded by the integral of the modulus, Monotonicity and nonnegative homogeneity of the nonnegative integral, Two integrable functions are equal almost everywhere exactly when all of their indefinite integrals agree)
Under the ball is Lebesgue measurable with ; every continuous map is Borel measurable; and sums, scalar multiples and pointwise products of measurable functions are measurable. (Euclidean balls have positive finite Lebesgue measure, Continuous functions on Euclidean spaces are Borel measurable, Arithmetic and lattice operations preserve measurability whenever they are defined)
Mean value theorem: if is continuous on and differentiable on then for some . (The mean value theorem, as the case of Cauchy's: for continuous on with and differentiable on there is with )
Parameter integrals over a fixed compact measurable set of finite measure: if is compact, measurable and of finite measure, if , and if the real-valued and are continuous on a neighbourhood of , then is differentiable at every with derivative and has the corresponding one-sided relative derivatives at the endpoints of ; the lemma is stated pointwise in its one real parameter and explicitly asserts nothing for moving parameter sets or for singularities crossing . Applying it once per parameter direction with its parameter renamed to or (all other variables held fixed), and iterating on the resulting integrals, yields the corresponding partial derivatives of a parameter integral whose integrand is smooth in all variables on a neighbourhood of the fixed . (Differentiation under the integral sign over a compact measurable set and over a compact surface)
Chain rule and algebra of derivatives for the composite maps appearing below, such as and . (The chain rule for total derivatives: , Sums, scalar multiples, products and quotients: , , , and when ) The spatial gradient, divergence and curl are the coordinate operators specified in the Statement (The Jacobian matrix of partial derivatives and the gradient in the scalar-valued case, Divergence and curl of a vector field).
A map has continuous word partial derivatives through order , and means this for every ( Euclidean maps and diffeomorphisms). Finite sums, products and composites preserve these classes ( Euclidean maps are closed under componentwise algebra and composition). On , and real powers agree with rational powers (Continuity and derivatives of positive-base real powers, The exponential definition of real powers agrees with the existing rational powers); iterating this rule makes and smooth there. Closed bounded Euclidean sets are compact, continuous functions on compact sets are uniformly continuous and attain finite extrema (Heine-Borel in : with the Euclidean metric a subset of is compact if and only if it is closed and bounded, and the proof by bisection uses no choice principle; the same holds on the real line, Heine-Cantor: a continuous map from a compact metric space to any metric space is uniformly continuous, A continuous real-valued function on a nonempty compact metric space is bounded and attains a greatest and a least value).
Zero-data wave Cauchy problem of speed from time with source in the extension sense: its solution is on , it is there, and it satisfies ; here . (The three-dimensional wave Cauchy problem: Kirchhoff representation, uniqueness, domain of dependence and compact support)
Polar-coordinates formula: for every nonnegative Borel , ; here is the polar surface measure of the cited formula, which equals the chart surface measure of [F13] (Agreement with the existing polar sphere measure), so the two symbols are used interchangeably; a signed or complex is handled by applying the formula to positive and negative parts and subtracting. (Polar coordinates decompose Lebesgue measure into r^{n-1} dr d sigma, Agreement with the existing polar sphere measure)
One-dimensional change of variables: for a diffeomorphism of open subsets of and , . (A C^1 diffeomorphism satisfies the change-of-variables formula for L^1 functions)
Divergence theorem for a bounded Euclidean domain and : , with the outward normal. (Divergence on a bounded C1 Euclidean domain)
The Euclidean norm satisfies the triangle and Cauchy-Schwarz inequalities (Cauchy-Schwarz with its equality case, the triangle inequality for , the parallelogram law and polarisation). Cross product and inner product on : is bilinear and antisymmetric, , and for the identities and hold, so . (The cross product in , The Euclidean inner product on )
Surface integral on the compact embedded hypersurface : for a nonnegative Borel the integral is defined by finitely many regular parametrizations and an ambient partition of unity, the empty surface integrates to , the definition is independent of the chosen presentation, the total surface measure is finite, and the integral is monotone in ; the definition carries the convention already declared. (Surface integration on compact C1 hypersurfaces)
change of variables for nonnegative Borel functions: under , for a diffeomorphism of open subsets of and every nonnegative Borel , with equality in ; in particular the translation of is a diffeomorphism with , and a signed integrand is handled through its positive and negative parts by linearity. (Borel change of variables from the compact-support formula and Radon uniqueness, The Lebesgue integral is linear on )
Proof
Smoothness of the potentials: for and one has , so the maps and are on a neighbourhood of by [F6] and [F7]. Apply [F5] to the fixed compact set once for each parameter direction with its one real parameter renamed to , , and (the remaining variables held fixed) and iterate on the resulting integrals: every differentiated integrand is again continuous on a neighbourhood of , so each application is covered by the lemma and and each component of have continuous partial derivatives of every order on , these differentiated parameter integrals are jointly continuous: on each compact parameter neighbourhood the continuous differentiated integrands are uniformly continuous on its product with , so the integral of their difference is bounded by times their uniformly vanishing difference [F2]. Hence the potentials are on by [F7], so the derivatives defining the fields are ordinary derivatives even at .
Elementary estimates in the far zone: for , and , expanding with gives because ; consequently , , , and , all uniformly in .
Field formulas: by [F6], , and , while ; hence and . Each of these first derivatives of the integrands is continuous on a neighbourhood of , so by [F5] the derivatives may be taken under the integral: and are given on , in particular for , by the two displayed zero-extended integrals of the statement, since and .
Polar-coordinates identity: fix and , and let be either or one component ; then vanishes off and there, so the quotient on , extended by zero elsewhere, defines a bounded compactly supported Borel function on all of . The translation is a diffeomorphism of with , so [F14] applied to the positive and negative parts of gives ; applying [F9] to the positive and negative parts of , which at equals and therefore has inner angular integral , gives with , because the inner angular integral is and the radial factor is .
Continuity identity: fix and let ; the map is on , and [F6] gives with . By [F11] on , whose boundary flux vanishes because for , ; substituting the chain-rule expression and using (H2), . The integrands vanish for by (H1), so [F2] lets the integrals be taken over ; the second is by the definition of , whence .
Identification with the Cauchy solution: fix . For the radial integrand of step 2.2 vanishes when , because then its source time is less than . Apply [F10] to the affine diffeomorphism from onto , with absolute derivative ; the integrand is bounded on this finite interval, hence integrable. Endpoint values do not affect the Lebesgue integrals, and this gives . At both sides are zero by (H1), so the identity holds throughout . Multiplying it by for , and by for , identifies and respectively with the zero-data Cauchy solutions of [F8] with sources and . This holds on and in particular at .
Uniform error estimates: fix , let denote the argument and the argument , and write and , so that the field formula of step 2.1 and the definition of give by the linearity of the integral. Every source factor is bounded by its supremum on , and (H1) makes and vanish on the open set , hence makes all their partial derivatives vanish there too, so these suprema also dominate the retarded arguments ; the mean value theorem [F4] gives and : when the difference is nonzero, apply [F4] to its scalar projection onto the unit direction of that difference, and use Cauchy-Schwarz from [F12], and using , and yields , with for all ; hence, by the triangle inequality for the integral and the finiteness of , with . The same computation applied to and to gives , for .
Smoothness of the far-zone moments: the map and its partial derivative are in : apply [F5] repeatedly in the directions with the fixed compact set , each differentiated integrand again being continuous on a neighbourhood of ; the integrals over and agree because the smooth sources and all their derivatives vanish on by continuity from . In particular is continuous for each fixed .
Pointwise flux asymptotics: by step 3.2 write and at with , ; then and by [F12], while because . Expanding the cross product bilinearly, the error terms are , so with for a constant depending only on and the source suprema, uniformly in and .
Flux limit: by [F13] the surface integral over the compact sphere of a bounded Borel function is finite and monotone, so for every and the difference has absolute value at most , which tends to ; the function is continuous by step 4.1, so its surface integral is the displayed finite constant. Hence the stated limit at fixed retarded time follows; no step compares different values of , so the limit is asserted only at fixed retarded time.
Depends on
A C^1 diffeomorphism satisfies the change-of-variables formula for L^1 functions
Continuous functions on Euclidean spaces are Borel measurable
The mean value theorem, as the case of Cauchy's: for continuous on with and differentiable on there is with
Euclidean maps and diffeomorphisms
The Axiom of Countable Choice ()
The cross product in
The Euclidean inner product on
Integrable real and complex functions, and their integrals
Integral over a measurable subset
The class of integrable functions
Surface integration on compact C1 hypersurfaces
Borel change of variables from the compact-support formula and Radon uniqueness
Differentiation under the integral sign over a compact measurable set and over a compact surface
Euclidean balls have positive finite Lebesgue measure
Agreement with the existing polar sphere measure
Monotonicity and nonnegative homogeneity of the nonnegative integral
Sums, scalar multiples, products and quotients: , , , and when
Arithmetic and lattice operations preserve measurability whenever they are defined
The chain rule for total derivatives:
Divergence on a bounded C1 Euclidean domain
The three-dimensional wave Cauchy problem: Kirchhoff representation, uniqueness, domain of dependence and compact support
The modulus of an integral is bounded by the integral of the modulus
The Lebesgue integral is linear on
Polar coordinates decompose Lebesgue measure into r^{n-1} dr d sigma
Two integrable functions are equal almost everywhere exactly when all of their indefinite integrals agree
Divergence and curl of a vector field
The Jacobian matrix of partial derivatives and the gradient in the scalar-valued case
Cauchy-Schwarz with its equality case, the triangle inequality for , the parallelogram law and polarisation
Euclidean maps are closed under componentwise algebra and composition
Continuity and derivatives of positive-base real powers
The exponential definition of real powers agrees with the existing rational powers
Heine-Borel in : with the Euclidean metric a subset of is compact if and only if it is closed and bounded, and the proof by bisection uses no choice principle; the same holds on the real line
Heine-Cantor: a continuous map from a compact metric space to any metric space is uniformly continuous
A continuous real-valued function on a nonempty compact metric space is bounded and attains a greatest and a least value
Dependency tree · 2 levels
Sources
- D. Tong, Electromagnetism (University of Cambridge lecture notes)
- R. Fitzpatrick, Classical Electromagnetism (University of Texas at Austin lecture notes), chapter 'Retarded potentials' (node 50)
- R. Fitzpatrick, Classical Electromagnetism (University of Texas at Austin lecture notes), chapter 'Retarded fields' (node 52)