[proofplan] The first assertion is the kernel wave front mapping theorem applied to the Schwartz kernel of the Fourier integral operator, together with the defining inclusion $WF'(K_A)\subset C$. The local formulation follows by cutting off microlocally with a properly supported pseudodifferential operator and using the pseudodifferential characterization of smooth microlocal regularity. For the elliptic graph refinement, the canonical graph assumption gives a microlocal inverse Fourier integral operator; the no-other-branches hypothesis ensures that singularities of $u$ outside the chosen input cone cannot contribute to the tested output cone. The two implications in the final equivalence then follow from the mapping inclusion and from applying the parametrix identity to recover the input singularity modulo smoothing terms. [/proofplan]

[step:Apply the kernel wave front mapping theorem to the Schwartz kernel of $A$]Let \begin{align*} R_A := WF'(K_A) \subset (T^*X \setminus 0) \times (T^*Y \setminus 0) \end{align*} denote the twisted wave front relation of the Schwartz kernel of $A$. Since $A$ is properly supported, the kernel action defining $Au$ is well-defined for every $u \in \mathcal{D}'(Y)$. The [[Wave Front Set Mapping Theorem for Properly Supported Fourier Integral Kernels](/theorems/8165)][citetheorem:8165] applies to the properly supported kernel $K_A$: the operator is properly supported, the distribution $u$ lies in $\mathcal{D}'(Y)$, the twisted relation is $R_A$, and the stated no-one-sided-wave-front hypothesis excludes pure $X$- or pure $Y$-covector contributions. It gives \begin{align*} WF(Au) \subset R_A \circ WF(u). \end{align*} Here \begin{align*} R_A \circ WF(u) := \{(x,\xi) \in T^*X \setminus 0 : \text{there exists } (y,\eta) \in WF(u) \text{ such that } (x,\xi;y,\eta) \in R_A\}. \end{align*} The hypothesis $R_A=WF'(K_A)\subset C$ implies \begin{align*} R_A \circ WF(u) \subset C \circ WF(u). \end{align*} Therefore \begin{align*} WF(Au) \subset C \circ WF(u). \end{align*}[/step]

[guided]Define \begin{align*} R_A := WF'(K_A) \end{align*} as the twisted wave front relation of the Schwartz kernel of $A$. The word "twisted" matters: a kernel covector $(x,y;\xi,-\eta)$ is recorded as an operator relation $(x,\xi;y,\eta)$. This is exactly the convention used in the statement, so the output covector $(x,\xi)$ is related to the input covector $(y,\eta)$ without an additional sign change. Because $A$ is properly supported, the transpose operator \begin{align*} A^t:C_c^\infty(X)\to C_c^\infty(Y) \end{align*} maps compactly supported test functions on $X$ to compactly supported test functions on $Y$. Hence, for every $u\in\mathcal D'(Y)$, the formula \begin{align*} (Au)(\phi):=u(A^t\phi), \qquad \phi\in C_c^\infty(X), \end{align*} defines a distribution on $X$. We now apply the [Wave Front Set Mapping Theorem for Properly Supported Fourier Integral Kernels][citetheorem:8165]. Its hypotheses are satisfied because $K_A\in\mathcal D'(X\times Y)$ is the Schwartz kernel of a properly supported operator, $Au$ is defined by the corresponding properly supported kernel action, the twisted relation is $R_A$, and the stated no-one-sided-wave-front hypothesis rules out pure covectors of the form $(x,y;\xi,0)$ and $(x,y;0,\eta)$ in the kernel wave front set. The theorem gives \begin{align*} WF(Au) \subset R_A \circ WF(u). \end{align*} By the explicit assumption in the present theorem, \begin{align*} R_A=WF'(K_A)\subset C. \end{align*} Composing both sides with the set $WF(u)$ preserves inclusion: if $(x,\xi)\in R_A\circ WF(u)$, then there is $(y,\eta)\in WF(u)$ with $(x,\xi;y,\eta)\in R_A$, and therefore $(x,\xi;y,\eta)\in C$. Thus \begin{align*} R_A \circ WF(u) \subset C \circ WF(u). \end{align*} Combining the two inclusions gives \begin{align*} WF(Au) \subset C \circ WF(u). \end{align*}[/guided]

