[proofplan] We prove the inclusion locally in a real-analytic coordinate chart. In such a chart, the CR condition is a real-analytic linear differential system $\bar L_j f=0$, and the complement of $\operatorname{Char}(\bar\partial_b)$ is precisely the microlocally elliptic region of this system. Analytic microlocal elliptic regularity for real-analytic differential systems excludes analytic wave-front directions in every conic neighbourhood where one principal symbol is nonzero. The final equivalence is the standard fibrewise characterization of real-analytic regularity by the analytic wave-front set. [/proofplan]

[step:Localize the CR equations in real-analytic coordinates] Fix $p\in M$. Choose a real-analytic coordinate chart $(U,\varphi)$ on $M$ with $p\in U$ and \begin{align*} \varphi:U\to \varphi(U)\subset\mathbb R^d, \end{align*} where $d:=\dim_{\mathbb R}M$. After shrinking $U$ if necessary, choose a real-analytic local frame \begin{align*} \bar L_1,\dots,\bar L_m\in \Gamma(U,T^{0,1}M), \end{align*} where $m:=\operatorname{rank}_{\mathbb C}T^{0,1}M$. Let $x=(x_1,\dots,x_d)$ denote the coordinates on $\varphi(U)$. For each $1\le j\le m$, write the pushed-forward vector field as \begin{align*} (\varphi_*\bar L_j)_x=\sum_{k=1}^d a_{jk}(x)\partial_{x_k}, \end{align*} where each coefficient \begin{align*} a_{jk}:\varphi(U)\to\mathbb C \end{align*} is real-analytic. Define the first-order differential operator \begin{align*} P_j:C^\infty(\varphi(U);\mathbb C)\to C^\infty(\varphi(U);\mathbb C) \end{align*} by \begin{align*} P_j u=\sum_{k=1}^d a_{jk}\partial_{x_k}u. \end{align*} Let \begin{align*} g\in \mathcal D'(\varphi(U)) \end{align*} denote the distributional pushforward of $f|_U$ by $\varphi$. Since $f$ is CR and $\bar L_j$ is a local section of $T^{0,1}M$, one has \begin{align*} P_j g=0 \end{align*} in $\mathcal D'(\varphi(U))$ for every $1\le j\le m$. [/step]

[step:Identify noncharacteristic covectors with microlocally elliptic directions]For $1\le j\le m$, define the principal symbol \begin{align*} p_j:\varphi(U)\times(\mathbb R^d\setminus\{0\})\to\mathbb C \end{align*} by \begin{align*} p_j(x,\xi)=i\sum_{k=1}^d a_{jk}(x)\xi_k. \end{align*} The characteristic set of the local system $P=(P_1,\dots,P_m)$ is \begin{align*} \operatorname{Char}(P)=\{(x,\xi)\in \varphi(U)\times(\mathbb R^d\setminus\{0\}):p_j(x,\xi)=0\text{ for every }1\le j\le m\}. \end{align*} This is the coordinate representation of $\operatorname{Char}(\bar\partial_b)$ under the cotangent map induced by $\varphi$. Let $(x_0,\xi_0)\in \varphi(U)\times(\mathbb R^d\setminus\{0\})$ satisfy \begin{align*} (x_0,\xi_0)\notin \operatorname{Char}(P). \end{align*} By the displayed definition of $\operatorname{Char}(P)$, there exists an index $j_0\in\{1,\dots,m\}$ such that \begin{align*} p_{j_0}(x_0,\xi_0)\ne 0. \end{align*} Since $p_{j_0}$ is continuous and homogeneous of degree $1$ in $\xi$, there exist an open neighbourhood $V\subset\varphi(U)$ of $x_0$ and an open conic neighbourhood $\Gamma\subset\mathbb R^d\setminus\{0\}$ of $\xi_0$ such that \begin{align*} p_{j_0}(x,\xi)\ne 0 \end{align*} for every $(x,\xi)\in V\times\Gamma$.[/step]

