[proofplan] The proof has two parts. First, properness on $\operatorname{supp}u$ makes the relevant portion of the support compact for each compactly supported [test function](/page/Test%20Function), so a cutoff exists and the formula for $F_*u$ is independent of the cutoff. Second, the wave front estimate is local on $Y$ and on $X$; using the submersion normal form theorem, we reduce near each relevant point to the projection map $(y,z) \mapsto y$. In that model, a localized [Fourier transform](/page/Fourier%20Transform) of $F_*u$ in the base variable is exactly a localized Fourier transform of $u$ at covectors of the form $(\eta,0)$, and compactness gives one uniform conic neighbourhood on which the required rapid decay holds. [/proofplan]

[step:Use properness to define the pushforward on test functions]Fix $\phi \in C_c^\infty(Y)$, and define the compact set \begin{align*} K_\phi := \operatorname{supp}u \cap F^{-1}(\operatorname{supp}\phi). \end{align*} Since $\operatorname{supp}\phi$ is compact in $Y$ and $F|_{\operatorname{supp}u}: \operatorname{supp}u \to Y$ is proper, the set $K_\phi$ is compact in $X$. We use the smooth cutoff lemma for second-countable Hausdorff manifolds: if $K \subset X$ is compact, then there is $\chi \in C_c^\infty(X)$ with $\chi = 1$ on an open neighbourhood of $K$. Its hypotheses hold because $X$ is a smooth second-countable Hausdorff manifold and $K_\phi$ is compact. Hence there exists $\chi \in C_c^\infty(X)$ such that $\chi = 1$ on an open neighbourhood of $K_\phi$. The function \begin{align*} \chi(\phi \circ F): X \to \mathbb{C} \end{align*} is smooth and compactly supported, so $u\bigl(\chi(\phi \circ F)\bigr)$ is defined. Let $\chi_1,\chi_2 \in C_c^\infty(X)$ be two such cutoffs, and define \begin{align*} h: X \to \mathbb{C}, \qquad h := (\chi_1-\chi_2)(\phi \circ F). \end{align*} We show that $u(h)=0$. If $x \in \operatorname{supp}u$ and $F(x) \in \operatorname{supp}\phi$, then $x \in K_\phi$, and $\chi_1-\chi_2$ vanishes on a neighbourhood of $x$. If $x \in \operatorname{supp}u$ and $F(x) \notin \operatorname{supp}\phi$, then, because $\operatorname{supp}\phi$ is closed and $\phi$ vanishes on $Y \setminus \operatorname{supp}\phi$, the function $\phi \circ F$ vanishes on a neighbourhood of $x$. Thus $h$ vanishes on an open neighbourhood of every point of $\operatorname{supp}u$. By the definition of the support of a distributional density, $u(h)=0$. Therefore $u\bigl(\chi_1(\phi\circ F)\bigr)=u\bigl(\chi_2(\phi\circ F)\bigr)$, so the definition of $(F_*u)(\phi)$ is independent of $\chi$.[/step]