[step:Derive the local microlocal smoothness formulation from the inclusion] Let $(x_0,\xi_0)\in T^*X\setminus 0$, and let $V\subset T^*X\setminus 0$ be an open conic neighbourhood of $(x_0,\xi_0)$ satisfying \begin{align*} V\cap (C\circ WF(u))=\varnothing. \end{align*} Let $P\in\Psi^0(X)$ be properly supported with essential support contained in $V$. By the composition calculus for pseudodifferential operators and Fourier integral operators, the wave front set of $PAu$ is contained in the part of $WF(Au)$ [lying over](/theorems/2876) the essential support of $P$. More precisely, the [[Pseudodifferential Characterization of the Wave Front Set](/theorems/8174)][citetheorem:8174] gives \begin{align*} WF(PAu)\subset WF(Au)\cap \operatorname{ess\,supp}(P). \end{align*} Using the inclusion proved above, \begin{align*} WF(PAu)\subset (C\circ WF(u))\cap V. \end{align*} The right-hand side is empty. Hence \begin{align*} WF(PAu)=\varnothing. \end{align*} A distribution with empty wave front set is smooth, again by the [Pseudodifferential Characterization of the Wave Front Set][citetheorem:8174]. Thus \begin{align*} PAu\in C^\infty(X). \end{align*} If $P$ is chosen elliptic at a covector of $V$, this proves that $Au$ is microlocally smooth at that covector. [/step]

[step:Construct the microlocal inverse in the elliptic canonical graph region]Assume now the elliptic graph hypotheses. Shrink $U_0$ and $V_0$ only within the neighbourhoods allowed in the statement, so that the graph identity \begin{align*} C \cap (V_0 \times U_0)=\{(\kappa(y,\eta);y,\eta):(y,\eta)\in U_0\} \end{align*} holds on the relevant microlocal supports, the branch-isolation condition \begin{align*} C \cap (V_0 \times (WF(u)\setminus U_0))=\varnothing \end{align*} remains valid, and the principal symbol of $A$ is elliptic on the graph over these smaller cones. Choose a conic neighbourhood $U\subset U_0$ of $(y_0,\eta_0)$, then choose a conic neighbourhood $V\subset V_0$ of $(x_0,\xi_0)$, and finally choose an open conic neighbourhood $W\subset V_0$ of $\overline V$ such that \begin{align*} \kappa^{-1}(W)\subset U. \end{align*} Thus every point of $C\cap(W\times U_0)$ has its $Y$-covector component in $U$. The [[Microlocal Parametrix Theorem for Elliptic Fourier Integral Operators](/theorems/8211)][citetheorem:8211] applies to $A$ on this elliptic canonical graph: the canonical relation is the graph of the homogeneous canonical diffeomorphism $\kappa:U_0\to V_0$, $A$ is properly supported, and its principal symbol is elliptic near $(x_0,\xi_0;y_0,\eta_0)$. Therefore there exist properly supported pseudodifferential cutoffs $Q_1,Q_0\in\Psi^0(Y)$ and $P_1,P_0\in\Psi^0(X)$, and an elliptic properly supported Fourier integral operator $B$ of order $-m$ associated with the inverse graph $\kappa^{-1}:V_0\to U_0$, such that $Q_1$ is elliptic on $U$, $P_1$ is elliptic on $V$, $\operatorname{ess\,supp}(P_1)\subset W$, $\operatorname{ess\,supp}(P_0)\subset W$, $Q_0$ is microlocally the identity on a conic neighbourhood of $\kappa^{-1}(W)$, $P_0$ is microlocally the identity on a conic neighbourhood of $W$, the essential supports of $Q_0$ and $P_0$ are contained in $U_0$ and $V_0$, respectively, and \begin{align*} Q_1BP_0AQ_0=Q_1+R \end{align*} microlocally on $U$, where $R$ is smoothing microlocally over $U\times U$. The order $-m$ and the ellipticity of the principal symbol of $B$ are chosen so that the principal symbol of $BP_0AQ_0$ in the graph region is the identity modulo lower order terms; the residual lower order error is removed by the asymptotic symbolic construction in the parametrix theorem. This is precisely the asserted parametrix identity.[/step]

