## Formalized Name Semiclassical Pseudolocality Theorem ## Formalized Statement Let $h \in (0,h_0]$ with $h_0 > 0$, let $m \in \mathbb{R}$, let $(A_h)_{0<h\le h_0}$ be a properly supported family of semiclassical pseudodifferential operators in $\Psi_h^m(\mathbb{R}^n)$, and let $(u_h)_{0<h\le h_0}$ be a globally $h$-tempered family of distributions $u_h \in \mathcal{D}'(\mathbb{R}^n)$ in the following sense: for every compactly supported semiclassical pseudodifferential operator $P_h \in \Psi_h^0(\mathbb{R}^n)$, there exist $r \in \mathbb{R}$ and $M \in \mathbb{N}$ such that $\|P_hu_h\|_{H_h^r(\mathbb{R}^n)} = O(h^{-M})$ as $h \to 0$. Let $\operatorname{MS}_h(A_h) \subset T^*\mathbb{R}^n$ denote the semiclassical microsupport of the family $(A_h)$, and let $\operatorname{WF}_h(u_h) \subset T^*\mathbb{R}^n$ denote the semiclassical wavefront set of $(u_h)$, where $q \notin \operatorname{WF}_h(u_h)$ means that some $B_h \in \Psi_h^0(\mathbb{R}^n)$ elliptic at $q$ satisfies $B_hu_h = O(h^\infty)$ in $H_h^s(\mathbb{R}^n)$ for every $s \in \mathbb{R}$. Then \begin{align*} \operatorname{WF}_h(A_h u_h) \subset \operatorname{MS}_h(A_h) \cap \operatorname{WF}_h(u_h). \end{align*} Equivalently, if $q \in T^*\mathbb{R}^n$ satisfies either $q \notin \operatorname{MS}_h(A_h)$ or $q \notin \operatorname{WF}_h(u_h)$, then $q \notin \operatorname{WF}_h(A_h u_h)$. ## Proof [proofplan] We prove the inclusion by testing $A_hu_h$ with an arbitrary zeroth-order microlocal cutoff $B_h$ elliptic at a point $q$ outside the right-hand side. If $q$ is outside the microsupport of $A_h$, then the symbolic composition $B_hA_h$ has symbol $O(h^\infty)$ and is therefore rapidly smoothing. If $q$ is outside the wavefront set of $u_h$, we insert a cutoff $C_h$ which kills $u_h$ microlocally near the region where $B_hA_h$ can see it; the remaining term has separated microsupports and is again rapidly smoothing. In both cases, proper support ensures that all compositions act on the distribution family without global support issues. [/proofplan] [step:Choose a microlocal cutoff at a point outside the proposed wavefront set] Let \begin{align*} q \in T^*\mathbb{R}^n \setminus \bigl(\operatorname{MS}_h(A_h) \cap \operatorname{WF}_h(u_h)\bigr). \end{align*} We must prove that $q \notin \operatorname{WF}_h(A_hu_h)$. By the definition of semiclassical wavefront set, it is enough to find an operator $B_h \in \Psi_h^0(\mathbb{R}^n)$ elliptic at $q$ such that, for every $s \in \mathbb{R}$ and every $N \in \mathbb{N}$, \begin{align*} \|B_hA_hu_h\|_{H_h^s(\mathbb{R}^n)} = O(h^N) \quad \text{as } h \to 0. \end{align*} Since $q$ is outside the intersection, either $q \notin \operatorname{MS}_h(A_h)$ or $q \notin \operatorname{WF}_h(u_h)$. Choose a sufficiently small precompact microlocal neighbourhood $U \subset T^*\mathbb{R}^n$ of $q$. Choose \begin{align*} B_h \in \Psi_h^0(\mathbb{R}^n) \end{align*} properly supported, elliptic at $q$, and with $\operatorname{MS}_h(B_h) \subset U$. [guided] We localize the question at one phase-space point. The desired inclusion means that every point outside $\operatorname{MS}_h(A_h) \cap \operatorname{WF}_h(u_h)$ is absent from the output wavefront set. Thus fix \begin{align*} q \in T^*\mathbb{R}^n \setminus \bigl(\operatorname{MS}_h(A_h) \cap \operatorname{WF}_h(u_h)\bigr). \end{align*} To prove $q \notin \operatorname{WF}_h(A_hu_h)$, the definition of semiclassical wavefront set asks us to find a zeroth-order semiclassical pseudodifferential operator which is elliptic at $q$ and which makes $A_hu_h$ rapidly small in every semiclassical Sobolev norm. We therefore choose a properly supported operator \begin{align*} B_h \in \Psi_h^0(\mathbb{R}^n) \end{align*} whose microsupport lies in a small microlocal neighbourhood $U$ of $q$ and whose principal symbol is nonzero at $q$. Why does this localization split into two cases? Since $q$ is not in the intersection, at least one obstruction is absent at $q$: either $A_h$ is microlocally zero there, meaning $q \notin \operatorname{MS}_h(A_h)$, or the input is microlocally smooth there, meaning $q \notin \operatorname{WF}_h(u_h)$. The proof treats these two alternatives separately, but the same test operator $B_h$ is used to certify the absence of wavefront set for the output. [/guided] [/step] [step:Eliminate the case where the operator is microlocally zero near $q$] Assume first that $q \notin \operatorname{MS}_h(A_h)$. Shrinking $U$ if necessary, arrange that \begin{align*} U \cap \operatorname{MS}_h(A_h) = \varnothing. \end{align*} Since $\operatorname{MS}_h(B_h) \subset U$ and $U \cap \operatorname{MS}_h(A_h)=\varnothing$, the semiclassical composition theorem with microsupport control applies to the properly supported composition $B_hA_h$ and gives \begin{align*} B_hA_h \in h^\infty \Psi_h^{-\infty}(\mathbb{R}^n). \end{align*} Here $h^\infty \Psi_h^{-\infty}(\mathbb{R}^n)$ means a properly supported smoothing family $R_h: \mathcal{D}'(\mathbb{R}^n) \to C^\infty(\mathbb{R}^n)$ such that, after inserting a compactly supported zeroth-order cutoff on the input side, its operator norm from $H_h^r(\mathbb{R}^n)$ to $H_h^s(\mathbb{R}^n)$ is $O(h^N)$ for every $r,s \in \mathbb{R}$ and every $N \in \mathbb{N}$. More explicitly, every full symbol coefficient of the localized composition is $O(h^N)$ for every $N \in \mathbb{N}$, and proper support gives a fixed compact input projection after the cutoff is inserted. Choose a compactly supported cutoff $P_h \in \Psi_h^0(\mathbb{R}^n)$ equal to the identity on that input projection. The global $h$-temperedness hypothesis applied to this $P_h$ gives numbers $r \in \mathbb{R}$ and $M \in \mathbb{N}$ such that \begin{align*} \|P_hu_h\|_{H_h^r(\mathbb{R}^n)} = O(h^{-M}). \end{align*} For every $s \in \mathbb{R}$ and every target power $K \in \mathbb{N}$, the defining rapid smoothing estimate with exponent $K+M$ gives \begin{align*} \|B_hA_hu_h\|_{H_h^s(\mathbb{R}^n)} \le C_{s,r,K} h^{K+M} \|P_hu_h\|_{H_h^r(\mathbb{R}^n)}. \end{align*} Using the preceding $h$-tempered bound gives \begin{align*} \|B_hA_hu_h\|_{H_h^s(\mathbb{R}^n)} = O(h^K) \end{align*} for every $s \in \mathbb{R}$ and every $K \in \mathbb{N}$. Hence $q \notin \operatorname{WF}_h(A_hu_h)$ in this case. [/step] [step:Insert an input cutoff when $u_h$ is microlocally smooth near $q$] Assume now that $q \notin \operatorname{WF}_h(u_h)$. By the definition of the complement of $\operatorname{WF}_h(u_h)$, choose a microlocal neighbourhood $W \subset T^*\mathbb{R}^n$ of $q$ on which $u_h$ is microlocally smooth, meaning that every properly supported compactly microsupported cutoff $Q_h \in \Psi_h^0(\mathbb{R}^n)$ with $\operatorname{MS}_h(Q_h) \subset W$ satisfies $Q_hu_h = O(h^\infty)$ in $H_h^s(\mathbb{R}^n)$ for every $s \in \mathbb{R}$. Shrink $U$ so that $U \subset W$. The semiclassical composition theorem with microsupport control applies to the properly supported operators $B_h$ and $A_h$ and gives \begin{align*} \operatorname{MS}_h(B_hA_h) \subset \operatorname{MS}_h(B_h) \cap \operatorname{MS}_h(A_h) \subset U \subset W, \end{align*} where the proper support of $A_h$ and $B_h$ ensures that the composition is defined on distribution families. Choose \begin{align*} C_h \in \Psi_h^0(\mathbb{R}^n) \end{align*} properly supported, microlocally equal to the identity on a microlocal neighbourhood $V \subset W$ of $\operatorname{MS}_h(B_hA_h)$, and with $\operatorname{MS}_h(C_h) \subset W$. Since $u_h$ is microlocally smooth on $W$, the cutoff construction and elliptic parametrix characterization of $\operatorname{WF}_h(u_h)$ give \begin{align*} C_hu_h = O(h^\infty) \quad \text{in } H_h^s(\mathbb{R}^n) \text{ for every } s \in \mathbb{R}. \end{align*} Decompose \begin{align*} B_hA_hu_h = B_hA_hC_hu_h + B_hA_h(I-C_h)u_h, \end{align*} where $I$ denotes the identity operator on distributions on $\mathbb{R}^n$. The first term is rapidly small in every Sobolev norm. Indeed, $B_hA_hC_h \in \Psi_h^m(\mathbb{R}^n)$ is properly supported, and the semiclassical Sobolev mapping property gives, for every $s \in \mathbb{R}$, \begin{align*} \|B_hA_hC_hu_h\|_{H_h^s(\mathbb{R}^n)} \le C_s h^{-L_s}\|C_hu_h\|_{H_h^{s+m}(\mathbb{R}^n)} \end{align*} for some constants $C_s > 0$ and $L_s \in \mathbb{N}$ depending on finitely many seminorms of the operator family (citing a result not yet in the wiki: mapping properties of semiclassical pseudodifferential operators on $H_h^s$). Since $C_hu_h = O(h^\infty)$ in $H_h^{s+m}(\mathbb{R}^n)$, it follows that \begin{align*} \|B_hA_hC_hu_h\|_{H_h^s(\mathbb{R}^n)} = O(h^\infty). \end{align*} [guided] Here the point is that $u_h$ is already microlocally smooth near $q$, but $A_h$ can only contribute to $B_hA_hu_h$ through the microlocal region visible to the composition $B_hA_h$. Let $W \subset T^*\mathbb{R}^n$ be a microlocal neighbourhood of $q$ on which $u_h$ is microlocally smooth. We shrink the support neighbourhood $U$ of $B_h$ so that $U \subset W$. The composition theorem with microsupport control applies because $B_h$ and $A_h$ are properly supported, and it gives \begin{align*} \operatorname{MS}_h(B_hA_h) \subset \operatorname{MS}_h(B_h) \cap \operatorname{MS}_h(A_h) \subset U \subset W. \end{align*} Thus every microlocal point seen by $B_hA_h$ lies in the region where the input is smooth. Here microlocal smoothness on $W$ means that every properly supported compactly microsupported cutoff $Q_h \in \Psi_h^0(\mathbb{R}^n)$ with $\operatorname{MS}_h(Q_h) \subset W$ sends $u_h$ to $O(h^\infty)$ in $H_h^s(\mathbb{R}^n)$ for every $s \in \mathbb{R}$. We now choose a cutoff \begin{align*} C_h \in \Psi_h^0(\mathbb{R}^n) \end{align*} which is properly supported, microlocally equal to the identity on a microlocal neighbourhood $V$ containing $\operatorname{MS}_h(B_hA_h)$, and satisfies $\operatorname{MS}_h(C_h) \subset W$. Because $u_h$ is microlocally smooth on $W$, the cutoff-nesting construction, equivalently the elliptic parametrix characterization of $\operatorname{WF}_h(u_h)$, gives \begin{align*} C_hu_h = O(h^\infty) \quad \text{in } H_h^s(\mathbb{R}^n) \text{ for every } s \in \mathbb{R}. \end{align*} Now split the input into the part seen by $C_h$ and the part killed by $C_h$: \begin{align*} B_hA_hu_h = B_hA_hC_hu_h + B_hA_h(I-C_h)u_h. \end{align*} The first term is controlled because $C_hu_h$ is rapidly small in every Sobolev norm. The operator $B_hA_hC_h$ has order $m$ and is properly supported, so the standard semiclassical Sobolev mapping estimate gives, for each $s \in \mathbb{R}$, \begin{align*} \|B_hA_hC_hu_h\|_{H_h^s(\mathbb{R}^n)} \le C_s h^{-L_s}\|C_hu_h\|_{H_h^{s+m}(\mathbb{R}^n)} \end{align*} for constants $C_s > 0$ and $L_s \in \mathbb{N}$ depending only on the relevant operator seminorms. The factor $h^{-L_s}$ is only polynomially bad, while $C_hu_h$ is $O(h^N)$ for every $N$. Choosing $N$ larger than any prescribed target power plus $L_s$ gives \begin{align*} \|B_hA_hC_hu_h\|_{H_h^s(\mathbb{R}^n)} = O(h^\infty). \end{align*} Thus the portion of the input localized where $u_h$ is smooth contributes no wavefront set to the output. The second term is controlled by the identity property of $C_h$. Because $C_h$ is microlocally equal to the identity on a neighbourhood of $\operatorname{MS}_h(B_hA_h)$, the complementary cutoff $I-C_h$ is microlocally zero on that neighbourhood. Hence the separated-microsupport composition theorem applies to the properly supported factors and gives \begin{align*} B_hA_h(I-C_h) \in h^\infty\Psi_h^{-\infty}(\mathbb{R}^n). \end{align*} By the definition of this residual class, after inserting a compactly supported input cutoff $P_h \in \Psi_h^0(\mathbb{R}^n)$, the operator norm from $H_h^r(\mathbb{R}^n)$ to $H_h^s(\mathbb{R}^n)$ is $O(h^N)$ for every $r,s \in \mathbb{R}$ and every $N \in \mathbb{N}$. The global $h$-temperedness hypothesis supplies $r \in \mathbb{R}$ and $M \in \mathbb{N}$ with $\|P_hu_h\|_{H_h^r(\mathbb{R}^n)} = O(h^{-M})$. Choosing the residual estimate with exponent $K+M$ gives \begin{align*} \|B_hA_h(I-C_h)u_h\|_{H_h^s(\mathbb{R}^n)} = O(h^K) \end{align*} for every $s \in \mathbb{R}$ and every $K \in \mathbb{N}$. Combining this with the estimate for $B_hA_hC_hu_h$ proves that $B_hA_hu_h$ is $O(h^K)$ in every $H_h^s(\mathbb{R}^n)$, so $q \notin \operatorname{WF}_h(A_hu_h)$ in the case $q \notin \operatorname{WF}_h(u_h)$. [/guided] [/step] [step:Use microsupport separation to remove the complementary cutoff term] It remains to estimate $B_hA_h(I-C_h)u_h$. Since $C_h$ was chosen microlocally equal to the identity, not merely elliptic, on a microlocal neighbourhood of $\operatorname{MS}_h(B_hA_h)$, the operator $I-C_h$ is microlocally zero there. Therefore \begin{align*} \operatorname{MS}_h(B_hA_h) \cap \operatorname{MS}_h(I-C_h) = \varnothing \end{align*} after the preceding shrinkings, in the sense relevant to the semiclassical composition calculus. The composition theorem with separated microsupports applies to the properly supported factors and gives \begin{align*} B_hA_h(I-C_h) \in h^\infty\Psi_h^{-\infty}(\mathbb{R}^n). \end{align*} As above, this means a properly supported rapidly smoothing family whose localized operator norms from $H_h^r(\mathbb{R}^n)$ to $H_h^s(\mathbb{R}^n)$ are $O(h^N)$ for every $r,s \in \mathbb{R}$ and every $N \in \mathbb{N}$. Using again the localized $h$-temperedness hypothesis with a compact input cutoff for the properly supported kernel of $B_hA_h(I-C_h)$, and then choosing the smoothing exponent large enough to absorb the polynomial $h$-tempering loss, we obtain, for every $s \in \mathbb{R}$ and every $K \in \mathbb{N}$, \begin{align*} \|B_hA_h(I-C_h)u_h\|_{H_h^s(\mathbb{R}^n)} = O(h^K). \end{align*} Combining this estimate with the estimate for $B_hA_hC_hu_h$ gives \begin{align*} \|B_hA_hu_h\|_{H_h^s(\mathbb{R}^n)} = O(h^K) \end{align*} for every $s \in \mathbb{R}$ and every $K \in \mathbb{N}$. Hence $q \notin \operatorname{WF}_h(A_hu_h)$ in the second case. [/step] [step:Conclude the wavefront inclusion] We have shown that every point \begin{align*} q \notin \operatorname{MS}_h(A_h) \cap \operatorname{WF}_h(u_h) \end{align*} satisfies $q \notin \operatorname{WF}_h(A_hu_h)$. Taking contrapositives gives \begin{align*} \operatorname{WF}_h(A_hu_h) \subset \operatorname{MS}_h(A_h) \cap \operatorname{WF}_h(u_h). \end{align*} This is the asserted semiclassical pseudolocality statement. [/step]