[guided]Fix a test function $\phi \in C_c^\infty(Y)$. The only possible obstruction to writing $u(\phi \circ F)$ is that $\phi \circ F$ need not have compact support in $X$. Properness is exactly what lets us repair this by multiplying by a cutoff without changing what $u$ sees. Define \begin{align*} K_\phi := \operatorname{supp}u \cap F^{-1}(\operatorname{supp}\phi). \end{align*} The set $\operatorname{supp}\phi$ is compact because $\phi$ is compactly supported. Since $F|_{\operatorname{supp}u}$ is proper, the inverse image of this compact set inside $\operatorname{supp}u$ is compact. Hence $K_\phi$ is compact in $X$. We use the smooth cutoff lemma for second-countable Hausdorff manifolds: if $K \subset X$ is compact, then there is $\chi \in C_c^\infty(X)$ with $\chi=1$ on an open neighbourhood of $K$. The hypotheses are satisfied because $X$ is smooth, second-countable, and Hausdorff, and because $K_\phi$ is compact. Applying this result to $K_\phi$, choose $\chi \in C_c^\infty(X)$ with $\chi=1$ on an open neighbourhood of $K_\phi$. Then \begin{align*} \chi(\phi \circ F): X \to \mathbb{C} \end{align*} is smooth and compactly supported, so the distributional density $u$ may act on it. Now we check that the value does not depend on the cutoff. Let $\chi_1,\chi_2 \in C_c^\infty(X)$ both equal $1$ near $K_\phi$, and set \begin{align*} h := (\chi_1-\chi_2)(\phi \circ F). \end{align*} To prove $u(h)=0$, it is enough to prove that $h$ vanishes on a neighbourhood of $\operatorname{supp}u$. Take any $x \in \operatorname{supp}u$. If $F(x) \in \operatorname{supp}\phi$, then $x \in K_\phi$, so $\chi_1-\chi_2=0$ near $x$. If $F(x) \notin \operatorname{supp}\phi$, then $\phi$ vanishes on some neighbourhood of $F(x)$ because $\operatorname{supp}\phi$ is closed; therefore $\phi \circ F$ vanishes on some neighbourhood of $x$. In both cases $h$ vanishes near $x$. Thus $h$ vanishes on an open neighbourhood of $\operatorname{supp}u$. By the defining support property of a distributional density, $u(h)=0$. Hence \begin{align*} u\bigl(\chi_1(\phi\circ F)\bigr)=u\bigl(\chi_2(\phi\circ F)\bigr). \end{align*} So the formula defining $(F_*u)(\phi)$ is independent of the auxiliary cutoff.[/guided]

[step:Prove that the pushforward is a distributional density] The assignment \begin{align*} F_*u: C_c^\infty(Y) \to \mathbb{C}, \qquad \phi \mapsto u\bigl(\chi(\phi\circ F)\bigr) \end{align*} is linear by linearity of $u$ and by the cutoff independence just proved. It remains to prove continuity in the usual test-function topology. Let $(\phi_j)_{j=1}^\infty$ be a sequence in $C_c^\infty(Y)$ converging to $0$ with all supports contained in a fixed compact set $K \subset Y$. Define \begin{align*} K_X := \operatorname{supp}u \cap F^{-1}(K). \end{align*} By properness of $F|_{\operatorname{supp}u}$, the set $K_X$ is compact. Choose one function $\chi_K \in C_c^\infty(X)$ such that $\chi_K=1$ on an open neighbourhood of $K_X$. For every $j$, cutoff independence gives \begin{align*} (F_*u)(\phi_j)=u\bigl(\chi_K(\phi_j\circ F)\bigr). \end{align*} The pullback map $\phi \mapsto \phi\circ F$ is continuous from $C_K^\infty(Y)$ to $C^\infty(F^{-1}(K))$ on compact sets after restriction to the compact set $\operatorname{supp}\chi_K$, and multiplication by $\chi_K$ maps the resulting functions continuously into $C_c^\infty(X)$. Therefore \begin{align*} \chi_K(\phi_j\circ F) \to 0 \end{align*} in $C_c^\infty(X)$. Since $u \in \mathcal{D}'(X;|\Omega_X|)$ is continuous on $C_c^\infty(X)$, it follows that $(F_*u)(\phi_j) \to 0$. Thus $F_*u \in \mathcal{D}'(Y;|\Omega_Y|)$. [/step]

