[proofplan] We prove the contrapositive. First, if $q$ is outside the semiclassical microsupport of $A_h$, then every test operator microlocalized near $q$ composes with $A_h$ to a residual operator, hence sends a tempered family to $O(h^\infty)$. Second, if $q$ is outside the semiclassical wavefront set of $u_h$, we choose a microlocal annihilator $C_h$ for $u_h$ near $q$, construct an elliptic parametrix for $C_h$, and insert the microlocal identity before $u_h$. The term containing $C_hu_h$ is rapidly small, and the residual remainder is rapidly small on tempered families. [/proofplan] [step:Fix the microlocal testing criterion at the point $q$] Fix $q \in T^*X$. By the definition of semiclassical wavefront set, to prove $q \notin \operatorname{WF}_h(A_hu_h)$ it is enough to find an operator $B_h \in \Psi_h^0(X)$ whose principal symbol is elliptic at $q$ and such that \begin{align*} B_h A_h u_h = O(h^\infty) \end{align*} in $C^\infty$ on a neighbourhood of the base point of $q$, equivalently in every local semiclassical Sobolev norm after applying a compactly supported coordinate cutoff. Here $B_h$ denotes an arbitrary microlocal test operator elliptic at $q$ with sufficiently small microsupport. The phrase “sufficiently small” means that $\operatorname{MS}_h(B_h)$ is contained in a conic neighbourhood of $q$ on which the relevant microlocal condition is valid. [/step] [step:Exclude points outside the microsupport of $A_h$] Assume first that $q \notin \operatorname{MS}_h(A_h)$. Choose $B_h \in \Psi_h^0(X)$ elliptic at $q$ with $\operatorname{MS}_h(B_h)$ contained in an open neighbourhood $V \subset T^*X$ such that $V \cap \operatorname{MS}_h(A_h)=\varnothing$. By the defining property of the semiclassical microsupport and the semiclassical composition calculus, the composition $B_hA_h$ is residual: \begin{align*} B_hA_h \in h^\infty \Psi_h^{-\infty}(X). \end{align*} Since $(u_h)$ is semiclassically tempered, every residual operator in $h^\infty \Psi_h^{-\infty}(X)$ maps $u_h$ to a smooth family that is $O(h^\infty)$ in all local $C^\infty$ seminorms. Therefore \begin{align*} B_hA_hu_h = O(h^\infty). \end{align*} The operator $B_h$ is elliptic at $q$, so the microlocal testing criterion gives $q \notin \operatorname{WF}_h(A_hu_h)$. [guided] Assume $q \notin \operatorname{MS}_h(A_h)$. This means that $A_h$ has no microlocal contribution near $q$: after shrinking to an open neighbourhood $V \subset T^*X$ of $q$, the full symbol of $A_h$ is $O(h^\infty)$ there, modulo the standard coordinate description of semiclassical pseudodifferential operators. Choose an operator $B_h \in \Psi_h^0(X)$ whose principal symbol is elliptic at $q$ and whose semiclassical microsupport satisfies \begin{align*} \operatorname{MS}_h(B_h) \subset V. \end{align*} Because $V$ is disjoint from $\operatorname{MS}_h(A_h)$, the composition calculus gives \begin{align*} B_hA_h \in h^\infty \Psi_h^{-\infty}(X). \end{align*} This is the precise microlocal meaning of “$A_h$ is absent near $q$”: any operator $B_h$ that only tests near $q$ sees $A_h$ as residual to infinite order in $h$. Now use the temperedness hypothesis. A semiclassically tempered distribution family may grow at most polynomially in $h^{-1}$ in local distribution seminorms. A residual operator in $h^\infty\Psi_h^{-\infty}(X)$ has a smooth kernel that gains arbitrarily many powers of $h$, so applying it to a polynomially bounded family still gives a rapidly decaying smooth family. Hence \begin{align*} B_hA_hu_h = O(h^\infty) \end{align*} in all local smooth seminorms. Since $B_h$ is elliptic at $q$, the definition of $\operatorname{WF}_h$ implies \begin{align*} q \notin \operatorname{WF}_h(A_hu_h). \end{align*} [/guided] [/step] [step:Choose a microlocal annihilator for $u_h$ near $q$] Assume now that $q \notin \operatorname{WF}_h(u_h)$. By definition, there exists an operator $C_h \in \Psi_h^0(X)$ elliptic at $q$ such that \begin{align*} C_hu_h = O(h^\infty) \end{align*} in all local smooth seminorms. Choose $B_h \in \Psi_h^0(X)$ elliptic at $q$ with $\operatorname{MS}_h(B_h)$ contained in a sufficiently small neighbourhood on which $C_h$ is elliptic. By the semiclassical elliptic parametrix construction for $C_h$ microlocally near $\operatorname{MS}_h(B_h)$, there exists $E_h \in \Psi_h^0(X)$ and a residual remainder $R_h \in h^\infty\Psi_h^{-\infty}(X)$ such that \begin{align*} B_h = B_hE_hC_h + B_hR_h. \end{align*} Here $E_h$ is a microlocal inverse for $C_h$ on a neighbourhood of $\operatorname{MS}_h(B_h)$, and $R_h$ is residual on that neighbourhood. This is the standard semiclassical elliptic parametrix theorem, cited here as a result not yet in the wiki: semiclassical elliptic parametrix theorem. [/step] [step:Insert the parametrix identity before applying $A_h$] Apply the identity from the previous step to $A_hu_h$. Since $A_h$ is properly supported, $A_hu_h$ is a well-defined semiclassically tempered distribution family, and \begin{align*} B_hA_hu_h = B_hE_hC_hA_hu_h + B_hR_hA_hu_h. \end{align*} For the first term, it is more useful to place the annihilator $C_h$ immediately next to $u_h$. We therefore choose the parametrix identity in the equivalent microlocal form \begin{align*} I = E_hC_h + R_h \end{align*} on a neighbourhood of $\operatorname{MS}_h(B_hA_h)$, after shrinking the microsupport of $B_h$ if necessary. Substituting this identity before $u_h$ gives \begin{align*} B_hA_hu_h = B_hA_hE_hC_hu_h + B_hA_hR_hu_h. \end{align*} The shrinking is legitimate because the test operator in the definition of wavefront set only needs to remain elliptic at the single point $q$. [guided] The goal is to use the fact that $C_hu_h$ is rapidly small. Therefore the operator $C_h$ must stand directly next to $u_h$. The ellipticity of $C_h$ near $q$ gives a microlocal inverse $E_h$ near $q$, so microlocally near $q$ we may write the identity operator as \begin{align*} I = E_hC_h + R_h, \end{align*} where $R_h \in h^\infty\Psi_h^{-\infty}(X)$ is residual near the microsupport of the test operator. We now choose $B_h$ so that it is elliptic at $q$ and so tightly supported in phase space that the above identity is valid wherever $B_hA_h$ can detect singularities. This is allowed because wavefront set membership is tested microlocally at one point. Substituting the identity immediately before $u_h$ gives \begin{align*} B_hA_hu_h = B_hA_h(E_hC_h + R_h)u_h. \end{align*} Using linearity of the operators, this becomes \begin{align*} B_hA_hu_h = B_hA_hE_hC_hu_h + B_hA_hR_hu_h. \end{align*} This decomposition separates the proof into two estimates: the first term contains $C_hu_h$, which is $O(h^\infty)$ by the assumption $q \notin \operatorname{WF}_h(u_h)$; the second term contains the residual operator $R_h$, which is $O(h^\infty)$ on every tempered family. [/guided] [/step] [step:Estimate the term containing the annihilator $C_hu_h$] Since \begin{align*} C_hu_h = O(h^\infty) \end{align*} in all local smooth seminorms, and since $B_hA_hE_h$ is a properly supported semiclassical pseudodifferential operator of finite order, the standard continuity estimates for semiclassical pseudodifferential operators imply \begin{align*} B_hA_hE_hC_hu_h = O(h^\infty) \end{align*} in all local smooth seminorms. The finite order of $B_hA_hE_h$ can lose only a fixed power of $h$, while $C_hu_h$ gains arbitrarily many powers of $h$, so rapid decay is preserved. [/step] [step:Estimate the residual remainder on the tempered family] The family $(u_h)$ is semiclassically tempered, and $R_h \in h^\infty\Psi_h^{-\infty}(X)$. Therefore \begin{align*} R_hu_h = O(h^\infty) \end{align*} in all local smooth seminorms. Applying the properly supported finite-order operator $B_hA_h$ preserves rapid decay up to a fixed polynomial loss in $h^{-1}$, so \begin{align*} B_hA_hR_hu_h = O(h^\infty). \end{align*} Combining this estimate with the estimate for $B_hA_hE_hC_hu_h$ yields \begin{align*} B_hA_hu_h = O(h^\infty). \end{align*} Since $B_h$ is elliptic at $q$, the microlocal testing criterion gives \begin{align*} q \notin \operatorname{WF}_h(A_hu_h). \end{align*} [/step] [step:Conclude the set inclusion] We have proved both implications: if $q \notin \operatorname{MS}_h(A_h)$, then $q \notin \operatorname{WF}_h(A_hu_h)$, and if $q \notin \operatorname{WF}_h(u_h)$, then $q \notin \operatorname{WF}_h(A_hu_h)$. Hence \begin{align*} T^*X \setminus \operatorname{WF}_h(A_hu_h) \supset \left(T^*X \setminus \operatorname{MS}_h(A_h)\right) \cup \left(T^*X \setminus \operatorname{WF}_h(u_h)\right). \end{align*} Taking complements in $T^*X$ gives \begin{align*} \operatorname{WF}_h(A_hu_h) \subset \operatorname{WF}_h(u_h) \cap \operatorname{MS}_h(A_h). \end{align*} This is the desired semiclassical pseudolocality statement. [/step]