Original exposition and proofs: GPT-6 Astra (OpenAI), October 2026. CC0.
Integrating out a variable can remove a singularity or concentrate it at a critical value. For a hyperfunction, the construction must work even when no finite distributional order is available. We build integration using compact analytic representatives, then prove that only covectors with zero fiber component can survive. The proof keeps the original spherical measure when a higher-dimensional holomorphic representation is projected into fewer variables.
Let , be open, initially with , and put . A closed set is proper over when
We assume this for . The integration convention is the scalar distribution convention with ordinary Lebesgue measure in the fiber coordinates.
Compact representatives with controlled fiber support
Lemma 1 (a representative over an output patch). For every relatively compact open , the restriction of to has a compactly supported global hyperfunction representative on which is zero on . It is therefore represented by a compact real analytic functional .
Proof. Choose a bounded open with . Properness gives a compact set containing the fiber projection of . The section is zero on . Glue it with zero on ; these two open sets cover , since . Denote the resulting section by .
Now prescribe on and zero on the complement of the compact set . On their overlap both prescriptions are zero. They define a section on the open set
The full extension theorem extends this section to , retaining all its prescribed values on . Its support is contained in , because its prescribed value on the complement is zero. Proposition 4 identifies this compact section with a unique analytic functional carried by that compact set. This is the required .
The specified zeros in (I2) are part of the construction. They ensure that an auxiliary fiber boundary cannot contribute to the integral.
Theorem 2 (proper integration). There is a well-defined linear operation for hyperfunctions with support proper over . On a patch as in Lemma 1 it is the restriction of the compact analytic functional
It commutes with restriction of the output open set, satisfies
and agrees with the existing proper integral of a distribution.
Proof. Formula (I3) is the previously proved pushforward under the analytic projection. Suppose are two representatives valid over . Their difference, as a global hyperfunction, is zero on . Its support is compact and lies outside this product. The compact-section theorem identifies the difference with an analytic functional carried by that actual support. Injectivity identifies this functional with . Its projection misses , so its pushforward restricts to zero on . Thus the definition is independent of the representative.
On overlaps the same argument applies after restriction to the common output patch. Arbitrary-cover gluing gives . The construction is linear: a finite union of proper supports is proper, and sums of representatives are representatives of sums. The same uniqueness proves restriction compatibility.
The set is closed in . Indeed, a convergent sequence in lies in a compact subset of ; its lifts in have a convergent subsequence by properness, whose limit is still in . If a neighborhood of an output point misses , the input is zero over that whole neighborhood, so its local representative may be zero. This proves (I4).
For a distributional input, choose smooth compact cutoffs in the output and fiber variables, equal to one on the smaller output patch and near all its relevant support fibers. Properness supplies one compact fiber neighborhood for this choice. The resulting compact distribution, extended by zero, is a representative allowed in Lemma 1. Its analytic-functional pushforward agrees with its ordinary compact distribution integral by Proposition 7 of the analytic-functional lesson. On the smaller output patch that integral is exactly the original proper integral. Independence of the representative proves the claimed agreement.
A projected sphere gives a closed ball
The next lemma keeps track of the measure that appears when some imaginary coordinates are discarded. Write .
Lemma 3 (closed-ball angular averaging). Let be holomorphic on , let be bounded and open, and let be a finite complex Borel measure with compact support . Assume has compatible holomorphic continuations near . For , put
These functionals extend continuously to every height in , in each analytic-functional carrier seminorm for . Hence
At an interior point , a nonzero covector is absent from its analytic wavefront if either
In particular only the part of on the unit sphere can produce a singular direction.
Proof: continuity at every height. At an interior-ball height, continuity follows directly from uniform convergence on the compact real domain, with bound by for any complex neighborhood of . At a unit height , choose a boundary collar on which the given extension exists and a cutoff equal to one off that collar. For small , the inward contour argument gives, at interior heights near ,
This is the exact contour formula proved in Proposition 2 of the boundary lesson. Its elementary height check is
For interior near , a small fixed keeps the homotopy in the tube away from the collar; the collar uses the continuation. The final graph also exists at . Choose so its test arguments lie in the prescribed . On this compact graph the -factor converges uniformly, so differences are bounded by . The same graph works for all nearby allowed heights, including interior heights approaching nearby sphere points. A finite cover of the compact therefore gives uniform continuity and a uniform bound in every carrier seminorm. Integration against proves (A2) and allows the radial limit through its integral.
Proof: inward wedges. Suppose a compact subset and a nonempty open convex cone satisfy
for some . For small ,
Thus the integral is holomorphic on that wedge. On each compact subset, all arguments stay in a compact subset of the tube; finite total variation and Cauchy estimates justify every derivative. The given boundary continuations also continue near .
Fubini and the uniform carrier continuity just proved show
in every carrier seminorm. The complete boundary-regular comparison identifies the local class with . Its wavefront is in . If lies compactly inside the unit ball, the same integral is instead holomorphic on a whole neighborhood of the real base, so its local class is analytic.
Proof: excluding a direction. Fix a unit with . At a sphere point choose . Then
On a sufficiently small closed-ball neighborhood of , the first inequality has a uniform negative margin. Choose a small open convex cone about retaining that margin and the negative pairing with . Finitely many such neighborhoods cover near its sphere part. Their complement in is compactly inside the ball. Assign the measure to these neighborhoods in order, using a finite Borel partition with supports in their closures. The interior contribution is analytic. Each boundary contribution is the boundary of an inward-wedge function as in (A8), whose positive dual excludes . Their finite sum is therefore regular at .
If continues at , choose a small relative neighborhood of in the closed ball and a real ball about , such that continues near . Split into its restrictions to and its complement. The complementary support avoids , so its contribution is regular by the preceding paragraph. The first contribution on is the analytic function
To identify its local class, split (A1) into and . The omitted real sphere has Lebesgue measure zero. Both domains satisfy the needed continuation on their boundaries for the restricted measure. Passing to the carrier limits leaves a remainder carried by , while the integral over has the ordinary trace (A10). This proves (A3). The compact functional vanishes off ; its boundary points impose no assertion here.
Integrating the canonical holomorphic field
Put . The canonical field of a compact real analytic functional is
Here is ordinary unnormalized surface measure. The exact earlier construction extends to
Lemma 4 (fiber tails and continuation). The integral
is holomorphic for . It satisfies
If no , , belongs to , then continues holomorphically at .
Proof. Fix a compact set of output real coordinates and a bound for all imaginary coordinates. For large real fiber , the vectors
, with in one fixed small complex neighborhood of , lie in a closed cone close to the real directions. For instance one can use , with , once is sufficiently large. Then for nonzero , so the full complex conic estimate for applies. Its derivative form, followed by the fixed-neighborhood bound for , gives
on those tails, uniformly in the chosen compact parameters. Every fixed derivative is included. The bounded part of the fiber has the ordinary compact holomorphic bounds wherever the integrand is defined.
The exponential is integrable in ; this follows also from
and product integration. Thus (K3) and its parameter derivatives converge locally uniformly. Taylor remainders on a slightly larger compact parameter set give holomorphy. For (K4), shift one fiber coordinate at a time on a finite rectangle. All intermediate imaginary vectors have norm at most the final joint norm, after ordering the coordinate shifts from zero, so the contour stays in the tube. Complex Green and the fixed-derivative estimates justify the identity on the finite contours. The vertical faces tend to zero by (K5); their integrals in the remaining real variables also tend to zero by the product exponential bound. Successive absolute integrations prove (K4).
For the continuation assertion, the actual canonical-field definition of gives continuation of at for every real . Cover a large compact fiber ball by finitely many real neighborhoods with these continuations and shrink to one common complex output neighborhood of . The local extensions agree on overlaps: after shrinking to product neighborhoods, their overlaps meet the original tube, where both are , and the holomorphic identity principle applies. On the complementary fiber tail, (K2) already gives continuation to that output neighborhood, while (K5) gives integrable bounds for every fixed derivative. Integrating the finite part and the tail therefore continues holomorphically as claimed.
Theorem 5 (compact integration and its exact direction bound). For compact real ,
Proof. Choose a bounded open containing with positive distance from to . Formula (K2) and the tail proof show that continues near , and continues near .
For sufficiently large , the exact spherical recovery on
gives, for every entire in the output variables,
The tail estimate (K5) is uniform for , , and close to one. Its integral outside the fiber box tends to zero as , uniformly in . Thus the radial limit of the integral over the whole fiber is still the left side of (K7): subtract the finite-box integral, bound the tail uniformly, and then let increase.
For each , use (K4) with and . The strict inequality follows from . Put
a finite measure on the closed output unit ball. The recovered identity becomes
Its normalization is exactly that of (K1); no division by a sphere area has occurred. Lemma 3 identifies the right side with on entire tests. Equality on these tests gives equality of the analytic functionals; the unique extension to real-carrier germs proved in Theorem 5 of the analytic-functional lesson then gives equality on every admissible local test.
Now suppose a nonzero is absent from the right side of (K6), and set . Enlarge to include if needed. Lemma 4 continues at , and Lemma 3 excludes this direction from . Homogeneity proves (K6). The zero functional is covered by .
The field in (K3) need not be the canonical -dimensional field of . Formula (K9), with the projected measure (K8), is the identity used in the proof.
Proper fibers and the integration calculus
Theorem 6 (the full proper-support bound). Under (I1),
The right side is closed off zero locally in the output cotangent bundle.
Proof. Fix an excluded pair . Choose the compact representative of Lemma 1 on an output neighborhood of . It agrees with on and is zero on . The zero extension actually vanishes off a compact subset of , so there is no artificial singularity at its boundary. Therefore every , for real , is absent from . Theorem 5 excludes from , whose restriction is .
For closedness, consider a sequence of pairs on the right converging to a nonzero output pair. Its base points lie in a compact output set. Every contributing input point belongs to , and properness bounds their fiber coordinates in a compact subset of . Take a convergent subsequence of those coordinates. The full input covectors converge to the nonzero pair , so closedness of supplies a lift of the limit.
Proposition 7 (derivatives, multipliers and repeated integration). For analytic on ,
If the support of on is proper over , integration over agrees with either iterated order.
Proof. Differentiation and analytic multiplication preserve support, so every input in (P2) is admissible. Choose a compact representative on an output patch, with its carrier inside the domain of the analytic germ of . The output derivative pairs with as , on both sides. The multiplier pairs as , on both sides. The fiber derivative pairs as . The compact-germ formulas and locality therefore prove (P2).
For repeated integration, properness over implies properness over and over : a compact set in either intermediate base has compact projection to , and the relevant support lies in the corresponding compact part of the original support. The projected support is proper over , by the compact-image property. Use Lemma 1 with the combined fiber to choose one compact representative agreeing with the input over a whole output patch and every fiber point. Its compact projection gives a representative for the intermediate integral, by the independence proved in Theorem 2. Each iterated order, and direct integration, gives exactly . Gluing proves the assertion.
Proposition 8 (fiber coordinates and analytic inputs). Suppose
is an analytic diffeomorphism between the two product domains, and let . Set . Then
Also, if has support proper over and is analytic on , then
Proof. The inverse diffeomorphism takes compact support pieces over a compact output set to compact sets, so the transformed support remains proper. Its block derivative has determinant ; its absolute value is analytic, since the determinant is nonzero with locally constant sign.
On compact representatives the existing coordinate pullback is
.
Choose . Since and
, its value is .
The local representatives may be chosen inside the coordinate domains;
their proper fiber supports are compact there. This proves (P3) by
independence and gluing.
For (P4), analytic multiplication gives
and support in
.
This closed subset remains proper. Apply Theorem 6, retaining that support
restriction on the possible fiber point.
If , properness means that the input support is compact. Its integral is the scalar , and there are no nonzero output covectors. If , integration is the identity. The derivative statements use empty sums or empty lists in these cases.
Exercises with complete solutions
Exercise 1 (basic) — which point moments survive? Let be a point-carried analytic functional at , written in the proved convergent moment form
Compute , and compute the integral of a fiber derivative.
Solution. Substitute . Every term with vanishes, so
This series is legitimate by the original moment convergence on holomorphic germs; the subseries satisfies the same every-radius bounds. A derivative in a fiber coordinate pairs as minus the derivative of in that coordinate, hence integrates to zero. In particular is when , and zero otherwise, with the distributional derivative signs retained.
Exercise 2 (intermediate) — retaining a singular object exactly. Let be any compactly supported hyperfunction on , and let . Compute the integral of .
Solution. Its support is compact, and the existing iterated analytic-functional pairing gives
since the second factor acts on the constant function with value one. This includes the nondistribution point functionals already constructed in the analytic-functional lesson. Thus proper integration is not limited to distributional inputs. The bound in (P1) allows the full wavefront of , with zero fiber component.
Exercise 3 (intermediate) — a vertical singularity integrates to zero. On , integrate , and check (P1).
Solution. Its support is proper over the first factor. Proposition 7 gives . Exact projection equality puts its wavefront at , : the nonzero derivative of a point delta has both one-dimensional singular directions, as seen from its polynomial Fourier transform. No such pair has zero fiber covector, so the right side of (P1) is empty. This is consistent with the computed zero.
Exercise 4 (intermediate) — a smooth family of delta points. On , compute the integral of .
Solution. The support is the graph , proper over . The fiber diffeomorphism has , and the pullback composition law gives . Formula (P3) therefore gives . The exact submersion bound gives joint covectors proportional to , with nonzero proportionality factor. Their fiber component never vanishes, so (P1) also proves analyticity of the integral.
Exercise 5 (advanced) — a fold creates an integrable singularity. Let , and integrate in . Compute the resulting distribution, determine its analytic wavefront, and compare with the horizontal conormals of the parabola.
Solution. The support is proper over . The analytic coordinate map has determinant one. Hence for a compact output test,
The last equality follows by the substitutions and on the two open half-lines. First make the substitutions away from zero, then let that neighborhood shrink; the bound justifies the limit. There is no point mass added at zero. Thus the output is the locally integrable function
with arbitrary value at its single undefined point.
It is analytic on each half-line and is not smooth at zero. Its ordinary wavefront there is nonempty by the proved wavefront projection theorem. For a real distribution, the localized Fourier transform with a real cutoff satisfies ; therefore ordinary regularity in one one-dimensional direction implies it in the other, using the same cutoff estimates. Both ordinary directions, and hence both analytic directions, occur at zero.
The input conormals are
Their fiber component vanishes precisely at . The bound (P1) consequently gives exactly the two nonzero output directions at , agreeing with the calculation.
Left: the exact support and selected conormals , using the Euclidean coordinate identification. Only the vertex has a horizontal nonzero conormal. Right: the exact density for , with zero density for ; the plotting window omits the unbounded endpoint value. Each nonzero fiber branch contributes . Their sum and its local integrability are proved in Exercise 5. Editable figure source.
Exercise 6 (basic) — a sufficient support hypothesis. Compare the ordinary fiber integrals of and on . What do they say about the role of properness?
Solution. Both supports are the whole plane and are not proper over . The integral of diverges, while the Gaussian integral proved in the supplied foundations gives . Properness supplies a construction for every hyperfunction meeting it. Its failure does not exclude additional input-specific integrals, as the Gaussian shows; the theorem does not assign a value to the divergent example.
Exercise 7 (intermediate) — orientation and fiber volume. Let , , and , where is a hyperfunction. Compute and check (P3).
Solution. Tensor naturality and the inverse absolute Jacobian give
Thus , while . The negative orientation does not produce a negative mass; the scalar density uses the absolute determinant.
Exercise 8 (advanced) — the measure in the one-dimensional output. Project ordinary arclength on the unit circle onto its first coordinate . Find the measure in (K8) for , including its total mass.
Solution. Parameterize the circle by , , with arclength . On the upper and lower open semicircles, has absolute derivative . Each contributes , so
The two endpoint preimages are single points of arclength measure zero, so there are no endpoint atoms. The density is integrable there, as the original finite angular parameterization also shows. Formula (K9) uses this entire ball measure, not only its two boundary points and not a measure normalized to mass one.
The supplied metric foundation, Sections 12–13, integration foundation, Sections 15–16, and complex contour foundation, CX7–CX11 and CMI6–CMI8, give the compactness, cutoffs, absolute integrals, substitutions and complex differentiation used above. The ordinary wavefront and Gaussian comparison proofs are in the complete Fourier and pullback reading, Sections 18.1–18.5.
Lars Hörmander, The Analysis of Linear Partial Differential Operators I: Distribution Theory and Fourier Analysis, reprint of the second edition, Springer, 2003, doi:10.1007/978-3-642-61497-2, Theorems 8.5.4 and 8.5.4′ and the hyperfunction extension required in Section 9.3. The compact extension, closed-ball measure argument, exposition, examples, exercises and figure here are independently expressed.
General singular kernel action, kernel composition, convolution and the further support-normal assertions require their additional arguments. The proper integral and bound proved here supply their integration step.