[step:Reduce the wave front estimate to the projection model] Let $(y_0,\eta_0) \in T^*Y\setminus\{0\}$ and suppose that \begin{align*} (y_0,\eta_0) \notin \{(F(x), \eta) : x \in X,\ \eta \in T^*_{F(x)}Y\setminus\{0\},\ (x,dF_x^*\eta)\in \operatorname{WF}(u)\}. \end{align*} We prove that $(y_0,\eta_0)\notin \operatorname{WF}(F_*u)$. Choose a coordinate chart $(V,\kappa)$ on $Y$ with $y_0 \in V$, and use this chart to identify covectors over $V$ with elements of $\mathbb{R}^m$. Shrink $V$ if necessary and choose $\psi \in C_c^\infty(V)$ with $\psi(y_0)\neq 0$. Define \begin{align*} K := \operatorname{supp}u \cap F^{-1}(\operatorname{supp}\psi). \end{align*} This set is compact by properness. We use the submersion normal form theorem in a form adapted to the fixed target chart: if $F:X\to Y$ is a smooth submersion at $x$ and $F(x)\in V$, then, after possibly shrinking $V$ around $F(x)$, there is a coordinate chart $(U_x,\theta_x)$ on $X$ with $x\in U_x$ and $F(U_x)\subset V$ such that, in the coordinates $\theta_x=(y,z)$ on $U_x$ and $\kappa$ on $V$, the map $F$ is the projection \begin{align*} (y,z) \mapsto y. \end{align*} Its hypothesis is satisfied at every $x\in K$ because $F$ is a smooth submersion on all of $X$. Since $K$ is compact, shrink $\operatorname{supp}\psi$ inside $V$ once more and choose finitely many such source charts $U_1,\dots,U_M$ covering $K$ for which the same target coordinates $\kappa$ describe the base variable near $y_0$. Here $y \in \mathbb{R}^m$, $z \in \mathbb{R}^{n-m}$, $m=\dim Y$, and $n=\dim X$. Choose functions $\rho_1,\dots,\rho_M \in C_c^\infty(X)$ with $\operatorname{supp}\rho_j \subset U_j$ and \begin{align*} \sum_{j=1}^M \rho_j = 1 \end{align*} on an open neighbourhood of $K$. It is enough to prove rapid decay for each localized distributional density $\rho_j u$. To make the localization identity precise, let $W\subset V$ be an open neighbourhood of $y_0$ such that $\operatorname{supp}\varphi\subset W$ implies $\operatorname{supp}\varphi\subset\operatorname{supp}\psi$ for the base test functions $\varphi\in C_c^\infty(W)$ used to test the localized distribution. For such a $\varphi$, define \begin{align*} K_\varphi := \operatorname{supp}u\cap F^{-1}(\operatorname{supp}\varphi). \end{align*} Then $K_\varphi\subset K$, and $\sum_{j=1}^M\rho_j=1$ on an open neighbourhood of $K_\varphi$. Choose a cutoff $\chi_\varphi\in C_c^\infty(X)$ equal to $1$ on an open neighbourhood of $K_\varphi$. Since the function \begin{align*} \chi_\varphi\left(1-\sum_{j=1}^M\rho_j\right)(\varphi\circ F):X\to\mathbb{C} \end{align*} vanishes on an open neighbourhood of $\operatorname{supp}u$, the support property of $u$ gives \begin{align*} (F_*u)(\varphi)=\sum_{j=1}^M(F_*(\rho_j u))(\varphi). \end{align*} Multiplication by the fixed cutoff $\psi$ means the product distributional density defined by $(\psi F_*u)(\varphi):=(F_*u)(\psi\varphi)$ for $\varphi\in C_c^\infty(W)$. The preceding identity applied to $\psi\varphi$ gives \begin{align*} \psi F_*u = \sum_{j=1}^M \psi F_*(\rho_j u) \end{align*} as distributional densities on $W$. In each coordinate chart $U_j$, choose the coordinate density trivialization determined by [Lebesgue measure](/page/Lebesgue%20Measure) in the coordinates $(y,z)$. Under this trivialization, $\rho_j u$ is represented by an ordinary compactly supported distribution on an open subset of $\mathbb{R}^m_y\times \mathbb{R}^{n-m}_z$. The wave front set of a distributional density in a chart is defined by this local trivialization, and multiplication by the smooth nonvanishing coordinate density does not change the wave front condition. Thus the remaining argument may be carried out in the local model \begin{align*} F: \mathbb{R}^m_y \times \mathbb{R}^{n-m}_z \to \mathbb{R}^m_y, \qquad F(y,z)=y. \end{align*} In this model, \begin{align*} dF_{(y,z)}^*\eta = (\eta,0) \in T^*_y\mathbb{R}^m \times T_z^*\mathbb{R}^{n-m}. \end{align*} [/step]

