Hasse's bound for the local Euler factors: $|a_{p^k}(E)| \le (k+1)\,p^{k/2}$

Let $E$ be an elliptic curve over $\mathbb{Q}$ (a Weierstrass equation with rational coefficients and non-zero discriminant), and let $L(E,s) = \sum_{n\ge1} a_n n^{-s}$ be its Hasse–Weil L-series. For every prime $p$ and every integer $k \ge 0$,

Here $a_{p^k}$ is the $k$-th coefficient of the power series $1/f_p(T)$, where $f_p$ is the local polynomial of $E$ at $p$:

1. at a prime of good reduction, $f_p(T) = 1 - a_p T + pT^2$ with $a_p = p + 1 - \#\tilde E(\mathbb{F}_p)$, computed on a model of $E$ minimal at $p$;
2. at a prime of split, resp. non-split, multiplicative reduction, $f_p(T) = 1 - T$, resp. $1 + T$;
3. at a prime of additive reduction, $f_p(T) = 1$.

At primes of good reduction the case $k = 1$ is Hasse's theorem $|a_p| \le 2\sqrt p$ (Silverman, Theorem V.1.1), and the statement for all $k$ is its standard reformulation for the local Euler factor. Combined with the multiplicativity of $n \mapsto a_n$ (BSD.lFunction_isMultiplicative), it yields $|a_n| \le d(n)\sqrt n$, the bound behind the convergence of $L(E,s)$ for $\operatorname{Re} s > 3/2$ asserted in Wiles' problem description; the platform reduction of BSD.lSeriesSummable uses exactly this.

Formalization Note $a_{p^k}$ is Mathlib's WeierstrassCurve.LFunction W (p ^ k), cast from $\mathbb{Z}$ to $\mathbb{R}$; $p^{k/2}$ is written $(\sqrt p)^k$. The hypothesis IsElliptic is $\Delta \ne 0$.