[proofplan] The proof is a direct verification of the defining seminorm estimates. Differentiation is stable because differentiating an already differentiated symbol only asks for a higher-order derivative estimate that is already included in the definition of $S(m)$. Multiplication is handled by the multi-index Leibniz formula: every derivative of $ab$ is a finite sum of products of derivatives of $a$ and $b$, and the symbol bounds for those factors multiply to give a bound by $m_1m_2$. The classical statement for $S^r$ follows after first checking that each weight $(x,\xi)\mapsto \langle \xi\rangle^q$ is an order function, then substituting $m_1(x,\xi)=\langle \xi\rangle^r$ and $m_2(x,\xi)=\langle \xi\rangle^s$ and using $\langle \xi\rangle^r\langle \xi\rangle^s=\langle \xi\rangle^{r+s}$. [/proofplan]

[step:Verify that the product of the two order functions is again an order function] Define \begin{align*} m_1m_2: T^*\mathbb{R}^n &\to (0,\infty) \end{align*} \begin{align*} \rho &\mapsto m_1(\rho)m_2(\rho). \end{align*} Let $\rho,\rho' \in T^*\mathbb{R}^n$. Since $m_1$ and $m_2$ are order functions, there exist constants $C_1,C_2>0$ and $N_1,N_2 \in \mathbb{N}$ such that \begin{align*} m_1(\rho) \leq C_1\langle \rho-\rho'\rangle^{N_1}m_1(\rho') \end{align*} and \begin{align*} m_2(\rho) \leq C_2\langle \rho-\rho'\rangle^{N_2}m_2(\rho'). \end{align*} Multiplying these two inequalities gives \begin{align*} m_1(\rho)m_2(\rho) \leq C_1C_2\langle \rho-\rho'\rangle^{N_1+N_2}m_1(\rho')m_2(\rho'). \end{align*} Thus $m_1m_2$ is an order function, with admissible constants $C_1C_2$ and $N_1+N_2$. [/step]

[step:Differentiate a symbol by shifting the multi-index in the defining estimate]Let $a \in S(m_1)$, and fix multi-indices $\alpha,\beta \in \mathbb{N}_0^n$. Define \begin{align*} c: T^*\mathbb{R}^n &\to \mathbb{C} \end{align*} \begin{align*} (x,\xi) &\mapsto \partial_x^\alpha\partial_\xi^\beta a(x,\xi). \end{align*} Since $a \in C^\infty(T^*\mathbb{R}^n;\mathbb{C})$, the function $c$ is smooth. To prove $c \in S(m_1)$, let $\gamma,\delta \in \mathbb{N}_0^n$ be arbitrary. By commutativity of partial derivatives for smooth functions, \begin{align*} \partial_x^\gamma\partial_\xi^\delta c = \partial_x^{\alpha+\gamma}\partial_\xi^{\beta+\delta}a. \end{align*} Because $a \in S(m_1)$, there exists a constant $C_{\alpha+\gamma,\beta+\delta}>0$ such that, for all $(x,\xi)\in T^*\mathbb{R}^n$, \begin{align*} |\partial_x^{\alpha+\gamma}\partial_\xi^{\beta+\delta}a(x,\xi)| \leq C_{\alpha+\gamma,\beta+\delta}m_1(x,\xi). \end{align*} Therefore \begin{align*} |\partial_x^\gamma\partial_\xi^\delta c(x,\xi)| \leq C_{\alpha+\gamma,\beta+\delta}m_1(x,\xi) \end{align*} for all $(x,\xi)\in T^*\mathbb{R}^n$. Since $\gamma,\delta$ were arbitrary, $c \in S(m_1)$.[/step]

[guided]We want to prove that taking derivatives does not move a symbol out of its symbol class. Fix the derivatives that are already being taken, namely $\partial_x^\alpha\partial_\xi^\beta$, and define the resulting function \begin{align*} c: T^*\mathbb{R}^n &\to \mathbb{C} \end{align*} \begin{align*} (x,\xi) &\mapsto \partial_x^\alpha\partial_\xi^\beta a(x,\xi). \end{align*} The definition of $S(m_1)$ requires two things: smoothness and a bound for every further derivative of $c$. Smoothness follows from $a \in C^\infty(T^*\mathbb{R}^n;\mathbb{C})$. Now let $\gamma,\delta \in \mathbb{N}_0^n$ be arbitrary. These are the extra derivatives required by the symbol-class test for $c$. Since $a$ is smooth, mixed partial derivatives commute, so \begin{align*} \partial_x^\gamma\partial_\xi^\delta c = \partial_x^{\alpha+\gamma}\partial_\xi^{\beta+\delta}a. \end{align*} The right-hand side is not a new kind of expression; it is simply a higher-order derivative of $a$. Because $a \in S(m_1)$, the defining estimate for $a$ applied to the multi-indices $\alpha+\gamma$ and $\beta+\delta$ gives a constant $C_{\alpha+\gamma,\beta+\delta}>0$ such that \begin{align*} |\partial_x^{\alpha+\gamma}\partial_\xi^{\beta+\delta}a(x,\xi)| \leq C_{\alpha+\gamma,\beta+\delta}m_1(x,\xi) \end{align*} for every $(x,\xi)\in T^*\mathbb{R}^n$. Substituting the identity for $\partial_x^\gamma\partial_\xi^\delta c$ yields \begin{align*} |\partial_x^\gamma\partial_\xi^\delta c(x,\xi)| \leq C_{\alpha+\gamma,\beta+\delta}m_1(x,\xi) \end{align*} for every $(x,\xi)\in T^*\mathbb{R}^n$. Since this estimate holds for every pair $\gamma,\delta$, the definition of $S(m_1)$ gives $c \in S(m_1)$.[/guided]

[step:Expand every derivative of the product by the multi-index Leibniz formula] Let $a \in S(m_1)$ and $b \in S(m_2)$. Define \begin{align*} p: T^*\mathbb{R}^n &\to \mathbb{C} \end{align*} \begin{align*} (x,\xi) &\mapsto a(x,\xi)b(x,\xi). \end{align*} Since $a$ and $b$ are smooth, $p$ is smooth. Let $\alpha,\beta \in \mathbb{N}_0^n$ be arbitrary. Applying the ordinary product rule successively to the $x$ variables and then to the $\xi$ variables gives the finite expansion \begin{align*} \partial_x^\alpha\partial_\xi^\beta p = \sum_{\gamma\leq \alpha}\sum_{\delta\leq \beta} \binom{\alpha}{\gamma}\binom{\beta}{\delta} (\partial_x^\gamma\partial_\xi^\delta a) (\partial_x^{\alpha-\gamma}\partial_\xi^{\beta-\delta} b), \end{align*} where $\gamma\leq \alpha$ and $\delta\leq \beta$ mean componentwise inequalities, and \begin{align*} \binom{\alpha}{\gamma}:=\prod_{i=1}^n \binom{\alpha_i}{\gamma_i}, \qquad \binom{\beta}{\delta}:=\prod_{i=1}^n \binom{\beta_i}{\delta_i}. \end{align*} [/step]

[step:Bound the finite Leibniz sum by the product order function]For each pair $\gamma\leq\alpha$ and $\delta\leq\beta$, the symbol estimates for $a$ and $b$ give constants $A_{\gamma,\delta}>0$ and $B_{\alpha-\gamma,\beta-\delta}>0$ such that \begin{align*} |\partial_x^\gamma\partial_\xi^\delta a(x,\xi)| \leq A_{\gamma,\delta}m_1(x,\xi) \end{align*} and \begin{align*} |\partial_x^{\alpha-\gamma}\partial_\xi^{\beta-\delta} b(x,\xi)| \leq B_{\alpha-\gamma,\beta-\delta}m_2(x,\xi) \end{align*} for all $(x,\xi)\in T^*\mathbb{R}^n$. Taking absolute values in the Leibniz formula and applying these two estimates term by term yields \begin{align*} |\partial_x^\alpha\partial_\xi^\beta p(x,\xi)| \leq C_{\alpha,\beta}m_1(x,\xi)m_2(x,\xi), \end{align*} where the finite constant $C_{\alpha,\beta}>0$ is defined by \begin{align*} C_{\alpha,\beta} := \sum_{\gamma\leq \alpha}\sum_{\delta\leq \beta} \binom{\alpha}{\gamma}\binom{\beta}{\delta} A_{\gamma,\delta}B_{\alpha-\gamma,\beta-\delta}. \end{align*} Since $\alpha,\beta$ were arbitrary, $p=ab \in S(m_1m_2)$.[/step]

[guided]The goal is to show that every derivative of the product $ab$ is bounded by a constant times $m_1m_2$. Fix arbitrary multi-indices $\alpha,\beta \in \mathbb{N}_0^n$. Applying the ordinary product rule successively to the $x$ variables and then to the $\xi$ variables gives \begin{align*} \partial_x^\alpha\partial_\xi^\beta(ab) = \sum_{\gamma\leq \alpha}\sum_{\delta\leq \beta} \binom{\alpha}{\gamma}\binom{\beta}{\delta} (\partial_x^\gamma\partial_\xi^\delta a) (\partial_x^{\alpha-\gamma}\partial_\xi^{\beta-\delta} b). \end{align*} This formula says that each derivative is distributed between the two factors: $\gamma,\delta$ derivatives land on $a$, and the remaining $\alpha-\gamma,\beta-\delta$ derivatives land on $b$. For each fixed pair $\gamma\leq\alpha$ and $\delta\leq\beta$, the hypothesis $a\in S(m_1)$ gives a constant $A_{\gamma,\delta}>0$ satisfying \begin{align*} |\partial_x^\gamma\partial_\xi^\delta a(x,\xi)| \leq A_{\gamma,\delta}m_1(x,\xi) \end{align*} for every $(x,\xi)\in T^*\mathbb{R}^n$. Likewise, the hypothesis $b\in S(m_2)$ gives a constant $B_{\alpha-\gamma,\beta-\delta}>0$ satisfying \begin{align*} |\partial_x^{\alpha-\gamma}\partial_\xi^{\beta-\delta} b(x,\xi)| \leq B_{\alpha-\gamma,\beta-\delta}m_2(x,\xi) \end{align*} for every $(x,\xi)\in T^*\mathbb{R}^n$. Multiplying these two inequalities gives, for every $(x,\xi)\in T^*\mathbb{R}^n$, \begin{align*} |(\partial_x^\gamma\partial_\xi^\delta a)(x,\xi) (\partial_x^{\alpha-\gamma}\partial_\xi^{\beta-\delta} b)(x,\xi)| \leq A_{\gamma,\delta}B_{\alpha-\gamma,\beta-\delta}m_1(x,\xi)m_2(x,\xi). \end{align*} There are only finitely many pairs $\gamma,\delta$ with $\gamma\leq\alpha$ and $\delta\leq\beta$, so all constants can be summed into one constant. Define \begin{align*} C_{\alpha,\beta} := \sum_{\gamma\leq \alpha}\sum_{\delta\leq \beta} \binom{\alpha}{\gamma}\binom{\beta}{\delta} A_{\gamma,\delta}B_{\alpha-\gamma,\beta-\delta}. \end{align*} Then $C_{\alpha,\beta}$ is finite and positive, and taking absolute values in the Leibniz formula gives \begin{align*} |\partial_x^\alpha\partial_\xi^\beta(ab)(x,\xi)| \leq C_{\alpha,\beta}m_1(x,\xi)m_2(x,\xi) \end{align*} for every $(x,\xi)\in T^*\mathbb{R}^n$. Since this is exactly the defining estimate for $ab\in S(m_1m_2)$, the product belongs to the product symbol class.[/guided]

[step:Specialize the product estimate to the classical symbol classes]Let $r,s\in\mathbb{R}$, and suppose $a\in S^r(T^*\mathbb{R}^n)$ and $b\in S^s(T^*\mathbb{R}^n)$. By the convention $S^q(T^*\mathbb{R}^n)=S(\langle \xi\rangle^q)$ for $q\in\mathbb{R}$, this means \begin{align*} a\in S(\langle \xi\rangle^r) \end{align*} and \begin{align*} b\in S(\langle \xi\rangle^s). \end{align*} We first verify that the weights used here are order functions. Fix $q\in\mathbb{R}$, and define $m_q:T^*\mathbb{R}^n\to (0,\infty)$ by $m_q(x,\xi):=\langle \xi\rangle^q$. For $u,v\in\mathbb{R}^n$, the triangle inequality and the estimate $(A+B)^2\leq 2A^2+2B^2$ give \begin{align*} 1+|u+v|^2\leq 1+2|u|^2+2|v|^2. \end{align*} Since \begin{align*} 1+2|u|^2+2|v|^2\leq 2(1+|u|^2)(1+|v|^2), \end{align*} taking square roots gives the Peetre-type estimate \begin{align*} \langle u+v\rangle\leq \sqrt{2}\langle u\rangle\langle v\rangle. \end{align*} Let $\rho=(x,\xi)$ and $\rho'=(x',\xi')$ in $T^*\mathbb{R}^n$. Applying this estimate with $u=\xi-\xi'$ and $v=\xi'$ gives \begin{align*} \langle \xi\rangle\leq \sqrt{2}\langle \xi-\xi'\rangle\langle \xi'\rangle. \end{align*} Because $|\xi-\xi'|\leq |\rho-\rho'|$, we have $\langle \xi-\xi'\rangle\leq \langle \rho-\rho'\rangle$. If $q\geq 0$, then \begin{align*} \langle \xi\rangle^q\leq 2^{q/2}\langle \rho-\rho'\rangle^q\langle \xi'\rangle^q. \end{align*} Choose an integer $N_q\in\mathbb{N}$ with $N_q\geq q$. Since $\langle \rho-\rho'\rangle\geq 1$, this implies \begin{align*} \langle \xi\rangle^q\leq 2^{q/2}\langle \rho-\rho'\rangle^{N_q}\langle \xi'\rangle^q. \end{align*} If $q<0$, applying the same estimate with $\xi$ and $\xi'$ interchanged gives \begin{align*} \langle \xi'\rangle^{-q}\leq 2^{-q/2}\langle \rho-\rho'\rangle^{-q}\langle \xi\rangle^{-q}. \end{align*} Rearranging this positive inequality yields \begin{align*} \langle \xi\rangle^q\leq 2^{-q/2}\langle \rho-\rho'\rangle^{-q}\langle \xi'\rangle^q. \end{align*} Choose an integer $N_q\in\mathbb{N}$ with $N_q\geq -q$. Since $\langle \rho-\rho'\rangle\geq 1$, this gives \begin{align*} \langle \xi\rangle^q\leq 2^{-q/2}\langle \rho-\rho'\rangle^{N_q}\langle \xi'\rangle^q. \end{align*} Thus $m_q$ is an order function. More explicitly, admissible constants are $C_q=2^{q/2}$ and any integer $N_q\geq q$ when $q\geq 0$, and $C_q=2^{-q/2}$ and any integer $N_q\geq -q$ when $q<0$. Applying the multiplication result with \begin{align*} m_1(x,\xi):=\langle \xi\rangle^r, \qquad m_2(x,\xi):=\langle \xi\rangle^s \end{align*} gives \begin{align*} ab\in S(\langle \xi\rangle^r\langle \xi\rangle^s). \end{align*} Since \begin{align*} \langle \xi\rangle^r\langle \xi\rangle^s = \langle \xi\rangle^{r+s}, \end{align*} we obtain \begin{align*} ab\in S(\langle \xi\rangle^{r+s}) = S^{r+s}(T^*\mathbb{R}^n). \end{align*} This proves the final assertion and completes the proof.[/step]

[guided]The product result can be applied to classical symbol classes only after checking that the classical weights are order functions. Fix $q\in\mathbb{R}$, and define $m_q:T^*\mathbb{R}^n\to (0,\infty)$ by $m_q(x,\xi):=\langle \xi\rangle^q$. We must prove that there are constants $C_q>0$ and $N_q\in\mathbb{N}$ such that \begin{align*} m_q(\rho)\leq C_q\langle \rho-\rho'\rangle^{N_q}m_q(\rho') \end{align*} for all $\rho,\rho'\in T^*\mathbb{R}^n$. The needed estimate is a Peetre-type inequality with a constant. For $u,v\in\mathbb{R}^n$, the triangle inequality gives $|u+v|\leq |u|+|v|$, and hence $(|u|+|v|)^2\leq 2|u|^2+2|v|^2$. Therefore \begin{align*} 1+|u+v|^2\leq 1+2|u|^2+2|v|^2. \end{align*} Also, \begin{align*} 1+2|u|^2+2|v|^2\leq 2(1+|u|^2)(1+|v|^2). \end{align*} Taking square roots of both sides gives \begin{align*} \langle u+v\rangle\leq \sqrt{2}\langle u\rangle\langle v\rangle. \end{align*} This constant cannot simply be dropped; it is exactly what makes the order-function verification correct. Now take $\rho=(x,\xi)$ and $\rho'=(x',\xi')$ in $T^*\mathbb{R}^n$. Applying the Peetre estimate with $u=\xi-\xi'$ and $v=\xi'$ gives \begin{align*} \langle \xi\rangle\leq \sqrt{2}\langle \xi-\xi'\rangle\langle \xi'\rangle. \end{align*} Since $|\xi-\xi'|\leq |\rho-\rho'|$, we also have \begin{align*} \langle \xi-\xi'\rangle\leq \langle \rho-\rho'\rangle. \end{align*} If $q\geq 0$, raising the inequality to the power $q$ preserves the inequality and gives \begin{align*} \langle \xi\rangle^q\leq 2^{q/2}\langle \rho-\rho'\rangle^q\langle \xi'\rangle^q. \end{align*} Choose an integer $N_q\in\mathbb{N}$ with $N_q\geq q$. Because $\langle \rho-\rho'\rangle\geq 1$, the bound becomes \begin{align*} \langle \xi\rangle^q\leq 2^{q/2}\langle \rho-\rho'\rangle^{N_q}\langle \xi'\rangle^q. \end{align*} Thus the order-function inequality holds for $q\geq 0$ with $C_q=2^{q/2}$. If $q<0$, raising the previous estimate directly would reverse the desired comparison, so we first interchange $\xi$ and $\xi'$. The same argument gives \begin{align*} \langle \xi'\rangle\leq \sqrt{2}\langle \rho-\rho'\rangle\langle \xi\rangle. \end{align*} Since $-q>0$, raising this inequality to the power $-q$ gives \begin{align*} \langle \xi'\rangle^{-q}\leq 2^{-q/2}\langle \rho-\rho'\rangle^{-q}\langle \xi\rangle^{-q}. \end{align*} Dividing by the positive factor $\langle \xi'\rangle^{-q}\langle \xi\rangle^{-q}$ yields \begin{align*} \langle \xi\rangle^q\leq 2^{-q/2}\langle \rho-\rho'\rangle^{-q}\langle \xi'\rangle^q. \end{align*} Choose an integer $N_q\in\mathbb{N}$ with $N_q\geq -q$. Since $\langle \rho-\rho'\rangle\geq 1$, this implies \begin{align*} \langle \xi\rangle^q\leq 2^{-q/2}\langle \rho-\rho'\rangle^{N_q}\langle \xi'\rangle^q. \end{align*} So $m_q$ is an order function for every real $q$. Now return to $r$ and $s$. Since $a\in S^r(T^*\mathbb{R}^n)$ and $b\in S^s(T^*\mathbb{R}^n)$, we have \begin{align*} a\in S(\langle \xi\rangle^r) \end{align*} and \begin{align*} b\in S(\langle \xi\rangle^s). \end{align*} The weights $\langle \xi\rangle^r$ and $\langle \xi\rangle^s$ have just been verified to be order functions, so the product result applies and gives \begin{align*} ab\in S(\langle \xi\rangle^r\langle \xi\rangle^s). \end{align*} Finally, \begin{align*} \langle \xi\rangle^r\langle \xi\rangle^s=\langle \xi\rangle^{r+s}, \end{align*} so \begin{align*} ab\in S(\langle \xi\rangle^{r+s})=S^{r+s}(T^*\mathbb{R}^n). \end{align*} This is exactly the classical-symbol multiplication statement.[/guided]