Brumer's theorem, Lemme 3: one extrapolation step by the $p$-adic Schwarz lemma and the size inequality

Let $p$ be a prime, $L$ a number field of degree $d$, $w$ a prime of $L$ above $p$, and $a_1,\dots,a_n \in L$ with $\|a_i - 1\|_w \le \|p\|_w^2$. Let $c \in L^n$ with

and let $k$ be an index with $c_k \ne 0$ and $\|c_i\|_w \le \|c_k\|_w$ for all $i$. For $\lambda \in \{0,\dots,N-1\}^n$, integers $P(\lambda)$, $q \ge 0$, $m \in \mathbb{N}^n$ and $\ell \ge 1$ put, as in NumberField.Brumer.exists_int_coeffs_vanishing,

The statement asserts that there is a constant $C \ge 1$, which depends only on $p, L, w, a, c, k$, with this property. Let $q, N, S, T, S', R, R'$ be natural numbers, $B$ a real number and $P$ integers with $|P(\lambda)| \le B$. Assume $S' + T \le S$,

and the numerical condition

Then

Meaning. The order of vanishing goes down from $S$ to $S'$, and the number of points goes up from $R$ to $R'$.

Proof idea. Fix $m$ with $|m| \le S'$ and put $u_\lambda = \prod_i a_i^{\lambda_i}$. The function $\varphi_m(z) = \sum_\lambda P(\lambda) \prod_i \gamma_i(\lambda)^{m_i}\, u_\lambda^{z}$ is a restricted power series in $z$ (by PadicLog.hasSum_inv_factorial_mul_pow_log), and $\varphi_m(q\ell) = Q(m,\ell)$. The relation gives $c_k \log_p u_\lambda = \sum_i \gamma_i(\lambda)\log_p a_i$, so $c_k^t\, t!$ times the Hasse derivative of order $t$ of $\varphi_m$ at $q\ell$ is a combination of the $Q(m + j, \ell)$ with $|j| = t$. Hence $\varphi_m$ vanishes to order more than $T$ at the $R$ points $q\ell$, which have norm at most $\|q\|_w$. The Schwarz lemma (IsUltrametricDist.norm_tsum_mul_pow_le_of_hasseDeriv_eq_zero) gives $\|Q(m,\ell')\|_w \le \|q\|_w^{R(T+1)} \max(1,\|c_k\|_w)^{S'}$ for $\ell' \le R'$. The number $Q(m,\ell')$ has a denominator and conjugates bounded by $N^n B C_0^{qNR'+S'} N^{S'}$, so the size inequality (NumberField.inv_pow_finrank_le_norm_adicCompletion) and the numerical condition show that it is zero.

Use. This is the induction step in the proof of NumberField.Brumer.exists_auxiliary_polynomial, applied with $q = p$.

Formalization Note. $L_w$ is w.1.adicCompletion L with the norm of Definitions.Def_PrimesOverNorm; $\log_p$ is PadicLog.log (p := p). The hypothesis on the pivot ($\|c_i\|_w \le \|c_k\|_w$) is not necessary for the proof but makes the constant simpler. The exponent of $\|q\|_w$ is $R\,T$; the proof gives $R\,(T+1)$. For $q = 0$ the quantity $Q(m,\ell)$ does not depend on $\ell$. A proof needs a CharZero instance on the completion (charZero_of_injective_algebraMap).