[proofplan] The construction is local in the $X$ variable and proper support supplies the compact part of $Y$ on which the kernel can see a fixed [test function](/page/Test%20Function). This gives the cutoff, proves cutoff independence, and reduces continuity to the ordinary continuity of a compactly supported distribution acting on test functions. For the wave front estimate, we localize the kernel by the smooth factor $\chi f$ in the $Y$ variable and identify $Af$ over $X_0$ with the pushforward of this localized distribution under $p_X$. The pushforward wave front estimate then says that only covectors annihilating the $Y$ fibres can survive; since a conormal distribution has wave front set contained in $N^*S\setminus 0$, the displayed inclusion follows. [/proofplan]

[step:Use proper support to choose the cutoff seen by a test function] Let $f \in C^\infty(Y)$ and let $\varphi \in C_c^\infty(X)$. Define the compact set \begin{align*} C_\varphi := \operatorname{supp}\varphi \subset X. \end{align*} By the proper support hypothesis, the set \begin{align*} L_\varphi := p_Y\bigl(\operatorname{supp}K \cap (C_\varphi \times Y)\bigr) \end{align*} is compact in $Y$. Since $Y$ is a smooth manifold, it is locally compact and admits smooth compactly supported cutoffs. Hence there exists $\chi \in C_c^\infty(Y)$ such that $\chi = 1$ on an open neighbourhood of $L_\varphi$. The function \begin{align*} \Phi_{\varphi,\chi,f}:X\times Y&\to \mathbb C \end{align*} \begin{align*} (x,y)&\mapsto \varphi(x)\chi(y)f(y) \end{align*} belongs to $C_c^\infty(X\times Y)$, because $\operatorname{supp}\varphi$ and $\operatorname{supp}\chi$ are compact. Therefore the value \begin{align*} K(\Phi_{\varphi,\chi,f}) \end{align*} is defined by the distributional action of $K$ on compactly supported smooth test densities, using the fixed product density on $X\times Y$. [/step]

[step:Prove that the definition does not depend on the cutoff]Let $\chi_1,\chi_2 \in C_c^\infty(Y)$ be two cutoffs equal to $1$ on open neighbourhoods of $L_\varphi$. Define \begin{align*} \psi:X\times Y&\to \mathbb C \end{align*} \begin{align*} (x,y)&\mapsto \varphi(x)(\chi_1(y)-\chi_2(y))f(y). \end{align*} Then $\psi \in C_c^\infty(X\times Y)$. We claim that $\psi$ vanishes on an open neighbourhood of $\operatorname{supp}K$. Indeed, if $(x,y)\in \operatorname{supp}K$ and $x\in C_\varphi$, then $y\in L_\varphi$, so $\chi_1(y)-\chi_2(y)=0$ on a neighbourhood of $y$. If $x\notin C_\varphi$, then $\varphi$ vanishes on an open neighbourhood of $x$. Thus every point of $\operatorname{supp}K$ has a product neighbourhood on which $\psi=0$. Since a distribution acts only on the germ of the test function along its support, this gives \begin{align*} K(\varphi\otimes \chi_1 f)-K(\varphi\otimes \chi_2 f) =K(\psi) =0. \end{align*} Therefore $Af(\varphi)$ is independent of the cutoff.[/step]