[guided]The graph hypothesis identifies the only branch of $C$ in $V_0\times U_0$ with the map $(y,\eta)\mapsto \kappa(y,\eta)$. We first choose $U\subset U_0$ around $(y_0,\eta_0)$, then choose $V\subset V_0$ around $(x_0,\xi_0)$, and then choose an open conic neighbourhood $W\subset V_0$ of $\overline V$ so small that $\kappa^{-1}(W)\subset U$. This choice is important: if $(x,\xi;y,\eta)\in C\cap(W\times U_0)$, then the graph identity forces $(x,\xi)=\kappa(y,\eta)$, so $(y,\eta)=\kappa^{-1}(x,\xi)\in U$. Thus input covectors in $U_0\setminus U$ cannot reach the output cone $W$, and hence cannot reach the smaller cone $V$, through the graph branch. We can now invoke the [Microlocal Parametrix Theorem for Elliptic Fourier Integral Operators][citetheorem:8211]. Its hypotheses are met because $A$ is properly supported, the canonical relation is a homogeneous canonical graph over $U_0\to V_0$, and the principal symbol of $A$ is elliptic near the graph point $(x_0,\xi_0;y_0,\eta_0)$. The theorem supplies cutoffs $Q_1,Q_0\in\Psi^0(Y)$ and $P_1,P_0\in\Psi^0(X)$ and an elliptic inverse Fourier integral operator $B$ of order $-m$ associated with $\kappa^{-1}:V_0\to U_0$. The cutoff $Q_0$ is chosen microlocally equal to the identity on a conic neighbourhood of $\kappa^{-1}(W)$, not merely near $(y_0,\eta_0)$, because this is the whole input region that can map into the output support cone $W$. The cutoffs $P_0$ and $P_1$ are chosen with essential supports contained in $W$, and $P_0$ is chosen microlocally equal to the identity on a conic neighbourhood of $W$. With these choices the parametrix theorem gives \begin{align*} Q_1BP_0AQ_0=Q_1+R \end{align*} microlocally on $U$, where $R$ is smoothing microlocally over $U\times U$. The inverse order is $-m$ because $B$ must cancel the order $m$ of $A$ in the leading symbolic product. Ellipticity is what permits the leading symbol to be inverted; the remaining lower-order errors are removed by the standard asymptotic symbolic construction contained in the parametrix theorem.[/guided]

[step:Use branch isolation to remove the contribution from input covectors outside $U_0$] Let $I_Y:\mathcal D'(Y)\to\mathcal D'(Y)$ denote the identity operator on distributions on $Y$. Since $Q_0$ is microlocally equal to the identity on a conic neighbourhood of $U_0\cap\kappa^{-1}(V)$, the operator $I_Y-Q_0$ removes all singularities of $u$ in that part of the input cone. Because $\kappa^{-1}(W)\subset U$, every point of $C\cap(W\times U_0)$ has its $Y$-covector component in $\kappa^{-1}(W)$, where $Q_0$ is microlocally equal to the identity. Hence any element of $WF((I_Y-Q_0)u)$ that can map by $C$ into $W$ must lie in $WF(u)\setminus U_0$. By the branch-isolation assumption, \begin{align*} C \cap (V_0 \times (WF(u)\setminus U_0))=\varnothing. \end{align*} Since $\operatorname{ess\,supp}(P_1)\subset W\subset V_0$, the mapping inclusion already proved gives \begin{align*} WF(P_1A(I_Y-Q_0)u)\cap V=\varnothing. \end{align*} Equivalently, \begin{align*} P_1A(I_Y-Q_0)u \end{align*} is smooth microlocally in $V$. [/step]