[step:Convert the localized base Fourier transform into a lifted Fourier transform] Work in one projection chart from the previous step. Let \begin{align*} v \in \mathcal{D}'(\mathbb{R}^m_y\times\mathbb{R}^{n-m}_z) \end{align*} denote the compactly supported local representative of one localized piece of $u$ in the coordinate density trivialization. The notation $\widehat{\alpha F_*v}$ below means the Euclidean Fourier transform, in the $y$ variable, of the distribution obtained by multiplying the local pushforward by the smooth cutoff $\alpha$. Let \begin{align*} \alpha \in C_c^\infty(\mathbb{R}^m) \end{align*} be a base cutoff supported in the chosen coordinate neighbourhood and equal to the coordinate representative of $\psi$ near $y_0$. By properness already localized to the compact set under consideration, choose \begin{align*} \beta \in C_c^\infty(\mathbb{R}^{n-m}) \end{align*} such that $\beta(z)=1$ on an open neighbourhood of the set of $z$ for which $(y,z)\in \operatorname{supp}v$ for some $y \in \operatorname{supp}\alpha$. Define the compactly supported test amplitude \begin{align*} a: \mathbb{R}^m\times\mathbb{R}^{n-m}\to\mathbb{C}, \qquad a(y,z):=\alpha(y)\beta(z). \end{align*} For $\eta \in \mathbb{R}^m$, define \begin{align*} e_\eta: \mathbb{R}^m\times\mathbb{R}^{n-m}\to\mathbb{C}, \qquad e_\eta(y,z):=e^{-i y\cdot \eta}. \end{align*} Then the Fourier transform in the base variable of the localized pushforward is \begin{align*} \widehat{\alpha F_*v}(\eta) = v(a e_\eta). \end{align*} Indeed, the cutoff $\beta$ equals $1$ on the part of $\operatorname{supp}v$ over $\operatorname{supp}\alpha$, so inserting $\beta$ does not change the action of $v$ on $\alpha(y)e^{-iy\cdot\eta}$. Since \begin{align*} e_\eta(y,z)=e^{-i(y,z)\cdot(\eta,0)}, \end{align*} the quantity $v(ae_\eta)$ is precisely the localized Fourier transform of $v$ tested at the lifted covector $(\eta,0)$. [/step]

