## Formalized Name Wavefront Set under Semiclassical Pseudodifferential Operators ## Formalized Statement Let $X$ be a smooth manifold, let $m \in \mathbb{R}$, let $A \in \Psi_h^m(X)$ be a semiclassical pseudodifferential operator, and let $(u_h)_{0<h\le h_0}$ be a semiclassically tempered family of distributions on $X$. Then \begin{align*} \operatorname{WF}_h(Au_h) \subset \operatorname{WF}_h(u_h). \end{align*} Moreover, if $q \in \overline{T}^*X$ and $A$ is elliptic at $q$, then \begin{align*} q \in \operatorname{WF}_h(u_h) \iff q \in \operatorname{WF}_h(Au_h). \end{align*} ## Proof [proofplan] The first assertion is semiclassical pseudolocality: a semiclassical pseudodifferential operator cannot create new semiclassical singularities away from the wavefront set of the input. Define $F_h = O(h^\infty)$ in $C^\infty(X)$ to mean that for every compact $K \subset X$, every integer $k \ge 0$, and every integer $N \ge 0$, the $C^k(K)$ seminorm of $F_h$ is bounded by $C_{K,k,N} h^N$ for all sufficiently small $h$. Also, let $I: \mathcal D'(X) \to \mathcal D'(X)$ denote the identity operator. We say that a family $F_h$ is microlocally $O(h^\infty)$ near a point or set if every semiclassical cutoff elliptic there sends it to a family that is $O(h^\infty)$ in $C^\infty(X)$. For the elliptic assertion, we use a microlocal parametrix for $A$ at the elliptic point $q$. If $Au_h$ is microlocally $O(h^\infty)$ at $q$, applying the parametrix recovers $u_h$ up to a residual term, and residual operators send semiclassically tempered families to microlocally negligible families. The converse implication follows from the first inclusion. [/proofplan] [step:Apply semiclassical pseudolocality to obtain the wavefront inclusion] Let $Q \in \Psi_h^0(X)$ be a semiclassical pseudodifferential cutoff. Define its semiclassical microsupport by \begin{align*} \operatorname{MS}_h(Q) := \{ q \in \overline{T}^*X : Q \text{ is not microlocally smoothing at } q \}. \end{align*} Assume that $\operatorname{MS}_h(Q)$ is contained in an open subset of $\overline{T}^*X \setminus \operatorname{WF}_h(u_h)$. By the definition of $\operatorname{WF}_h(u_h)$, there exists $Q_1 \in \Psi_h^0(X)$ elliptic on $\operatorname{MS}_h(Q)$ such that $Q_1u_h = O(h^\infty)$ in $C^\infty(X)$ microlocally on $\operatorname{MS}_h(Q)$. By the semiclassical pseudolocality theorem for pseudodifferential operators (citing a result not yet in the wiki: Semiclassical Pseudolocality Theorem), the composition $QA$ is microlocally supported only where $u_h$ may have semiclassical wavefront. Hence $QAu_h = O(h^\infty)$ in $C^\infty(X)$. Since this holds for every cutoff $Q$ microsupported away from $\operatorname{WF}_h(u_h)$, we obtain \begin{align*} \operatorname{WF}_h(Au_h) \subset \operatorname{WF}_h(u_h). \end{align*} [guided] We prove that no point outside $\operatorname{WF}_h(u_h)$ can lie in $\operatorname{WF}_h(Au_h)$. Let $Q \in \Psi_h^0(X)$ be a microlocal cutoff whose semiclassical microsupport is contained in the complement of $\operatorname{WF}_h(u_h)$. The definition of the semiclassical wavefront set says exactly that $u_h$ is microlocally $O(h^\infty)$ on this region: after inserting an elliptic cutoff $Q_1 \in \Psi_h^0(X)$ on $\operatorname{MS}_h(Q)$, one has $Q_1u_h = O(h^\infty)$ in $C^\infty(X)$ microlocally there. Now apply the semiclassical pseudolocality theorem for pseudodifferential operators (citing a result not yet in the wiki: Semiclassical Pseudolocality Theorem). Its content is that applying $A \in \Psi_h^m(X)$ cannot generate a new semiclassical singularity at a point where the input is already microlocally $O(h^\infty)$. The hypotheses are satisfied because $A$ is a semiclassical pseudodifferential operator and $u_h$ is semiclassically tempered, so the operator calculus applies to the family $u_h$. Therefore $QAu_h = O(h^\infty)$ in $C^\infty(X)$. Since every microlocal cutoff $Q$ supported outside $\operatorname{WF}_h(u_h)$ annihilates $Au_h$ modulo $O(h^\infty)$, no point outside $\operatorname{WF}_h(u_h)$ belongs to $\operatorname{WF}_h(Au_h)$. This proves \begin{align*} \operatorname{WF}_h(Au_h) \subset \operatorname{WF}_h(u_h). \end{align*} [/guided] [/step] [step:Construct an elliptic parametrix for $A$ near $q$] Assume that $A$ is elliptic at $q \in \overline{T}^*X$. By the semiclassical elliptic parametrix theorem (citing a result not yet in the wiki: Semiclassical Elliptic Parametrix Theorem), there exist an operator $B \in \Psi_h^{-m}(X)$, an operator $R \in \Psi_h^{-\infty}(X)$ residual microlocally near $q$, and an open neighborhood $V \subset \overline{T}^*X$ of $q$ such that \begin{align*} BA = I + R \end{align*} microlocally on $V$. Here $I: \mathcal D'(X) \to \mathcal D'(X)$ denotes the identity operator on distributions on $X$. The hypotheses of the parametrix theorem are satisfied because $A \in \Psi_h^m(X)$ and its principal symbol is elliptic at $q$ by assumption. [/step] [step:Use the parametrix to remove the wavefront of $u_h$ when $Au_h$ is regular near $q$] Suppose $q \notin \operatorname{WF}_h(Au_h)$. Choose $C \in \Psi_h^0(X)$ elliptic at $q$ and microsupported in the neighbourhood $V$ from the previous step such that \begin{align*} CAu_h = O(h^\infty) \end{align*} in $C^\infty(X)$. Shrinking $V$ if necessary, choose $C$ so that $B$ is applied only where the microlocal identity $BA = I + R$ holds. Then \begin{align*} BCAu_h = O(h^\infty) \end{align*} because $B \in \Psi_h^{-m}(X)$ maps microlocally $O(h^\infty)$ families to microlocally $O(h^\infty)$ families. On a possibly smaller neighbourhood of $q$, the operator $BC$ is a parametrix for $A$ in the same sense as $B$, and the identity gives \begin{align*} u_h = BCAu_h - Ru_h \end{align*} microlocally near $q$. The first term on the right is $O(h^\infty)$ microlocally near $q$. The second term is also $O(h^\infty)$ microlocally near $q$ because $R$ is residual microlocally near $q$ and $u_h$ is semiclassically tempered. Hence $u_h$ is microlocally $O(h^\infty)$ near $q$, so \begin{align*} q \notin \operatorname{WF}_h(u_h). \end{align*} [guided] We now prove the implication that uses ellipticity. Assume \begin{align*} q \notin \operatorname{WF}_h(Au_h). \end{align*} This means that $Au_h$ is microlocally $O(h^\infty)$ at $q$. More concretely, we may choose a cutoff $C \in \Psi_h^0(X)$ elliptic at $q$, with microsupport contained in the neighbourhood where the parametrix identity is valid, such that \begin{align*} CAu_h = O(h^\infty) \end{align*} in $C^\infty(X)$. The role of ellipticity is that it lets us invert $A$ microlocally. From the previous step, the semiclassical elliptic parametrix theorem gives $B \in \Psi_h^{-m}(X)$ and a residual operator $R \in \Psi_h^{-\infty}(X)$ such that \begin{align*} BA = I + R \end{align*} microlocally near $q$. Applying $B$ to the microlocally negligible family $CAu_h$ preserves $O(h^\infty)$ regularity, because semiclassical pseudodifferential operators act continuously on such microlocally negligible families. Thus \begin{align*} BCAu_h = O(h^\infty) \end{align*} microlocally near $q$. On the neighbourhood where $C$ is elliptic and the parametrix identity holds, inserting $C$ does not change the microlocal information at $q$. Therefore the parametrix identity gives \begin{align*} u_h = BCAu_h - Ru_h \end{align*} microlocally near $q$. The first term is already $O(h^\infty)$. For the second term, the residual nature of $R$ means that its full semiclassical symbol vanishes to infinite order microlocally near $q$; when applied to a semiclassically tempered family, it produces an $O(h^\infty)$ family microlocally near $q$. Hence \begin{align*} Ru_h = O(h^\infty) \end{align*} microlocally near $q$. Both terms on the right-hand side are microlocally negligible, so $u_h$ itself is microlocally $O(h^\infty)$ near $q$. By the definition of the semiclassical wavefront set, this proves \begin{align*} q \notin \operatorname{WF}_h(u_h). \end{align*} [/guided] [/step] [step:Combine the contrapositive with pseudolocality to prove the equivalence] The previous step proves the contrapositive implication \begin{align*} q \notin \operatorname{WF}_h(Au_h) \implies q \notin \operatorname{WF}_h(u_h). \end{align*} Equivalently, \begin{align*} q \in \operatorname{WF}_h(u_h) \implies q \in \operatorname{WF}_h(Au_h). \end{align*} The first step gives the reverse implication \begin{align*} q \in \operatorname{WF}_h(Au_h) \implies q \in \operatorname{WF}_h(u_h). \end{align*} Therefore, when $A$ is elliptic at $q$, \begin{align*} q \in \operatorname{WF}_h(u_h) \iff q \in \operatorname{WF}_h(Au_h). \end{align*} This completes the proof. [/step]