## Formalized Name
Microlocal Partition Lemma
## Formalized Statement
Let $K \subset T^*\mathbb{R}^n$ be compact, let $h_0>0$, and let $\chi_1,\dots,\chi_N \in C_c^\infty(T^*\mathbb{R}^n)$ satisfy
\begin{align*}
\sum_{j=1}^N \chi_j=1
\end{align*}
on an open neighbourhood $U$ of $K$. For $a\in C_c^\infty(T^*\mathbb{R}^n)$ define the left semiclassical quantization on $\mathcal{S}(\mathbb{R}^n)$ by
\begin{align*}
\operatorname{Op}_h(a)v(x)=(2\pi h)^{-n}\int_{\mathbb{R}^n}\int_{\mathbb{R}^n}e^{i(x-y)\cdot\xi/h}a(x,\xi)v(y)\,dy\,d\xi.
\end{align*}
Here $dy$ and $d\xi$ denote Lebesgue measure on the corresponding copies of $\mathbb{R}^n$.
For each $j$, put $A_j=\operatorname{Op}_h(\chi_j)$. Let $u_h\in\mathcal{S}'(\mathbb{R}^n)$ be a semiclassically tempered family such that, for one cutoff $\rho\in C_c^\infty(T^*\mathbb{R}^n)$ with $\rho=1$ on a neighbourhood of $K$ and $\operatorname{supp}\rho\subset U$, the remainder
\begin{align*}
(I-\operatorname{Op}_h(\rho))u_h
\end{align*}
is $O(h^\infty)$ in $H_h^s(\mathbb{R}^n)$ for every $s\in\mathbb{R}$. Then, for every $s\in\mathbb{R}$ and every $M\in\mathbb{N}$, there is a constant $C_{s,M}>0$ such that
\begin{align*}
\left\|u_h-\sum_{j=1}^N A_j u_h\right\|_{H_h^s}\le C_{s,M}h^M
\end{align*}
for all $0<h\le h_0$. Consequently, for every $s\in\mathbb{R}$ and every $M\in\mathbb{N}$, there are constants $C_s,C_{s,M}>0$ such that
\begin{align*}
\|u_h\|_{H_h^s}\le C_s\sum_{j=1}^N\|A_j u_h\|_{H_h^s}+C_{s,M}h^M
\end{align*}
for all $0<h\le h_0$.
## Proof
[proofplan]
Choose a cutoff $\rho$ supported where the partition sums to one. The symbol identity $\rho=\sum_j\chi_j\rho$ converts, after quantization and composition, into an operator identity modulo a smoothing remainder with compactly supported symbol. Applying this identity to $u_h$ gives the desired decomposition because the hypothesis makes $(I-\operatorname{Op}_h(\rho))u_h$ rapidly small in every semiclassical Sobolev norm. The norm estimate then follows from the triangle inequality.
[/proofplan]
[step:Insert a cutoff supported where the partition is exact]
Choose $\rho\in C_c^\infty(T^*\mathbb{R}^n)$ with $\rho=1$ on a neighbourhood of $K$ and $\operatorname{supp}\rho\subset U$. Since $\sum_{j=1}^N\chi_j=1$ on $U$, we have the exact symbol identity
\begin{align*}
\rho=\sum_{j=1}^N \chi_j\rho.
\end{align*}
Let $R_{j,h}$ denote the composition remainder
\begin{align*}
R_{j,h}=\operatorname{Op}_h(\chi_j)\operatorname{Op}_h(\rho)-\operatorname{Op}_h(\chi_j\rho).
\end{align*}
The compactly supported semiclassical composition formula gives
\begin{align*}
R_{j,h}=h\,\operatorname{Op}_h(r_{j,h})
\end{align*}
with $r_j$ a uniformly bounded family in $S^{-1}(T^*\mathbb{R}^n)$ with compact phase-space support. More generally, expanding the composition to order $L$ gives a remainder bounded by $C_{s,L}h^L$ as an operator $H_h^s\to H_h^s$, because all symbols involved are compactly supported and smooth.
[/step]
[step:Compare the partition sum with the microlocal cutoff]
Summing the preceding identity over $j$ and using $\rho=\sum_j\chi_j\rho$ gives, for every $L\in\mathbb{N}$,
\begin{align*}
\sum_{j=1}^N A_j\operatorname{Op}_h(\rho)=\operatorname{Op}_h(\rho)+E_{L,h},
\end{align*}
where $E_{L,h}:H_h^s(\mathbb{R}^n)\to H_h^s(\mathbb{R}^n)$ has operator norm at most $C_{s,L}h^L$. Therefore
\begin{align*}
u_h-\sum_{j=1}^N A_j u_h
=
(I-\operatorname{Op}_h(\rho))u_h
-\sum_{j=1}^N A_j(I-\operatorname{Op}_h(\rho))u_h
-E_{L,h}u_h.
\end{align*}
The first term is $O(h^\infty)$ in $H_h^s$ by hypothesis. Since each $A_j$ is an order-zero compactly supported semiclassical pseudodifferential operator, it is uniformly bounded on $H_h^s$, so the finite sum in the second term is also $O(h^\infty)$ in $H_h^s$. Finally, semiclassical temperedness gives an exponent $Q_s$ such that $\|u_h\|_{H_h^s}\le C_sh^{-Q_s}$ after decreasing $s$ if necessary and applying an elliptic compact cutoff equal to one on $\operatorname{supp}\rho$. Taking $L\ge M+Q_s+1$ gives
\begin{align*}
\|E_{L,h}u_h\|_{H_h^s}\le C_{s,M}h^M.
\end{align*}
This proves
\begin{align*}
\left\|u_h-\sum_{j=1}^N A_j u_h\right\|_{H_h^s}\le C_{s,M}h^M.
\end{align*}
[/step]
[step:Derive the Sobolev norm estimate]
From the decomposition estimate and the triangle inequality,
\begin{align*}
\|u_h\|_{H_h^s}
\le
\sum_{j=1}^N\|A_j u_h\|_{H_h^s}
+\left\|u_h-\sum_{j=1}^N A_j u_h\right\|_{H_h^s}.
\end{align*}
Using the bound from the previous step gives
\begin{align*}
\|u_h\|_{H_h^s}\le \sum_{j=1}^N\|A_j u_h\|_{H_h^s}+C_{s,M}h^M.
\end{align*}
The stated form follows with $C_s=1$, or with any larger constant. This completes the proof.
[guided]
The decomposition estimate says that the difference between $u_h$ and the finite partition sum is small:
\begin{align*}
\left\|u_h-\sum_{j=1}^N A_j u_h\right\|_{H_h^s}\le C_{s,M}h^M.
\end{align*}
Applying the triangle inequality to
\begin{align*}
u_h=\sum_{j=1}^N A_j u_h+\left(u_h-\sum_{j=1}^N A_j u_h\right)
\end{align*}
gives
\begin{align*}
\|u_h\|_{H_h^s}
\le
\sum_{j=1}^N\|A_j u_h\|_{H_h^s}
+\left\|u_h-\sum_{j=1}^N A_j u_h\right\|_{H_h^s}.
\end{align*}
Substituting the first displayed bound gives
\begin{align*}
\|u_h\|_{H_h^s}\le \sum_{j=1}^N\|A_j u_h\|_{H_h^s}+C_{s,M}h^M.
\end{align*}
Thus the norm estimate follows with $C_s=1$, or with any larger constant.
[/guided]
[/step]