[guided]We now unpack the meaning of being outside the characteristic set. The local CR system consists of the operators \begin{align*} P_j=\sum_{k=1}^d a_{jk}\partial_{x_k} \end{align*} for $1\le j\le m$, and the principal symbol of $P_j$ is the function \begin{align*} p_j:\varphi(U)\times(\mathbb R^d\setminus\{0\})\to\mathbb C,\qquad p_j(x,\xi)=i\sum_{k=1}^d a_{jk}(x)\xi_k. \end{align*} The characteristic set of the full system is not the characteristic set of one chosen vector field. It is the common zero set of all the principal symbols: \begin{align*} \operatorname{Char}(P)=\{(x,\xi)\in \varphi(U)\times(\mathbb R^d\setminus\{0\}):p_j(x,\xi)=0\text{ for every }1\le j\le m\}. \end{align*} Thus, if $(x_0,\xi_0)$ is not in $\operatorname{Char}(P)$, then the symbols cannot all vanish at $(x_0,\xi_0)$. Hence there is an index $j_0\in\{1,\dots,m\}$ with \begin{align*} p_{j_0}(x_0,\xi_0)\ne 0. \end{align*} This is the exact point at which the full-system definition matters: one nonvanishing principal symbol is enough to give microlocal ellipticity for the overdetermined system in that direction. Because the coefficient functions $a_{j_0k}$ are real-analytic, they are continuous, and therefore $p_{j_0}$ is continuous on $\varphi(U)\times(\mathbb R^d\setminus\{0\})$. Since $p_{j_0}(x_0,\xi_0)\ne0$, continuity gives a neighbourhood of $(x_0,\xi_0)$ on which $p_{j_0}$ remains nonzero. Using the homogeneity of $p_{j_0}$ in $\xi$, we may take this neighbourhood in the product form $V\times\Gamma$, where $V\subset\varphi(U)$ is open and $\Gamma\subset\mathbb R^d\setminus\{0\}$ is an open conic neighbourhood of $\xi_0$. Therefore \begin{align*} p_{j_0}(x,\xi)\ne 0 \end{align*} for every $(x,\xi)\in V\times\Gamma$.[/guided]

[step:Apply analytic microlocal elliptic regularity to exclude the covector] We use the analytic [microlocal elliptic regularity theorem](/theorems/8175) for real-analytic scalar differential operators: if a first-order differential operator $Q$ has real-analytic coefficients and its principal symbol is nonzero on a conic neighbourhood of $(x_0,\xi_0)$, then every distribution $u$ satisfying $Qu=0$ on the base neighbourhood has \begin{align*} (x_0,\xi_0)\notin \operatorname{WF}_a(u). \end{align*} Equivalently, an analytic pseudodifferential parametrix exists in that conic neighbourhood and yields the exponential FBI-transform decay that defines absence from the analytic wave-front set. The hypotheses of this theorem hold with $Q=P_{j_0}$ and $u=g$. The coefficients $a_{j_0k}$ are real-analytic on $\varphi(U)$, the previous step gives the required nonvanishing of the principal symbol $p_{j_0}$ on $V\times\Gamma$, and the CR condition gives \begin{align*} P_{j_0}g=0 \end{align*} in $\mathcal D'(\varphi(U))$. The other equations $P_jg=0$ are not needed for this scalar microlocal elliptic conclusion; they were used only to identify that some member of the full CR system is elliptic away from the common characteristic set. Hence \begin{align*} (x_0,\xi_0)\notin \operatorname{WF}_a(g). \end{align*} Since $(x_0,\xi_0)$ was an arbitrary noncharacteristic covector, we obtain \begin{align*} \operatorname{WF}_a(g)\subset \operatorname{Char}(P). \end{align*} [/step]

[step:Transfer the local inclusion back to the manifold] The analytic wave-front set is invariant under real-analytic coordinate changes by the induced cotangent transformation. Therefore the inclusion \begin{align*} \operatorname{WF}_a(g)\subset \operatorname{Char}(P) \end{align*} in the chart $(U,\varphi)$ is equivalent to \begin{align*} \operatorname{WF}_a(f|_U)\subset \operatorname{Char}(\bar\partial_b)\cap (T^*U\setminus\{0\}). \end{align*} Since the point $p\in M$ and the chart $(U,\varphi)$ were arbitrary, these local inclusions combine to give \begin{align*} \operatorname{WF}_a(f)\subset \operatorname{Char}(\bar\partial_b). \end{align*} [/step]

[step:Use the fibre criterion for real-analyticity] Fix $p\in M$ and choose a real-analytic coordinate chart $(U,\varphi)$ with $p\in U$. Let $x_0:=\varphi(p)$ and let $g\in\mathcal D'(\varphi(U))$ be the coordinate representative of $f|_U$. By the [[FBI Characterization of Real-Analytic Regularity](/theorems/9231)][citetheorem:9231], $g$ is represented by a real-[analytic function](/page/Analytic%20Function) in a neighbourhood of $x_0$ if and only if \begin{align*} \operatorname{WF}_a(g)\cap\bigl(T_{x_0}^*\varphi(U)\setminus\{0\}\bigr)=\varnothing. \end{align*} The analytic chart $\varphi$ identifies real-analytic representatives of $f$ near $p$ with real-analytic representatives of $g$ near $x_0$, and it identifies the punctured cotangent fibre $T_p^*M\setminus\{0\}$ with $T_{x_0}^*\varphi(U)\setminus\{0\}$. Hence $f$ is represented by a real-analytic function near $p$ if and only if \begin{align*} \operatorname{WF}_a(f)\cap\bigl(T_p^*M\setminus\{0\}\bigr)=\varnothing. \end{align*} This proves the stated fibrewise analyticity criterion and completes the proof. [/step]