[step:Prove that an input singularity on the graph produces the corresponding output singularity] We prove the contrapositive. Suppose \begin{align*} (x_0,\xi_0)\notin WF(Au). \end{align*} Before constructing the parametrix, shrink the output cone $V\subset V_0$ and choose the support cone $W\subset V_0$ so that $W\cap WF(Au)=\varnothing$, then carry out the preceding parametrix construction with these choices. Thus the operators $P_0$, $P_1$, $Q_0$, $Q_1$, and $B$ are the same operators appearing in the identity \begin{align*} Q_1BP_0AQ_0=Q_1+R. \end{align*} Since $P_0$ has essential support in $W$ and $W\cap WF(Au)=\varnothing$, the [Pseudodifferential Characterization of the Wave Front Set][citetheorem:8174] implies \begin{align*} P_0Au\in C^\infty(X) \end{align*} microlocally on $V$. Applying the properly supported Fourier integral operator $B$ and then the pseudodifferential cutoff $Q_1$ preserves microlocal smoothness in $U$ by the wave front mapping inclusion already proved for Fourier integral operators. Hence \begin{align*} Q_1BP_0Au \end{align*} is smooth microlocally in $U$. Decompose \begin{align*} u=Q_0u+(I_Y-Q_0)u. \end{align*} The branch-isolation argument applies with any properly supported output cutoff whose essential support is contained in $W$; in particular it applies to $P_0$. Therefore \begin{align*} P_0A(I_Y-Q_0)u \end{align*} is smooth microlocally in $W$, and consequently \begin{align*} Q_1BP_0A(I_Y-Q_0)u \end{align*} is smooth microlocally in $U$. Subtracting this smooth microlocal contribution from $Q_1BP_0Au$, we obtain that \begin{align*} Q_1BP_0AQ_0u \end{align*} is smooth microlocally in $U$. Using the parametrix identity, \begin{align*} Q_1BP_0AQ_0u=(Q_1+R)u \end{align*} microlocally on $U$. The term $Ru$ is smooth microlocally on $U$ because $R$ is smoothing there. Therefore \begin{align*} Q_1u \end{align*} is smooth microlocally on $U$. Since $Q_1$ is elliptic at $(y_0,\eta_0)$, the [[Microlocal Elliptic Regularity Theorem](/theorems/8175)][citetheorem:8175] gives \begin{align*} (y_0,\eta_0)\notin WF(u). \end{align*} Thus \begin{align*} (y_0,\eta_0)\in WF(u) \implies (x_0,\xi_0)\in WF(Au). \end{align*} [/step]

[step:Use the mapping inclusion to prove the reverse implication and conclude the equivalence] Assume \begin{align*} (y_0,\eta_0)\notin WF(u). \end{align*} After shrinking $U\subset U_0$ and $V\subset V_0$ if necessary, we may assume \begin{align*} U\cap WF(u)=\varnothing \end{align*} near $(y_0,\eta_0)$. Choose the support cone $W\subset V_0$ with $V\subset W$ and $\kappa^{-1}(W)\subset U$. If $(x,\xi)\in V\cap(C\circ WF(u))$, then there is $(y,\eta)\in WF(u)$ with $(x,\xi;y,\eta)\in C$. The branch-isolation assumption rules out $(y,\eta)\in WF(u)\setminus U_0$, while the graph identity on $V_0\times U_0$ and the inclusion $V\subset W$ force $(y,\eta)=\kappa^{-1}(x,\xi)\in\kappa^{-1}(W)\subset U$ for any remaining possibility. Since there are no such input covectors in $WF(u)$, we have \begin{align*} V\cap (C\circ WF(u))=\varnothing. \end{align*} The local microlocal smoothness formulation proved above then gives that $Au$ is microlocally smooth in $V$. In particular, \begin{align*} (x_0,\xi_0)\notin WF(Au). \end{align*} Taking the contrapositive gives \begin{align*} (x_0,\xi_0)\in WF(Au) \implies (y_0,\eta_0)\in WF(u). \end{align*} Together with the implication proved in the previous step, this yields \begin{align*} (y_0,\eta_0)\in WF(u) \quad \Longleftrightarrow \quad (x_0,\xi_0)\in WF(Au). \end{align*} This completes the proof. [/step]