[proofplan] The assertion is exactly the defining seminorm estimate for the remainder in an asymptotic symbol expansion. We fix the truncation order $N$ and name the truncated remainder $r_N$. The hypothesis $a \sim \sum_{j=0}^\infty a_j$ says precisely that $r_N$ belongs to the symbol class $S^{m_N}_{1,0}(U \times \mathbb{R}^n)$. Applying the defining compact-set estimate for that symbol class gives the desired constant and bound. [/proofplan]

[step:Define the truncated remainder at order $N$]Fix $N \geq 1$. Define the smooth map \begin{align*} r_N: U \times \mathbb{R}^n \to \mathbb{C} \end{align*} by \begin{align*} r_N(x,\xi) = a(x,\xi)-\sum_{j=0}^{N-1}a_j(x,\xi). \end{align*} By the definition of the asymptotic relation $a \sim \sum_{j=0}^{\infty} a_j$, this remainder satisfies \begin{align*} r_N \in S^{m_N}_{1,0}(U \times \mathbb{R}^n). \end{align*}[/step]

[guided]Fix $N \geq 1$. The theorem concerns the error made by stopping the asymptotic expansion before the term $a_N$, so we name that error. Define the smooth map \begin{align*} r_N: U \times \mathbb{R}^n \to \mathbb{C} \end{align*} by \begin{align*} r_N(x,\xi) = a(x,\xi)-\sum_{j=0}^{N-1}a_j(x,\xi). \end{align*} The crucial point is that the asymptotic expansion hypothesis is not a limiting statement to be proved again here. It is already a symbolic membership statement for every truncated remainder. Namely, the meaning of $a \sim \sum_{j=0}^{\infty} a_j$ is that, for each $N \geq 1$, \begin{align*} a-\sum_{j=0}^{N-1}a_j \in S^{m_N}_{1,0}(U \times \mathbb{R}^n). \end{align*} With the notation above, this says exactly that \begin{align*} r_N \in S^{m_N}_{1,0}(U \times \mathbb{R}^n). \end{align*} This is the only place where the asymptotic expansion assumption is used.[/guided]

[step:Apply the defining seminorm estimate for $S^{m_N}_{1,0}$]Let $K \subset U$ be compact, and let $\alpha,\beta \in (\mathbb{N} \cup \{0\})^n$ be multi-indices. Since $r_N \in S^{m_N}_{1,0}(U \times \mathbb{R}^n)$, the defining estimate for the symbol class gives a constant $C_{K,\alpha,\beta,N} > 0$ such that \begin{align*} |\partial_x^\alpha \partial_\xi^\beta r_N(x,\xi)| \leq C_{K,\alpha,\beta,N}\langle \xi\rangle^{m_N-|\beta|} \end{align*} for all $x \in K$ and all $\xi \in \mathbb{R}^n$. Substituting the definition of $r_N$ gives \begin{align*} \left|\partial_x^\alpha \partial_\xi^\beta\left(a(x,\xi)-\sum_{j=0}^{N-1}a_j(x,\xi)\right)\right| \leq C_{K,\alpha,\beta,N}\langle \xi\rangle^{m_N-|\beta|}. \end{align*} This is the desired estimate.[/step]

[guided]Let $K \subset U$ be compact, and let $\alpha,\beta \in (\mathbb{N} \cup \{0\})^n$ be multi-indices. The definition of the symbol class $S^{m_N}_{1,0}(U \times \mathbb{R}^n)$ says that every mixed derivative of $r_N$ satisfies a compact-set estimate with loss $|\beta|$ in the order of decay in the frequency variable. Since the preceding step proved \begin{align*} r_N \in S^{m_N}_{1,0}(U \times \mathbb{R}^n), \end{align*} this definition applies to the compact set $K$ and the multi-indices $\alpha$ and $\beta$. Hence there is a constant $C_{K,\alpha,\beta,N} > 0$ such that \begin{align*} |\partial_x^\alpha \partial_\xi^\beta r_N(x,\xi)| \leq C_{K,\alpha,\beta,N}\langle \xi\rangle^{m_N-|\beta|} \end{align*} for all $x \in K$ and all $\xi \in \mathbb{R}^n$. Now insert the definition of the remainder. For every $(x,\xi) \in U \times \mathbb{R}^n$, \begin{align*} r_N(x,\xi) = a(x,\xi)-\sum_{j=0}^{N-1}a_j(x,\xi). \end{align*} Therefore the derivative estimate for $r_N$ is exactly \begin{align*} \left|\partial_x^\alpha \partial_\xi^\beta\left(a(x,\xi)-\sum_{j=0}^{N-1}a_j(x,\xi)\right)\right| \leq C_{K,\alpha,\beta,N}\langle \xi\rangle^{m_N-|\beta|} \end{align*} for all $x \in K$ and all $\xi \in \mathbb{R}^n$. This is the claimed remainder estimate.[/guided]