## Formalized Name
Elliptic Localization Theorem for Semiclassical Schrödinger Operators
## Formalized Statement
Let $h_0>0$, let $V\in C^\infty(\mathbb{R}^n;\mathbb{R})$, let $E\in\mathbb{R}$, and put
\begin{align*}
P_h=-h^2\Delta+V(x)-E.
\end{align*}
Let
\begin{align*}
p(x,\xi)=|\xi|^2+V(x)-E
\end{align*}
be its semiclassical principal symbol. Let $K\subset T^*\mathbb{R}^n$ be compact. Assume there are an open neighbourhood $U$ of $K$ and a constant $c>0$ such that
\begin{align*}
|p(x,\xi)|\ge c
\end{align*}
for all $(x,\xi)\in U$, and assume all derivatives of $V$ that occur on the projection of a fixed compact neighbourhood of $U$ are bounded. Let $u_h\in\mathcal{S}'(\mathbb{R}^n)$ be semiclassically tempered: for every compactly supported symbol $a\in C_c^\infty(T^*\mathbb{R}^n)$ and every $s\in\mathbb{R}$ there are constants $C,Q>0$ with
\begin{align*}
\|\operatorname{Op}_h(a)u_h\|_{H_h^s}\le Ch^{-Q}
\end{align*}
for $0<h\le h_0$. Suppose that for one cutoff $\theta\in C_c^\infty(U)$ with $\theta=1$ on a neighbourhood of $K$,
\begin{align*}
\operatorname{Op}_h(\theta)P_hu_h=O(h^\infty)
\end{align*}
in $H_h^s(\mathbb{R}^n)$ for every $s\in\mathbb{R}$. Then $K\cap\operatorname{WF}_h(u_h)=\varnothing$. Equivalently, for every $\chi\in C_c^\infty(T^*\mathbb{R}^n)$ with $\operatorname{supp}\chi\subset U$ and $\theta=1$ on a neighbourhood of $\operatorname{supp}\chi$,
\begin{align*}
\operatorname{Op}_h(\chi)u_h=O(h^\infty)
\end{align*}
in $H_h^s(\mathbb{R}^n)$ for every $s\in\mathbb{R}$.
## Proof
[proofplan]
Choose a cutoff $\chi$ inside the elliptic region and a larger cutoff $\theta$ equal to one near its support. Since $p$ is bounded away from zero on the support of $\theta$, the symbol $\theta/p$ is smooth and compactly supported. The symbolic composition of this inverse with $P_h$ gives an identity equal to the smaller cutoff modulo a smoothing remainder and arbitrarily high powers of $h$. Applying the identity to the tempered family $u_h$ shows that $\operatorname{Op}_h(\chi)u_h$ is rapidly small whenever $P_hu_h$ is rapidly small on the larger elliptic neighbourhood.
[/proofplan]
[step:Build a local inverse symbol]
Fix $\chi\in C_c^\infty(T^*\mathbb{R}^n)$ with $\operatorname{supp}\chi\subset U$, and choose $\theta\in C_c^\infty(U)$ with $\theta=1$ on a neighbourhood of $\operatorname{supp}\chi$. Since $|p|\ge c$ on $U$, the symbol
\begin{align*}
q_0(x,\xi)=\theta(x,\xi)p(x,\xi)^{-1}
\end{align*}
is smooth and compactly supported in $U$. The bounded-derivative hypothesis on $V$ over this compact region implies that $q_0$ has bounded symbol seminorms of every order. Hence $\operatorname{Op}_h(q_0)$ is an order $-2$ microlocal inverse candidate for $P_h$ on the support of $\chi$.
[/step]
[step:Construct the microlocal parametrix identity]
The full semiclassical symbol of $P_h$ is $p$ plus lower-order terms coming from the differential operator convention; for the Schrödinger operator in the standard left quantization, the principal part is $p$ and no first-order differential term changes the ellipticity on $U$. By the compactly supported semiclassical composition calculus, one can choose symbols
\begin{align*}
q_j\in C_c^\infty(U),\qquad j\ge 1,
\end{align*}
recursively so that, for each $L\in\mathbb{N}$, the partial sum
\begin{align*}
q^{(L)}=\sum_{j=0}^{L-1}h^j q_j
\end{align*}
satisfies
\begin{align*}
\operatorname{Op}_h(\chi)\operatorname{Op}_h(q^{(L)})P_h=\operatorname{Op}_h(\chi)+h^L R_{L,h}
\end{align*}
as an operator $H_h^{-N_L}\to H_h^s$, where $R_{L,h}$ is uniformly bounded between the indicated Sobolev spaces for suitable $N_L$ depending on $s$ and $L$. The recursive construction is possible because each error coefficient is supported where $\theta=1$ and can be multiplied by $p^{-1}$ there.
[/step]
[step:Apply the parametrix to the equation]
Apply the parametrix identity to $u_h$:
\begin{align*}
\operatorname{Op}_h(\chi)u_h
=
\operatorname{Op}_h(\chi)\operatorname{Op}_h(q^{(L)})P_hu_h
-h^L R_{L,h}u_h.
\end{align*}
Since $\theta=1$ near $\operatorname{supp}\chi$ and the symbols $q_j$ are supported in the region where $\theta=1$, the first term only uses the microlocalized equation $\operatorname{Op}_h(\theta)P_hu_h=O(h^\infty)$. Order-zero and compactly supported pseudodifferential operators preserve rapid Sobolev smallness, so for every $s$ and every $M$ this first term is $O(h^M)$ in $H_h^s$.
For the second term, semiclassical temperedness gives constants $C,Q>0$ and a Sobolev order $-N_L$ such that
\begin{align*}
\|R_{L,h}u_h\|_{H_h^s}\le Ch^{-Q}.
\end{align*}
Choosing $L\ge M+Q+1$ gives
\begin{align*}
\|h^L R_{L,h}u_h\|_{H_h^s}\le C h^M.
\end{align*}
Thus $\operatorname{Op}_h(\chi)u_h=O(h^\infty)$ in every $H_h^s$.
[/step]
[step:Conclude absence of wavefront on the compact set]
The preceding step holds for every cutoff $\chi$ supported in the elliptic neighbourhood and with a larger cutoff $\theta$ equal to one near $\operatorname{supp}\chi$. Cover the compact set $K$ by finitely many such cutoff supports, or choose a single $\chi$ equal to one on a neighbourhood of $K$ and supported where $\theta=1$. Then
\begin{align*}
\operatorname{Op}_h(\chi)u_h=O(h^\infty)
\end{align*}
in every semiclassical Sobolev norm, which is the definition that no point of $K$ belongs to $\operatorname{WF}_h(u_h)$. Hence
\begin{align*}
K\cap\operatorname{WF}_h(u_h)=\varnothing.
\end{align*}
This proves the theorem.
[guided]
The previous step proves that the chosen elliptic cutoff satisfies
\begin{align*}
\operatorname{Op}_h(\chi)u_h=O(h^\infty)
\end{align*}
in every semiclassical Sobolev norm. Choosing $\chi$ equal to one on a neighbourhood of $K$ gives the wavefront conclusion by definition:
\begin{align*}
K\cap\operatorname{WF}_h(u_h)=\varnothing.
\end{align*}
Thus ellipticity of $p$ on $K$ and microlocal rapid smallness of $P_hu_h$ near $K$ force $u_h$ to be microlocally rapidly small on $K$.
[/guided]
[/step]
