These are Sections 18.1–18.5 of the programme reading Detecting regularity without choosing coordinates. They construct arbitrary noncharacteristic smooth pullbacks, prove their Fourier bound, and identify diffeomorphism and submersion cases. Section numbers and formula labels retain their source meanings within this reading.
The earlier proofs used here are all supplied in this reader. The Schwartz and Fourier foundation, F1–F5, proves Fourier inversion, finite seminorm estimates and the full Gaussian mass and transform in WF13. Order, positivity and distributional limits, Section 1, proves compact finite order. Convolution as addition of supports, B0–B2 and Theorem 1.1, proves partitions, distributional gluing, smooth parameter pairings, tensor products and their exact support. Tempered growth and spectral cutoffs, Lemma 2.1, supplies Schwartz convolution and differentiation of its pairings. The scalar foundation, Sections 12–13, gives compactness, finite smooth partitions and the product, chain and segment-integral rules. The integration foundation, Sections 15–16, gives absolute integration, Fubini, convergence and linear substitution. Every reference below to the integration, Fourier or calculus chapters means these supplied proofs.
For coordinate substitutions, Zero hypersurfaces as curvature measures, Lemma 3.0, proves the complete nonlinear change-of-variables formula with its determinant. Regular level sets and transverse convolution, Lemmas 0.1–0.2, proves the smooth inverse and coordinate-completion theorems by a convergent iteration. These are the inverse and measure substitution results used in Sections 18.3 and 18.5. Smooth pullbacks by a diffeomorphism are given by the displayed test formula WF5: the product and chain rules prove continuity, the determinant chain rule proves composition, and Lemma 3.0 identifies it with composition of smooth functions. No general distributional pullback is assumed before WF12 constructs it.
18.1. The original Fourier estimate and every cutoff
Use the original convention
For a compactly supported distribution , its Fourier transform is , with a compact smooth cutoff equal to one on its support inserted in that pairing. The full finite-order test estimate and product rule give
for some actual integer . Every frequency derivative has the same type of estimate, with its original multiplier in the test. The estimate keeps the derivatives of the inserted support cutoff. A compact smooth test has rapidly decreasing transform by repeated integration by parts with , whose full multiplier is . These facts follow on the original coordinates.
For , inverse Fourier transformation of the test and the finite-order bound justify
The integral is absolutely convergent: take the Schwartz decrease of beyond the original polynomial order plus . It also converges in every test seminorm needed in the pairing, so the distribution can be passed through the integral. No Fourier multiplier constant is suppressed.
Suppose decreases rapidly in an open cone , and the angular closure of a smaller cone lies in . For , angular separation gives
for some . To prove this, restrict to ; the two closed angular sets are disjoint, so the continuous difference has a positive minimum. Scaling restores the original lengths. Split WF2 at . On that region both original transforms decrease rapidly, and
. Taking their exponents larger than gives the requested output power and an integrable residual power in . On the complement, take the cutoff exponent larger than ; angular separation beats the full polynomial input bound. Thus multiplication preserves rapid decrease on .
Consequently the definition of using a cutoff equal to one near the original base point is unchanged if the cutoff is only nonzero there: multiply by its actual smooth reciprocal on a smaller neighborhood and use WF2. It is local. Its complement is open in the nonzero cotangent variables by the same smaller-neighborhood and smaller-cone construction, so the wavefront set is closed and conic. If all directions are regular over a compactly localized neighborhood, a finite cover of the original unit sphere and the cutoff estimate give rapid decrease everywhere. WF1 then proves smoothness with every derivative. Conversely compactly localized smooth functions have that decrease, so absence of all wavefront directions is exactly smoothness.
18.2. A full nonstationary integral bound
Let be a fixed compact coordinate set and
, with smooth and supported in . In each application below the original phase is linear in the frequency parameters, and its coordinate derivatives on satisfy
. Suppose its actual gradient satisfies
on , for . Retain the entire operators
The superscript denotes the bilinear integration transpose, not a conjugate adjoint. Boundary terms vanish because the original amplitude is compactly supported. Every derivative of each coefficient of is bounded by : the numerator has one frequency power, the denominator has two, and each differentiated quotient has the same net power, with the positive lower gradient bound retained. The full iterated product and chain rules in the calculus chapter give a finite sum at every , keeping every differentiated coefficient and amplitude. They therefore prove
on the separated region, enlarging for bounded frequencies. Every fixed additional derivative of the amplitude or phase parameters has the corresponding estimate after increasing the number of integrations; its original polynomial frequency factors must be included before choosing . The constants depend on the actual compact set, gradient margin and finitely many original derivatives, rather than a replaced phase.
18.3. The exact diffeomorphism covector map
Let be a smooth diffeomorphism between coordinate opens of dimension , and put . The already constructed scalar pullback retains its full test Jacobian:
Fix , , and , and put
. Suppose is regular for . Choose an original compact cutoff equal to one on a neighborhood of so that has rapidly decreasing transform on a cone about . Shrink an -cutoff about until its image lies in that neighborhood. Its transform after pullback is exactly
For each fixed , this is the Fourier inverse formula applied to a compact smooth test, and is absolutely convergent at large by WF3. Its phase gradient is the original
. On the compact support, both and its inverse have uniform finite norm bounds. Thus when is below a sufficiently small multiple of , or above a sufficiently large multiple, the gradient is bounded below by . For the remaining comparable lengths, continuity of and sufficiently small base/direction neighborhoods place in an angular cone whose closure lies in . If , compact angular separation gives the same lower bound. This compactness argument retains the full derivative matrix and its original covectors.
On those separated regions WF4 beats the polynomial bound for , with larger than that order, the requested decay exponent and . On the remaining region and comparable with , use the rapid input decrease and the original constant bound . The integration volume is at most ; choosing the input decay exponent larger than that volume power and the requested output exponent proves rapid output decrease. Hence regularity at implies regularity at . Applying this proved implication to the actual inverse diffeomorphism and using WF5's composition law proves both inclusions, giving the exact equality
Invertibility keeps every displayed output covector nonzero. Both original Jacobians remain in WF5--WF6; they do not change the covector relation.
18.4. Products and the exact projection converse
For compact localizations on and on , their already constructed tensor product has
Here the order of the two factors is input-coordinate order, as indicated by the variables; converting to the geometric chapter's output-then-input notation requires that actual permutation. The equality follows by its two original iterated test pairings and the factored exponential.
Write . Then
Outside the product support the tensor distribution vanishes, by the proved exact support formula. At a point inside it but outside the displayed covector set, at least one nonzero component is a regular direction for its factor. Near that pair direction its length is at least a fixed positive fraction of the total frequency length. Its factor in WF8 decreases to every order, while the other has its original polynomial bound. Their product therefore decreases to every order in that product cone. Product spatial cutoffs are equal to one near the base point, so this proves the claimed inclusion with the correct original Fourier definition. WF2 then handles all smaller nonproduct cutoffs. No general equality for two arbitrary singular factors is asserted.
For the original projection , define by
. The integral test is smooth with compact support and every -derivative is its actual integrated derivative, so this is a continuous distribution. The constant factor is smooth, and WF9 gives one inclusion in
For the converse suppose is regular at . By WF2 choose product cutoffs supported in that regular base neighborhood, both equal to one near their respective points, with and . Their full transform is
. The regular cone contains for all in a smaller cone about . Its restriction at is the original nonzero scalar . Division by that scalar proves rapid decrease of the original factor, contradicting singularity at . This proves the exact converse, not only the forward inclusion.
18.5. Constructing the pullback for the original smooth map
Let be smooth. Its precise normal set and the required condition are
We construct the map under this original transversality condition; no pullback at a forbidden covector is assumed. Near any fixed , the unit directions in the kernel of form a compact set, possibly empty. WF11 makes every such direction regular at . A finite regular cone cover, a common sufficiently small target cutoff , and WF2 give an open cone on which decreases to every order, containing an angular neighborhood of those kernel directions. On the compact complementary unit directions has a positive lower norm. Continuity allows a fixed original neighborhood of and a constant with
there for every complementary direction. Shrink so its image lies in the region where .
For , put and define
On , the rapid input decrease and give an integrable bound. On its complement, the actual phase gradient is , so WF4 gives a bound . Multiplying by the original polynomial bound for and choosing proves absolute convergence. It also proves a continuous finite-order distribution estimate on each original compact test support, with its complete coordinate and map derivative constants. For smooth , WF1 and absolute testing show that this is exactly the smooth scalar function .
Here is the needed independence and locality, rather than an assumed gluing rule. Use the original Cartesian Gaussian regularization
Its full mass and Fourier identity are proved in the integration/Fourier chapters. The two absolute bounds for WF12 dominate uniformly for , since . Thus WF12 is the limit of the actual smooth pullbacks .
If two target cutoffs equal one near , their difference times is a compact distribution vanishing near that compact image. The distance between that image and is positive. Its original compact finite-order estimate, applied to every derivative of , shows uniform convergence to zero on that image, including every fixed -derivative: the full differentiated Gaussian has finitely many polynomial factors in the original difference coordinates and inverse powers of , times the same exponential. For distance at least , each such factor is bounded by , tending to zero. The inserted support cutoff derivatives also remain in this estimate. Consequently the two limits agree on .
The same argument handles restriction to smaller original neighborhoods. For a compact test crossing several 's, choose a finite smooth partition subordinate to them and sum WF12. On an overlap the preceding common Gaussian comparison gives equality; refinements therefore have the same sum. This constructs a unique local distribution on all of with these formulas, preserving the original map. It proves its locality and compatibility with restriction. At a diffeomorphism, the smooth Gaussian approximations and the full measure substitution show agreement with WF5, including its actual inverse Jacobian. At the projection the same approximations and the integrated test show agreement with WF10's construction.
Its precise wavefront bound is
For completeness fix a nonzero outside the displayed set over . The singular unit target directions over are compact. WF11 says their images under never vanish, and the chosen output direction is different from every resulting direction. Compactness yields positive margins for both assertions. Choose a closed angular neighborhood of that singular set retaining these margins. Its complementary directions have a finite regular cone cover; WF2 again chooses a common target cutoff so that decreases to every order outside . Shrink both original base and output direction neighborhoods so the margins hold for all in the support of a cutoff and every allowed output . If the singular set is empty, local smoothness already proved in Section18.1 supplies the conclusion directly.
The localized output transform is WF12 with . Its inner phase is exactly , with gradient . For , the two compact margins give
: normalize their combined lengths to one; if the continuous difference had zero minimum, the covectors would have the excluded common direction, or a nonzero singular target direction would map to zero. WF4 therefore beats the full polynomial input bound and gives every output inverse power after integration in .
For , use the rapidly decreasing input. Split at , with smaller than the reciprocal of twice the actual compact bound for . On that region the gradient has norm at least , so WF4 and the rapid input bound give every output power. On the other region , the original bound for the inner integral is ; taking the input decay exponent larger than the requested output exponent plus gives every output power after integrating the full tail. This proves WF14 with the original Fourier constant still present in WF12. It proves a bound, and does not claim a converse for an arbitrary smooth map.
For a submersion , the normal set is empty, so the construction applies to every . Retain a nonzero -row derivative minor at and complete 's coordinates by the remaining original -coordinates. The resulting map has its actual nonzero determinant. The proved inverse/implicit theorem gives a local diffeomorphism; in these coordinates . Gaussian comparison in WF12 proves . WF7 and the exact WF10 converse therefore give
The derivative identity is the original chain rule
. Its injectivity on target covectors is precisely full row rank, so every right-hand covector is nonzero. Every dimension-zero case has its point mass and empty Fourier factor; when the target has dimension zero, its distributions are smooth constants and both wavefront sets are empty.