[proofplan] We first construct the action of $P$ on distributions by duality, using proper support to ensure that the transpose sends test functions to test functions continuously. To prove pseudolocality, we fix a point $x_0$ where $u$ is smooth, localize $u$ into a smooth near-field piece and a far-field piece supported away from $x_0$, and treat the two terms separately. The near-field term is smooth after applying $P$ by the standard smooth mapping property of pseudodifferential operators, while the far-field term is smooth near $x_0$ because the kernel of $P$ is smooth off the diagonal. Since every point outside $\operatorname{sing\,supp}u$ is also outside $\operatorname{sing\,supp}(Pu)$, the desired inclusion follows. [/proofplan] [step:Extend the properly supported operator to distributions by transposition] Let \begin{align*} P^t:C_c^\infty(U) \to C_c^\infty(U) \end{align*} denote the formal transpose of $P$. Since $P$ is properly supported, $P^t$ is again properly supported; hence it maps compactly supported smooth functions to compactly supported smooth functions continuously. This is the standard continuous [extension theorem](/theorems/59) for properly supported pseudodifferential operators on distributions, cited here as a result not yet in the wiki: Continuous extension of properly supported pseudodifferential operators to distributions. For $u \in \mathcal{D}'(U)$, define \begin{align*} Pu:\mathcal{D}(U) \to \mathbb{C} \end{align*} by \begin{align*} (Pu)(\varphi) := u(P^t\varphi) \end{align*} for every [test function](/page/Test%20Function) $\varphi \in \mathcal{D}(U)=C_c^\infty(U)$. Because $P^t:\mathcal{D}(U)\to \mathcal{D}(U)$ is continuous and $u:\mathcal{D}(U)\to \mathbb{C}$ is continuous, the composition $\varphi \mapsto u(P^t\varphi)$ is a distribution. Thus $P:\mathcal{D}'(U)\to \mathcal{D}'(U)$ is well defined and continuous by the continuity of composition in the test-function topology. On test functions this definition agrees with the original operator by the defining property of the formal transpose. [/step] [step:Localize the distribution into a smooth part and an exterior part] Fix $u \in \mathcal{D}'(U)$ and choose a point \begin{align*} x_0 \in U \setminus \operatorname{sing\,supp}u. \end{align*} By the definition of singular support, there exist an open neighbourhood $O \subset U$ of $x_0$ and a smooth function \begin{align*} f:O \to \mathbb{C} \end{align*} such that $u|_{\mathcal{D}'(O)}$ equals the [regular distribution](/page/Regular%20Distribution) induced by $f$. Choose open sets $V_0,V_1 \subset U$ with \begin{align*} x_0 \in V_0,\qquad \overline{V_0}\subset V_1,\qquad \overline{V_1}\subset O, \end{align*} and choose a cutoff function \begin{align*} \psi:U \to \mathbb{R} \end{align*} with $\psi \in C_c^\infty(O)$ and $\psi=1$ on $V_1$. Define distributions \begin{align*} u_{\mathrm{near}} := \psi u,\qquad u_{\mathrm{far}} := (1-\psi)u. \end{align*} Then \begin{align*} u = u_{\mathrm{near}} + u_{\mathrm{far}} \end{align*} in $\mathcal{D}'(U)$. Moreover $u_{\mathrm{near}}$ is represented by the compactly supported smooth function $\psi f \in C_c^\infty(O)$, extended by $0$ to a function in $C_c^\infty(U)$, and \begin{align*} \operatorname{supp}u_{\mathrm{far}} \cap V_1 = \varnothing. \end{align*} [/step] [step:Apply the smooth mapping property to the localized smooth term] Since $u_{\mathrm{near}}\in C_c^\infty(U)$ and $P\in \Psi^m_{1,0}(U)$, the standard smooth mapping property of pseudodifferential operators gives \begin{align*} P u_{\mathrm{near}} \in C^\infty(U). \end{align*} This invokes the standard result, cited here as a result not yet in the wiki: Pseudodifferential operators map smooth functions to smooth functions. Therefore $P u_{\mathrm{near}}$ is smooth on a neighbourhood of $x_0$. [/step] [step:Use off-diagonal smoothness of the kernel for the exterior term] Choose an [open set](/page/Open%20Set) $V \subset U$ with \begin{align*} x_0 \in V,\qquad \overline{V}\subset V_0. \end{align*} Let \begin{align*} \chi:U \to \mathbb{R} \end{align*} be any function in $C_c^\infty(V)$. Since $\operatorname{supp}\chi \subset V$ and $\operatorname{supp}u_{\mathrm{far}}\cap V_1=\varnothing$, while $\overline{V}\subset V_0\subset \overline{V_0}\subset V_1$, the compact set $\operatorname{supp}\chi$ is separated from $\operatorname{supp}u_{\mathrm{far}}$. Hence \begin{align*} (\operatorname{supp}\chi \times \operatorname{supp}u_{\mathrm{far}})\cap \{(x,x):x\in U\}=\varnothing. \end{align*} The Schwartz kernel $K_P$ of a pseudodifferential operator is smooth off the diagonal, cited here as a result not yet in the wiki: Schwartz kernel of a pseudodifferential operator is smooth off the diagonal. Therefore the localized kernel \begin{align*} K_\chi := \chi(x)K_P(x,y)(1-\psi(y)) \end{align*} is smooth on the relevant part of $U\times U$. Proper support of $P$ ensures that, for the compact set $\operatorname{supp}\chi$, only a compact subset of the $y$-variable can contribute. Thus the operator with kernel $K_\chi$ is a smoothing operator from distributions to smooth functions near $\operatorname{supp}\chi$. By the smoothing-kernel theorem for distributions, cited here as a result not yet in the wiki: Smoothing kernels map distributions to smooth functions locally, we obtain \begin{align*} \chi P u_{\mathrm{far}} \in C_c^\infty(V). \end{align*} [guided] We now prove carefully why the part of $u$ supported away from $x_0$ cannot create a singularity at $x_0$. Choose an open set $V\subset U$ such that $x_0\in V$ and $\overline{V}\subset V_0$. Then every test cutoff supported in $V$ is supported strictly inside the region where $\psi=1$. Let \begin{align*} \chi:U\to \mathbb{R} \end{align*} be a test function with $\chi\in C_c^\infty(V)$. Since $\psi=1$ on $V_1$ and $\overline{V}\subset V_1$, the distribution \begin{align*} u_{\mathrm{far}}=(1-\psi)u \end{align*} has support disjoint from $V_1$. In particular, the $x$-support of $\chi$ and the $y$-support of $u_{\mathrm{far}}$ cannot meet on the diagonal: \begin{align*} (\operatorname{supp}\chi \times \operatorname{supp}u_{\mathrm{far}})\cap \{(x,x):x\in U\}=\varnothing. \end{align*} This separation is the key point. A pseudodifferential kernel may be singular on the diagonal, but it is smooth away from the diagonal. We use the standard off-diagonal kernel theorem for pseudodifferential operators, cited here as a result not yet in the wiki: Schwartz kernel of a pseudodifferential operator is smooth off the diagonal. Applying it to $K_P$, the kernel of $P$, shows that after multiplying by $\chi(x)$ and by $(1-\psi(y))$, the localized kernel \begin{align*} K_\chi := \chi(x)K_P(x,y)(1-\psi(y)) \end{align*} is smooth on the part of $U\times U$ where it is used. There remains one support issue: $u_{\mathrm{far}}$ need not be compactly supported. This is exactly where proper support is used. Proper support of $P$ means that the projection of $\operatorname{supp}K_P\cap(\operatorname{supp}\chi\times U)$ to the $y$-factor is compact whenever $\operatorname{supp}\chi$ is compact. Thus, when testing near $\operatorname{supp}\chi$, the kernel interacts with $u_{\mathrm{far}}$ only on a compact subset of $U$. A smooth kernel with this compact interaction property defines a smoothing operator on distributions. Therefore, by the standard smoothing-kernel theorem for distributions, cited here as a result not yet in the wiki: Smoothing kernels map distributions to smooth functions locally, the localized distribution \begin{align*} \chi P u_{\mathrm{far}} \end{align*} is represented by a smooth compactly supported function on $V$. Hence $P u_{\mathrm{far}}$ is smooth on $V$. [/guided] Because $\chi\in C_c^\infty(V)$ was arbitrary, the distribution $P u_{\mathrm{far}}$ is smooth on $V$. [/step] [step:Conclude that no new singularity appears at the chosen point] By linearity of the extended operator, \begin{align*} Pu = P u_{\mathrm{near}} + P u_{\mathrm{far}}. \end{align*} The first term is smooth on $U$, and the second term is smooth on the neighbourhood $V$ of $x_0$. Hence $Pu$ is smooth on $V$, so \begin{align*} x_0 \notin \operatorname{sing\,supp}(Pu). \end{align*} Since $x_0$ was an arbitrary point of $U\setminus \operatorname{sing\,supp}u$, we have \begin{align*} U\setminus \operatorname{sing\,supp}u \subseteq U\setminus \operatorname{sing\,supp}(Pu). \end{align*} Taking complements in $U$ gives \begin{align*} \operatorname{sing\,supp}(Pu)\subseteq \operatorname{sing\,supp}u. \end{align*} This proves the pseudolocality theorem. [/step]