[proofplan] We first shrink the spatial region from $V$ to an open neighbourhood $W$ of $K$ whose closure stays inside the elliptic set. On this region, ellipticity gives a symbolic inverse to the principal symbol, and the standard symbolic composition formula lets us correct it recursively to all orders. Borel summation realizes the resulting formal inverse as an actual symbol $q \in S^{-m}$, whose quantization has smoothing left and right composition errors after localization inside $W$. Finally, we cut off the Schwartz kernel away from the diagonal to make the parametrix properly supported; this does not affect any localized expression $\chi(\cdot)\psi$ because $\psi=1$ near $\operatorname{supp}\chi$. [/proofplan] [step:Choose a neighbourhood of $K$ contained in the elliptic region] Since $K \subset V$ is compact and $V \subset \mathbb{R}^n$ is open, choose $\rho>0$ such that \begin{align*} \{x \in \mathbb{R}^n : \operatorname{dist}(x,K) \leq 3\rho\} \subset V. \end{align*} Define \begin{align*} W := \{x \in \mathbb{R}^n : \operatorname{dist}(x,K) < \rho\}. \end{align*} Then $W$ is open, $K \subset W$, and \begin{align*} \overline{W} \subset \{x \in \mathbb{R}^n : \operatorname{dist}(x,K) \leq \rho\} \subset V. \end{align*} Choose a cutoff function $\theta \in C_c^\infty(V)$ such that $\theta=1$ on an open neighbourhood of $\overline{W}$. [guided] The ellipticity assumption is only available over $V$, so the first task is to localize strictly inside $V$. Because $K$ is compact and $V$ is open, the distance from $K$ to the [closed set](/page/Closed%20Set) $\mathbb{R}^n \setminus V$ is positive. Thus we may choose $\rho>0$ so small that the closed $3\rho$-neighbourhood of $K$ is still contained in $V$: \begin{align*} \{x \in \mathbb{R}^n : \operatorname{dist}(x,K) \leq 3\rho\} \subset V. \end{align*} We then set \begin{align*} W := \{x \in \mathbb{R}^n : \operatorname{dist}(x,K) < \rho\}. \end{align*} This gives an open neighbourhood of $K$, and its closure lies in the closed $\rho$-neighbourhood of $K$, hence in $V$. The extra room between $\rho$ and $3\rho$ is used only for cutoffs. Since $\overline{W}$ is closed in a compact neighbourhood contained in $V$, the smooth Urysohn cutoff construction gives $\theta \in C_c^\infty(V)$ with $\theta=1$ on an open neighbourhood of $\overline{W}$. This cutoff ensures that every symbol we construct is supported in the spatial region where ellipticity is valid. [/guided] [/step] [step:Construct the leading inverse symbol on the elliptic region] Fix the Kohn-Nirenberg quantization convention on $U$, and let $p \in S^m_{\mathrm{cl}}(U \times \mathbb{R}^n)$ denote the corresponding full classical symbol of $P$, with principal homogeneous component $p_m$. With this convention, $a \# b$ denotes the symbol of $\operatorname{Op}(a)\operatorname{Op}(b)$ modulo smoothing terms. Define the leading homogeneous inverse symbol \begin{align*} q_{-m}: U \times (\mathbb{R}^n \setminus \{0\}) \to \mathbb{C} \end{align*} by \begin{align*} q_{-m}(x,\xi) := \theta(x)p_m(x,\xi)^{-1}. \end{align*} Since $p_m(x,\xi)\neq 0$ for $x \in \operatorname{supp}\theta \subset V$ and $\xi \neq 0$, the definition is meaningful. Homogeneity of $p_m$ in $\xi$ gives that $q_{-m}$ is smooth and homogeneous of degree $-m$ on $U\times(\mathbb{R}^n\setminus\{0\})$. Moreover, on a neighbourhood of $\overline{W}$ and for every $\xi\neq 0$, \begin{align*} q_{-m}(x,\xi)p_m(x,\xi)=1 \end{align*} and \begin{align*} p_m(x,\xi)q_{-m}(x,\xi)=1. \end{align*} [/step] [step:Construct separate right and left formal inverses] We use the standard symbolic composition theorem for classical pseudodifferential operators in the fixed Kohn-Nirenberg convention: if $a \in S^{r}_{\mathrm{cl}}(U \times \mathbb{R}^n)$ and $b \in S^{s}_{\mathrm{cl}}(U \times \mathbb{R}^n)$, then $a \# b \in S^{r+s}_{\mathrm{cl}}(U \times \mathbb{R}^n)$ has an asymptotic expansion whose homogeneous component of degree $r+s-\ell$ is a finite sum of derivatives of the homogeneous components of $a$ and $b$ with total differentiation order at most $\ell$. We use this theorem only in local coordinate form on the [open set](/page/Open%20Set) $U \subset \mathbb{R}^n$, and its hypotheses are met because all symbols under consideration are classical symbols on $U \times \mathbb{R}^n$. Construct first a right formal inverse. Starting from $q^{R}_{-m}:=q_{-m}$, choose homogeneous symbols \begin{align*} q^{R}_{-m-j}: U \times (\mathbb{R}^n \setminus \{0\}) \to \mathbb{C} \end{align*} of degree $-m-j$ for $j \geq 1$. Suppose $q^{R}_{-m},\dots,q^{R}_{-m-j+1}$ have been chosen so that the formal product \begin{align*} \left(\sum_{k=0}^{j-1}q^{R}_{-m-k}\right) \# p \end{align*} has homogeneous components equal to $1$ through order $-j+1$ on an open neighbourhood of $\overline{W}$. Let $e^{R}_{-j}: U \times (\mathbb{R}^n \setminus \{0\}) \to \mathbb{C}$ denote the resulting homogeneous order $-j$ error on that neighbourhood. Choose a cutoff $\theta_j \in C_c^\infty(V)$ equal to $1$ on an open neighbourhood of $\overline{W}$, and define near $\overline{W}$ \begin{align*} q^{R}_{-m-j}(x,\xi) := -\theta_j(x)e^{R}_{-j}(x,\xi)p_m(x,\xi)^{-1}. \end{align*} Since the contribution of the new term to order $-j$ in $q^{R}\#p$ is $q^{R}_{-m-j}p_m$, this cancels $e^{R}_{-j}$ on the neighbourhood where $\theta_j=1$. Away from that neighbourhood, extend $q^{R}_{-m-j}$ by the same displayed formula with the cutoff factor $\theta_j$; because $\theta_j$ is smooth and compactly supported in $V$, and because $p_m^{-1}$ is smooth and homogeneous of degree $-m$ on $\operatorname{supp}\theta_j \times (\mathbb{R}^n \setminus \{0\})$, the extension is a globally defined homogeneous classical symbol on $U \times (\mathbb{R}^n \setminus \{0\})$. Construct independently a left formal inverse. Starting from $q^{L}_{-m}:=q_{-m}$, choose homogeneous symbols $q^{L}_{-m-j}$ so that $p\#q^{L}_{\mathrm{formal}}\sim 1$ near $\overline{W}$. At the $j$th stage, if $e^{L}_{-j}$ is the order $-j$ error in $p\#q^{L}$, set \begin{align*} q^{L}_{-m-j}(x,\xi) := -\theta_j(x)p_m(x,\xi)^{-1}e^{L}_{-j}(x,\xi) \end{align*} near $\overline{W}$. The new term contributes $p_mq^{L}_{-m-j}$ to order $-j$, so it cancels the left error. As in the right construction, the cutoff formula extends $q^{L}_{-m-j}$ to a globally defined homogeneous classical symbol on $U \times (\mathbb{R}^n \setminus \{0\})$. Thus the two formal symbols \begin{align*} q^{R}_{\mathrm{formal}} \sim \sum_{j=0}^{\infty} q^{R}_{-m-j} \end{align*} and \begin{align*} q^{L}_{\mathrm{formal}} \sim \sum_{j=0}^{\infty} q^{L}_{-m-j} \end{align*} satisfy \begin{align*} q^{R}_{\mathrm{formal}} \# p \sim 1 \end{align*} and \begin{align*} p \# q^{L}_{\mathrm{formal}} \sim 1 \end{align*} on an open neighbourhood of $\overline{W}$, modulo $S^{-\infty}$. [guided] The symbolic product is not commutative, so we do not try to prove that one recursive correction simultaneously cancels the right and left errors. Instead we build two formal inverses, one for each side, and later prove that they differ only by a smoothing symbol after localization. For the right inverse, define $q^{R}_{-m}:=q_{-m}$. The principal part has already arranged \begin{align*} q^{R}_{-m}(x,\xi)p_m(x,\xi)=1 \end{align*} near $\overline{W}$ for $|\xi|\geq 2$. Suppose now that $q^{R}_{-m},\dots,q^{R}_{-m-j+1}$ have been chosen. The symbolic composition formula says that the homogeneous order $-j$ component of \begin{align*} \left(\sum_{k=0}^{j-1}q^{R}_{-m-k}\right) \# p \end{align*} is determined by the already chosen terms and the full symbol $p$. Call the order $-j$ error $e^{R}_{-j}$. Since $p_m(x,\xi)\neq 0$ for $x\in V$ and $\xi\neq 0$, multiplication by $p_m(x,\xi)^{-1}$ is legitimate on the cutoff region. Choose $\theta_j \in C_c^\infty(V)$ equal to $1$ near $\overline{W}$ and set \begin{align*} q^{R}_{-m-j}(x,\xi) := -\theta_j(x)e^{R}_{-j}(x,\xi)p_m(x,\xi)^{-1}. \end{align*} The only contribution of this new term to the order $-j$ part of $q^{R}\#p$ is $q^{R}_{-m-j}p_m$, because all differentiated contributions have lower order. On the region where $\theta_j=1$, this contribution equals $-e^{R}_{-j}$, so the order $-j$ right error is cancelled. The left inverse is constructed separately because the order $-j$ error in $p\#q$ need not equal the order $-j$ error in $q\#p$. Define $q^{L}_{-m}:=q_{-m}$. If $e^{L}_{-j}$ is the order $-j$ error in $p\#q^{L}$ after the previous corrections, define \begin{align*} q^{L}_{-m-j}(x,\xi) := -\theta_j(x)p_m(x,\xi)^{-1}e^{L}_{-j}(x,\xi) \end{align*} near $\overline{W}$. The new term contributes $p_mq^{L}_{-m-j}$ to the order $-j$ part of $p\#q^{L}$, and this equals $-e^{L}_{-j}$ where $\theta_j=1$. Thus the left error is cancelled independently. Repeating these two recursions for every $j\geq 1$ gives formal classical symbols \begin{align*} q^{R}_{\mathrm{formal}} \sim \sum_{j=0}^{\infty} q^{R}_{-m-j} \end{align*} and \begin{align*} q^{L}_{\mathrm{formal}} \sim \sum_{j=0}^{\infty} q^{L}_{-m-j} \end{align*} with \begin{align*} q^{R}_{\mathrm{formal}} \# p \sim 1 \end{align*} and \begin{align*} p \# q^{L}_{\mathrm{formal}} \sim 1 \end{align*} on an open neighbourhood of $\overline{W}$, modulo rapidly decreasing symbols. [/guided] [/step] [step:Realize the formal inverses and compare them] By Borel summation for classical symbols, choose symbols $q_R,q_L \in S^{-m}_{\mathrm{cl}}(U \times \mathbb{R}^n)$ such that \begin{align*} q_R \sim \sum_{j=0}^{\infty} q^{R}_{-m-j} \end{align*} and \begin{align*} q_L \sim \sum_{j=0}^{\infty} q^{L}_{-m-j} \end{align*} in the classical symbol sense. Let \begin{align*} Q_R := \operatorname{Op}(q_R): C_c^\infty(U) \to C^\infty(U) \end{align*} and \begin{align*} Q_L := \operatorname{Op}(q_L): C_c^\infty(U) \to C^\infty(U) \end{align*} be the corresponding pseudodifferential operators. There is an open set $N$ with $\overline{W}\subset N\subset V$ such that the symbols of $Q_RP-I$ and $PQ_L-I$ belong to $S^{-\infty}(N\times\mathbb{R}^n)$. This follows from the preceding formal equations and the symbolic composition formula, because equality of all homogeneous components on $N$ is precisely the statement that the remainder is rapidly decreasing in $\xi$ with all derivatives on compact subsets of $N$. Now fix $\chi,\psi\in C_c^\infty(W)$ with $\psi=1$ on an open neighbourhood of $\operatorname{supp}\chi$. Choose $\eta\in C_c^\infty(N)$ such that $\eta=1$ on an open neighbourhood of $\operatorname{supp}\chi\cup\operatorname{supp}\psi$. The rapidly decreasing-symbol smoothing theorem applies to $\eta(Q_RP-I)\eta$ and $\eta(PQ_L-I)\eta$, because their full symbols lie in $S^{-\infty}(N\times\mathbb{R}^n)$. Hence \begin{align*} \chi(Q_RP-I)\psi \in \Psi^{-\infty}(U) \end{align*} and \begin{align*} \chi(PQ_L-I)\psi \in \Psi^{-\infty}(U). \end{align*} The same symbolic identities imply that $Q_R-Q_L$ is microlocally smoothing on $N$. Indeed, using associativity of the symbolic product modulo $S^{-\infty}(N\times\mathbb{R}^n)$, \begin{align*} q_R-q_L \equiv q_R\#p\#q_L-q_R\#p\#q_L \equiv 0 \pmod{S^{-\infty}(N\times\mathbb{R}^n)}, \end{align*} where the first replacement uses $p\#q_L\equiv 1$ and the second uses $q_R\#p\equiv 1$ on $N$. Therefore \begin{align*} \chi(Q_R-Q_L)\psi \in \Psi^{-\infty}(U). \end{align*} Consequently, \begin{align*} \chi(PQ_R-I)\psi = \chi(PQ_L-I)\psi + \chi P(Q_R-Q_L)\psi \in \Psi^{-\infty}(U), \end{align*} because composition of a pseudodifferential operator with a smoothing operator is smoothing. Set $Q_0:=Q_R$. Then both localized remainders \begin{align*} \chi(Q_0P-I)\psi \in \Psi^{-\infty}(U) \end{align*} and \begin{align*} \chi(PQ_0-I)\psi \in \Psi^{-\infty}(U) \end{align*} are smoothing. [guided] Borel summation is the passage from a formal asymptotic symbol to an actual symbol. We apply the Borel summation theorem for classical symbols to the two formal sequences already constructed. Its hypotheses are exactly that the terms are homogeneous classical symbols of orders $-m-j$, and this was established in the recursive construction, including the cutoff extension away from $\overline{W}$. Hence there exist $q_R,q_L \in S^{-m}_{\mathrm{cl}}(U \times \mathbb{R}^n)$ with \begin{align*} q_R \sim \sum_{j=0}^{\infty} q^{R}_{-m-j} \end{align*} and \begin{align*} q_L \sim \sum_{j=0}^{\infty} q^{L}_{-m-j}. \end{align*} Define \begin{align*} Q_R := \operatorname{Op}(q_R): C_c^\infty(U) \to C^\infty(U) \end{align*} and \begin{align*} Q_L := \operatorname{Op}(q_L): C_c^\infty(U) \to C^\infty(U). \end{align*} Because every homogeneous component of $q_R \# p-1$ vanishes on some open neighbourhood of $\overline{W}$, after shrinking to a single open set $N$ with $\overline{W}\subset N\subset V$, the full symbol of $Q_RP-I$ belongs to $S^{-\infty}(N\times\mathbb{R}^n)$. The same argument gives that the full symbol of $PQ_L-I$ belongs to $S^{-\infty}(N\times\mathbb{R}^n)$. Fix $\chi,\psi\in C_c^\infty(W)$ with $\psi=1$ near $\operatorname{supp}\chi$, and choose $\eta\in C_c^\infty(N)$ equal to $1$ on an open neighbourhood of $\operatorname{supp}\chi\cup\operatorname{supp}\psi$. The rapidly decreasing-symbol smoothing theorem applies to the localized operators $\eta(Q_RP-I)\eta$ and $\eta(PQ_L-I)\eta$, because their full symbols are rapidly decreasing in $\xi$ with all derivatives on the spatial support of $\eta$. Since multiplication by $\chi$ and $\psi$ only restricts these localized smoothing operators further, we obtain \begin{align*} \chi(Q_RP-I)\psi \in \Psi^{-\infty}(U) \end{align*} and \begin{align*} \chi(PQ_L-I)\psi \in \Psi^{-\infty}(U). \end{align*} It remains to show that the right inverse also works on the left. The symbolic product is associative modulo $S^{-\infty}(N\times\mathbb{R}^n)$. Since $q_R\#p\equiv 1$ and $p\#q_L\equiv 1$ modulo $S^{-\infty}(N\times\mathbb{R}^n)$, we have \begin{align*} q_R-q_L \equiv q_R\#(p\#q_L)-(q_R\#p)\#q_L \equiv 0 \pmod{S^{-\infty}(N\times\mathbb{R}^n)}. \end{align*} Thus the full symbol of $Q_R-Q_L$ is rapidly decreasing on $N$, and the same cutoff argument with $\eta$ gives \begin{align*} \chi(Q_R-Q_L)\psi \in \Psi^{-\infty}(U). \end{align*} Finally, \begin{align*} \chi(PQ_R-I)\psi = \chi(PQ_L-I)\psi + \chi P(Q_R-Q_L)\psi. \end{align*} Both terms on the right are smoothing, because composition of a pseudodifferential operator with a smoothing operator is smoothing. Hence $Q_0:=Q_R$ has both localized smoothing remainders. [/guided] [/step] [step:Modify the kernel to make the parametrix properly supported] Let $K_{Q_0}$ denote the Schwartz kernel of $Q_0$ on $U \times U$. Choose a locally finite exhaustion of $U$ by relatively compact open sets $U_j\Subset U_{j+1}$, and choose an open neighbourhood $G\subset U\times U$ of the diagonal such that, for each $j$, the set $G\cap (\overline{U_j}\times U)$ is contained in $\overline{U_{j+1}}\times\overline{U_{j+1}}$ and the analogous containment holds after interchanging the two factors. By the smooth Urysohn lemma, choose $\omega \in C^\infty(U \times U;[0,1])$ such that $\omega=1$ on a smaller open neighbourhood of the diagonal and $\operatorname{supp}\omega\subset G$. Then both coordinate projections are proper on $\operatorname{supp}\omega$. Define \begin{align*} \Delta_U := \{(x,x) : x \in U\}. \end{align*} Define $Q$ to be the operator with Schwartz kernel \begin{align*} K_Q(x,y) := \omega(x,y)K_{Q_0}(x,y). \end{align*} The standard proper-support modification theorem for pseudodifferential kernels applies because $\omega$ is smooth, equals $1$ near $\Delta_U$, and has support on which both coordinate projections are proper. Hence $Q$ is properly supported and $Q \in \Psi^{-m}(U)$. The operator $R:=Q-Q_0$ has Schwartz kernel \begin{align*} K_R(x,y) := -(1-\omega(x,y))K_{Q_0}(x,y). \end{align*} Since $K_{Q_0}$ is smooth off $\Delta_U$ and $1-\omega$ vanishes on an open neighbourhood of $\Delta_U$, $K_R$ is a smooth function on $U\times U$. Now fix $\chi,\psi \in C_c^\infty(W)$ with $\psi=1$ on a neighbourhood of $\operatorname{supp}\chi$. Because $P$ is properly supported and $\operatorname{supp}\psi$ is compact, the set \begin{align*} C_1 := \operatorname{proj}_1\bigl(\operatorname{supp}K_P \cap (U\times \operatorname{supp}\psi)\bigr) \end{align*} is compact in $U$, where $K_P$ denotes the Schwartz kernel of $P$ and $\operatorname{proj}_1:U\times U\to U$ is projection onto the first factor. The kernel of $\chi R P\psi$ is obtained by integrating the smooth kernel $\chi(x)K_R(x,z)$ against the compactly supported distribution kernel $K_P(z,y)\psi(y)$ with $z\in C_1$; the standard composition theorem for a smoothing kernel with a properly supported pseudodifferential kernel therefore gives \begin{align*} \chi(Q-Q_0)P\psi \in \Psi^{-\infty}(U). \end{align*} Similarly, because $\operatorname{supp}\psi$ is compact and $K_R$ is smooth, the localized operator $R\psi$ has a smooth kernel with compact support in the input variable. Composing on the left with the properly supported pseudodifferential operator $\chi P$ gives \begin{align*} \chi P(Q-Q_0)\psi \in \Psi^{-\infty}(U). \end{align*} Combining these two smoothing errors with the already proved smoothing remainders for $Q_0$ yields \begin{align*} \chi(QP-I)\psi \in \Psi^{-\infty}(U) \end{align*} and \begin{align*} \chi(PQ-I)\psi \in \Psi^{-\infty}(U). \end{align*} [guided] The purpose of this step is not to improve the symbolic inverse; it is only to make the operator properly supported. Let $K_{Q_0}$ be the Schwartz kernel of $Q_0$. We choose a smooth cutoff $\omega:U\times U\to[0,1]$ that equals $1$ on an open neighbourhood of the diagonal \begin{align*} \Delta_U := \{(x,x):x\in U\} \end{align*} and whose support has proper coordinate projections. Such a cutoff is obtained by taking a locally finite exhaustion $U_j\Subset U_{j+1}$, choosing a neighbourhood $G$ of the diagonal whose intersection with $\overline{U_j}\times U$ and with $U\times\overline{U_j}$ lies in $\overline{U_{j+1}}\times\overline{U_{j+1}}$, and then applying the smooth Urysohn lemma to place $\operatorname{supp}\omega$ inside $G$. Define $Q$ by the kernel formula \begin{align*} K_Q(x,y) := \omega(x,y)K_{Q_0}(x,y). \end{align*} Because $\omega=1$ near the diagonal, this multiplication does not change the conormal singularity of the pseudodifferential kernel near $\Delta_U$; because $\operatorname{supp}\omega$ has proper coordinate projections, the resulting operator is properly supported. Thus the proper-support modification theorem gives $Q\in\Psi^{-m}(U)$. Now we check that this modification does not spoil the localized parametrix identities. Put $R:=Q-Q_0$. Its kernel is \begin{align*} K_R(x,y) := -(1-\omega(x,y))K_{Q_0}(x,y). \end{align*} The kernel $K_{Q_0}$ is smooth away from the diagonal, while $1-\omega$ is zero near the diagonal. Hence $K_R$ is smooth on all of $U\times U$. This is the key support point: no singularity remains after the cutoff. Fix $\chi,\psi\in C_c^\infty(W)$ with $\psi=1$ near $\operatorname{supp}\chi$. Since $P$ is properly supported and $\operatorname{supp}\psi$ is compact, the part of the $P$-kernel that can interact with $\psi$ has compact projection in the output variable. Therefore composing the smooth kernel $\chi K_R$ with $P\psi$ gives a smoothing operator: \begin{align*} \chi(Q-Q_0)P\psi \in \Psi^{-\infty}(U). \end{align*} The same reasoning applies to $\chi P(Q-Q_0)\psi$: first $R\psi$ has smooth localized kernel, and then proper support of $P$ makes the composition well-defined and smoothing. Thus \begin{align*} \chi P(Q-Q_0)\psi \in \Psi^{-\infty}(U). \end{align*} Adding these smoothing errors to the already established identities for $Q_0$ gives the two desired identities for $Q$. [/guided] [/step] [step:Conclude that $Q$ is a two-sided microlocal parametrix over $K$] The open set $W$ satisfies \begin{align*} K \subset W \subset \overline{W} \subset V, \end{align*} and the operator $Q$ is properly supported with $Q \in \Psi^{-m}(U)$. The preceding step proves that for every $\chi,\psi \in C_c^\infty(W)$ with $\psi=1$ on a neighbourhood of $\operatorname{supp}\chi$, \begin{align*} \chi(QP-I)\psi \in \Psi^{-\infty}(U) \end{align*} and \begin{align*} \chi(PQ-I)\psi \in \Psi^{-\infty}(U). \end{align*} This is precisely the asserted two-sided localized parametrix property, and therefore $Q$ is a microlocal parametrix for $P$ over $K$. [guided] We now collect the objects constructed above. The set $W$ was chosen so that \begin{align*} K \subset W \subset \overline{W} \subset V. \end{align*} The operator $Q$ was obtained from $Q_0$ by the proper-support kernel cutoff, so $Q$ is properly supported and $Q\in\Psi^{-m}(U)$. The previous step proves that every cutoff pair $\chi,\psi\in C_c^\infty(W)$ with $\psi=1$ on a neighbourhood of $\operatorname{supp}\chi$ satisfies \begin{align*} \chi(QP-I)\psi \in \Psi^{-\infty}(U) \end{align*} and \begin{align*} \chi(PQ-I)\psi \in \Psi^{-\infty}(U). \end{align*} These are exactly the two localized left and right inverse conditions required in the theorem statement, so $Q$ is a two-sided microlocal parametrix for $P$ over $K$. [/guided] [/step]