[proofplan]
We take a point $x \in \operatorname{sing\,supp}(u)\cap K$ and choose a nonzero covector $q$ over $x$ in $WF(u)$. If $q$ is elliptic for $P$, microlocal elliptic regularity forces $q \in WF(Pu)$, so the base point lies in $S_K$. If $q$ is characteristic, then either $q$ itself lies in $WF(Pu)$ or we trace the oriented null bicharacteristic through $q$ backward as long as it remains over $K$ and avoids $WF(Pu)$. The backward trace either meets a source singularity of $Pu$, reaches the boundary of $K$, or remains over $K$ and avoids $WF(Pu)$ for its whole backward lifetime, giving membership in $F_K$, $E_K$, or $T_K$, respectively.
[/proofplan]
[step:Choose a wave front covector over the singular base point]
Let $x \in \operatorname{sing\,supp}(u)\cap K$. The theorem statement declares $WF(v)\subset T^*X\setminus 0$ for each distribution $v\in\mathcal{D}'(X)$. By the characterization of singular support as the projection of the wave front set, there exists a nonzero covector $q \in T_x^*X \setminus 0$ such that $q \in WF(u)$.
Here and below we use the standard microlocal identity
\begin{align*}
\operatorname{sing\,supp}(u)=\pi(WF(u)).
\end{align*}
(citing a result not yet verified in the wiki: singular support is the projection of the wave front set)
Since $x \in K$, the covector $q$ belongs to $T^*K$.
[/step]
[step:Put non-characteristic covectors into the source set $S_K$]
Assume first that $q \notin \operatorname{Char}(P)$. Then $p(q)\neq 0$, so, since $p$ is continuous and homogeneous, $P$ is microlocally elliptic on a conic neighbourhood of $q$. Proper support of $P$ ensures that $Pu\in\mathcal{D}'(X)$ is defined for every $u\in\mathcal{D}'(X)$. Microlocal elliptic regularity, applied contrapositively at $q$, gives
\begin{align*}
q \in WF(u) \implies q \in WF(Pu).
\end{align*}
(citing a result not yet verified in the wiki: [microlocal elliptic regularity for pseudodifferential operators](/theorems/8163))
Because $q \in T^*K$, we have $q \in WF(Pu)\cap T^*K$, and therefore
\begin{align*}
x=\pi(q)\in \pi\bigl(WF(Pu)\cap T^*K\bigr)=S_K.
\end{align*}
Thus the desired containment holds in the non-characteristic case.
[guided]
We first separate the elliptic case from the characteristic case. The reason is that away from $\operatorname{Char}(P)$, the operator $P$ detects exactly the microlocal singularities of $u$: if $P$ is elliptic at a covector and $Pu$ is microlocally smooth there, then $u$ must also be microlocally smooth there.
Here $q \notin \operatorname{Char}(P)$ means precisely that $p(q)\neq 0$. Since $p$ is continuous and homogeneous in the cotangent variable, there is a conic neighbourhood of $q$ on which $p$ does not vanish; this is exactly microlocal ellipticity of $P$ near $q$. Proper support of $P$ ensures that $Pu\in\mathcal{D}'(X)$ is defined. By microlocal elliptic regularity for pseudodifferential operators, applied contrapositively at $q$,
\begin{align*}
q \in WF(u) \implies q \in WF(Pu).
\end{align*}
(citing a result not yet verified in the wiki: microlocal elliptic regularity for pseudodifferential operators)
We already know that $q \in T^*K$, because $\pi(q)=x$ and $x\in K$. Hence
\begin{align*}
q \in WF(Pu)\cap T^*K.
\end{align*}
Applying the projection $\pi:T^*X\setminus 0\to X$ gives
\begin{align*}
x=\pi(q)\in \pi\bigl(WF(Pu)\cap T^*K\bigr)=S_K.
\end{align*}
This proves the theorem for any singular base point whose chosen wave front covector is non-characteristic.
[/guided]
[/step]
[step:Handle characteristic covectors that already lie in $WF(Pu)$]
It remains to consider the case $q \in \operatorname{Char}(P)$. If $q \in WF(Pu)$, then, since $q \in T^*K$,
\begin{align*}
x=\pi(q)\in \pi\bigl(WF(Pu)\cap T^*K\bigr)=S_K.
\end{align*}
Equivalently, the same point is also covered by $F_K$: take $t_s=0$, so that $\gamma_q(t_s)=\gamma_q(0)=q \in WF(Pu)\cap T^*K$ and $\gamma_q([0,0])=\{q\}\subset T^*K$.
[/step]
[step:Trace the backward bicharacteristic while it stays inside $K$ and avoids $WF(Pu)$]
Assume now that
\begin{align*}
q \in \operatorname{Char}(P)\cap T^*K
\end{align*}
and
\begin{align*}
q\notin WF(Pu).
\end{align*}
Let
\begin{align*}
J_q:=I_q\cap(-\infty,0]
\end{align*}
denote the backward time interval of the maximal null bicharacteristic through $q$. Define the backward source-time set
\begin{align*}
A_q:=\{t\in J_q:\gamma_q(t)\in WF(Pu)\cap T^*K\text{ and }\gamma_q([t,0])\subset T^*K\}.
\end{align*}
If $A_q\neq\varnothing$, choose any $t_s\in A_q$. Then $t_s\le 0$, $\gamma_q(t_s)\in WF(Pu)\cap T^*K$, and $\gamma_q([t_s,0])\subset T^*K$. Thus $q$ belongs to the covector set defining $F_K$, and consequently
\begin{align*}
x=\pi(q)\in F_K.
\end{align*}
The preceding classification uses only the maximal integral curve $\gamma_q:I_q\to\operatorname{Char}(P)$ declared in the theorem statement. The hypotheses that $P$ is classical, properly supported, and of real principal type are the microlocal assumptions under which these oriented null bicharacteristics are the propagation curves for singularities.
[/step]
[step:Classify backward traces that meet the boundary before meeting a source]
Suppose $A_q=\varnothing$. Define the backward interior-time set
\begin{align*}
B_q:=\{t\in J_q:\pi(\gamma_q(s))\in K\text{ for every }s\in[t,0]\}.
\end{align*}
The set $B_q$ is an interval containing $0$, because $\pi(q)=x\in K$ and the map
\begin{align*}
\pi\circ\gamma_q:I_q\to X
\end{align*}
is continuous. If there exists $t_b\in J_q$ with $t_b<0$ such that
\begin{align*}
\pi(\gamma_q(t_b))\in \partial K
\end{align*}
and
\begin{align*}
\pi(\gamma_q(t))\in K
\end{align*}
for every $t\in(t_b,0]$, then the assumption $A_q=\varnothing$ implies
\begin{align*}
\gamma_q(t)\notin WF(Pu)\cap T^*K
\end{align*}
for every $t\in(t_b,0]$. Therefore $q$ belongs to the covector set defining $E_K$, and
\begin{align*}
x=\pi(q)\in E_K.
\end{align*}
[guided]
At this stage the backward bicharacteristic has not produced a source point of $WF(Pu)$ inside $T^*K$ that can be connected to $q$ while staying over $K$. We now ask what can stop the backward trace from remaining an entirely interior curve over $K$.
The base projection of the bicharacteristic is the continuous map
\begin{align*}
\pi\circ\gamma_q:I_q\to X.
\end{align*}
Since $\pi(q)=x\in K$ and $K$ is open, the curve is inside $K$ for all sufficiently small negative times. If, moving backward, the base curve first leaves the [open set](/page/Open%20Set) $K$, continuity forces the exit point to lie on the boundary $\partial K$. Thus a boundary exit has the form: there is a time $t_b\in I_q\cap(-\infty,0)$ such that
\begin{align*}
\pi(\gamma_q(t_b))\in \partial K
\end{align*}
and
\begin{align*}
\pi(\gamma_q(t))\in K
\end{align*}
for every $t\in(t_b,0]$.
We are also assuming that the source-time set $A_q$ is empty. This means there is no time $t\le 0$ such that $\gamma_q(t)\in WF(Pu)\cap T^*K$ and the segment from $t$ to $0$ remains in $T^*K$. In particular, along the interior segment $(t_b,0]$, every point $\gamma_q(t)$ lies in $T^*K$, so no such point can lie in $WF(Pu)\cap T^*K$. Hence
\begin{align*}
\gamma_q(t)\notin WF(Pu)\cap T^*K
\end{align*}
for every $t\in(t_b,0]$.
The defining conditions of $E_K$ are now exactly satisfied by the same covector $q$: it is characteristic, it lies over $K$, its backward bicharacteristic reaches the boundary at time $t_b$, the base projection stays inside $K$ for all later times up to $0$, and the open interior segment contains no source point of $WF(Pu)$. Therefore
\begin{align*}
x=\pi(q)\in E_K.
\end{align*}
[/guided]
[/step]
[step:Put the remaining backward lifetime into the terminal set $T_K$]
We are left with the case in which $A_q=\varnothing$ and no boundary time $t_b<0$ as in the preceding step exists. The backward exit alternative assumed in the theorem statement applies to this $q$, because $q\in\operatorname{Char}(P)\cap T^*K$, $q\notin WF(Pu)$, and $A_q=\varnothing$. Since the boundary alternative is absent, that hypothesis gives
\begin{align*}
\gamma_q(t)\in T^*K
\end{align*}
for every $t\in J_q$.
Since $A_q=\varnothing$ and $\gamma_q([t,0])\subset T^*K$ for every $t\in J_q$, no point $\gamma_q(t)$ with $t\in J_q$ can belong to $WF(Pu)$. Therefore
\begin{align*}
\gamma_q(t)\in T^*K\setminus WF(Pu)
\end{align*}
for every $t\in I_q\cap(-\infty,0]$.
Thus $q$ belongs to the covector set defining $T_K$, and hence
\begin{align*}
x=\pi(q)\in T_K.
\end{align*}
[/step]
[step:Project the covector alternatives to obtain the asserted containment]
For the arbitrary point $x\in \operatorname{sing\,supp}(u)\cap K$, we selected a particular covector $q\in WF(u)\cap T_x^*X$. The preceding steps show that this covector forces exactly one of the following projected conclusions:
\begin{align*}
x\in S_K,\qquad x\in F_K,\qquad x\in E_K,\qquad x\in T_K.
\end{align*}
Therefore
\begin{align*}
x\in S_K\cup F_K\cup E_K\cup T_K.
\end{align*}
Since $x\in \operatorname{sing\,supp}(u)\cap K$ was arbitrary, we obtain
\begin{align*}
\operatorname{sing\,supp}(u)\cap K\subset S_K\cup F_K\cup E_K\cup T_K.
\end{align*}
The proof uses only the chosen covector over $x$; it does not assert that all covectors over the same base point satisfy the same alternative.
[/step]
