## Formalized Name
Calderón-Vaillancourt Theorem
## Formalized Statement
Let $n \in \mathbb{N}$, and let $a: \mathbb{R}^n_x \times \mathbb{R}^n_\theta \to \mathbb{C}$ be a $C^\infty$ symbol in $S^0_{1,0}(\mathbb{R}^n_x \times \mathbb{R}^n_\theta)$, meaning that for every pair of multi-indices $\alpha,\beta \in \mathbb{N}_0^n$ there is a constant $C_{\alpha,\beta}>0$ such that $|\partial_x^\alpha\partial_\theta^\beta a(x,\theta)| \leq C_{\alpha,\beta}\langle \theta\rangle^{-|\beta|}$ for all $x,\theta \in \mathbb{R}^n$, where $\langle \theta\rangle = (1+|\theta|^2)^{1/2}$. Define the Kohn-Nirenberg pseudodifferential operator $\operatorname{Op}(a): \mathcal{S}(\mathbb{R}^n) \to \mathcal{S}'(\mathbb{R}^n)$ by the oscillatory integral $(\operatorname{Op}(a)u)(x) = (2\pi)^{-n}\int_{\mathbb{R}^n}\int_{\mathbb{R}^n} e^{i(x-y)\cdot \theta} a(x,\theta)u(y)\,d\mathcal{L}^n(y)\,d\mathcal{L}^n(\theta)$, interpreted by Schwartz cutoff regularization. Then there exist an integer $N=N(n)\in\mathbb{N}$ and a constant $C=C(n)>0$ such that $\|\operatorname{Op}(a)u\|_{L^2(\mathbb{R}^n)} \leq C \left(\max_{|\alpha|+|\beta|\leq N}\sup_{x,\theta \in \mathbb{R}^n} \langle \theta\rangle^{|\beta|}|\partial_x^\alpha\partial_\theta^\beta a(x,\theta)|\right)\|u\|_{L^2(\mathbb{R}^n)}$ for every $u \in \mathcal{S}(\mathbb{R}^n)$. Consequently $\operatorname{Op}(a)$ extends uniquely to a bounded linear operator on $L^2(\mathbb{R}^n)$.
## Proof
[proofplan]
We reduce the stated estimate to the standard finite-seminorm Calderón-Vaillancourt theorem for Kohn-Nirenberg operators. The symbol hypothesis gives uniform boundedness of all ordinary derivatives needed by that theorem, because $\langle\theta\rangle^{-|\beta|}\leq 1$. After applying the standard theorem on the dense domain $\mathcal{S}(\mathbb{R}^n)$, the claimed extension follows from the bounded extension theorem for operators defined on a dense subspace.
[/proofplan]
[step:Record the finite symbol seminorm controlled by the hypothesis]
For each integer $M\geq 0$, define the finite weighted symbol seminorm $p_M(a)\in[0,\infty)$ by
\begin{align*}
p_M(a)=\max_{|\alpha|+|\beta|\leq M}\sup_{x,\theta\in\mathbb{R}^n}\langle\theta\rangle^{|\beta|}|\partial_x^\alpha\partial_\theta^\beta a(x,\theta)|.
\end{align*}
The defining $S^0_{1,0}$ estimates imply $p_M(a)<\infty$ for every $M$. Moreover, for every pair of multi-indices $\alpha,\beta\in\mathbb{N}_0^n$ with $|\alpha|+|\beta|\leq M$ and all $x, heta\in\mathbb{R}^n$,
\begin{align*}
|\partial_x^\alpha\partial_\theta^\beta a(x,\theta)|\leq p_M(a)\langle\theta\rangle^{-|\beta|}.
\end{align*}
Since $\langle\theta\rangle\geq 1$, this gives
\begin{align*}
\sup_{x, heta\in\mathbb{R}^n}|\partial_x^\alpha\partial_\theta^\beta a(x,\theta)|\leq p_M(a).
\end{align*}
[/step]
[step:Apply the standard Calderón-Vaillancourt estimate]
We use the following standard Calderón-Vaillancourt theorem for Kohn-Nirenberg quantization. For every $n\in\mathbb{N}$ there are an integer $N_0=N_0(n)\in\mathbb{N}$ and a constant $C_0=C_0(n)>0$ such that, whenever $b: \mathbb{R}^n_x\times\mathbb{R}^n_\theta\to\mathbb{C}$ is a $C^\infty$ function satisfying
\begin{align*}
q_{N_0}(b):=\max_{|\alpha|+|\beta|\leq N_0}\sup_{x, heta\in\mathbb{R}^n}|\partial_x^\alpha\partial_\theta^\beta b(x, heta)|<\infty,
\end{align*}
the operator $\operatorname{Op}(b)$, defined on $\mathcal{S}(\mathbb{R}^n)$ by the Kohn-Nirenberg oscillatory integral with Schwartz cutoff regularization, satisfies
\begin{align*}
\|\operatorname{Op}(b)u\|_{L^2(\mathbb{R}^n)}\leq C_0 q_{N_0}(b)\|u\|_{L^2(\mathbb{R}^n)}
\end{align*}
for every $u\in\mathcal{S}(\mathbb{R}^n)$.
We apply this theorem with $b=a$. Its smoothness hypothesis is part of the assumption $a\in S^0_{1,0}$. Its finite ordinary derivative hypothesis holds by the previous step with $M=N_0$, and
\begin{align*}
q_{N_0}(a)\leq p_{N_0}(a).
\end{align*}
Therefore, for every $u\in\mathcal{S}(\mathbb{R}^n)$,
\begin{align*}
\|\operatorname{Op}(a)u\|_{L^2(\mathbb{R}^n)}\leq C_0 p_{N_0}(a)\|u\|_{L^2(\mathbb{R}^n)}.
\end{align*}
[guided]
The point of this step is to avoid reproving the full Calderón-Vaillancourt machinery inside this theorem. We invoke the standard finite-seminorm form of the Calderón-Vaillancourt theorem, and we must verify that our symbol satisfies exactly its hypotheses.
The standard theorem requires a smooth function $b: \mathbb{R}^n_x\times\mathbb{R}^n_\theta\to\mathbb{C}$ whose ordinary derivatives up to some dimension-dependent order $N_0$ are uniformly bounded. In symbols, it requires
\begin{align*}
q_{N_0}(b)=\max_{|\alpha|+|\beta|\leq N_0}\sup_{x, heta\in\mathbb{R}^n}|\partial_x^\alpha\partial_\theta^\beta b(x, heta)|<\infty.
\end{align*}
We take $b=a$. The smoothness requirement is satisfied because the theorem assumes that $a$ is a $C^\infty$ Hörmander symbol. It remains to check the uniform derivative bound. For every $\alpha,\beta\in\mathbb{N}_0^n$ with $|\alpha|+|\beta|\leq N_0$, the definition of $p_{N_0}(a)$ gives
\begin{align*}
|\partial_x^\alpha\partial_\theta^\beta a(x,\theta)|\leq p_{N_0}(a)\langle\theta\rangle^{-|\beta|}
\end{align*}
for every $x, heta\in\mathbb{R}^n$. Since $\langle\theta\rangle\geq 1$, the factor $\langle\theta\rangle^{-|\beta|}$ is at most $1$. Hence
\begin{align*}
\sup_{x, heta\in\mathbb{R}^n}|\partial_x^\alpha\partial_\theta^\beta a(x, heta)|\leq p_{N_0}(a).
\end{align*}
Taking the maximum over all $|\alpha|+|\beta|\leq N_0$ gives $q_{N_0}(a)\leq p_{N_0}(a)$. The standard Calderón-Vaillancourt theorem then gives
\begin{align*}
\|\operatorname{Op}(a)u\|_{L^2(\mathbb{R}^n)}\leq C_0 p_{N_0}(a)\|u\|_{L^2(\mathbb{R}^n)}
\end{align*}
for every $u\in\mathcal{S}(\mathbb{R}^n)$. This is exactly the desired estimate on the dense test-function domain, with the weighted seminorm appearing in the statement.
[/guided]
[/step]
[step:Choose the constants in the statement]
Define $N(n):=N_0(n)$ and $C(n):=C_0(n)$. By the definition of $p_{N(n)}(a)$, the estimate from the preceding step becomes
\begin{align*}
\|\operatorname{Op}(a)u\|_{L^2(\mathbb{R}^n)}\leq C(n)\left(\max_{|\alpha|+|\beta|\leq N(n)}\sup_{x, heta\in\mathbb{R}^n}\langle\theta\rangle^{|\beta|}|\partial_x^\alpha\partial_\theta^\beta a(x,\theta)|\right)\|u\|_{L^2(\mathbb{R}^n)}
\end{align*}
for every $u\in\mathcal{S}(\mathbb{R}^n)$.
[/step]
[step:Extend the operator from the Schwartz space to $L^2$]
Let $T: \mathcal{S}(\mathbb{R}^n)\to L^2(\mathbb{R}^n)$ denote the map $T u=\operatorname{Op}(a)u$. The preceding estimate shows that $T$ is bounded as a map from the normed space $(\mathcal{S}(\mathbb{R}^n),\|\cdot\|_{L^2(\mathbb{R}^n)})$ into $L^2(\mathbb{R}^n)$. Since $\mathcal{S}(\mathbb{R}^n)$ is dense in $L^2(\mathbb{R}^n)$, the bounded extension theorem for linear operators on dense subspaces gives a unique bounded linear operator $\widetilde{T}:L^2(\mathbb{R}^n)\to L^2(\mathbb{R}^n)$ such that $\widetilde{T}u=Tu$ for every $u\in\mathcal{S}(\mathbb{R}^n)$. Its operator norm is bounded by the same constant appearing in the estimate above. This unique extension is the asserted bounded $L^2$ extension of $\operatorname{Op}(a)$.
[/step]
