Let $n \in \mathbb{N}$, let $h_0>0$, and let $m,m' \in \mathbb{R}$. Let $a=(a_h)_{0<h\le h_0}$ and $b=(b_h)_{0<h\le h_0}$ be semiclassical symbol families on $T^*\mathbb{R}^n=\mathbb{R}^n_x\times \mathbb{R}^n_\xi$ with

\begin{align*} a\in S^m(T^*\mathbb{R}^n) \end{align*}

and

\begin{align*} b\in S^{m'}(T^*\mathbb{R}^n). \end{align*}

Thus, for every multi-indices $\alpha,\beta\in\mathbb{N}_0^n$, there are constants $C^a_{\alpha\beta},C^b_{\alpha\beta}>0$, independent of $h$, such that

\begin{align*} |\partial_x^\alpha\partial_\xi^\beta a_h(x,\xi)|\le C^a_{\alpha\beta}\langle \xi\rangle^{m-|\beta|} \end{align*}

and

\begin{align*} |\partial_x^\alpha\partial_\xi^\beta b_h(x,\xi)|\le C^b_{\alpha\beta}\langle \xi\rangle^{m'-|\beta|} \end{align*}

for all $(x,\xi,h)\in T^*\mathbb{R}^n\times(0,h_0]$. For $u\in\mathcal{S}(\mathbb{R}^n)$ define the left semiclassical quantization

\begin{align*} \operatorname{Op}_h(a):\mathcal{S}(\mathbb{R}^n)\to\mathcal{S}'(\mathbb{R}^n) \end{align*}

by the regularized oscillatory integral

\begin{align*} \operatorname{Op}_h(a)u(x)=(2\pi h)^{-n}\operatorname{Os}\!\int_{\mathbb{R}^n}\int_{\mathbb{R}^n}e^{i(x-y)\cdot\xi/h}a_h(x,\xi)u(y)\,d\mathcal{L}^n(y)\,d\mathcal{L}^n(\xi). \end{align*}

The composed operator $\operatorname{Op}_h(a)\operatorname{Op}_h(b)$ on $\mathcal{S}(\mathbb{R}^n)$ is understood as the regularized fourfold oscillatory integral obtained by inserting admissible Schwartz cutoffs in $(y,z,\xi,\eta)$, evaluating the absolutely convergent cutoff integrals, and passing to the cutoff limit:

\begin{align*} (\operatorname{Op}_h(a)\operatorname{Op}_h(b)u)(x)=(2\pi h)^{-2n}\operatorname{Os}\!\int_{\mathbb{R}^n}\int_{\mathbb{R}^n}\int_{\mathbb{R}^n}\int_{\mathbb{R}^n}e^{i(x-y)\cdot\eta/h}e^{i(y-z)\cdot\xi/h}a_h(x,\eta)b_h(y,\xi)u(z)\,d\mathcal{L}^n(z)\,d\mathcal{L}^n(\xi)\,d\mathcal{L}^n(y)\,d\mathcal{L}^n(\eta). \end{align*}

Here $\operatorname{Os}\!\int$ is defined by inserting Schwartz cutoffs equal to $1$ near the origin and passing to the cutoff limit in the standard oscillatory-integral topology for amplitudes with polynomial growth. Assume the standard semiclassical oscillatory-integral calculus for such amplitudes: cutoff limits are continuous under symbol-seminorm convergence; Fubini and affine changes of variables are valid after cutoff regularization and passage to the limit; semiclassical Fourier inversion holds in the oscillatory sense; integration by parts with explicitly defined phase-dual operators gives the usual local stationary and off-stationary amplitude estimates; the bilinear oscillatory product map

\begin{align*} A_h\mapsto (2\pi h)^{-n}\operatorname{Os}\!\int_{\mathbb{R}^n}\int_{\mathbb{R}^n}e^{-iY\cdot\theta/h}A_h(x,Y,\theta,\xi)\,d\mathcal{L}^n(Y)\,d\mathcal{L}^n(\theta) \end{align*}

is continuous on polynomial-growth amplitudes and satisfies the standard symbol estimate that amplitudes of the form $(\partial_\xi^\alpha a_h)(x,\xi+\theta)q_{\alpha,h}(x,Y,\xi)$, with $|\alpha|=N$ and $q_{\alpha,h}$ a symbol of order $m'$ in $\xi$ with polynomial control in $Y$, produce symbols in $S^{m+m'-N}(T^*\mathbb{R}^n)$ with seminorm constants controlled by finitely many seminorms of $a$ and $q_\alpha$; and Borel summation holds for semiclassical symbol families. A residual operator means a family of operators whose Schwartz kernels $K_h\in C^\infty(\mathbb{R}^n\times\mathbb{R}^n)$ satisfy, for every compact set $K\subset\mathbb{R}^n\times\mathbb{R}^n$, every multi-indices $\alpha,\beta\in\mathbb{N}_0^n$, and every $M\in\mathbb{N}$,

\begin{align*} \sup_{(x,y)\in K}|\partial_x^\alpha\partial_y^\beta K_h(x,y)|\le C_{K\alpha\beta M}h^M. \end{align*}

Then there exists a semiclassical symbol family $a\# b=(c_h)_{0<h\le h_0}\in S^{m+m'}(T^*\mathbb{R}^n)$ such that, for every $u\in\mathcal{S}(\mathbb{R}^n)$,

\begin{align*} \operatorname{Op}_h(a)\operatorname{Op}_h(b)u=\operatorname{Op}_h(a\# b)u \end{align*}

modulo a residual operator. Moreover $a\# b$ may be chosen to have the asymptotic expansion

\begin{align*} a\# b\sim\sum_{\alpha\in\mathbb{N}_0^n}\frac{h^{|\alpha|}}{i^{|\alpha|}\alpha!}(\partial_\xi^\alpha a_h)(x,\xi)(\partial_x^\alpha b_h)(x,\xi) \end{align*}

in the following precise sense: for every $N\in\mathbb{N}$,

\begin{align*} (a\# b)_h-\sum_{|\alpha|<N}\frac{h^{|\alpha|}}{i^{|\alpha|}\alpha!}(\partial_\xi^\alpha a_h)(\partial_x^\alpha b_h)\in h^N S^{m+m'-N}(T^*\mathbb{R}^n). \end{align*}

Any two symbol families satisfying this complete asymptotic expansion differ by an element of $h^\infty S^{-\infty}(T^*\mathbb{R}^n)$.