[step:Extract uniform rapid decay from absence of lifted wave front directions]Define \begin{align*} R := \{(F(x),\eta)\in T^*Y\setminus\{0\}: x\in\operatorname{supp}u,\ (x,dF_x^*\eta)\in\operatorname{WF}(u)\}. \end{align*} We first record the local closedness of $R$ near $(y_0,\eta_0)$. Let $Q\subset Y$ be a compact neighbourhood of $y_0$. Properness of $F|_{\operatorname{supp}u}$ implies that \begin{align*} K_Q:=\operatorname{supp}u\cap F^{-1}(Q) \end{align*} is compact. If $(F(x_k),\eta_k)$ is a sequence in $R$ with $F(x_k)\in Q$ and $(F(x_k),\eta_k)\to(y,\eta)$ in $T^*Y\setminus\{0\}$, then $x_k\in K_Q$. Passing to a subsequence, $x_k\to x\in K_Q$, and continuity of $F$ gives $F(x)=y$. The bundle map \begin{align*} (x,\eta)\mapsto (x,dF_x^*\eta) \end{align*} from $F^*(T^*Y)$ to $T^*X$ is continuous. We also use the closedness theorem for wave front sets: for any distribution, its wave front set is a closed conic subset of the punctured cotangent bundle. Applied to $u$, this gives that $\operatorname{WF}(u)$ is closed conic in $T^*X\setminus\{0\}$. Since $F$ is a submersion, $dF_x^*$ is injective for every $x$, so $dF_x^*\eta\neq 0$ whenever $\eta\neq 0$. Hence $(x,dF_x^*\eta)\in\operatorname{WF}(u)$, and $(y,\eta)\in R$. Thus $R\cap T^*Q$ is closed in $T^*Q\setminus\{0\}$. Because $(y_0,\eta_0)\notin R$, this local closedness allows us to shrink the support of $\alpha$ around $y_0$ and choose a conic neighbourhood $\Gamma_0\subset\mathbb{R}^m\setminus\{0\}$ of $\eta_0$ such that no covector in $R$ lies over $\operatorname{supp}\alpha$ with coordinate covector in $\Gamma_0$. In the projection chart this means that, for every point $(y,z)$ in \begin{align*} L:=\operatorname{supp}v\cap(\operatorname{supp}\alpha\times\operatorname{supp}\beta) \end{align*} and every $\eta\in\Gamma_0$, one has \begin{align*} ((y,z),(\eta,0))\notin\operatorname{WF}(v). \end{align*} Since $a$ is supported in $\operatorname{supp}\alpha\times\operatorname{supp}\beta$, the wave front set of $av$ is contained in the portion of $\operatorname{WF}(v)$ over this set. Therefore no covector of the form $((y,z),(\eta,0))$ with $(y,z)\in\operatorname{supp}a$ and $\eta\in\Gamma_0$ belongs to $\operatorname{WF}(av)$. We now enlarge this exact-direction exclusion to the full conic neighbourhood required by the Fourier characterization. Choose an open conic neighbourhood $\Gamma\subset\mathbb{R}^m\setminus\{0\}$ of $\eta_0$ whose angular closure \begin{align*} \overline{\Gamma\cap S^{m-1}} \end{align*} is contained in $\Gamma_0\cap S^{m-1}$, where $S^{m-1}:=\{\eta\in\mathbb{R}^m:|\eta|=1\}$. Define the compact angular set \begin{align*} A:=\{((y,z),(\eta,0)): (y,z)\in\operatorname{supp}a,\ \eta\in\overline{\Gamma\cap S^{m-1}}\}. \end{align*} The set $A$ is compact in the cosphere bundle over $\operatorname{supp}a$, and the preceding exclusion shows that $A\cap\operatorname{WF}(av)=\varnothing$. Since $\operatorname{WF}(av)$ is closed in the punctured cotangent bundle, there exists an open conic neighbourhood $\Omega\subset(\mathbb{R}^{m+n-m})^*\setminus\{0\}$ of the lifted directions $\{(\eta,0):\eta\in\Gamma\}$ such that \begin{align*} \operatorname{WF}(av)\cap(\operatorname{supp}a\times\Omega)=\varnothing. \end{align*} We now apply the Fourier characterization of the wave front set to the compactly supported distribution $av$. Its hypotheses are satisfied because $av$ is compactly supported, $\operatorname{supp}(av)\subset\operatorname{supp}a$, and the open conic set $\Omega$ satisfies \begin{align*} \operatorname{WF}(av)\cap(\operatorname{supp}(av)\times\Omega)=\varnothing. \end{align*} Therefore, for every integer $N\geq 0$, there is a constant $C_N>0$ such that \begin{align*} |v(ae_\eta)| \leq C_N(1+|\eta|)^{-N} \end{align*} for every $\eta \in \Gamma$, because $(\eta,0)\in\Omega$ for all $\eta\in\Gamma$. Using the identity from the previous step, \begin{align*} |\widehat{\alpha F_*v}(\eta)| \leq C_N(1+|\eta|)^{-N} \end{align*} for every $\eta \in \Gamma$ and every $N\geq 0$. This is precisely the Fourier decay condition excluding $(y_0,\eta_0)$ from the wave front set of the localized pushforward.[/step]

