Convergence of the Hasse–Weil L-series of an elliptic curve over $\mathbb{Q}$ for $\operatorname{Re} s > 3/2$ (Hasse)

Read-back

Declaration. BSD.lSeriesSummable (a theorem in the namespace BSD; it does not use BSD.IsLFunction or BSD.rank, the only two names declared by the bundle Definitions.Def_BSD).

Binders and hypotheses. The statement quantifies over:

• a Weierstrass curve $W$ over the field $\mathbb{Q}$, i.e. an arbitrary quintuple of rational numbers $(a_1, a_2, a_3, a_4, a_6)$ thought of as the equation

$$Y^2 + a_1 XY + a_3 Y = X^3 + a_2 X^2 + a_4 X + a_6;$$

• a typeclass assumption that $W$ "is elliptic", which literally means: the discriminant

$$\Delta(W) = -b_2^2 b_8 - 8 b_4^3 - 27 b_6^2 + 9 b_2 b_4 b_6$$

(with $b_2 = a_1^2 + 4a_2$, $b_4 = 2a_4 + a_1 a_3$, $b_6 = a_3^2 + 4a_6$, $b_8 = a_1^2 a_6 + 4a_2 a_6 - a_1 a_3 a_4 + a_2 a_3^2 - a_4^2$) is a unit of $\mathbb{Q}$; since $\mathbb{Q}$ is a field this is exactly $\Delta(W) \neq 0$;

• a complex number $s$;
• the hypothesis $\tfrac{3}{2} < \operatorname{Re}(s)$ (strict inequality; $\tfrac{3}{2}$ is the real number $1.5$; no condition is placed on $\operatorname{Im}(s)$).

Conclusion. Writing $L_n \in \mathbb{Z}$ for the $n$-th coefficient of the arithmetic function $W.\mathrm{LFunction}$ described below, and regarding $L_n$ as a complex number via the canonical inclusion $\mathbb{Z} \hookrightarrow \mathbb{C}$, the conclusion is that the sequence of complex numbers

$$t_n = \begin{cases} 0 & n = 0, \\[2pt] \dfrac{L_n}{n^{s}} & n \geq 1, \end{cases} \qquad (n^s = \exp(s \log n))$$

is summable as a function on $\mathbb{N}$, in the sense of unconditional convergence in $\mathbb{C}$ (for complex numbers this is equivalent to $\sum_{n \ge 1} |L_n| \, n^{-\operatorname{Re} s} < \infty$). The $n = 0$ term is defined to be $0$ regardless of $L_0$ (and in any case $L_0 = 0$, since every arithmetic function vanishes at $0$). Nothing is asserted about the value of the sum, about analytic continuation, or about convergence of any Euler product of complex numbers.

What $W.\mathrm{LFunction}$ literally is. It is an integer-valued arithmetic function (a function $\mathbb{N} \to \mathbb{Z}$ with value $0$ at $0$), defined as the formal Euler product

$$W.\mathrm{LFunction} = \prod_{\mathfrak{p}}{}^{\!\prime}\; E_{\mathfrak{p}},$$

where $\mathfrak{p}$ ranges over the "height-one spectrum" of the ring of integers $\mathcal{O}_{\mathbb{Q}}$ of $\mathbb{Q}$ regarded as a number field, i.e. over all nonzero prime ideals $\mathfrak{p} \subset \mathcal{O}_{\mathbb{Q}}$ (the abstract ring of integers of the number field $\mathbb{Q}$; it is not syntactically $\mathbb{Z}$, and its nonzero primes are not syntactically the prime numbers). The product $\prod'$ is an infinite product (tprod) taken in the following topology on arithmetic functions: give $\mathbb{Z}$ the discrete topology and arithmetic functions the induced topology of pointwise convergence; multiplication of arithmetic functions is Dirichlet convolution

$$(f * g)(n) = \sum_{d \mid n} f(d)\, g(n/d).$$

Concretely: if for every $n$ all but finitely many $E_{\mathfrak{p}}$ have $E_{\mathfrak{p}}(n) = \mathbf{1}(n)$ (where $\mathbf{1}$ is the identity arithmetic function, $\mathbf{1}(1) = 1$ and $\mathbf{1}(n) = 0$ otherwise), then the family is multipliable and $L_n$ equals the $n$-th coefficient of the finite Dirichlet-convolution product $\prod_{\mathfrak{p} \in S} E_{\mathfrak{p}}$ for every sufficiently large finite set $S$ of primes. If the family is not multipliable in this topology, the infinite product is by convention the identity arithmetic function $\mathbf{1}$, so that $L_1 = 1$ and $L_n = 0$ for all $n \ne 1$.

