[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)$.
[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]
[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)$.
[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]
[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.
[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]
[/step]
