[proofplan]
We use the standard properly supported pseudodifferential calculus on $\mathbb{R}^n$. Proper support ensures that $B$ and its formal adjoint act on test functions with the support control needed for the $L^2$ pairing. The adjoint theorem gives $B^* \in \Psi^r_{1,0}$ and identifies its principal symbol as the complex conjugate of the principal symbol of $B$. The composition theorem then places $B^*B$ in $\Psi^{2r}_{1,0}$, and the formal-adjoint identity gives the nonnegative quadratic form. Finally, the principal-symbol product rule gives $\sigma_{2r}(B^*B)=\overline{\sigma_r(B)}\sigma_r(B)$.
[/proofplan]
[step:Use proper support to put the formal adjoint and pairings on test functions]
Let
\begin{align*}
(\cdot,\cdot)_{L^2(\mathbb{R}^n)}: C_c^\infty(\mathbb{R}^n) \times C_c^\infty(\mathbb{R}^n) \to \mathbb{C}
\end{align*}
denote the Lebesgue $L^2$ [inner product](/page/Inner%20Product), defined by
\begin{align*}
(f,g)_{L^2(\mathbb{R}^n)} = \int_{\mathbb{R}^n} f(x)\,\overline{g(x)}\,d\mathcal{L}^n(x).
\end{align*}
The formal adjoint of $B$ is the properly supported operator
\begin{align*}
B^*: C_c^\infty(\mathbb{R}^n) \to C_c^\infty(\mathbb{R}^n)
\end{align*}
characterized by
\begin{align*}
(B^*v,w)_{L^2(\mathbb{R}^n)} = (v,Bw)_{L^2(\mathbb{R}^n)}
\end{align*}
whenever $v,w \in C_c^\infty(\mathbb{R}^n)$.
Because $B$ is properly supported, the standard mapping property for properly supported pseudodifferential operators gives
\begin{align*}
B(C_c^\infty(\mathbb{R}^n)) \subset C_c^\infty(\mathbb{R}^n).
\end{align*}
Thus, for every $u \in C_c^\infty(\mathbb{R}^n)$, the expression $Bu$ is an $L^2$ function with compact support, and the norm $\|Bu\|_{L^2(\mathbb{R}^n)}$ is defined.
[guided]
We first fix the pairing because the positivity statement is a statement about a quadratic form, not just about symbols. The Lebesgue $L^2$ inner product on test functions is the map
\begin{align*}
(\cdot,\cdot)_{L^2(\mathbb{R}^n)}: C_c^\infty(\mathbb{R}^n) \times C_c^\infty(\mathbb{R}^n) \to \mathbb{C}
\end{align*}
given by
\begin{align*}
(f,g)_{L^2(\mathbb{R}^n)} = \int_{\mathbb{R}^n} f(x)\,\overline{g(x)}\,d\mathcal{L}^n(x).
\end{align*}
The measure is explicitly $\mathcal{L}^n$, the $n$-dimensional [Lebesgue measure](/page/Lebesgue%20Measure).
The formal adjoint is the operator
\begin{align*}
B^*: C_c^\infty(\mathbb{R}^n) \to C_c^\infty(\mathbb{R}^n)
\end{align*}
defined by the identity
\begin{align*}
(B^*v,w)_{L^2(\mathbb{R}^n)} = (v,Bw)_{L^2(\mathbb{R}^n)}
\end{align*}
for test functions $v,w \in C_c^\infty(\mathbb{R}^n)$. This is the convention compatible with the displayed identity in the theorem.
Why is proper support present? It guarantees the support control needed for the pseudodifferential operator to preserve compact support on test functions. In the standard properly supported calculus, if $B \in \Psi^r_{1,0}(\mathbb{R}^n)$ is properly supported, then
\begin{align*}
B(C_c^\infty(\mathbb{R}^n)) \subset C_c^\infty(\mathbb{R}^n).
\end{align*}
Consequently, when $u \in C_c^\infty(\mathbb{R}^n)$, $Bu$ is a compactly supported smooth function and hence belongs to $L^2(\mathbb{R}^n)$. Therefore the norm
\begin{align*}
\|Bu\|_{L^2(\mathbb{R}^n)}^2 = \int_{\mathbb{R}^n} |Bu(x)|^2\,d\mathcal{L}^n(x)
\end{align*}
is well-defined.
[/guided]
[/step]
[step:Apply the adjoint theorem to identify the order and principal symbol of $B^*$]
By the adjoint theorem for properly supported $\Psi^r_{1,0}$ operators, included in the standard properly supported calculus assumed in the theorem statement, the formal adjoint is properly supported and satisfies
\begin{align*}
B^* \in \Psi^r_{1,0}(\mathbb{R}^n).
\end{align*}
If $b_r:\mathbb{R}^n \times \mathbb{R}^n_0 \to \mathbb{C}$ is any representative of the principal symbol class $\sigma_r(B)$, then the principal symbol class $\sigma_r(B^*)$ is represented by the map $\overline{b_r}:\mathbb{R}^n \times \mathbb{R}^n_0 \to \mathbb{C}$ given by $(x,\xi) \mapsto \overline{b_r(x,\xi)}$.
[guided]
The adjoint theorem is the calculus result that transfers both order and proper support from $B$ to its formal adjoint. Its hypotheses are met because $B$ is assumed to be a properly supported element of $\Psi^r_{1,0}(\mathbb{R}^n)$. Therefore the theorem gives a properly supported operator $B^* \in \Psi^r_{1,0}(\mathbb{R}^n)$.
The same adjoint theorem also identifies the leading symbol class. If $b_r:\mathbb{R}^n \times \mathbb{R}^n_0 \to \mathbb{C}$ represents the principal symbol class $\sigma_r(B)$, then the principal symbol class $\sigma_r(B^*)$ is represented by the pointwise complex conjugate map $\overline{b_r}:\mathbb{R}^n \times \mathbb{R}^n_0 \to \mathbb{C}$ given by $(x,\xi) \mapsto \overline{b_r(x,\xi)}$. This is the input needed later: the normal square has leading symbol class represented by the product of a representative with its complex conjugate.
[/guided]
[/step]
[step:Compose $B^*$ with $B$ in the properly supported calculus]
Since $B^* \in \Psi^r_{1,0}(\mathbb{R}^n)$ and $B \in \Psi^r_{1,0}(\mathbb{R}^n)$, and since both $B^*$ and $B$ are properly supported, the support compatibility required for composition holds. Thus the composition theorem for properly supported $\Psi_{1,0}$ operators, included in the standard properly supported calculus assumed in the theorem statement, applies. Therefore
\begin{align*}
B^*B \in \Psi^{r+r}_{1,0}(\mathbb{R}^n).
\end{align*}
Since $r+r=2r$, this gives
\begin{align*}
B^*B \in \Psi^{2r}_{1,0}(\mathbb{R}^n).
\end{align*}
[guided]
We now apply the composition theorem in the properly supported pseudodifferential calculus. The theorem requires two inputs: the two factors must have specified orders in the $\Psi_{1,0}$ calculus, and the relevant support condition must hold. The order inputs are $B^* \in \Psi^r_{1,0}(\mathbb{R}^n)$ from the adjoint step and $B \in \Psi^r_{1,0}(\mathbb{R}^n)$ from the theorem hypothesis. The support input holds because $B$ is properly supported by hypothesis and $B^*$ is properly supported by the adjoint theorem.
The composition theorem therefore gives
\begin{align*}
B^*B \in \Psi^{r+r}_{1,0}(\mathbb{R}^n).
\end{align*}
Since addition in the order parameter gives $r+r=2r$, this is exactly
\begin{align*}
B^*B \in \Psi^{2r}_{1,0}(\mathbb{R}^n).
\end{align*}
[/guided]
[/step]
[step:Use the formal adjoint identity to prove nonnegativity of the quadratic form]
Let $u \in C_c^\infty(\mathbb{R}^n)$. Apply the defining identity of the formal adjoint with
\begin{align*}
v = Bu
\end{align*}
and
\begin{align*}
w = u.
\end{align*}
Then
\begin{align*}
(B^*Bu,u)_{L^2(\mathbb{R}^n)} = (Bu,Bu)_{L^2(\mathbb{R}^n)}.
\end{align*}
By the definition of the $L^2$ inner product,
\begin{align*}
(Bu,Bu)_{L^2(\mathbb{R}^n)} = \int_{\mathbb{R}^n} |Bu(x)|^2\,d\mathcal{L}^n(x).
\end{align*}
The integrand $|Bu(x)|^2$ is nonnegative for every $x \in \mathbb{R}^n$, so
\begin{align*}
\int_{\mathbb{R}^n} |Bu(x)|^2\,d\mathcal{L}^n(x) \geq 0.
\end{align*}
Hence
\begin{align*}
(B^*Bu,u)_{L^2(\mathbb{R}^n)} = \|Bu\|_{L^2(\mathbb{R}^n)}^2 \geq 0.
\end{align*}
[guided]
This is the step where the word “nonnegative” is justified. We are not proving an abstract spectral statement about a closed self-adjoint Hilbert-space operator; we are proving nonnegativity of the quadratic form on the stated test-function domain.
Let $u \in C_c^\infty(\mathbb{R}^n)$. Since $B$ is properly supported, the preceding support discussion gives that $Bu$ is an $L^2$ function in this setting. We now use the defining identity of the formal adjoint:
\begin{align*}
(B^*v,w)_{L^2(\mathbb{R}^n)} = (v,Bw)_{L^2(\mathbb{R}^n)}.
\end{align*}
Choose
\begin{align*}
v = Bu
\end{align*}
and
\begin{align*}
w = u.
\end{align*}
Substituting these choices into the formal-adjoint identity gives
\begin{align*}
(B^*Bu,u)_{L^2(\mathbb{R}^n)} = (Bu,Bu)_{L^2(\mathbb{R}^n)}.
\end{align*}
Now expand the right-hand side using the Lebesgue $L^2$ inner product:
\begin{align*}
(Bu,Bu)_{L^2(\mathbb{R}^n)} = \int_{\mathbb{R}^n} Bu(x)\,\overline{Bu(x)}\,d\mathcal{L}^n(x).
\end{align*}
For each $x \in \mathbb{R}^n$,
\begin{align*}
Bu(x)\,\overline{Bu(x)} = |Bu(x)|^2.
\end{align*}
Therefore
\begin{align*}
(Bu,Bu)_{L^2(\mathbb{R}^n)} = \int_{\mathbb{R}^n} |Bu(x)|^2\,d\mathcal{L}^n(x).
\end{align*}
Since $|Bu(x)|^2 \geq 0$ pointwise, monotonicity of the [Lebesgue integral](/page/Lebesgue%20Integral) gives
\begin{align*}
\int_{\mathbb{R}^n} |Bu(x)|^2\,d\mathcal{L}^n(x) \geq 0.
\end{align*}
Thus
\begin{align*}
(B^*Bu,u)_{L^2(\mathbb{R}^n)} = \|Bu\|_{L^2(\mathbb{R}^n)}^2 \geq 0.
\end{align*}
This proves precisely the quadratic-form nonnegativity asserted in the theorem.
[/guided]
[/step]
[step:Multiply the principal symbols to compute the principal symbol of $B^*B$]
Let $b_r:\mathbb{R}^n \times \mathbb{R}^n_0 \to \mathbb{C}$ be a representative of the principal symbol class $\sigma_r(B)$. By the principal-symbol product rule for pseudodifferential compositions, included in the standard properly supported calculus assumed in the theorem statement, the principal symbol class $\sigma_{2r}(B^*B)$ is represented by the pointwise product of the representative $\overline{b_r}$ for $\sigma_r(B^*)$ and the representative $b_r$ for $\sigma_r(B)$. For every phase-space point $(x,\xi) \in \mathbb{R}^n \times \mathbb{R}^n_0$, this representative is
\begin{align*}
\overline{b_r(x,\xi)}\,b_r(x,\xi) = |b_r(x,\xi)|^2.
\end{align*}
Hence $\sigma_{2r}(B^*B)$ is represented by the map $(x,\xi) \mapsto |b_r(x,\xi)|^2$.
This completes the proof.
[guided]
The composition theorem also supplies the leading-symbol multiplication rule. Its hypotheses have already been checked in the composition step: $B^*$ and $B$ are properly supported operators in $\Psi^r_{1,0}(\mathbb{R}^n)$. Let $b_r:\mathbb{R}^n \times \mathbb{R}^n_0 \to \mathbb{C}$ be a representative of the principal symbol class $\sigma_r(B)$. From the adjoint theorem, the principal symbol class $\sigma_r(B^*)$ is represented by $\overline{b_r}$. Therefore the principal symbol class of the composition $B^*B$ is represented by the pointwise product $\overline{b_r}\,b_r$.
At each phase-space point $(x,\xi) \in \mathbb{R}^n \times \mathbb{R}^n_0$, this representative satisfies
\begin{align*}
\overline{b_r(x,\xi)}\,b_r(x,\xi) = |b_r(x,\xi)|^2.
\end{align*}
Thus $\sigma_{2r}(B^*B)$ is represented by the map $(x,\xi) \mapsto |b_r(x,\xi)|^2$.
This completes the proof.
[/guided]
[/step]
