[proofplan]
We work locally on compact subsets of $U$, where proper support allows the composed kernel to be represented by the standard Kohn-Nirenberg oscillatory integral for the composition symbol. Taylor expansion of $b(x+y,\xi)$ in the spatial increment $y$ through order $N-1$ gives the finite sum and an integral remainder. Each Taylor monomial is evaluated by [integration by parts](/theorems/210) in the dual variable, converting $y^\alpha$ into $i^{-|\alpha|}\partial_\xi^\alpha a$. The order-$N$ Taylor remainder is estimated by the standard oscillatory integration-by-parts argument, which gains exactly $N$ powers of $\langle\xi\rangle^{-1}$ and places the remainder in $S^{m+m'-N}$.
[/proofplan]
[step:Localize the composed operator to the standard oscillatory product formula]
Let $K\subset U$ be compact. Since $\operatorname{Op}(a)$, $\operatorname{Op}(b)$, and $\operatorname{Op}(a\# b)$ are properly supported, there exists a compact set $K_1\subset U$ such that, for every $u\in C_c^\infty(U)$ with $\operatorname{supp}u\subset K$, all spatial variables appearing in the kernels of $\operatorname{Op}(a)$, $\operatorname{Op}(b)$, $\operatorname{Op}(a\# b)$, and the composition $\operatorname{Op}(a)\operatorname{Op}(b)$ over $K$ remain in $K_1$. Choose $\psi\in C_c^\infty(U)$ with $\psi=1$ on a neighbourhood of $K_1$.
By the local Kohn-Nirenberg composition formula for properly supported pseudodifferential operators, applied with this cutoff, the composition is represented modulo a smoothing operator over $K$ by a symbol $c:K\times\mathbb{R}^n\to\mathbb{C}$ given by the oscillatory integral
\begin{align*}
c(x,\xi)=\operatorname{Os}\,(2\pi)^{-n}\int_{\mathbb{R}^n}\int_{\mathbb{R}^n}e^{-iy\cdot\eta}a(x,\xi+\eta)\psi(x+y)b(x+y,\xi)\,d\mathcal{L}^n(y)\,d\mathcal{L}^n(\eta).
\end{align*}
Here $\operatorname{Os}$ denotes the regularized oscillatory integral obtained by inserting a Schwartz cutoff $\rho(\varepsilon y,\varepsilon\eta)$ with $\rho(0,0)=1$ and passing to the limit as $\varepsilon\downarrow 0$; the standard oscillatory-integral theorem permits differentiation under $\operatorname{Os}$ and [integration by parts](/theorems/2098) with differential operators whose formal adjoints fix $e^{-iy\cdot\eta}$, provided the differentiated amplitudes have polynomial growth. These hypotheses hold here because $a$ and $b$ are symbols and $\psi$ is compactly supported. The cutoff is harmless on $K$ because $\psi=1$ on the spatial region reached by the properly supported composition.
We use the localized symbol uniqueness modulo smoothing theorem for Kohn-Nirenberg quantization: if $q\in S^r(U_0\times\mathbb{R}^n)$ on an [open set](/page/Open%20Set) $U_0\subset U$, if $\chi\in C_c^\infty(U_0)$ is identically $1$ on a neighbourhood of $K$, and if the localized operator $\chi\operatorname{Op}(q)\chi$ has a $C^\infty$ Schwartz kernel on $U_0\times U_0$, then $q\in S^{-\infty}(K\times\mathbb{R}^n)$. This localized form does not require $q$ itself to define a globally properly supported operator; the cutoffs provide the needed proper support.
Apply this theorem on an open neighbourhood $U_0$ of $K_1$ on which the above cutoff construction represents $\operatorname{Op}(a)\operatorname{Op}(b)$ modulo a smoothing operator. The symbol $q:=a\# b-c$ belongs locally to $S^{m+m'}$, and the hypothesis that $\operatorname{Op}(a\# b)-\operatorname{Op}(a)\operatorname{Op}(b)$ is smoothing, together with the construction of $c$, gives $\chi\operatorname{Op}(q)\chi$ smoothing for every $\chi\in C_c^\infty(U_0)$ equal to $1$ near $K$. Therefore $a\# b-c\in S^{-\infty}(K\times\mathbb{R}^n)$, hence $a\# b-c\in S^{m+m'-N}(K\times\mathbb{R}^n)$. It is enough to prove the claimed finite-order expansion for $c$ on every compact $K\subset U$.
[/step]
[step:Taylor expand the spatial dependence of $b$ to order $N-1$]
For fixed $\xi\in\mathbb{R}^n$, define $B_\xi:\mathbb{R}^n\to\mathbb{C}$ by extending $z\mapsto \psi(z)b(z,\xi)$ by zero outside $U$. This extension is smooth on $\mathbb{R}^n$ because $\psi\in C_c^\infty(U)$ has support compactly contained in $U$. For fixed $x\in K$, $\xi\in\mathbb{R}^n$, and $y\in\mathbb{R}^n$, apply Taylor's formula with integral remainder on $\mathbb{R}^n$ to the smooth map $B_\xi$ at $x$ in the direction $y$. Then
\begin{align*}
B_\xi(x+y)=\sum_{|\alpha|<N}\frac{y^\alpha}{\alpha!}\partial_x^\alpha B_\xi(x)+\sum_{|\alpha|=N}\frac{N y^\alpha}{\alpha!}\int_0^1(1-t)^{N-1}\partial_x^\alpha B_\xi(x+ty)\,d\mathcal{L}^1(t).
\end{align*}
Since $\psi=1$ near $K$, for $x\in K$ one has $\partial_x^\alpha B_\xi(x)=\partial_x^\alpha b(x,\xi)$ for every multi-index $\alpha$.
Substituting the Taylor expansion into the oscillatory integral defining $c$ gives
\begin{align*}
c(x,\xi)=\sum_{|\alpha|<N}\frac{\partial_x^\alpha b(x,\xi)}{\alpha!}I_\alpha(x,\xi)+R_N(x,\xi),
\end{align*}
where $I_\alpha:K\times\mathbb{R}^n\to\mathbb{C}$ is defined by
\begin{align*}
I_\alpha(x,\xi)=\operatorname{Os}\,(2\pi)^{-n}\int_{\mathbb{R}^n}\int_{\mathbb{R}^n}e^{-iy\cdot\eta}y^\alpha a(x,\xi+\eta)\,d\mathcal{L}^n(y)\,d\mathcal{L}^n(\eta)
\end{align*}
and $R_N:K\times\mathbb{R}^n\to\mathbb{C}$ is the corresponding oscillatory integral containing the Taylor remainder.
[guided]
The composition formula has reduced the problem to understanding the factor $\psi(x+y)b(x+y,\xi)$ inside the oscillatory integral. We expand only in the spatial variable because the final symbolic product contains $\partial_x^\alpha b$ and $\partial_\xi^\alpha a$.
For each fixed $\xi\in\mathbb{R}^n$, define the smooth function $B_\xi:\mathbb{R}^n\to\mathbb{C}$ by setting $B_\xi(z)=\psi(z)b(z,\xi)$ for $z\in U$ and $B_\xi(z)=0$ for $z\notin U$. This is smooth because the support of $\psi$ is a compact subset of $U$, so the product $\psi b$ vanishes on a neighbourhood of $\mathbb{R}^n\setminus U$. Taylor's formula on $\mathbb{R}^n$ at the point $x$ in the direction $y$ gives
\begin{align*}
B_\xi(x+y)=\sum_{|\alpha|<N}\frac{y^\alpha}{\alpha!}\partial_x^\alpha B_\xi(x)+\sum_{|\alpha|=N}\frac{N y^\alpha}{\alpha!}\int_0^1(1-t)^{N-1}\partial_x^\alpha B_\xi(x+ty)\,d\mathcal{L}^1(t).
\end{align*}
The factor $N(1-t)^{N-1}$ is the standard integral remainder coefficient for total order $N$. The cutoff $\psi$ was chosen to equal $1$ on a neighbourhood of the compact region where $x$ lies, so at $x\in K$ all derivatives of $B_\xi$ that occur in the polynomial part agree with those of $b(\cdot,\xi)$:
\begin{align*}
\partial_x^\alpha B_\xi(x)=\partial_x^\alpha b(x,\xi).
\end{align*}
Substituting this identity into the oscillatory integral separates $c$ into polynomial Taylor terms and one remainder term:
\begin{align*}
c(x,\xi)=\sum_{|\alpha|<N}\frac{\partial_x^\alpha b(x,\xi)}{\alpha!}I_\alpha(x,\xi)+R_N(x,\xi).
\end{align*}
The point of this separation is that the polynomial terms can be computed exactly by integration by parts, while the integral remainder already contains $N$ powers of $y$, which will become $N$ derivatives of $a$ in the dual variable and therefore lower the symbol order by $N$.
[/guided]
[/step]
[step:Convert Taylor monomials into $\xi$-derivatives of $a$]
For each multi-index $\alpha$ with $|\alpha|<N$, use the identity
\begin{align*}
y^\alpha e^{-iy\cdot\eta}=i^{|\alpha|}\partial_\eta^\alpha e^{-iy\cdot\eta}.
\end{align*}
The oscillatory integration-by-parts theorem applies because every $\eta$-derivative of $a(x,\xi+\eta)$ has polynomial growth uniformly for $x\in K$. Integrating by parts in $\eta$ in the oscillatory integral defining $I_\alpha$ gives
\begin{align*}
I_\alpha(x,\xi)=i^{-|\alpha|}\operatorname{Os}\,(2\pi)^{-n}\int_{\mathbb{R}^n}\int_{\mathbb{R}^n}e^{-iy\cdot\eta}\partial_\eta^\alpha\{a(x,\xi+\eta)\}\,d\mathcal{L}^n(y)\,d\mathcal{L}^n(\eta).
\end{align*}
Because $\partial_\eta^\alpha a(x,\xi+\eta)=\partial_\xi^\alpha a(x,\xi+\eta)$, the inverse Fourier identity for the oscillatory kernel, namely $\operatorname{Os}\,(2\pi)^{-n}\int_{\mathbb{R}^n}\int_{\mathbb{R}^n}e^{-iy\cdot\eta}f(\xi+\eta)\,d\mathcal{L}^n(y)\,d\mathcal{L}^n(\eta)=f(\xi)$ for symbols $f$, gives
\begin{align*}
I_\alpha(x,\xi)=i^{-|\alpha|}\partial_\xi^\alpha a(x,\xi).
\end{align*}
Thus the polynomial part of $c$ is
\begin{align*}
\sum_{|\alpha|<N}\frac{i^{-|\alpha|}}{\alpha!}\partial_\xi^\alpha a(x,\xi)\partial_x^\alpha b(x,\xi).
\end{align*}
[guided]
Fix a multi-index $\alpha$ with $|\alpha|<N$. The polynomial Taylor term contains the factor $y^\alpha$, and the purpose of this step is to move that factor onto $a$ as a derivative in the dual variable $\eta$. The elementary identity
\begin{align*}
y^\alpha e^{-iy\cdot\eta}=i^{|\alpha|}\partial_\eta^\alpha e^{-iy\cdot\eta}
\end{align*}
turns multiplication by $y^\alpha$ into differentiation of the oscillatory exponential. Since $a\in S^m(U\times\mathbb{R}^n)$, every derivative $\partial_\eta^\delta a(x,\xi+\eta)$ has polynomial growth in $\eta$ uniformly for $x\in K$, so the oscillatory integration-by-parts theorem is applicable.
Integrating by parts in $\eta$ transfers $\partial_\eta^\alpha$ from the exponential onto $a(x,\xi+\eta)$ and contributes the sign factor $i^{-|\alpha|}$:
\begin{align*}
I_\alpha(x,\xi)=i^{-|\alpha|}\operatorname{Os}\,(2\pi)^{-n}\int_{\mathbb{R}^n}\int_{\mathbb{R}^n}e^{-iy\cdot\eta}\partial_\eta^\alpha\{a(x,\xi+\eta)\}\,d\mathcal{L}^n(y)\,d\mathcal{L}^n(\eta).
\end{align*}
The variables $\eta$ and $\xi$ enter $a$ only through the sum $\xi+\eta$, hence
\begin{align*}
\partial_\eta^\alpha\{a(x,\xi+\eta)\}=\partial_\xi^\alpha a(x,\xi+\eta).
\end{align*}
Finally, the oscillatory kernel is the identity kernel in the frequency variable: for every symbol $f:\mathbb{R}^n\to\mathbb{C}$,
\begin{align*}
\operatorname{Os}\,(2\pi)^{-n}\int_{\mathbb{R}^n}\int_{\mathbb{R}^n}e^{-iy\cdot\eta}f(\xi+\eta)\,d\mathcal{L}^n(y)\,d\mathcal{L}^n(\eta)=f(\xi).
\end{align*}
Applying this identity to $f(\zeta)=\partial_\xi^\alpha a(x,\zeta)$ gives
\begin{align*}
I_\alpha(x,\xi)=i^{-|\alpha|}\partial_\xi^\alpha a(x,\xi).
\end{align*}
Therefore the polynomial part of the composed symbol is
\begin{align*}
\sum_{|\alpha|<N}\frac{i^{-|\alpha|}}{\alpha!}\partial_\xi^\alpha a(x,\xi)\partial_x^\alpha b(x,\xi).
\end{align*}
[/guided]
[/step]
[step:Estimate the Taylor remainder as a symbol of order $m+m'-N$]
It remains to prove $R_N\in S^{m+m'-N}(K\times\mathbb{R}^n)$. Let $\beta$ and $\gamma$ be multi-indices. Differentiating $R_N$ by $\partial_x^\beta\partial_\xi^\gamma$ is justified by the differentiation property of regularized oscillatory integrals. After applying Leibniz's rule, each summand is a finite constant multiple of an oscillatory integral of the form
\begin{align*}
\operatorname{Os}\int_0^1\int_{\mathbb{R}^n}\int_{\mathbb{R}^n}e^{-iy\cdot\eta}y^\alpha A_{\beta_1,\gamma_1}(x,\xi+\eta)B_{\beta_2,\gamma_2,t}(x,y,\xi)\,d\mathcal{L}^n(y)\,d\mathcal{L}^n(\eta)\,d\mathcal{L}^1(t)
\end{align*}
with $|\alpha|=N$. Here $A_{\beta_1,\gamma_1}:K\times\mathbb{R}^n\to\mathbb{C}$ denotes a derivative of $a$ of order $\beta_1$ in $x$ and $\gamma_1$ in $\xi$, and $B_{\beta_2,\gamma_2,t}:K\times\mathbb{R}^n\times\mathbb{R}^n\to\mathbb{C}$ denotes a derivative of the zero-extended function $B_\xi$ evaluated at $x+ty$, including the derivatives falling on the affine map $x\mapsto x+ty$.
Integrating by parts in $\eta$ converts $y^\alpha$ into $i^{-N}\partial_\eta^\alpha$ falling on $A_{\beta_1,\gamma_1}(x,\xi+\eta)$. Hence the $a$ factor becomes a derivative of $a$ of total $\xi$-order $|\gamma_1|+N$. The symbol estimates for $a$ and for the compactly supported zero extension of $\psi b$ give constants $C_a>0$ and $C_b>0$, depending only on $K$, the displayed multi-indices, and finitely many symbol seminorms of $a$ and $b$, such that
\begin{align*}
|\partial_\eta^\delta A_{\beta_1,\gamma_1+\alpha}(x,\xi+\eta)|\le C_a\langle\xi+\eta\rangle^{m-|\gamma_1|-N-|\delta|}
\end{align*}
for every multi-index $\delta$ occurring below, and
\begin{align*}
|\partial_y^\mu B_{\beta_2,\gamma_2,t}(x,y,\xi)|\le C_b\langle\xi\rangle^{m'-|\gamma_2|}
\end{align*}
for every multi-index $\mu$ occurring below, every $x\in K$, every $y\in\mathbb{R}^n$, every $\xi\in\mathbb{R}^n$, and every $t\in[0,1]$. The latter estimate is uniform in $t$ because each $y$-derivative of $B_{\beta_2,\gamma_2,t}(x,y,\xi)$ contributes a factor $t^{|\mu|}$, and $0\le t\le 1$.
We now apply the integration-by-parts operators
\begin{align*}
L_y=(1+|\eta|^2)^{-1}(1-\Delta_y)
\end{align*}
and
\begin{align*}
L_\eta=(1+|y|^2)^{-1}(1-\Delta_\eta),
\end{align*}
which satisfy $L_y e^{-iy\cdot\eta}=e^{-iy\cdot\eta}$ and $L_\eta e^{-iy\cdot\eta}=e^{-iy\cdot\eta}$. Choose an integer $M>n+|m|+|m'|+|\gamma|+N+1$ and integrate by parts $M$ times with each operator. Derivatives produced by the formal adjoints of $L_y$ and $L_\eta$ are controlled by the two estimates above, while the weights produce an integrable factor bounded by a finite sum of terms of the form
\begin{align*}
(1+|y|^2)^{-M}(1+|\eta|^2)^{-M}\langle\xi+\eta\rangle^{m-|\gamma_1|-N}\langle\xi\rangle^{m'-|\gamma_2|}.
\end{align*}
The formal adjoints of $L_y$ and $L_\eta$ only differentiate the amplitude finitely many times and multiply it by rational weights bounded by constants times powers of $(1+|y|^2)^{-1}$ and $(1+|\eta|^2)^{-1}$. Thus the displayed majorant is valid after removing the regularizing cutoff, and it is independent of $t\in[0,1]$; dominated convergence for the regularized oscillatory integrals then permits the $t$-integration to be carried out against the same bound. The $y$-factor is integrable over $\mathbb{R}^n$. For the $\eta$-integral, the choice of $M$ and Peetre's inequality give
\begin{align*}
\int_{\mathbb{R}^n}(1+|\eta|^2)^{-M}\langle\xi+\eta\rangle^{m-|\gamma_1|-N}\,d\mathcal{L}^n(\eta)\le C_M\langle\xi\rangle^{m-|\gamma_1|-N}.
\end{align*}
Since the Leibniz splitting satisfies $|\gamma_1|+|\gamma_2|=|\gamma|$, every summand is bounded by
\begin{align*}
C_{\beta,\gamma,K}\langle\xi\rangle^{m+m'-N-|\gamma|}.
\end{align*}
Therefore
\begin{align*}
|\partial_x^\beta\partial_\xi^\gamma R_N(x,\xi)|\le C_{\beta,\gamma,K}\langle\xi\rangle^{m+m'-N-|\gamma|}
\end{align*}
for all $x\in K$ and all $\xi\in\mathbb{R}^n$. This is precisely the defining seminorm estimate for $R_N\in S^{m+m'-N}(K\times\mathbb{R}^n)$.
[guided]
The delicate point is that the Taylor remainder contains $\partial_x^\alpha B_\xi(x+ty)$, and for small $t$ the condition $x+ty\in\operatorname{supp}\psi$ does not confine $y$ to a fixed compact set. We therefore do not use compact support in $y$. Instead, we use oscillatory integration by parts to create explicit decay in both $y$ and $\eta$.
Let $\beta$ and $\gamma$ be multi-indices. Differentiating $R_N$ by $\partial_x^\beta\partial_\xi^\gamma$ is allowed because regularized oscillatory integrals may be differentiated when the differentiated amplitudes have polynomial growth; this follows from the symbol estimates for $a$ and $b$ and from the compact support of $\psi$ in the spatial variable. After Leibniz's rule, it is enough to estimate terms of the form
\begin{align*}
\operatorname{Os}\int_0^1\int_{\mathbb{R}^n}\int_{\mathbb{R}^n}e^{-iy\cdot\eta}y^\alpha A_{\beta_1,\gamma_1}(x,\xi+\eta)B_{\beta_2,\gamma_2,t}(x,y,\xi)\,d\mathcal{L}^n(y)\,d\mathcal{L}^n(\eta)\,d\mathcal{L}^1(t),
\end{align*}
where $|\alpha|=N$. The factor $A_{\beta_1,\gamma_1}$ is a derivative of $a$, while $B_{\beta_2,\gamma_2,t}$ is a derivative of the zero-extended cutoff product $B_\xi$ evaluated at $x+ty$.
First use the identity $y^\alpha e^{-iy\cdot\eta}=i^N\partial_\eta^\alpha e^{-iy\cdot\eta}$ and integrate by parts in $\eta$. This moves $N$ derivatives onto $a$, so the $a$ factor has $N$ additional derivatives in the frequency variable. Consequently, for every derivative $\partial_\eta^\delta$ that will appear later,
\begin{align*}
|\partial_\eta^\delta A_{\beta_1,\gamma_1+\alpha}(x,\xi+\eta)|\le C_a\langle\xi+\eta\rangle^{m-|\gamma_1|-N-|\delta|}.
\end{align*}
For the $b$ factor, the zero extension of $\psi b$ is smooth and compactly supported in the spatial variable. Derivatives in $y$ produce factors of $t$ because the spatial argument is $x+ty$, and these factors are bounded by $1$ for $t\in[0,1]$. Hence
\begin{align*}
|\partial_y^\mu B_{\beta_2,\gamma_2,t}(x,y,\xi)|\le C_b\langle\xi\rangle^{m'-|\gamma_2|}
\end{align*}
uniformly in $x\in K$, $y\in\mathbb{R}^n$, $\xi\in\mathbb{R}^n$, and $t\in[0,1]$.
Now apply the operators
\begin{align*}
L_y=(1+|\eta|^2)^{-1}(1-\Delta_y)
\end{align*}
and
\begin{align*}
L_\eta=(1+|y|^2)^{-1}(1-\Delta_\eta).
\end{align*}
They fix the oscillatory exponential, so integrating by parts with their formal adjoints leaves the value of the oscillatory integral unchanged and places decay factors on the amplitude. Taking an integer $M>n+|m|+|m'|+|\gamma|+N+1$ gives an absolutely integrable majorant of the form
\begin{align*}
(1+|y|^2)^{-M}(1+|\eta|^2)^{-M}\langle\xi+\eta\rangle^{m-|\gamma_1|-N}\langle\xi\rangle^{m'-|\gamma_2|}.
\end{align*}
This bound is uniform in $t$, so integration over $t\in[0,1]$ causes no singular factor. The $y$-integral is finite because $M>n$. For the $\eta$-integral, Peetre's inequality and the choice of $M$ imply
\begin{align*}
\int_{\mathbb{R}^n}(1+|\eta|^2)^{-M}\langle\xi+\eta\rangle^{m-|\gamma_1|-N}\,d\mathcal{L}^n(\eta)\le C_M\langle\xi\rangle^{m-|\gamma_1|-N}.
\end{align*}
Multiplying by the $b$ estimate and using $|\gamma_1|+|\gamma_2|=|\gamma|$ gives
\begin{align*}
|\partial_x^\beta\partial_\xi^\gamma R_N(x,\xi)|\le C_{\beta,\gamma,K}\langle\xi\rangle^{m+m'-N-|\gamma|}.
\end{align*}
This is exactly the symbol estimate of order $m+m'-N$ on $K\times\mathbb{R}^n$.
[/guided]
[/step]
[step:Pass from the local composition symbol to the chosen product symbol]
For every compact $K\subset U$, the preceding steps prove
\begin{align*}
c-\sum_{|\alpha|<N}\frac{i^{-|\alpha|}}{\alpha!}\partial_\xi^\alpha a\,\partial_x^\alpha b\in S^{m+m'-N}(K\times\mathbb{R}^n).
\end{align*}
Since $a\# b-c\in S^{-\infty}(K\times\mathbb{R}^n)$ and $S^{-\infty}(K\times\mathbb{R}^n)\subset S^{m+m'-N}(K\times\mathbb{R}^n)$, we obtain
\begin{align*}
a\# b-\sum_{|\alpha|<N}\frac{i^{-|\alpha|}}{\alpha!}\partial_\xi^\alpha a\,\partial_x^\alpha b\in S^{m+m'-N}(K\times\mathbb{R}^n).
\end{align*}
Because $K\subset U$ was arbitrary, the defining local seminorm estimates hold on every compact subset of $U$. Therefore the remainder belongs to $S^{m+m'-N}(U\times\mathbb{R}^n)$, which is the desired conclusion.
[/step]
