[proofplan] We rewrite the $t$-quantised operator as an amplitude operator whose amplitude is obtained by evaluating $a$ at the affine point $(1-t)x+ty$. The [amplitude reduction theorem](/theorems/7671) then gives an equivalent left symbol modulo smoothing, with an expansion involving $\partial_\xi^\alpha D_y^\alpha$ of that amplitude on the diagonal $y=x$. The chain rule converts the $y$-derivatives into the factor $t^{|\alpha|}D_x^\alpha a(x,\xi)$. Finally, the zeroth term is $a$, while all nonzero multi-index terms contain at least one $\xi$-derivative and therefore have order at most $m-1$. [/proofplan] [step:Rewrite the $t$-quantisation as an amplitude operator] Define the amplitude \begin{align*} A: U \times U \times \mathbb{R}^n \to \mathbb{C}, \qquad A(x,y,\xi) := a((1-t)x+ty,\xi). \end{align*} This map is globally well-defined because the repaired statement assumes $U$ is convex: for all $x,y \in U$ and $t \in [0,1]$, the point $(1-t)x+ty$ belongs to $U$. With this notation, \begin{align*} \operatorname{Op}_t(a)u(x) = (2\pi)^{-n}\operatorname{Os}\!\int_{\mathbb{R}^n}\int_U e^{i(x-y)\cdot \xi} A(x,y,\xi)u(y)\,d\mathcal{L}^n(y)\,d\mathcal{L}^n(\xi). \end{align*} Thus $\operatorname{Op}_t(a)$ is exactly the amplitude operator with amplitude $A$. [/step] [step:Apply amplitude reduction to obtain a left symbol] We use the amplitude reduction theorem for pseudodifferential amplitudes in the following form: if $A \in S^m(U \times U \times \mathbb{R}^n)$ is a smooth amplitude of order $m$ in $\xi$, uniformly on compact subsets of $U \times U$, then the corresponding amplitude operator differs by a smoothing operator from a left quantisation $\operatorname{Op}_L(a_L)$ with $a_L \in S^m(U \times \mathbb{R}^n)$, and \begin{align*} a_L(x,\xi) \sim \sum_{\alpha \in \mathbb{N}_0^n} \frac{1}{\alpha!}\partial_\xi^\alpha D_y^\alpha A(x,y,\xi)\big|_{y=x}. \end{align*} The hypotheses are satisfied here. The preceding step shows that $A$ is globally defined on $U \times U \times \mathbb{R}^n$. Since $a$ is a symbol of order $m$, the affine map $(x,y)\mapsto (1-t)x+ty$ is smooth from $U \times U$ to $U$, and differentiating $A$ in $x$ or $y$ only produces finite linear combinations of derivatives of $a$ with constant coefficients depending on $t$, the required symbol estimates hold uniformly on compact subsets of $U \times U$. [guided] The point of amplitude reduction is to replace an operator whose symbol depends on both $x$ and $y$ by a left-quantised operator whose symbol depends only on the output variable $x$ and the frequency variable $\xi$. We apply the amplitude reduction theorem to the amplitude \begin{align*} A: U \times U \times \mathbb{R}^n \to \mathbb{C}, \qquad A(x,y,\xi) := a((1-t)x+ty,\xi). \end{align*} First we check that this is a legitimate amplitude on the stated domain. Because the theorem statement now assumes that $U$ is convex, every affine combination $(1-t)x+ty$ with $x,y \in U$ and $t \in [0,1]$ lies in $U$. Hence the expression defining $A$ always evaluates $a$ at a point of its declared base domain. The theorem requires that $A$ be a smooth symbol of order $m$ in the frequency variable, uniformly on compact subsets of $U \times U$. This follows from the symbol estimates for $a \in S^m(U \times \mathbb{R}^n)$: each $x$- or $y$-derivative of $A$ is a finite constant-coefficient combination of derivatives of $a$ in its base variable, evaluated at $(1-t)x+ty$, and each $\xi$-derivative is the corresponding $\xi$-derivative of $a$. The affine map sends compact subsets of $U \times U$ into compact subsets of $U$, so the local symbol seminorm bounds for $a$ give the required uniform bounds for $A$. Therefore the same symbol order $m$ is preserved. Amplitude reduction then produces a left symbol $a_L \in S^m(U \times \mathbb{R}^n)$ such that the amplitude operator defined by $A$ differs from $\operatorname{Op}_L(a_L)$ by a smoothing operator. It also gives the asymptotic expansion \begin{align*} a_L(x,\xi) \sim \sum_{\alpha \in \mathbb{N}_0^n} \frac{1}{\alpha!}\partial_\xi^\alpha D_y^\alpha A(x,y,\xi)\big|_{y=x}. \end{align*} This is the exact place where the dependence on the quantisation parameter $t$ enters the symbol: all that remains is to compute the diagonal derivatives $D_y^\alpha A(x,y,\xi)\big|_{y=x}$. [/guided] [/step] [step:Compute the diagonal derivatives by the chain rule] Let $\alpha \in \mathbb{N}_0^n$ be a multi-index. Since \begin{align*} A(x,y,\xi) = a((1-t)x+ty,\xi), \end{align*} the chain rule gives \begin{align*} D_y^\alpha A(x,y,\xi) = t^{|\alpha|}D_x^\alpha a((1-t)x+ty,\xi). \end{align*} Evaluating on the diagonal $y=x$ gives \begin{align*} D_y^\alpha A(x,y,\xi)\big|_{y=x} = t^{|\alpha|}D_x^\alpha a(x,\xi). \end{align*} Substituting this identity into the amplitude reduction expansion yields \begin{align*} a_L(x,\xi) \sim \sum_{\alpha \in \mathbb{N}_0^n} \frac{t^{|\alpha|}}{\alpha!}\partial_\xi^\alpha D_x^\alpha a(x,\xi). \end{align*} This proves the asserted asymptotic formula. [/step] [step:Identify the principal part and conclude equivalence modulo lower order operators] The term corresponding to $\alpha=0$ in the expansion is exactly $a(x,\xi)$. If $\alpha \neq 0$, then $|\alpha| \geq 1$, and the factor $\partial_\xi^\alpha$ lowers the symbolic order by $|\alpha|$. Hence \begin{align*} \partial_\xi^\alpha D_x^\alpha a \in S^{m-|\alpha|}(U \times \mathbb{R}^n) \subset S^{m-1}(U \times \mathbb{R}^n). \end{align*} Therefore \begin{align*} a_L-a \in S^{m-1}(U \times \mathbb{R}^n) \end{align*} modulo symbols of arbitrarily low order in the asymptotic sense. Since the left quantisation of a symbol in $S^{m-1}$ is an operator in $\Psi^{m-1}(U)$, and since the already produced error is smoothing, $\operatorname{Op}_t(a)-\operatorname{Op}_L(a)$ is an operator of order at most $m-1$ modulo smoothing. Now let $s,t \in [0,1]$. Applying the preceding conclusion separately to $s$ and $t$ gives that both $\operatorname{Op}_s(a)-\operatorname{Op}_L(a)$ and $\operatorname{Op}_t(a)-\operatorname{Op}_L(a)$ lie in $\Psi^{m-1}(U)$ modulo smoothing. Subtracting these two relations gives \begin{align*} \operatorname{Op}_t(a)-\operatorname{Op}_s(a) \in \Psi^{m-1}(U) \end{align*} modulo smoothing operators. This is precisely the claimed independence of the quantisation parameter modulo lower order terms. [/step]