[guided]The only issue is whether different choices of $\chi$ can change the value of $K(\varphi\otimes \chi f)$. Let $\chi_1,\chi_2 \in C_c^\infty(Y)$ be two admissible cutoffs. We compare their contributions by defining the compactly supported smooth function \begin{align*} \psi:X\times Y&\to \mathbb C \end{align*} \begin{align*} (x,y)&\mapsto \varphi(x)(\chi_1(y)-\chi_2(y))f(y). \end{align*} We need to prove that $K(\psi)=0$. A distribution $K$ vanishes on every test function whose support is disjoint from $\operatorname{supp}K$; equivalently, it suffices to show that $\psi$ vanishes on an open neighbourhood of $\operatorname{supp}K$. Let $(x,y)\in \operatorname{supp}K$. If $x\notin \operatorname{supp}\varphi$, then $\varphi$ vanishes in some open neighbourhood of $x$, so $\psi$ vanishes near $(x,y)$. If $x\in \operatorname{supp}\varphi$, then by definition of \begin{align*} L_\varphi := p_Y\bigl(\operatorname{supp}K \cap (\operatorname{supp}\varphi \times Y)\bigr), \end{align*} we have $y\in L_\varphi$. Both cutoffs are equal to $1$ on neighbourhoods of $L_\varphi$, so $\chi_1-\chi_2$ vanishes near $y$, and again $\psi$ vanishes near $(x,y)$. Thus $\psi$ vanishes near every point of $\operatorname{supp}K$. Hence \begin{align*} K(\psi)=0. \end{align*} Substituting the definition of $\psi$ gives \begin{align*} K(\varphi\otimes \chi_1 f)=K(\varphi\otimes \chi_2 f). \end{align*} So the value $Af(\varphi)$ depends only on $f$ and $\varphi$, not on the auxiliary cutoff.[/guided]

[step:Verify that $A$ is a continuous linear map into distributions] Linearity in $f$ follows from linearity of multiplication by $\chi$ and linearity of the distribution $K$. We prove continuity. Let $C\subset X$ be compact, and let $B\subset C_c^\infty(X)$ be a bounded set with $\operatorname{supp}\varphi\subset C$ for every $\varphi\in B$. Define \begin{align*} L_C := p_Y\bigl(\operatorname{supp}K \cap (C\times Y)\bigr). \end{align*} By proper support, $L_C$ is compact. Choose $\chi_C\in C_c^\infty(Y)$ such that $\chi_C=1$ on an open neighbourhood of $L_C$. For every $\varphi\in B$ and every $f\in C^\infty(Y)$, cutoff independence gives \begin{align*} Af(\varphi)=K(\varphi\otimes \chi_C f). \end{align*} Let \begin{align*} M_C:=C\times \operatorname{supp}\chi_C\subset X\times Y. \end{align*} This set is compact. Since $K$ is a distribution, its restriction to test functions supported in $M_C$ is continuous. Therefore there exist an integer $r\in \mathbb N_0$ and a constant $C_K>0$ such that for every $\Psi\in C_c^\infty(X\times Y)$ with $\operatorname{supp}\Psi\subset M_C$, \begin{align*} |K(\Psi)| \le C_K\sum_{|\alpha|+|\beta|\le r} \sup_{(x,y)\in M_C}|D_x^\alpha D_y^\beta \Psi(x,y)| \end{align*} in any finite collection of coordinate charts covering $M_C$, with the usual [partition of unity](/page/Partition%20of%20Unity) interpretation of this seminorm estimate. Applying this estimate to $\Psi=\varphi\otimes \chi_C f$, the Leibniz rule gives constants $C_B>0$ and $C_{\chi_C}>0$, depending on finitely many seminorms of the bounded set $B$ and on finitely many derivatives of $\chi_C$, such that \begin{align*} |Af(\varphi)| \le C_K C_B C_{\chi_C} \sum_{|\beta|\le r} \sup_{y\in \operatorname{supp}\chi_C}|D_y^\beta f(y)|. \end{align*} The right-hand side is a continuous seminorm of $f$ in the Fréchet topology of $C^\infty(Y)$, uniformly for $\varphi\in B$. Hence $f\mapsto Af$ is continuous as a map \begin{align*} C^\infty(Y)\to \mathcal D'(X). \end{align*} [/step]