The local factor $E_{\mathfrak{p}}$. For each nonzero prime $\mathfrak{p}$ let $K_{\mathfrak{p}}$ be the $\mathfrak{p}$-adic completion of $\mathbb{Q}$ (the completion of $\mathbb{Q}$ with respect to the $\mathfrak{p}$-adic valuation, as a valued field with value group $\mathbb{Z}^{\mathrm{m}0}$, i.e. $\{0\} \cup \{\text{multiplicative } \mathbb{Z}\}$), let $R_{\mathfrak{p}} \subset K_{\mathfrak{p}}$ be its valuation ring (elements of valuation $\le 1$), which Mathlib equips with the structure of a discrete valuation ring with fraction field $K_{\mathfrak{p}}$, and let $k_{\mathfrak{p}} = R_{\mathfrak{p}}/\mathfrak{m}_{\mathfrak{p}}$ be its residue field. Let $W_{\mathfrak{p}}$ be the base change of $W$ to $K_{\mathfrak{p}}$ (the same five coefficients, mapped into $K_{\mathfrak{p}}$). Then $E_{\mathfrak{p}}$ is built in three steps.

1. Minimal model. $W'_{\mathfrak{p}} := (W_{\mathfrak{p}}).\mathrm{minimal}\,R_{\mathfrak{p}}$ is a chosen (via the axiom of choice) Weierstrass curve $C \cdot W_{\mathfrak{p}}$ over $K_{\mathfrak{p}}$ obtained from $W_{\mathfrak{p}}$ by some admissible change of variables $C = (u, r, s, t)$, $u \in K_{\mathfrak{p}}^\times$, such that $C \cdot W_{\mathfrak{p}}$ is integral (it equals the base change of some Weierstrass curve with coefficients in $R_{\mathfrak{p}}$) and the multiplicative valuation of its discriminant is maximal (equivalently, the additive valuation $\operatorname{ord}_{\mathfrak{p}}\Delta$ is minimal) among all such integral changes of variables. Any other minimal model would give an isomorphic curve, but the definition fixes one specific choice.

2. Local polynomial $P_{\mathfrak{p}}(T) \in \mathbb{Z}[T]$. Set

$$q_{\mathfrak{p}} := \#\, k_{\mathfrak{p}} \in \mathbb{Z}, \qquad N_{\mathfrak{p}} := \#\, \widetilde{W}'_{\mathfrak{p}}(k_{\mathfrak{p}}) \in \mathbb{Z}, \qquad a_{\mathfrak{p}} := q_{\mathfrak{p}} + 1 - N_{\mathfrak{p}},$$

where both cardinalities are Nat.card, which returns the actual cardinality for a finite type and the junk value $0$ for an infinite type. Here $\widetilde{W}'_{\mathfrak{p}}$ is the reduction: a chosen $R_{\mathfrak{p}}$-integral model of $W'_{\mathfrak{p}}$ (again via choice) with its five coefficients reduced modulo $\mathfrak{m}_{\mathfrak{p}}$ to $k_{\mathfrak{p}}$; and $\widetilde{W}'_{\mathfrak{p}}(k_{\mathfrak{p}})$ is Mathlib's type of affine nonsingular points: one distinguished "point at infinity" together with all pairs $(x, y) \in k_{\mathfrak{p}}^2$ that satisfy the Weierstrass equation and at which at least one of the two partial derivatives $a_1 y - (3x^2 + 2a_2 x + a_4)$, $2y + a_1 x + a_3$ (coefficients of the reduced curve) is nonzero. Singular points of the reduced curve are not counted. Then, with $v$ the multiplicative $\mathfrak{p}$-adic valuation on $K_{\mathfrak{p}}$ (so $v(x) = 1$ means $x$ is a unit and $v(x) < 1$ means $\operatorname{ord}_{\mathfrak{p}}(x) > 0$), and with $\Delta', c_4', a_i', b_i'$ the invariants of $W'_{\mathfrak{p}}$ (respectively of its chosen integral model $I$), the polynomial is defined by a case split, evaluated with classical decidability:

