Complex smooth division of order one
Complete proof excerpt from AN-04, “Fourier-integral operators,” lesson “Real and complex symplectic normal forms of functions,” §4. Original AN-04 exposition, CC0 1.0 Universal.
The fifty-line statement and proof below are preserved verbatim after LF newline normalization. The surrounding symplectic normal-form argument is outside this excerpt. Its citation to a book identifies the classical theorem; the complete proof is supplied here.
The dividend is used on its actual supplied neighborhood. A common output neighborhood applies to dividends actually supplied on one common domain; unrelated local germs first require intersection with their individual domains. In the receiver, the preparation of the divisor and all dividend restrictions retain this distinction.
Smooth complex division. If a complex function , with real , has and , then every smooth has a representation
on a neighborhood chosen from and the original domain, with smooth and complex valued. The remainder is independent of . This is the case of Hörmander I, Theorem 7.5.6; its hypotheses are those of Theorem 7.5.5. Neither the quotient nor the remainder is asserted to be unique. The following proof treats complex functions in real variables; it does not assume that their real zeros form a parameter graph.
Proof. First extend a smooth function almost analytically in . Multiply it by a fixed real cutoff equal to one on the patch in use. For , choose a fixed smooth cutoff , equal to one near zero, and put
All coefficients and their derivatives are bounded on a fixed larger compact patch. A derivative of total order of the -th term is bounded by . Choose positive radii decreasing to zero so that these bounds are at most for every . Each fixed derivative series then converges uniformly after finitely many terms. The sum is smooth on a fixed complex domain; only the radii and its seminorm bounds depend on . Its normal jets at are the formal analytic jets. Thus, with , Taylor's integral remainder gives
The derivatives here include all real parameters . No holomorphic continuation of an arbitrary smooth function is claimed.
Apply this construction to , writing its extension as . At the mark, its real derivative in is complex multiplication by . In particular it is invertible. A direct parameter argument produces a smooth complex root , with . Indeed the real map
has derivative zero at the mark. On a sufficiently small closed complex disc its derivative norm is at most , uniformly on a smaller parameter patch. Shrink that patch so that its value at has modulus at most times the disc radius. It maps the disc into itself and its fixed point lies in the interior. Iteration from zero has geometrically summable successive differences, so completeness of gives its unique fixed point . The same contraction estimate first bounds parameter differences of by a constant times the parameter differences. Taylor's formula in the fixed-point identity then proves differentiability, with real derivative
The inverse exists throughout the disc by the contraction bound. This formula has continuous coefficients. Induction differentiating it proves smoothness of every order. Thus , with no real-zero or holomorphic-root assumption.
We next divide by the known graph . For any almost-analytic extension as above, the segment stays inside its fixed domain after one shrink depending on . Set . The full real chain rule gives
The sign and the error term follow from . Every derivative of is bounded by every positive power of , because the imaginary part of is and the antiholomorphic derivative has all the preceding flat estimates. Put . For , define
Each derivative of this expression costs only finitely many negative powers of . The arbitrary positive powers in the bounds for absorb them, so every derivative tends to zero faster than every power of . Its zero extension across is smooth even if that zero set is singular: multiply the expression by a smooth cutoff vanishing for and equal to one for . On the transition region all differentiated cutoff factors cost finitely many powers of , while the flat estimates give arbitrarily many positive powers. These smooth functions and all their derivatives converge uniformly to the zero extension. The fundamental theorem of calculus identifies those derivative limits with the derivatives of the limit. Consequently
holds smoothly and exactly, including real zeros of the graph.
For , use the particular extension which constructed . Its remainder is zero, so . Differentiating at the mark gives ; shrink once so never vanishes. Apply the same graph division to , obtaining . Then proves (4.1). The real and complex neighborhoods were fixed before choosing ; its extension radii and coefficient bounds may depend on . This proves exactly the needed common-neighborhood division.
Component terms
The selected original AN-04 proof is dedicated to the public domain under CC0 1.0 Universal. The source course retains its original authorship and credits. External books and separately cited prerequisite lessons remain under their own terms. No book prose or external PDF is included in this component. Reader typography is licensed separately by the receiving edition.