The weights of Serre's mass formula

Let K be a nonarchimedean local field with residue field of cardinality q. Serre's mass formula weights each L ∈ σ_K(n) by q ^ (-c(L)), where c(L) = d(L) - n + 1 is the wild exponent. Serre proves it by integrating root counts over the Eisenstein region, whose volume is q ^ (-n) · (1 - q⁻¹) for 0 < n: the root count of L integrates to q ^ (-(d(L) + 1)) · (1 - q⁻¹), and since d(L) + 1 = n + c(L), this is the volume of the region times q ^ (-c(L)). This file records that factorization and its consequence: the mass formula ∑_{L ∈ σ_K(n)} q ^ (-c(L)) = n is equivalent to ∑_{L ∈ σ_K(n)} q ^ (-(d(L) + 1)) · (1 - q⁻¹) = n · q ^ (-n) · (1 - q⁻¹), the form in which the integration produces it.

The weighted count is a sum in ℝ≥0∞, which needs no convergence hypothesis. Its real-valued form, a series of positive reals, converges exactly when the ℝ≥0∞ sum is finite, and then has the same value. When σ_K(n) is infinite, this is the convergence half of Serre's Remark 1°.

Main results

• TauCeti.tsum_one_div_natCard_residueField_pow_discriminantExponent_add_one_mul: ∑_{L ∈ σ_K(n)} q ^ (-(d(L) + 1)) · (1 - q⁻¹) is q ^ (-n) · (1 - q⁻¹) · ∑_{L ∈ σ_K(n)} q ^ (-c(L)).
• TauCeti.tsum_one_div_natCard_residueField_pow_wildExponent_eq_iff: the mass formula is equivalent to ∑_{L ∈ σ_K(n)} q ^ (-(d(L) + 1)) · (1 - q⁻¹) = n · q ^ (-n) · (1 - q⁻¹).
• TauCeti.hasSum_one_div_natCard_residueField_pow_wildExponent_iff and TauCeti.summable_one_div_natCard_residueField_pow_wildExponent_iff: the real series ∑_{L ∈ σ_K(n)} q ^ (-c(L)) converges exactly when the ℝ≥0∞ sum is finite, with the same sum.

References

• 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 Sér. A 286 (1978), 1031–1036, §3 and Remarque 1°.

theorem TauCeti.tsum_one_div_natCard_residueField_pow_discriminantExponent_add_one_mul {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {n : ℕ} : ∑' (L : ↑(totallyRamifiedOfDegree K n)), 1 / ↑(Nat.card (IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer)) ^ ((↑L).discriminantExponent + 1) * (1 - 1 / ↑(Nat.card (IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer))) = 1 / ↑(Nat.card (IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer)) ^ n * (1 - 1 / ↑(Nat.card (IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer))) * ∑' (L : ↑(totallyRamifiedOfDegree K n)), 1 / ↑(Nat.card (IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer)) ^ (↑L).wildExponent

The discriminant weights factor through the wild exponents: the weights q ^ (-(d(L) + 1)) · (1 - q⁻¹) of the members of σ_K(n) sum to q ^ (-n) · (1 - q⁻¹) times the weighted count ∑_{L ∈ σ_K(n)} q ^ (-c(L)) of the mass formula.

theorem TauCeti.tsum_one_div_natCard_residueField_pow_wildExponent_eq_iff {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {n : ℕ} : ∑' (L : ↑(totallyRamifiedOfDegree K n)), 1 / ↑(Nat.card (IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer)) ^ (↑L).wildExponent = ↑n ↔ ∑' (L : ↑(totallyRamifiedOfDegree K n)), 1 / ↑(Nat.card (IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer)) ^ ((↑L).discriminantExponent + 1) * (1 - 1 / ↑(Nat.card (IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer))) = ↑n * (1 / ↑(Nat.card (IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer)) ^ n * (1 - 1 / ↑(Nat.card (IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer))))

The mass formula in discriminant weights: the weighted count ∑_{L ∈ σ_K(n)} q ^ (-c(L)) is n exactly when the weights q ^ (-(d(L) + 1)) · (1 - q⁻¹) sum to n · q ^ (-n) · (1 - q⁻¹), which for 0 < n is n times the volume of the Eisenstein region for the Haar measure normalized on the integer box. By TauCeti.tsum_lintegral_rootCount_eq_of_normalized, the right side holds once each root-count integral over the Eisenstein region is evaluated as q ^ (-(d(L) + 1)) · (1 - q⁻¹).

theorem TauCeti.hasSum_one_div_natCard_residueField_pow_wildExponent_iff {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {n : ℕ} {s : NNReal} : HasSum (fun (L : ↑(totallyRamifiedOfDegree K n)) => 1 / ↑(Nat.card (IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer)) ^ (↑L).wildExponent) ↑s ↔ ∑' (L : ↑(totallyRamifiedOfDegree K n)), 1 / ↑(Nat.card (IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer)) ^ (↑L).wildExponent = ↑s

The real-valued form of the weighted count: the real series ∑_{L ∈ σ_K(n)} q ^ (-c(L)) sums to s exactly when the ℝ≥0∞ sum is s. At s = n, this relates the mass formula to its real-valued restatement.

theorem TauCeti.summable_one_div_natCard_residueField_pow_wildExponent_iff {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {n : ℕ} : (Summable fun (L : ↑(totallyRamifiedOfDegree K n)) => 1 / ↑(Nat.card (IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer)) ^ (↑L).wildExponent) ↔ ∑' (L : ↑(totallyRamifiedOfDegree K n)), 1 / ↑(Nat.card (IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer)) ^ (↑L).wildExponent ≠ ⊤

The real-valued weighted count converges exactly when the ℝ≥0∞ sum is finite. With the mass formula, this makes the real series ∑_{L ∈ σ_K(n)} q ^ (-c(L)) converge, also when σ_K(n) is infinite.