[proofplan]
We compute the lower ramification groups $G_s(L_n/K)$ by determining the Herbrand function $i_{L_n/K}(\sigma)$ for each $\sigma \in \operatorname{Gal}(L_n/K)$. Under the isomorphism $\operatorname{Gal}(L_n/K) \cong U_K/U_K^{(n)}$, a non-identity element $\sigma_u$ with $u \equiv 1 \pmod{\pi^k}$ and $u \not\equiv 1 \pmod{\pi^{k+1}}$ satisfies $i_{L_n/K}(\sigma_u) = q^k$. This is computed by analyzing the valuation of $\sigma_u(\lambda_n) - \lambda_n = [u]_F(\lambda_n) - \lambda_n$ using the formal group structure. The ramification filtration then follows by determining which $\sigma_u$ belong to $G_s$ for each $s$.
[/proofplan]
[step:Identify $G_{-1}$ and $G_0$: the full Galois group]
For $-1 \leq s \leq 0$, the ramification groups are $G_{-1} = \operatorname{Gal}(L_n/K)$ (by definition) and $G_0$ is the inertia group. Since $L_n/K$ is totally ramified (by the [Galois Group of Lubin--Tate Extensions](/theorems/2394)), the inertia group equals the full Galois group: $G_0 = \operatorname{Gal}(L_n/K)$. Hence $G_s = \operatorname{Gal}(L_n/K)$ for $-1 \leq s \leq 0$.
[/step]
[step:Compute $i_{L_n/K}(\sigma_u)$ for a non-identity element $\sigma_u$]
Let $\sigma_u \in \operatorname{Gal}(L_n/K)$ correspond to $u \in U_K/U_K^{(n)}$ via the isomorphism $\sigma_u(\lambda) = [u]_F(\lambda)$ for $\lambda \in F(n)$. Write $u = 1 + c\pi^k$ with $c \in \mathcal{O}_K^\times$ and $1 \leq k \leq n - 1$ (so $u \in U_K^{(k)} \setminus U_K^{(k+1)}$).
Fix a uniformizer $\lambda_n \in F(n) \setminus F(n-1)$ of $L_n$. The Herbrand function value is
\begin{align*}
i_{L_n/K}(\sigma_u) = v_{L_n}(\sigma_u(\lambda_n) - \lambda_n) = v_{L_n}([u]_F(\lambda_n) - \lambda_n).
\end{align*}
We compute $[u]_F(\lambda_n) - \lambda_n$ using the formal group structure. Write $[u]_F = [1 + c\pi^k]_F$. By the $\mathcal{O}_K$-module structure of $F$:
\begin{align*}
[u]_F(\lambda_n) = [1]_F(\lambda_n) +_F [c\pi^k]_F(\lambda_n) = \lambda_n +_F [c]_F([\pi^k]_F(\lambda_n)),
\end{align*}
where $+_F$ denotes the formal group addition $F_e(X, Y)$.
[guided]
The decomposition $[u]_F = [1 + c\pi^k]_F$ uses the additive property of the formal $\mathcal{O}_K$-module structure: $[a + b]_F = F_e([a]_F, [b]_F)$, which gives $[1 + c\pi^k]_F(X) = F_e([1]_F(X), [c\pi^k]_F(X)) = F_e(X, [c]_F([\pi^k]_F(X)))$.
The element $[\pi^k]_F(\lambda_n) = [\pi]_F^k(\lambda_n) = e^k(\lambda_n)$. Since $\lambda_n \in F(n) \setminus F(n-1)$, i.e., $e^n(\lambda_n) = 0$ but $e^{n-1}(\lambda_n) \neq 0$, the $k$-fold iterate gives $e^k(\lambda_n) \in F(n-k) \setminus F(n-k-1)$ (the element drops $k$ levels in the torsion filtration). So $[\pi^k]_F(\lambda_n)$ is a uniformizer of $L_{n-k}$.
[/guided]
[/step]
[step:Determine the valuation $v_{L_n}([\pi^k]_F(\lambda_n))$ and compute the result]
Since $[\pi^k]_F(\lambda_n) = e^k(\lambda_n) \in F(n-k) \setminus F(n-k-1)$, this element is a uniformizer of $L_{n-k}$. The ramification index of $L_n/L_{n-k}$ is $[L_n : L_{n-k}] = q^k$ (since both extensions are totally ramified with $[L_n : K] = q^{n-1}(q-1)$ and $[L_{n-k} : K] = q^{n-k-1}(q-1)$). Therefore
\begin{align*}
v_{L_n}([\pi^k]_F(\lambda_n)) = q^k \cdot v_{L_{n-k}}([\pi^k]_F(\lambda_n)) = q^k \cdot 1 = q^k.
\end{align*}
Now $[c]_F$ is an automorphism of $F$ (since $c \in \mathcal{O}_K^\times$), so $[c]_F([\pi^k]_F(\lambda_n))$ has the same valuation $q^k$ in $L_n$. Using the formal group law $F_e(X, Y) = X + Y + (\text{higher-order terms})$:
\begin{align*}
[u]_F(\lambda_n) - \lambda_n &= F_e(\lambda_n, [c]_F([\pi^k]_F(\lambda_n))) - \lambda_n \\
&= [c]_F([\pi^k]_F(\lambda_n)) + \lambda_n \cdot [c]_F([\pi^k]_F(\lambda_n)) \cdot G(\lambda_n, [c]_F([\pi^k]_F(\lambda_n))),
\end{align*}
where $G \in \mathcal{O}_K[[X, Y]]$ comes from $F_e(X, Y) = X + Y + XYG(X, Y)$ (which holds since $F_e(X, 0) = X$ and $F_e(0, Y) = Y$). The first term has $v_{L_n} = q^k$, and the correction term $\lambda_n \cdot [c]_F([\pi^k]_F(\lambda_n)) \cdot G(\cdots)$ has valuation $\geq 1 + q^k > q^k$. Therefore the leading term dominates:
\begin{align*}
v_{L_n}(\sigma_u(\lambda_n) - \lambda_n) = q^k.
\end{align*}
Hence $i_{L_n/K}(\sigma_u) = q^k$ when $u \in U_K^{(k)} \setminus U_K^{(k+1)}$.
[/step]
[step:Determine the ramification filtration from the Herbrand function values]
By definition, $\sigma_u \in G_s(L_n/K)$ if and only if $i_{L_n/K}(\sigma_u) \geq s + 1$, i.e., $v_{L_n}(\sigma_u(\lambda_n) - \lambda_n) \geq s + 1$. For $\sigma_u = \operatorname{id}$ (i.e., $u \in U_K^{(n)}$), the convention is $i_{L_n/K}(\operatorname{id}) = +\infty$, so $\operatorname{id} \in G_s$ for all $s$.
For $\sigma_u \neq \operatorname{id}$ with $u \in U_K^{(k)} \setminus U_K^{(k+1)}$ where $1 \leq k \leq n-1$:
\begin{align*}
\sigma_u \in G_s \iff i_{L_n/K}(\sigma_u) \geq s + 1 \iff q^k \geq s + 1 \iff s \leq q^k - 1.
\end{align*}
Therefore $\sigma_u \in G_s$ if and only if $s \leq q^k - 1$, and $\sigma_u \notin G_s$ if $s > q^k - 1$.
[guided]
Let us now assemble the full ramification filtration. For a given $s > 0$, which automorphisms $\sigma_u$ belong to $G_s$?
$\sigma_u \in G_s$ requires $i_{L_n/K}(\sigma_u) \geq s + 1$, i.e., $q^{k(u)} \geq s + 1$ where $k(u)$ is the level of $u$ in the unit filtration (meaning $u \in U_K^{(k)} \setminus U_K^{(k+1)}$). This is equivalent to $k(u) \geq \lceil \log_q(s + 1) \rceil$.
For $q^{k-1} - 1 < s \leq q^k - 1$ (where $1 \leq k \leq n-1$), the condition $q^{k(u)} \geq s + 1$ requires $k(u) \geq k$, i.e., $u \in U_K^{(k)}$. Under the isomorphism $\operatorname{Gal}(L_n/K) \cong U_K/U_K^{(n)}$, the subset of elements with $u \in U_K^{(k)}$ corresponds to $U_K^{(k)}/U_K^{(n)} \cong \operatorname{Gal}(L_n/L_k)$.
For $s > q^{n-1} - 1$, the condition $q^{k(u)} \geq s + 1 > q^{n-1}$ requires $k(u) \geq n$, i.e., $u \in U_K^{(n)}$, which means $\sigma_u = \operatorname{id}$.
[/guided]
[/step]
[step:State the ramification filtration]
Collecting the results from the previous step:
**Case $-1 \leq s \leq 0$:** $G_s = \operatorname{Gal}(L_n/K)$ (the full group, since $L_n/K$ is totally ramified).
**Case $q^{k-1} - 1 < s \leq q^k - 1$ for $1 \leq k \leq n - 1$:** $G_s = \operatorname{Gal}(L_n/L_k) \cong U_K^{(k)}/U_K^{(n)}$. This is because $\sigma_u \in G_s$ iff $u \in U_K^{(k)}$, which corresponds to $\operatorname{Gal}(L_n/L_k)$ under the Lubin--Tate isomorphism.
**Case $s > q^{n-1} - 1$:** $G_s = \{1\}$ (only the identity has $i_{L_n/K} = +\infty$).
This gives the stated formula:
\begin{align*}
G_s(L_n/K) = \begin{cases}
\operatorname{Gal}(L_n/K) & -1 \leq s \leq 0, \\
\operatorname{Gal}(L_n/L_k) & q^{k-1} - 1 < s \leq q^k - 1,\; 1 \leq k \leq n-1, \\
\{1\} & s > q^{n-1} - 1.
\end{cases}
\end{align*}
[/step]
