Auxiliary file: summable_one_div_q_pow_c—the convergence claim of Remark 1° #
The paper remarks that even when sigma K n is infinite the series with general term
1 / (q K : ℝ) ^ c L.1 is convergent ([Serre 1978, Remark 1°, p.1031][Serre1978]). Over ℝ≥0∞ no
convergence claim is needed—the extended sum always exists—so this module restates the remark
over ℝ as Summable. The derivation runs through Theorem 1: by tsum_one_div_q_pow_c the
ℝ≥0∞-valued sum equals n, which is finite, and an ℝ≥0∞-valued family with finite sum has
summable toReals (ENNReal.summable_toReal); identifying the terms is toReal arithmetic.
References #
- [Serre1978] J-P. Serre, Une «formule de masse» pour les extensions totalement ramifiées de degré donné d'un corps local, C. R. Acad. Sci. Paris 286 (1978), Série A, 1031–1036.
theorem
MassFormula.summable_one_div_q_pow_c
(K : Type u_1)
[Field K]
[ValuativeRel K]
[UniformSpace K]
[IsUniformAddGroup K]
[IsNonarchimedeanLocalField K]
(n : ℕ)
(hn : 0 < n)
:
The series with general term 1 / (q K : ℝ) ^ c L.1 is convergent, derived from Theorem 1
([Serre 1978, Remark 1°, p.1031][Serre1978]).