[proofplan] We first use the Sobolev propagation estimate for real principal type operators, whose proof is the positive-commutator argument: a microlocal commutant is chosen so that its commutator with $P$ has a positive principal symbol in the forward Hamilton direction. This estimate propagates microlocal $H^r$ regularity locally along $H_p$, provided $Pu$ has the corresponding microlocal $H^{r-m+1}$ regularity. Since the bicharacteristic segment is compact and avoids $\operatorname{WF}(Pu)$, finitely many local propagation steps carry $H^r$ regularity from the given point to the whole segment. Applying this for every Sobolev order $r$ converts Sobolev regularity into absence from the $C^\infty$ wave front set. [/proofplan]

[step:Invoke the local Sobolev propagation estimate along the Hamilton flow] We use the standard Sobolev propagation theorem for real principal type operators, proved by the positive-commutator method. For each $a \in \mathbb{R}$, let $H^a_{\mathrm{loc}}(X)$ denote the local [Sobolev space](/page/Sobolev%20Space) of order $a$ on $X$, defined in coordinate charts, and let $\operatorname{WF}^a(v) \subset T^*X \setminus 0$ denote the Sobolev wave front set of a distribution $v \in \mathcal{D}'(X)$; by convention, $q \notin \operatorname{WF}^a(v)$ means that $v$ is microlocally in $H^a$ at the point $q \in T^*X \setminus 0$. Precisely, fix $r \in \mathbb{R}$ and a point $q_0 \in \Sigma_\Omega$. The local theorem gives a conic flow box $V \subset \Omega$ around $q_0$ and two smaller conic neighbourhoods $V_- , V_0 \subset V \cap \Sigma_\Omega$, with $V_-$ lying immediately upstream from $V_0$ along the $H_p$ flow, such that the following implication holds: if $Pu$ is microlocally in $H^{r-m+1}$ on $V$, and if $u$ is microlocally in $H^r$ on $V_-$ along the same bicharacteristic, then $u$ is microlocally in $H^r$ on $V_0$. The same statement applied after replacing the Hamilton parameter $s$ by $-s$ gives propagation in the opposite direction. The hypotheses of this estimate apply here locally on $\Sigma_\Omega$: the operator $P$ is classical and properly supported of order $m$, its principal symbol $p$ is real and homogeneous, $H_p(q) \neq 0$ for every $q \in \Sigma_\Omega$, and proper support ensures that $Pu \in \mathcal{D}'(X)$ is defined for every $u \in \mathcal{D}'(X)$. [/step]

[step:Use the absence of $\operatorname{WF}(Pu)$ to obtain all Sobolev regularities for $Pu$ near the segment] Since \begin{align*} \gamma([s_0,s_1]) \cap \operatorname{WF}(Pu)=\varnothing, \end{align*} each point of the compact set $\gamma([s_0,s_1])$ has a conic neighbourhood on which $Pu$ is microlocally smooth. Therefore, for every $r \in \mathbb{R}$, $Pu$ is microlocally in $H^{r-m+1}$ at every point of $\gamma([s_0,s_1])$. Because $\gamma([s_0,s_1])$ is compact, finitely many such conic neighbourhoods cover it. Shrinking the flow boxes used in the local Sobolev propagation estimate if necessary, we may assume that every local propagation step occurs inside a conic neighbourhood where $Pu$ is microlocally in the required Sobolev space. [/step]

[step:Propagate a fixed Sobolev order across a finite cover of the segment]Fix $r \in \mathbb{R}$. Since $\gamma(s_*) \notin \operatorname{WF}(u)$, the distribution $u$ is microlocally in $H^r$ at $\gamma(s_*)$. Recall that $\operatorname{WF}^r(u)$ denotes the Sobolev wave front set of order $r$, so $q \notin \operatorname{WF}^r(u)$ means that $u$ is microlocally in $H^r$ at $q$. Cover the compact interval $[s_0,s_1]$ by finitely many subintervals \begin{align*} I_j \subset [s_0,s_1], \qquad j=1,\dots,N, \end{align*} chosen so that the image $\gamma(I_j)$ lies in a single flow box where the local Sobolev propagation estimate applies, and refine the cover so consecutive subintervals overlap in their interiors. This refinement is possible by the [Lebesgue number lemma](/theorems/952) applied to the open cover of $[s_0,s_1]$ induced by the flow boxes. Starting from $s_*$, order the overlapping subintervals along the parameter direction from $s_*$ to $s_1$. Applying the local Sobolev propagation estimate on the first flow box gives microlocal $H^r$ regularity on an overlapping terminal portion of that box; this overlap supplies the upstream hypothesis for the next flow box. Iterating through the finite chain gives microlocal $H^r$ regularity of $u$ at every point $\gamma(s)$ with $s \in [s_*,s_1]$. Applying the same estimate to the reversed parameter direction gives microlocal $H^r$ regularity of $u$ at every point $\gamma(s)$ with $s \in [s_0,s_*]$. Hence \begin{align*} \gamma([s_0,s_1]) \cap \operatorname{WF}^r(u)=\varnothing. \end{align*}[/step]

