[proofplan]
We first replace the Kohn-Nirenberg quantisation by Weyl quantisation; the difference is a pseudodifferential operator of order $-1$, hence is bounded on $L^2(\mathbb{R}^n)$ by the Calderon-Vaillancourt theorem. For the Weyl operator, we invoke Friedrichs positive quantisation: a nonnegative order-zero symbol has a positive Friedrichs operator whose Weyl-symbol discrepancy has order $-1$. The positive part gives a nonnegative quadratic form, while the two order $-1$ remainders are controlled by $L^2$ boundedness. Combining these bounds gives the asserted lower estimate.
[/proofplan]
[step:Replace Kohn-Nirenberg quantisation by Weyl quantisation up to an order $-1$ operator]
The Weyl quantisation $\operatorname{Op}^w(a): \mathcal{S}(\mathbb{R}^n) \to \mathcal{S}'(\mathbb{R}^n)$ is declared in the theorem statement. The symbol class $S^{-1}_{1,0}(\mathbb{R}^n \times \mathbb{R}^n)$ is also defined there. We use the Kohn-Nirenberg-to-Weyl conversion formula for symbols in $S^0_{1,0}$: there exists a symbol $r_0 \in S^{-1}_{1,0}(\mathbb{R}^n \times \mathbb{R}^n)$ such that
\begin{align*}
\operatorname{Op}(a) = \operatorname{Op}^w(a) + \operatorname{Op}^w(r_0)
\end{align*}
on $\mathcal{S}(\mathbb{R}^n)$. Moreover, for every finite family of seminorms $q_{-1,\alpha,\beta}(r_0)$, the symbolic conversion estimates bound that family by a constant depending only on $n$ and finitely many seminorms $q_{0,\gamma,\delta}(a)$.
Since $S^{-1}_{1,0} \subset S^0_{1,0}$, the Calderon-Vaillancourt theorem applies to $r_0$; we use it here as an external analytic prerequisite. Thus there exists a constant $C_0 \geq 0$, depending only on $n$ and finitely many seminorms $q_{-1,\alpha,\beta}(r_0)$, such that
\begin{align*}
\|\operatorname{Op}^w(r_0)u\|_{L^2(\mathbb{R}^n)} \leq C_0\|u\|_{L^2(\mathbb{R}^n)}
\end{align*}
for every $u \in \mathcal{S}(\mathbb{R}^n)$. Therefore, by the [Cauchy-Schwarz inequality](/theorems/432) in the [Hilbert space](/page/Hilbert%20Space) $L^2(\mathbb{R}^n)$,
\begin{align*}
\left|\operatorname{Re}(\operatorname{Op}^w(r_0)u,u)_{L^2(\mathbb{R}^n)}\right| \leq C_0\|u\|_{L^2(\mathbb{R}^n)}^2.
\end{align*}
[/step]
[step:Decompose the Weyl operator into a positive Friedrichs part and a bounded remainder]
We invoke the Friedrichs positive quantisation theorem for order-zero symbols: for every real-valued nonnegative $a \in S^0_{1,0}(\mathbb{R}^n \times \mathbb{R}^n)$, there exists a positive operator
\begin{align*}
\operatorname{Op}^F(a): \mathcal{S}(\mathbb{R}^n) \to \mathcal{S}'(\mathbb{R}^n)
\end{align*}
and a symbol $r_1 \in S^{-1}_{1,0}(\mathbb{R}^n \times \mathbb{R}^n)$ such that
\begin{align*}
\operatorname{Op}^w(a) = \operatorname{Op}^F(a) + \operatorname{Op}^w(r_1)
\end{align*}
on $\mathcal{S}(\mathbb{R}^n)$. The positivity means
\begin{align*}
\operatorname{Re}(\operatorname{Op}^F(a)u,u)_{L^2(\mathbb{R}^n)} \geq 0
\end{align*}
for every $u \in \mathcal{S}(\mathbb{R}^n)$. For every finite family of seminorms $q_{-1,\alpha,\beta}(r_1)$, the Friedrichs comparison estimates bound that family by a constant depending only on $n$ and finitely many seminorms $q_{0,\gamma,\delta}(a)$.
This is an external analytic input: Friedrichs positive quantisation and its order $-1$ comparison with Weyl quantisation. More precisely, the construction gives a finite set $A_1 \subset \mathbb{N}_0^n \times \mathbb{N}_0^n$, determined only by $n$, such that the required finitely many seminorms $q_{-1,\alpha,\beta}(r_1)$ are bounded by a constant depending only on $n$ and the finitely many seminorms $q_{0,\gamma,\delta}(a)$ with $(\gamma,\delta) \in A_1$. Its proof uses coherent phase-space packets and almost-orthogonality to build $\operatorname{Op}^F(a)$ from positive local averages of $a$; the nonnegativity of $a$ is used in the local averages, while the comparison remainder is controlled by the symbol estimates.
[guided]
The goal of this step is not to factor $a$ pointwise as a square. Such a factorisation would be unstable at the zero set of $a$ and would not give the required symbolic estimates. Instead we use Friedrichs positive quantisation, which is designed to preserve positivity at the operator level.
The precise input is the following standard theorem. If $a \in S^0_{1,0}(\mathbb{R}^n \times \mathbb{R}^n)$ is real-valued and satisfies $a(x,\xi) \geq 0$ for all $(x,\xi)$, then Friedrichs quantisation assigns to $a$ an operator
\begin{align*}
\operatorname{Op}^F(a): \mathcal{S}(\mathbb{R}^n) \to \mathcal{S}'(\mathbb{R}^n)
\end{align*}
such that
\begin{align*}
\operatorname{Re}(\operatorname{Op}^F(a)u,u)_{L^2(\mathbb{R}^n)} \geq 0
\end{align*}
for every $u \in \mathcal{S}(\mathbb{R}^n)$. The theorem also gives a symbol $r_1 \in S^{-1}_{1,0}(\mathbb{R}^n \times \mathbb{R}^n)$ satisfying
\begin{align*}
\operatorname{Op}^w(a) = \operatorname{Op}^F(a) + \operatorname{Op}^w(r_1)
\end{align*}
on $\mathcal{S}(\mathbb{R}^n)$.
We verify the hypotheses of this input. The theorem requires an order-zero symbol in the class $S^0_{1,0}$, which is exactly the assumed symbol class of $a$. It requires real-valuedness, which is also assumed. It requires pointwise nonnegativity on phase space, and the hypothesis gives $a(x,\xi) \geq 0$ for every $(x,\xi) \in \mathbb{R}^n \times \mathbb{R}^n$. Therefore the Friedrichs theorem applies.
The role of almost-orthogonality is to keep the coherent-state localisation uniformly bounded on $L^2(\mathbb{R}^n)$ when the local positive pieces are summed. The discrepancy between the Weyl quantisation and the Friedrichs quantisation is not zero, but the symbolic calculus places it in the lower class $S^{-1}_{1,0}$. This loss of one order is the decisive point: order $-1$ symbols are $L^2$ bounded by Calderon-Vaillancourt, so the discrepancy can contribute only a bounded multiple of $\|u\|_{L^2(\mathbb{R}^n)}^2$ to the quadratic form.
[/guided]
[/step]
[step:Bound the Friedrichs comparison remainder on $L^2(\mathbb{R}^n)$]
Since $r_1 \in S^{-1}_{1,0}(\mathbb{R}^n \times \mathbb{R}^n)$ and $S^{-1}_{1,0} \subset S^0_{1,0}$, Calderon-Vaillancourt applies again. Hence there exists a constant $C_1 \geq 0$, depending only on $n$ and finitely many seminorms $q_{-1,\alpha,\beta}(r_1)$, such that
\begin{align*}
\|\operatorname{Op}^w(r_1)u\|_{L^2(\mathbb{R}^n)} \leq C_1\|u\|_{L^2(\mathbb{R}^n)}
\end{align*}
for every $u \in \mathcal{S}(\mathbb{R}^n)$. Applying the Cauchy-Schwarz inequality in $L^2(\mathbb{R}^n)$ gives
\begin{align*}
\left|\operatorname{Re}(\operatorname{Op}^w(r_1)u,u)_{L^2(\mathbb{R}^n)}\right| \leq C_1\|u\|_{L^2(\mathbb{R}^n)}^2.
\end{align*}
[/step]
[step:Combine positivity with the two bounded remainders]
Let $u \in \mathcal{S}(\mathbb{R}^n)$. Combining the two decompositions gives
\begin{align*}
\operatorname{Op}(a)u = \operatorname{Op}^F(a)u + \operatorname{Op}^w(r_1)u + \operatorname{Op}^w(r_0)u.
\end{align*}
Taking the real part of the $L^2(\mathbb{R}^n)$ [inner product](/page/Inner%20Product) with $u$ and using linearity in the first argument yields
\begin{align*}
\operatorname{Re}(\operatorname{Op}(a)u,u)_{L^2(\mathbb{R}^n)} = \operatorname{Re}(\operatorname{Op}^F(a)u,u)_{L^2(\mathbb{R}^n)} + \operatorname{Re}(\operatorname{Op}^w(r_1)u,u)_{L^2(\mathbb{R}^n)} + \operatorname{Re}(\operatorname{Op}^w(r_0)u,u)_{L^2(\mathbb{R}^n)}.
\end{align*}
The Friedrichs term is nonnegative, while the two remainder terms are bounded below by the negative of their absolute values. Therefore
\begin{align*}
\operatorname{Re}(\operatorname{Op}(a)u,u)_{L^2(\mathbb{R}^n)} \geq -C_1\|u\|_{L^2(\mathbb{R}^n)}^2 - C_0\|u\|_{L^2(\mathbb{R}^n)}^2.
\end{align*}
Define
\begin{align*}
C := C_0 + C_1.
\end{align*}
Then $C \geq 0$. The Kohn-Nirenberg-to-Weyl conversion gives a finite set $A_0 \subset \mathbb{N}_0^n \times \mathbb{N}_0^n$, determined only by $n$, such that the finitely many seminorms $q_{-1,\alpha,\beta}(r_0)$ used in $C_0$ are bounded in terms of the finitely many seminorms $q_{0,\gamma,\delta}(a)$ with $(\gamma,\delta) \in A_0$. The Friedrichs comparison gives the corresponding finite set $A_1$ for $r_1$, as stated above. Therefore $C$ depends only on $n$ and finitely many seminorms $q_{0,\alpha,\beta}(a)$. Hence
\begin{align*}
\operatorname{Re}(\operatorname{Op}(a)u,u)_{L^2(\mathbb{R}^n)} \geq -C\|u\|_{L^2(\mathbb{R}^n)}^2.
\end{align*}
Since $u \in \mathcal{S}(\mathbb{R}^n)$ was arbitrary, the theorem follows.
[/step]