[guided]The point of this step is to justify a uniform cone of rapid decay over the whole compact fibre portion. Define the projected microlocal relation \begin{align*} R := \{(F(x),\eta)\in T^*Y\setminus\{0\}: x\in\operatorname{supp}u,\ (x,dF_x^*\eta)\in\operatorname{WF}(u)\}. \end{align*} The hypothesis says that $(y_0,\eta_0)$ is not in $R$. To turn this single exclusion into a neighbourhood exclusion, we prove that $R$ is closed near $y_0$. Let $Q\subset Y$ be a compact neighbourhood of $y_0$, and set \begin{align*} K_Q:=\operatorname{supp}u\cap F^{-1}(Q). \end{align*} Because $F|_{\operatorname{supp}u}$ is proper, $K_Q$ is compact. Suppose $(F(x_k),\eta_k)$ is a sequence in $R$ with $F(x_k)\in Q$ and $(F(x_k),\eta_k)\to(y,\eta)$ in $T^*Y\setminus\{0\}$. Then $x_k\in K_Q$, so compactness gives a subsequence with $x_k\to x\in K_Q$. Continuity of $F$ gives $F(x)=y$. Now use the closedness theorem for wave front sets: the wave front set of any distribution is a closed conic subset of the punctured cotangent bundle. The map \begin{align*} (x,\eta)\mapsto (x,dF_x^*\eta) \end{align*} from the pulled-back cotangent bundle $F^*(T^*Y)$ to $T^*X$ is continuous because $F$ is smooth. For every $k$, the covector $(x_k,dF_{x_k}^*\eta_k)$ lies in $\operatorname{WF}(u)$. Taking the limit gives $(x,dF_x^*\eta)\in\operatorname{WF}(u)$, since $\operatorname{WF}(u)$ is closed in $T^*X\setminus\{0\}$. The limiting covector is nonzero: $\eta\neq0$, and $F$ is a submersion, so $dF_x^*$ is injective. Therefore $(y,\eta)\in R$. This proves that $R\cap T^*Q$ is closed in $T^*Q\setminus\{0\}$. Since $(y_0,η_0)\notin R$, closedness lets us shrink the base cutoff $\alpha$ around $y_0$ and choose a conic neighbourhood $\Gamma_0\subset\mathbb{R}^m\setminus\{0\}$ of $\eta_0$ so that no element of $R$ lies over $\operatorname{supp}\alpha$ with coordinate covector in $\Gamma_0$. In the projection coordinates, the relevant lifted covectors are exactly \begin{align*} (\eta,0)\in\mathbb{R}^m_\eta\times\mathbb{R}^{n-m}_\zeta. \end{align*} Thus, for the compact set \begin{align*} L:=\operatorname{supp}v\cap(\operatorname{supp}\alpha\times\operatorname{supp}\beta), \end{align*} we have \begin{align*} ((y,z),(\eta,0))\notin\operatorname{WF}(v) \end{align*} for every $(y,z)\in L$ and every $\eta\in\Gamma_0$. The amplitude $a$ is supported in $\operatorname{supp}\alpha\times\operatorname{supp}\beta$, so multiplying by $a$ cannot create wave front directions away from this support. Hence no covector of the form $((y,z),(\eta,0))$ with $(y,z)\in\operatorname{supp}a$ and $\eta\in\Gamma_0$ belongs to $\operatorname{WF}(av)$. There is one more point to check before invoking the Fourier characterization: that theorem requires an open conic neighbourhood in all covector variables, not merely exclusion of the exact line of covectors $(\eta,0)$. Choose an open conic neighbourhood $\Gamma\subset\mathbb{R}^m\setminus\{0\}$ of $\eta_0$ such that the angular closure \begin{align*} \overline{\Gamma\cap S^{m-1}} \end{align*} is contained in $\Gamma_0\cap S^{m-1}$, where $S^{m-1}:=\{\eta\in\mathbb{R}^m:|\eta|=1\}$. Now define \begin{align*} A:=\{((y,z),(\eta,0)): (y,z)\in\operatorname{supp}a,\ \eta\in\overline{\Gamma\cap S^{m-1}}\}. \end{align*} This set is compact: $\operatorname{supp}a$ is compact, and $\overline{\Gamma\cap S^{m-1}}$ is a closed subset of the compact sphere $S^{m-1}$. The exact-direction exclusion says $A\cap\operatorname{WF}(av)=\varnothing$. Since $\operatorname{WF}(av)$ is closed in the punctured cotangent bundle, the compact set $A$ has an open neighbourhood in the cosphere bundle disjoint from $\operatorname{WF}(av)$. Taking its conic saturation gives an open conic set $\Omega\subset(\mathbb{R}^{m+n-m})^*\setminus\{0\}$ containing every lifted covector $(\eta,0)$ with $\eta\in\Gamma$ and satisfying \begin{align*} \operatorname{WF}(av)\cap(\operatorname{supp}a\times\Omega)=\varnothing. \end{align*} This is the full neighbourhood condition required by the Fourier characterization of the wave front set. Applying that characterization to the compactly supported distribution $av$ is legitimate because $\operatorname{supp}(av)\subset\operatorname{supp}a$ and \begin{align*} \operatorname{WF}(av)\cap(\operatorname{supp}(av)\times\Omega)=\varnothing. \end{align*} It gives: for every integer $N\geq0$, there exists a constant $C_N>0$ such that \begin{align*} |v(ae_\eta)|\leq C_N(1+|\eta|)^{-N} \end{align*} for all $\eta\in\Gamma$, because $(\eta,0)\in\Omega$ for every $\eta\in\Gamma$. The previous step identified this expression with the Fourier transform of the localized pushforward: \begin{align*} \widehat{\alpha F_*v}(\eta)=v(ae_\eta). \end{align*} Therefore \begin{align*} |\widehat{\alpha F_*v}(\eta)|\leq C_N(1+|\eta|)^{-N} \end{align*} for every $\eta\in\Gamma$ and every integer $N\geq0$. This rapid decay proves that $(y_0,\eta_0)$ is not in the wave front set of the localized pushforward.[/guided]