[guided]Fix a Sobolev order $r \in \mathbb{R}$. The point of fixing $r$ is that the positive-commutator theorem propagates one Sobolev order at a time; smoothness will be recovered only after repeating the argument for all $r$. The assumption $\gamma(s_*) \notin \operatorname{WF}(u)$ means precisely that $u$ is microlocally smooth at $\gamma(s_*)$. In particular, $u$ is microlocally in $H^r$ at $\gamma(s_*)$ for this fixed value of $r$. Now choose finitely many intervals $I_1,\dots,I_N \subset [s_0,s_1]$ such that each image $\gamma(I_j)$ lies in a flow box for $H_p$ on which the Sobolev propagation estimate applies. This is possible because $H_p$ is nonzero on $\Sigma_\Omega$, so the Hamilton flow gives local flow-box coordinates near every point of the segment, and because the parameter interval $[s_0,s_1]$ is compact. Refining the finite cover using the Lebesgue number lemma, we choose the intervals so that consecutive intervals overlap in their interiors. On each such flow box, the local theorem says: if $Pu$ is microlocally in $H^{r-m+1}$ on the relevant conic neighbourhood in the flow box, and if $u$ is microlocally in $H^r$ on the upstream part of the same bicharacteristic, then $u$ is microlocally in $H^r$ on the next downstream part. The reversed-parameter form of the same theorem gives the identical implication in the opposite Hamilton direction. We also verify the hypothesis on $Pu$ inside this guided argument. Since \begin{align*} \gamma([s_0,s_1]) \cap \operatorname{WF}(Pu)=\varnothing, \end{align*} each point of $\gamma([s_0,s_1])$ has a conic neighbourhood on which $Pu$ is microlocally smooth. Microlocal smoothness implies microlocal $H^{r-m+1}$ regularity for this fixed $r$. Compactness of $\gamma([s_0,s_1])$ gives finitely many such conic neighbourhoods, and the flow boxes may be shrunk so that every local propagation step stays inside one of them. Beginning at $s_*$ and moving toward $s_1$, choose the flow boxes with consecutive overlaps in their interiors. The first application of the local estimate gives $H^r$ regularity on the next small portion of the curve. Because adjacent flow boxes overlap, that newly obtained regularity supplies the upstream $H^r$ hypothesis for the next flow box. Repeating this finite process reaches every point $\gamma(s)$ with $s \in [s_*,s_1]$. Reversing the parameter, equivalently applying the same local theorem to the Hamilton flow with parameter $-s$, gives the same conclusion on $[s_0,s_*]$. Thus $u$ is microlocally in $H^r$ at every point of $\gamma([s_0,s_1])$, which is exactly \begin{align*} \gamma([s_0,s_1]) \cap \operatorname{WF}^r(u)=\varnothing. \end{align*}[/guided]

[step:Upgrade propagation of every Sobolev order to propagation of smoothness] The previous step holds for every $r \in \mathbb{R}$. By the definition of the $C^\infty$ wave front set, a point $q \in T^*X \setminus 0$ is absent from $\operatorname{WF}(u)$ exactly when $u$ is microlocally in $H^r$ at $q$ for every $r \in \mathbb{R}$. Therefore \begin{align*} \gamma([s_0,s_1]) \cap \operatorname{WF}(u)=\varnothing. \end{align*} This proves the first assertion. [/step]

[step:Remove the elliptic region by elliptic regularity] Let $q \in \Omega \setminus \Sigma_\Omega$. By definition of $\Sigma_\Omega$, $p(q) \neq 0$, so $P$ is microlocally elliptic at $q$. Elliptic regularity for properly supported classical pseudodifferential operators gives the implication \begin{align*} q \notin \operatorname{WF}(Pu) \implies q \notin \operatorname{WF}(u). \end{align*} Hence no point of $\Omega \setminus \Sigma_\Omega$ can belong to $\operatorname{WF}(u) \setminus \operatorname{WF}(Pu)$, and therefore \begin{align*} \bigl(\operatorname{WF}(u)\setminus \operatorname{WF}(Pu)\bigr) \cap \Omega \subset \Sigma_\Omega. \end{align*} [/step]

[step:Interpret the conclusion as invariance of the singular set away from $\operatorname{WF}(Pu)$] Let $q \in \Sigma_\Omega \setminus \operatorname{WF}(Pu)$, and let \begin{align*} \eta : J \to \Sigma_\Omega \end{align*} be a bicharacteristic segment with $q=\eta(t_0)$ for some $t_0 \in J$, whose image is contained in $\Omega$ and disjoint from $\operatorname{WF}(Pu)$. Applying the result just proved to each compact subsegment of $\eta(J)$ shows that if one point of that subsegment is outside $\operatorname{WF}(u)$, then the whole subsegment is outside $\operatorname{WF}(u)$. Equivalently, along such a bicharacteristic segment, membership in $\operatorname{WF}(u)$ is constant away from $\operatorname{WF}(Pu)$. Hence, inside $\Omega$, \begin{align*} \operatorname{WF}(u)\setminus \operatorname{WF}(Pu) \end{align*} is invariant under the bicharacteristic flow in $\Sigma_\Omega$. This is the stated propagation principle. [/step]