$$P_{\mathfrak{p}}(T) = \begin{cases} 1 - a_{\mathfrak{p}} T + q_{\mathfrak{p}} T^2 & \text{if } W'_{\mathfrak{p}} \text{ has good reduction: } v(\Delta') = 1; \\[3pt] 1 - T & \text{else, if } W'_{\mathfrak{p}} \text{ has split multiplicative reduction: } v(\Delta') < 1,\ v(c_4') = 1, \text{ and the polynomial} \\ & \quad c_4^I X^2 + a_1^I c_4^I X - \bigl(54\, b_6^I - 3\, b_2^I b_4^I + a_2^I c_4^I\bigr), \text{ reduced to } k_{\mathfrak{p}}[X], \text{ splits over } k_{\mathfrak{p}}; \\[3pt] 1 + T & \text{else, if } W'_{\mathfrak{p}} \text{ has multiplicative reduction: } v(\Delta') < 1,\ v(c_4') = 1; \\[3pt] 1 & \text{otherwise (this is the remaining case } v(\Delta') < 1,\ v(c_4') < 1\text{, i.e. additive reduction).} \end{cases}$$

The reduction-type predicates all include the requirement that $W'_{\mathfrak{p}}$ be minimal, which holds by construction; Mathlib proves that exactly one of good / multiplicative / additive holds for a minimal model. In every case the constant coefficient of $P_{\mathfrak{p}}$ is $1$.

3. Inverse power series and Dirichlet-series reindexing. $F_{\mathfrak{p}}(T) := P_{\mathfrak{p}}(T)^{-1} \in \mathbb{Z}[[T]]$ is the power-series inverse relative to the unit $1$: its coefficients $c_k$ are given recursively by $c_0 = 1$ and $c_k = -\sum_{i + j = k,\, j < k} (P_{\mathfrak{p}})_i\, c_j$ for $k \ge 1$ (so $P_{\mathfrak{p}} F_{\mathfrak{p}} = 1$ as power series, since $P_{\mathfrak{p}}(0) = 1$). Finally $E_{\mathfrak{p}} := \mathrm{ofPowerSeries}(q_{\mathfrak{p}}, F_{\mathfrak{p}})$ is the arithmetic function

$$E_{\mathfrak{p}}(n) = \begin{cases} c_k & \text{if } 1 < q_{\mathfrak{p}} \text{ and } n = q_{\mathfrak{p}}^{\,k} \text{ for some } k \ge 0, \\ 0 & \text{if } 1 < q_{\mathfrak{p}} \text{ and } n \text{ is not a power of } q_{\mathfrak{p}} \text{ (including } n = 0), \\ c_0 \cdot \mathbf{1}(n) = \mathbf{1}(n) & \text{if } q_{\mathfrak{p}} \le 1 \ \text{(junk branch)}. \end{cases}$$

In words: $E_{\mathfrak{p}}$ is "$F_{\mathfrak{p}}(q_{\mathfrak{p}}^{-s})$ written as a Dirichlet series". Here $q_{\mathfrak{p}}$ is used as the natural number Nat.card $k_{\mathfrak{p}}$, so the junk branch is taken exactly when $k_{\mathfrak{p}}$ is infinite ($q_{\mathfrak{p}} = 0$; $q_{\mathfrak{p}} = 1$ cannot occur for a field), in which case $E_{\mathfrak{p}} = \mathbf{1}$ and $\mathfrak{p}$ contributes nothing to the Euler product. The statement itself contains no hypothesis or lemma about finiteness of $k_{\mathfrak{p}}$; whether $q_{\mathfrak{p}}$ equals the residue characteristic $p$ is a fact about Mathlib's construction, not something written in the theorem.

Degenerate and edge cases made explicit.

• The base curve $W$ is only required to have $\Delta(W) \neq 0$ over $\mathbb{Q}$; the statement applies to every such quintuple of rationals, with no integrality or minimality assumed on $W$ itself (integrality/minimality is handled prime by prime by the chosen models above).
• If, for a given $\mathfrak{p}$, the residue field $k_{\mathfrak{p}}$ or the point set $\widetilde{W}'_{\mathfrak{p}}(k_{\mathfrak{p}})$ were infinite, Nat.card would give $0$ there, making $a_{\mathfrak{p}} = 1 - N_{\mathfrak{p}}$ or $a_{\mathfrak{p}} = q_{\mathfrak{p}} + 1$ respectively; the statement does not exclude or address this.
• If the family $(E_{\mathfrak{p}})_{\mathfrak{p}}$ is not multipliable in the pointwise-discrete topology, then $L = \mathbf{1}$ and the conclusion reduces to summability of the single-term sequence $t_1 = 1$.
• The half-plane hypothesis is the open half-plane $\operatorname{Re}(s) > \tfrac{3}{2}$; the statement says nothing for $\operatorname{Re}(s) \le \tfrac{3}{2}$.
• The theorem is stated for $\mathbb{Q}$ only (the number-field parameter of Mathlib's $\mathrm{LFunction}$ is specialised to $\mathbb{Q}$); the primes are the nonzero prime ideals of $\mathcal{O}_{\mathbb{Q}}$.