[proofplan]
We prove the equivalent neighbourhood formulation and then take complements. If $u$ is microlocally smooth at a covector, an elliptic pseudodifferential cutoff sends $u$ to a smooth function, hence to every local [Sobolev space](/page/Sobolev%20Space), so a smaller conic neighbourhood avoids all Sobolev wave front sets. Conversely, if one conic neighbourhood avoids every $WF^s(u)$, we choose a compactly microlocalized elliptic cutoff near the covector and prove that its application to $u$ lies in $H^N_{\mathrm{loc}}$ for every integer $N$. A finite microlocal [partition of unity](/page/Partition%20of%20Unity) over the cutoff's compact cosphere support reduces this to the defining absence from $WF^N(u)$; the local Sobolev characterization of smoothness then gives microlocal smoothness.
[/proofplan]
[step:Show microlocal smoothness gives one conic neighbourhood avoiding every Sobolev wave front set]
Fix $(x_0,\xi_0)\in T^*X\setminus 0$ and suppose $(x_0,\xi_0)\notin WF(u)$. By the smooth wave front set elliptic cutoff characterization, there exist an open conic neighbourhood $U\subset T^*X\setminus 0$ of $(x_0,\xi_0)$ and a properly supported operator
\begin{align*}
A:\mathcal{D}'(X)\to \mathcal{D}'(X)
\end{align*}
with $A\in \Psi^0_{\mathrm{prop}}(X)$, whose principal symbol is elliptic on $U$, such that $Au\in C^\infty(X)$. Here we use the standard elliptic cutoff characterization of $WF(u)$ (citing a result not yet in the wiki: smooth wave front set via elliptic pseudodifferential cutoffs).
Choose an open conic neighbourhood $V\subset U$ of $(x_0,\xi_0)$ on which the same principal symbol remains elliptic. Since $Au\in C^\infty(X)$, the local Sobolev characterization of smooth functions gives
\begin{align*}
Au\in H^s_{\mathrm{loc}}(X)
\end{align*}
for every $s\in\mathbb R$ (citing a result not yet in the wiki: smooth functions are locally in every Sobolev space). By the elliptic cutoff characterization of the Sobolev wave front set $WF^s(u)$, the ellipticity of $A$ on $V$ and the inclusion $Au\in H^s_{\mathrm{loc}}(X)$ imply
\begin{align*}
V\cap WF^s(u)=\varnothing
\end{align*}
for every $s\in\mathbb R$ (citing a result not yet in the wiki: Sobolev wave front set via elliptic pseudodifferential cutoffs). Thus microlocal smoothness gives a single conic neighbourhood avoiding all Sobolev wave front sets.
[guided]
Fix a covector $(x_0,\xi_0)\in T^*X\setminus 0$ and assume that $(x_0,\xi_0)\notin WF(u)$. The definition of the smooth wave front set is microlocal: it says that there is a pseudodifferential operator which is elliptic near the covector and which regularizes $u$ to a smooth function. More precisely, by the smooth wave front set elliptic cutoff characterization, there are an open conic neighbourhood $U\subset T^*X\setminus 0$ of $(x_0,\xi_0)$ and a properly supported order-zero pseudodifferential operator
\begin{align*}
A:\mathcal{D}'(X)\to \mathcal{D}'(X)
\end{align*}
with $A\in\Psi^0_{\mathrm{prop}}(X)$ such that the principal symbol of $A$ is elliptic on $U$ and
\begin{align*}
Au\in C^\infty(X).
\end{align*}
This invocation is the standard elliptic cutoff characterization of $WF(u)$ (citing a result not yet in the wiki: smooth wave front set via elliptic pseudodifferential cutoffs).
Now choose an open conic neighbourhood $V\subset U$ of $(x_0,\xi_0)$. Since ellipticity is an open condition on the principal symbol away from the zero section, the principal symbol of $A$ is still elliptic on $V$. The point of using the same operator $A$ is that it gives a single neighbourhood that will work for every Sobolev order.
Because $Au$ is smooth, it has local Sobolev regularity of every real order:
\begin{align*}
Au\in H^s_{\mathrm{loc}}(X)
\end{align*}
for each $s\in\mathbb R$.
This is the standard local Sobolev characterization of smoothness, or equivalently the fact that smooth functions lie locally in every Sobolev space (citing a result not yet in the wiki: smooth functions are locally in every Sobolev space).
Finally fix any $s\in\mathbb R$. The Sobolev wave front set $WF^s(u)$ is defined by failure of microlocal $H^s$ regularity. Since $A$ is elliptic on $V$ and $Au\in H^s_{\mathrm{loc}}(X)$, the elliptic cutoff characterization of $WF^s(u)$ gives
\begin{align*}
V\cap WF^s(u)=\varnothing.
\end{align*}
Because the same argument applies to every real $s$, the same conic neighbourhood $V$ avoids all $WF^s(u)$. This proves the forward implication in the neighbourhood formulation.
[/guided]
[/step]
[step:Choose a compactly microlocalized elliptic cutoff inside the uniform Sobolev regularity region]
Conversely, suppose there is an open conic neighbourhood $V\subset T^*X\setminus 0$ of $(x_0,\xi_0)$ such that
\begin{align*}
V\cap WF^s(u)=\varnothing
\end{align*}
for every $s\in\mathbb R$.
Choose an open neighbourhood $O\subset X$ of $x_0$ whose closure is compact and contained in a coordinate chart. Since $V$ is open and conic, after shrinking $O$ and the angular variable in $S^*X$, choose an open conic neighbourhood $V_0\subset V$ of $(x_0,\xi_0)$ such that
\begin{align*}
\overline{\pi_S(V_0\cap T^*O)}\subset \pi_S(V)
\end{align*}
and the closure is compact in $S^*X$. By the standard pseudodifferential cutoff construction, there exists a properly supported operator
\begin{align*}
A:\mathcal{D}'(X)\to \mathcal{D}'(X)
\end{align*}
with $A\in\Psi^0_{\mathrm{prop}}(X)$ such that its principal symbol is equal to $1$ on $V_0$ and its essential support is contained over $O$, with projection to $S^*X$ compactly contained in $\pi_S(V)$. We use the standard construction of conic pseudodifferential cutoffs (citing a result not yet in the wiki: existence of properly supported pseudodifferential cutoffs with prescribed conic symbol support).
[/step]
[step:Prove the elliptic cutoff applied to $u$ has every integer Sobolev order locally]
We claim that
\begin{align*}
Au\in H^N_{\mathrm{loc}}(X)
\end{align*}
for every integer $N\in\mathbb Z$.
Fix $N\in\mathbb Z$. Let $K_A\subset S^*X$ denote the compact projection of the essential support of $A$ to the cosphere bundle. By construction $K_A\subset \pi_S(V)$. For each point $q\in K_A$, choose a covector representative $\tilde q\in V$ with $\pi_S(\tilde q)=q$. The assumption $V\cap WF^N(u)=\varnothing$ implies $\tilde q\notin WF^N(u)$. By the elliptic cutoff characterization of $WF^N(u)$, there exist an open conic neighbourhood $U_q\subset V$ of $\tilde q$ and a properly supported operator
\begin{align*}
B_q:\mathcal{D}'(X)\to \mathcal{D}'(X)
\end{align*}
with $B_q\in\Psi^0_{\mathrm{prop}}(X)$, elliptic on $U_q$, such that
\begin{align*}
B_q u\in H^N_{\mathrm{loc}}(X).
\end{align*}
Since $K_A$ is compact in $S^*X$, finitely many projected neighbourhoods $\pi_S(U_q)$ cover it. Choose points $q_1,\dots,q_m\in K_A$ such that
\begin{align*}
K_A\subset \pi_S(U_{q_1})\cup \cdots \cup \pi_S(U_{q_m})
\end{align*}
Write
\begin{align*}
B_j:=B_{q_j}
\end{align*}
for $1\le j\le m$.
By the microlocal partition of unity in the pseudodifferential calculus, there are properly supported operators
\begin{align*}
C_j:\mathcal{D}'(X)\to \mathcal{D}'(X)
\end{align*}
with $C_j\in\Psi^0_{\mathrm{prop}}(X)$ and a smoothing operator
\begin{align*}
R:\mathcal{D}'(X)\to C^\infty(X)
\end{align*}
such that the difference
\begin{align*}
A-\sum_{j=1}^m C_j B_j
\end{align*}
is smoothing. Equivalently, after defining this smoothing remainder to be $R$, we have the global operator identity
\begin{align*}
A=\sum_{j=1}^m C_j B_j+R.
\end{align*}
This uses elliptic parametrices for the $B_j$ on $U_{q_j}$ and a conic partition of unity subordinate to the finite cover of the full projected essential support of $A$ (citing a result not yet in the wiki: pseudodifferential microlocal partition of unity).
Applying this identity to $u$ gives
\begin{align*}
Au=\sum_{j=1}^m C_j(B_j u)+Ru.
\end{align*}
Each $B_j u$ lies in $H^N_{\mathrm{loc}}(X)$ by construction, and each properly supported order-zero operator $C_j$ maps $H^N_{\mathrm{loc}}(X)$ continuously to itself (citing a result not yet in the wiki: local Sobolev boundedness of properly supported order-zero pseudodifferential operators). Hence
\begin{align*}
C_j(B_j u)\in H^N_{\mathrm{loc}}(X)
\end{align*}
for every $1\le j\le m$. Also $Ru\in C^\infty(X)\subset H^N_{\mathrm{loc}}(X)$. Because $H^N_{\mathrm{loc}}(X)$ is a [vector space](/page/Vector%20Space), the finite sum belongs to $H^N_{\mathrm{loc}}(X)$. Therefore
\begin{align*}
Au\in H^N_{\mathrm{loc}}(X).
\end{align*}
Since $N\in\mathbb Z$ was arbitrary, this holds for every integer $N$.
[guided]
We now prove that the single cutoff $A$ constructed above gives all integer Sobolev orders. Fix an integer $N\in\mathbb Z$. The reason it is enough to work with integer orders is that smoothness will later be recovered from membership in $H^N_{\mathrm{loc}}$ for all integers $N$.
Let $K_A\subset S^*X$ be the compact image in the cosphere bundle of the essential support of $A$. This compactness is exactly why we chose $A$ with microsupport compactly contained in $\pi_S(V)$ on $S^*X$. Since $K_A\subset \pi_S(V)$, every $q\in K_A$ has a covector representative $\tilde q\in V$ with $\pi_S(\tilde q)=q$. The hypothesis says
\begin{align*}
V\cap WF^N(u)=\varnothing,
\end{align*}
so every such representative $\tilde q$ is outside $WF^N(u)$.
By the definition of the Sobolev wave front set, being outside $WF^N(u)$ means that $u$ is microlocally $H^N$ near that covector. Thus, for each $q\in K_A$, after choosing a representative $\tilde q\in V$ with $\pi_S(\tilde q)=q$, there are an open conic neighbourhood $U_q\subset V$ of $\tilde q$ and a properly supported order-zero pseudodifferential operator
\begin{align*}
B_q:\mathcal{D}'(X)\to \mathcal{D}'(X)
\end{align*}
such that $B_q$ is elliptic on $U_q$ and
\begin{align*}
B_q u\in H^N_{\mathrm{loc}}(X).
\end{align*}
This is the elliptic cutoff characterization of $WF^N(u)$ (citing a result not yet in the wiki: Sobolev wave front set via elliptic pseudodifferential cutoffs).
The family of projected open sets $\pi_S(U_q)$ covers $K_A$. Because $K_A$ is compact in $S^*X$, we may choose finitely many points $q_1,\dots,q_m\in K_A$ such that
\begin{align*}
K_A\subset \pi_S(U_{q_1})\cup \cdots \cup \pi_S(U_{q_m})
\end{align*}
Define
\begin{align*}
B_j:=B_{q_j}
\end{align*}
for $1\le j\le m$.
The finite cover lets us patch the local microlocal regularity cutoffs. Since each $B_j$ is elliptic on $U_{q_j}$, the pseudodifferential calculus gives a parametrix for $B_j$ on $U_{q_j}$. Taking a conic partition of unity subordinate to the finite cover of $K_A$, we obtain properly supported order-zero operators
\begin{align*}
C_j:\mathcal{D}'(X)\to \mathcal{D}'(X)
\end{align*}
and a smoothing operator
\begin{align*}
R:\mathcal{D}'(X)\to C^\infty(X)
\end{align*}
such that the difference
\begin{align*}
A-\sum_{j=1}^m C_j B_j
\end{align*}
is smoothing. Defining this smoothing difference to be $R$, we obtain the global operator identity
\begin{align*}
A=\sum_{j=1}^m C_j B_j+R.
\end{align*}
This is the standard pseudodifferential microlocal partition of unity applied to a finite cover of the full projected essential support of $A$ (citing a result not yet in the wiki: pseudodifferential microlocal partition of unity).
Apply this identity to $u$. We get
\begin{align*}
Au=\sum_{j=1}^m C_j(B_j u)+Ru.
\end{align*}
For each $j$, the distribution $B_j u$ belongs to $H^N_{\mathrm{loc}}(X)$ by construction. Since $C_j$ is properly supported and has order zero, it preserves local $H^N$ regularity:
\begin{align*}
C_j(B_j u)\in H^N_{\mathrm{loc}}(X).
\end{align*}
This uses the local Sobolev boundedness of properly supported order-zero pseudodifferential operators (citing a result not yet in the wiki: local Sobolev boundedness of properly supported order-zero pseudodifferential operators). The remainder is smoothing, so
\begin{align*}
Ru\in C^\infty(X)\subset H^N_{\mathrm{loc}}(X).
\end{align*}
A finite sum of elements of $H^N_{\mathrm{loc}}(X)$ is again in $H^N_{\mathrm{loc}}(X)$, and therefore
\begin{align*}
Au\in H^N_{\mathrm{loc}}(X).
\end{align*}
Because the integer $N$ was arbitrary, this proves that $Au$ has local Sobolev regularity of every integer order.
[/guided]
[/step]
[step:Convert all integer Sobolev orders into microlocal smoothness]
From the previous step,
\begin{align*}
Au\in H^N_{\mathrm{loc}}(X)
\end{align*}
for every integer $N\in\mathbb Z$. By the local Sobolev characterization of smoothness,
\begin{align*}
Au\in C^\infty(X)
\end{align*}
after restricting to the base projection of a sufficiently small neighbourhood of $x_0$ if necessary (citing a result not yet in the wiki: local Sobolev characterization of smoothness). Since the principal symbol of $A$ is equal to $1$ on the conic neighbourhood $V_0$ of $(x_0,\xi_0)$, the operator $A$ is elliptic on $V_0$. The smooth wave front set elliptic cutoff characterization then gives
\begin{align*}
(x_0,\xi_0)\notin WF(u).
\end{align*}
This proves the converse implication in the neighbourhood formulation.
[/step]
[step:Take complements to obtain the closure formula]
Let
\begin{align*}
E:=\bigcup_{s\in\mathbb R} WF^s(u)\subset T^*X\setminus 0.
\end{align*}
The neighbourhood formulation proved above says that a covector $(x_0,\xi_0)$ lies outside $WF(u)$ if and only if it has an open conic neighbourhood disjoint from every $WF^s(u)$, equivalently disjoint from $E$. This is precisely the statement that
\begin{align*}
(x_0,\xi_0)\notin \overline{E}.
\end{align*}
Therefore
\begin{align*}
(T^*X\setminus 0)\setminus WF(u)=(T^*X\setminus 0)\setminus \overline{E}.
\end{align*}
Taking complements inside $T^*X\setminus 0$ gives
\begin{align*}
WF(u)=\overline{E}=\overline{\bigcup_{s\in\mathbb R} WF^s(u)}.
\end{align*}
This is the desired formula.
[/step]