[step:Assemble the finite local estimates and conclude the inclusion] The compact set \begin{align*} K=\operatorname{supp}u\cap F^{-1}(\operatorname{supp}\psi) \end{align*} was covered by finitely many submersion charts, and the corresponding [partition of unity](/page/Partition%20of%20Unity) decomposes the localized pushforward into finitely many terms. For each term, the preceding projection-model argument gives a conic neighbourhood of $\eta_0$ and rapid decay of every order. Intersecting finitely many resulting conic neighbourhoods gives a conic neighbourhood $\Gamma_*$ of $\eta_0$, and summing finitely many estimates gives constants $C_N'>0$ such that \begin{align*} |\widehat{\psi F_*u}(\eta)| \leq C_N'(1+|\eta|)^{-N} \end{align*} for all $\eta\in\Gamma_*$ and all integers $N\geq 0$. By the Fourier characterization of the wave front set, this proves \begin{align*} (y_0,\eta_0)\notin \operatorname{WF}(F_*u). \end{align*} Since every covector outside the right-hand side of the asserted inclusion is absent from $\operatorname{WF}(F_*u)$, we obtain \begin{align*} \operatorname{WF}(F_*u)\subset \{(F(x), \eta)\in T^*Y\setminus\{0\}: x\in X,\ \eta\in T^*_{F(x)}Y\setminus\{0\},\ (x,dF_x^*\eta)\in\operatorname{WF}(u)\}. \end{align*} This completes the proof. [/step]