[proofplan] The argument is local in adapted coordinates, because both conormal and Lagrangian distributions are defined by local oscillatory integral representations and then patched by a [partition of unity](/page/Partition%20of%20Unity). In an adapted chart $x=(x',x'')$ with $Y=\{x''=0\}$, the conormal phase $\phi(x,\theta)=x''\cdot\theta$ has critical set $x''=0$ and parametrizes exactly the punctured conormal bundle by $(x',0,\theta)\mapsto (x',0,0,\theta)$. The order conventions agree because this phase has exactly $k$ phase variables. Conversely, any local phase parametrizing $N^*Y\setminus 0$ can be converted to this normal form by the standard phase-parametrization and change-of-phase results for conic Lagrangian distributions, and the low-frequency part of the amplitude contributes only a smooth [regular distribution](/page/Regular%20Distribution). [/proofplan]

[step:Separate the smooth case $k=0$] Assume first that $k=0$. Then $Y=X$, and for each $y\in Y$ one has $T_yY=T_yX$, so \begin{align*} N^*Y=\{(y,0):y\in X\}. \end{align*} Hence $N^*Y\setminus 0=\varnothing$. In an adapted coordinate chart there are no normal variables $x''$ and no phase variables $\theta$. The local expression in the statement becomes multiplication by a smooth amplitude depending only on $x$, because the zero-dimensional oscillatory integral is simply the amplitude itself. Therefore the conormal class given by the stated convention consists exactly of distributions locally represented by smooth functions. This is also the declared convention for $I^m(X,\varnothing)$ with smooth regular distributions included. Thus the theorem holds when $k=0$. [/step]

[step:Compute the Lagrangian parametrized by the conormal phase] Assume now that $k>0$. Let $(U,\varphi)$ be an adapted coordinate chart with coordinates $x=(x',x'')\in\mathbb{R}^{n-k}\times\mathbb{R}^k$ and $Y\cap U=\{x''=0\}$. Define the phase function \begin{align*} \phi:U\times(\mathbb{R}^k\setminus\{0\})\to\mathbb{R}, \qquad \phi(x,\theta)=x''\cdot\theta. \end{align*} For $j\in\{1,\dots,k\}$, differentiation in the phase variable gives \begin{align*} \partial_{\theta_j}\phi(x,\theta)=x''_j. \end{align*} The differentials $d_{(x,\theta)}(\partial_{\theta_1}\phi),\dots,d_{(x,\theta)}(\partial_{\theta_k}\phi)$ are $dx''_1,\dots,dx''_k$, which are linearly independent on $U\times(\mathbb{R}^k\setminus\{0\})$. Hence $\phi$ is a nondegenerate phase function. Thus the critical set in the phase variables is \begin{align*} C_\phi=\{(x',0,\theta):x'\in\mathbb{R}^{n-k},\theta\in\mathbb{R}^k\setminus\{0\}\}. \end{align*} The differential in the base variables is \begin{align*} d_x\phi(x',0,\theta)=(0,\theta)\in(\mathbb{R}^{n-k})^*\times(\mathbb{R}^k)^*. \end{align*} Therefore the parametrized conic Lagrangian is \begin{align*} \Lambda_\phi=\{(x',0,0,\theta):x'\in\mathbb{R}^{n-k},\theta\in\mathbb{R}^k\setminus\{0\}\}. \end{align*} In these coordinates, a covector at a point of $Y$ lies in $N^*Y$ precisely when it annihilates all tangent vectors in the $x'$ directions, so it has the form $(0,\theta)$. Hence $\Lambda_\phi=N^*Y\setminus 0$ over $U$. [/step]

[step:Show that every conormal oscillatory integral is Lagrangian]Let \begin{align*} u:U\to\mathbb{C} \end{align*} be locally represented, modulo a smooth regular distribution, by \begin{align*} u(x)=(2\pi)^{-k}\int_{\mathbb{R}^k} e^{i x''\cdot\theta}a(x,\theta)\,d\mathcal{L}^k(\theta), \end{align*} where $a\in S^{m-k/2+n/4}(U\times\mathbb{R}^k)$. Choose a cutoff function \begin{align*} \chi:\mathbb{R}^k\to[0,1] \end{align*} with $\chi\in C_c^\infty(\mathbb{R}^k)$ and $\chi(\theta)=1$ for $|\theta|\le 1$. Decompose $a=a_0+a_\infty$, where $a_0:U\times\mathbb{R}^k\to\mathbb{C}$ and $a_\infty:U\times\mathbb{R}^k\to\mathbb{C}$ are defined by \begin{align*} a_0(x,\theta):=\chi(\theta)a(x,\theta), \qquad a_\infty(x,\theta):=(1-\chi(\theta))a(x,\theta). \end{align*} The part with amplitude $a_0$ is smooth in $x$: for every multi-index $\alpha$ in the $x$ variables, the differentiated integrand $\partial_x^\alpha(e^{i x''\cdot\theta}a_0(x,\theta))$ is smooth and compactly supported in $\theta$, so differentiation under the integral sign is justified on compact subsets of $U$. Thus the low-frequency term is a smooth regular distribution. The remaining amplitude $a_\infty$ is supported away from $\theta=0$. By the computation of the previous step, the nondegenerate phase $\phi(x,\theta)=x''\cdot\theta$ parametrizes $N^*Y\setminus 0$. Since this phase has $N=k$ phase variables, the Lagrangian normalization assigns amplitude order \begin{align*} m-\frac{N}{2}+\frac{n}{4}=m-\frac{k}{2}+\frac{n}{4}, \end{align*} which is exactly the order of $a_\infty$. Therefore the conormal oscillatory integral belongs locally to $I^m(U,N^*Y\setminus 0)$, with the discarded part accounted for by the smooth regular summand.[/step]

[guided]We want to compare the conormal formula with the Lagrangian definition, but the Lagrangian is punctured: it lives over nonzero covectors. This is why the first move is to separate the amplitude into low and high frequency parts. We are working in an adapted coordinate chart $(U,\varphi)$ with coordinates $x=(x',x'')\in\mathbb{R}^{n-k}\times\mathbb{R}^k$ and $Y\cap U=\{x''=0\}$. The amplitude in the conormal representation satisfies \begin{align*} a\in S^{m-k/2+n/4}(U\times\mathbb{R}^k). \end{align*} Let \begin{align*} \chi:\mathbb{R}^k\to[0,1] \end{align*} be a smooth compactly supported cutoff such that $\chi(\theta)=1$ for $|\theta|\le 1$. Define $a_0:U\times\mathbb{R}^k\to\mathbb{C}$ and $a_\infty:U\times\mathbb{R}^k\to\mathbb{C}$ by \begin{align*} a_0(x,\theta):=\chi(\theta)a(x,\theta), \qquad a_\infty(x,\theta):=(1-\chi(\theta))a(x,\theta). \end{align*} Then $a=a_0+a_\infty$. The term with $a_0$ only sees bounded values of $\theta$. For each multi-index $\alpha$ in the $x$ variables, the function \begin{align*} (x,\theta)\mapsto \partial_x^\alpha(e^{i x''\cdot\theta}a_0(x,\theta)) \end{align*} is smooth and compactly supported in $\theta$ on compact subsets of $U$. Therefore differentiating under the integral sign gives a smooth function of $x$. Hence the low-frequency contribution is a smooth regular distribution. The term with $a_\infty$ is supported where $\theta\ne 0$, so it is a genuine oscillatory integral over the punctured phase space. The phase \begin{align*} \phi:U\times(\mathbb{R}^k\setminus\{0\})\to\mathbb{R}, \qquad \phi(x,\theta)=x''\cdot\theta \end{align*} has critical set $x''=0$, and its base differential at a critical point is $(0,\theta)$. Thus it parametrizes precisely those covectors over $Y$ that annihilate the tangent directions to $Y$, namely $N^*Y\setminus 0$. Finally, the order normalization matches without any hidden shift. The phase has $N=k$ phase variables, so the Lagrangian convention requires amplitudes of order \begin{align*} m-\frac{k}{2}+\frac{n}{4}. \end{align*} This is exactly the conormal amplitude order in the statement. Hence the high-frequency part is a Lagrangian distribution of order $m$, and the low-frequency part is included among the smooth regular distributions.[/guided]

[step:Reduce every local Lagrangian representation to the conormal normal form] Conversely, let $v\in I^m(U,N^*Y\setminus 0)$. In the adapted chart, $N^*Y\setminus 0$ is a smooth conic Lagrangian submanifold of $T^*U\setminus 0$: it is parametrized by $(x',\theta)\in\mathbb{R}^{n-k}\times(\mathbb{R}^k\setminus\{0\})$, has dimension $n$, is conic in the covector variable, and is Lagrangian because it is the image of the nondegenerate phase computed above. By the standard parametrization theorem for conic Lagrangian submanifolds by nondegenerate homogeneous phase functions, applied to this smooth conic Lagrangian, each local term in $v$ may be represented modulo a smooth regular distribution by an oscillatory integral with some nondegenerate homogeneous phase parametrizing $N^*Y\setminus 0$ and amplitude of order $m-N/2+n/4$, where $N$ is the number of phase variables in that representation. Since $N^*Y\setminus 0$ is, in the adapted chart, the set \begin{align*} \{(x',0,0,\theta):\theta\in\mathbb{R}^k\setminus\{0\}\}, \end{align*} the standard equivalence and change-of-phase theorem for Lagrangian distributions converts any such nondegenerate phase parametrization to the normal form \begin{align*} \phi(x,\theta)=x''\cdot\theta \end{align*} after possibly shrinking $U$, adding or removing nonessential phase variables, and modifying the amplitude by the induced elliptic symbol factor. The hypotheses for this change-of-phase theorem are met because both phase functions are nondegenerate homogeneous parametrizations of the same smooth conic Lagrangian $N^*Y\setminus 0$. The change-of-phase theorem preserves the represented distribution modulo smooth regular distributions and transforms the amplitude order according to the same Lagrangian normalization. In the normal form there are exactly $k$ phase variables, so the resulting amplitude has order \begin{align*} m-\frac{k}{2}+\frac{n}{4}. \end{align*} Therefore every local Lagrangian distribution associated to $N^*Y\setminus 0$ has, modulo a smooth regular distribution, the defining adapted-coordinate conormal form. [/step]

[step:Patch the local equality over $X$] Choose a locally finite smooth partition of unity subordinate to adapted coordinate charts covering a neighbourhood of $Y$, together with ordinary coordinate charts away from $Y$. On every adapted chart intersecting $Y$, the two preceding steps prove equality between the local conormal class of order $m$ and the local Lagrangian class $I^m(U,N^*Y\setminus 0)$. On charts disjoint from $Y$, the conormal bundle has no base points and both descriptions contribute only smooth regular distributions. Because multiplication by a compactly supported smooth cutoff preserves symbol classes and preserves the associated Lagrangian relation locally, the local equality is stable under the partition of unity. Summing the locally finite pieces gives equality of the global spaces as subspaces of $\mathcal{D}'(X)$. Thus, for $k>0$, the conormal distributions to $Y$ of order $m$ are exactly $I^m(X,N^*Y\setminus 0)$ with smooth regular distributions included on both sides. Together with the already proved $k=0$ case, this proves the theorem. [/step]