[step:Represent the localized operator as a pushforward] Let $X_0\subset X$ be compact, and choose $\chi\in C_c^\infty(Y)$ equal to $1$ on an open neighbourhood of \begin{align*} p_Y\bigl(\operatorname{supp}K\cap (X_0\times Y)\bigr). \end{align*} Fix $f\in C^\infty(Y)$ and define the smooth compactly supported function \begin{align*} g:Y&\to \mathbb C \end{align*} \begin{align*} y&\mapsto \chi(y)f(y). \end{align*} Let $M_g:X\times Y\to \mathbb C$ be the smooth function \begin{align*} M_g(x,y):=g(y). \end{align*} Define the localized distributional density \begin{align*} K_g:=M_g K\in \mathcal D'(X\times Y). \end{align*} Multiplication of distributions by smooth functions is defined by \begin{align*} K_g(\Psi):=K(M_g\Psi) \end{align*} for every $\Psi\in C_c^\infty(X\times Y)$. For every $\varphi\in C_c^\infty(X)$ with $\operatorname{supp}\varphi\subset X_0$, cutoff independence gives \begin{align*} Af(\varphi)=K(\varphi\otimes g). \end{align*} This is precisely the distributional pushforward of $K_g$ by $p_X$, because \begin{align*} (p_X)_*K_g(\varphi) =K_g(\varphi\circ p_X) =K((\varphi\circ p_X)M_g) =K(\varphi\otimes g). \end{align*} Thus, over $X_0$, \begin{align*} Af=(p_X)_*K_g. \end{align*} The pushforward is well-defined on this localized region because \begin{align*} \operatorname{supp}K_g\cap (X_0\times Y) \subset \operatorname{supp}K\cap (X_0\times \operatorname{supp}g), \end{align*} and $\operatorname{supp}g\subset \operatorname{supp}\chi$ is compact. [/step]

[step:Apply the pushforward wave front estimate] The projection \begin{align*} p_X:X\times Y\to X \end{align*} is a smooth submersion. The pushforward wave front estimate for properly supported submersions, applied to $p_X$ and the distributional density $K_g$, gives \begin{align*} \operatorname{WF}((p_X)_*K_g)\cap T^*X_0 \subset \{(x,\xi)\in T^*X_0\setminus 0:\text{ there exists }y\in Y\text{ with }(x,y;\xi,0)\in \operatorname{WF}(K_g)\}. \end{align*} This is the special case of [citetheorem:8182] for the coordinate projection $p_X$, whose cotangent pullback sends $\xi\in T_x^*X$ to $(\xi,0)\in T_{(x,y)}^*(X\times Y)$. By [microlocal stability under smooth multiplication](/theorems/8171), [citetheorem:8171], \begin{align*} \operatorname{WF}(K_g)\subset \operatorname{WF}(K)\cap \operatorname{supp}K_g. \end{align*} Since $K$ is conormal to $S$, the wave front inclusion for conormal distributions gives \begin{align*} \operatorname{WF}(K)\subset N^*S\setminus 0. \end{align*} This is the defining wave front property of conormal distributions, equivalently the local conormal wave front inclusion proved in [citetheorem:8185]. Also, \begin{align*} \operatorname{supp}K_g\subset X\times \operatorname{supp}g = X\times \operatorname{supp}(\chi f). \end{align*} Combining these inclusions yields \begin{align*} \operatorname{WF}(Af)\cap T^*X_0 \subset \{(x,\xi)\in T^*X_0\setminus 0:\text{ there exists }y\in \operatorname{supp}(\chi f)\text{ with }(x,y;\xi,0)\in N^*S\setminus 0\}. \end{align*} This is the asserted wave front estimate. [/step]

[step:Identify the equivalent geometric description] The last displayed set is exactly the image under the projection \begin{align*} T^*X\times T^*Y&\to T^*X \end{align*} \begin{align*} (x,\xi;y,\eta)&\mapsto (x,\xi) \end{align*} of the set \begin{align*} (N^*S\setminus 0)\cap \{(x,y;\xi,\eta):\eta=0,\ y\in \operatorname{supp}(\chi f)\}. \end{align*} Thus the only output covectors allowed over $X_0$ are those obtained from conormal covectors to $S$ whose $Y$ component vanishes. This proves both the displayed inclusion and its equivalent formulation, and completes the proof. [/step]