The total of the root-count integrals

For a nonarchimedean local field K, the root counts over the totally ramified degree-n subextensions of a separable closure sum to n almost everywhere on the Eisenstein region. Integrating this identity gives ∑' L, ∫⁻ a in eisensteinSet K n, L.rootCount a ∂μ = n * μ (eisensteinSet K n). Countability of the family and almost-everywhere measurability of each root count justify interchanging the sum and integral, also in equal characteristic.

This identity is the global counting step in the mass formula: evaluating the individual integrals in terms of discriminant exponents then determines the weighted count of extensions. The total is finite, and its real-valued counterpart is a convergent sum of ordinary integrals. No normalization of Haar measure is needed until the explicit volume formula is substituted.

Dividing by the volume of the Eisenstein region, which is positive and finite, turns the identity into Serre's first mass formula ∑' L, q ^ (-c(L)) = n as soon as each integral is known: the weighted count equals n exactly when the root-count integrals add up to ∑' L, q ^ (-c(L)) * μ (eisensteinSet K n). For Haar measure normalized on the integer box, q ^ (-c(L)) times the volume q ^ (-n) (1 - q⁻¹) of the region is q ^ (-(d(L) + 1)) (1 - q⁻¹), because c(L) + n = d(L) + 1. So Serre's local integral q ^ (-(d(L) + 1)) (1 - q⁻¹) for every L implies the mass formula.

Main results

• TauCeti.tsum_lintegral_rootCount_eq: the root-count integrals over σ_K(n) add up to n * μ (eisensteinSet K n).
• TauCeti.tsum_one_div_natCard_residueField_pow_wildExponent_eq_iff_tsum_lintegral_rootCount_eq: the first mass formula is equivalent to the root-count integrals adding up to ∑' L, q ^ (-c(L)) * μ (eisensteinSet K n).
• TauCeti.tsum_one_div_natCard_residueField_pow_wildExponent_eq_of_lintegral_rootCount_eq: the first mass formula follows from Serre's value of each root-count integral.

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.

theorem TauCeti.tsum_lintegral_rootCount_eq {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {n : ℕ} [MeasurableSpace (Fin n → K)] [BorelSpace (Fin n → K)] (μ : MeasureTheory.Measure (Fin n → K)) [μ.IsAddHaarMeasure] : ∑' (L : ↑(totallyRamifiedOfDegree K n)), ∫⁻ (a : Fin n → K) in eisensteinSet K n, ↑((↑L).rootCount a) ∂μ = ↑n * μ (eisensteinSet K n)

The root-count integrals over all totally ramified degree-n subextensions add up to n times the volume of the Eisenstein region. This holds for any additive Haar measure, including in equal characteristic.

theorem TauCeti.tsum_lintegral_rootCount_eq_of_normalized {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {n : ℕ} [MeasurableSpace (Fin n → K)] [BorelSpace (Fin n → K)] (μ : MeasureTheory.Measure (Fin n → K)) [μ.IsAddHaarMeasure] (hμ : μ (integerBox K (Fin n)) = 1) : ∑' (L : ↑(totallyRamifiedOfDegree K n)), ∫⁻ (a : Fin n → K) in eisensteinSet K n, ↑((↑L).rootCount a) ∂μ = ↑n * (1 / ↑(Nat.card (IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer)) ^ n * (1 - 1 / ↑(Nat.card (IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer))))

For Haar measure normalized on the integer box, the sum of root-count integrals is n * q⁻ⁿ * (1 - q⁻¹), where q is the residue cardinality.

theorem TauCeti.hasSum_integral_rootCount {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {n : ℕ} [MeasurableSpace (Fin n → K)] [BorelSpace (Fin n → K)] (μ : MeasureTheory.Measure (Fin n → K)) [μ.IsAddHaarMeasure] : HasSum (fun (L : ↑(totallyRamifiedOfDegree K n)) => ∫ (a : Fin n → K) in eisensteinSet K n, ↑((↑L).rootCount a) ∂μ) (↑n * (μ (eisensteinSet K n)).toReal)

The ordinary real root-count integrals form a convergent series whose sum is n times the real volume of the Eisenstein region, including when the family of extensions is infinite.

theorem TauCeti.tsum_one_div_natCard_residueField_pow_wildExponent_eq_iff_tsum_lintegral_rootCount_eq {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {n : ℕ} [MeasurableSpace (Fin n → K)] [BorelSpace (Fin n → K)] (μ : MeasureTheory.Measure (Fin n → K)) [μ.IsAddHaarMeasure] : ∑' (L : ↑(totallyRamifiedOfDegree K n)), 1 / ↑(Nat.card (IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer)) ^ (↑L).wildExponent = ↑n ↔ ∑' (L : ↑(totallyRamifiedOfDegree K n)), ∫⁻ (a : Fin n → K) in eisensteinSet K n, ↑((↑L).rootCount a) ∂μ = ∑' (L : ↑(totallyRamifiedOfDegree K n)), 1 / ↑(Nat.card (IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer)) ^ (↑L).wildExponent * μ (eisensteinSet K n)

Theorem 1 in integral form: for any additive Haar measure μ, the weighted count ∑ q ^ (-c(L)) of the totally ramified degree-n subextensions equals n exactly when the root-count integrals add up to ∑ q ^ (-c(L)) * μ(E_n), where E_n is the Eisenstein region. The total of the integrals is n * μ(E_n), and μ(E_n) is positive and finite.

theorem IntermediateField.one_div_pow_wildExponent_mul_measure_eisensteinSet {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {n : ℕ} [MeasurableSpace (Fin n → K)] [BorelSpace (Fin n → K)] {L : IntermediateField K (SeparableClosure K)} (hL : L ∈ TauCeti.totallyRamifiedOfDegree K n) (μ : MeasureTheory.Measure (Fin n → K)) [μ.IsAddLeftInvariant] (hμ : μ (TauCeti.integerBox K (Fin n)) = 1) : 1 / ↑(Nat.card (IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer)) ^ L.wildExponent * μ (TauCeti.eisensteinSet K n) = 1 / ↑(Nat.card (IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer)) ^ (L.discriminantExponent + 1) * (1 - 1 / ↑(Nat.card (IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer)))

For L ∈ σ_K(n) and Haar measure normalized on the integer box, q ^ (-c(L)) times the volume q ^ (-n) (1 - q⁻¹) of the Eisenstein region is q ^ (-(d(L) + 1)) (1 - q⁻¹), where d(L) is the discriminant exponent; this uses c(L) + n = d(L) + 1.

theorem TauCeti.tsum_one_div_natCard_residueField_pow_wildExponent_eq_of_lintegral_rootCount_eq {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {n : ℕ} [MeasurableSpace (Fin n → K)] [BorelSpace (Fin n → K)] (μ : MeasureTheory.Measure (Fin n → K)) [μ.IsAddHaarMeasure] (hμ : μ (integerBox K (Fin n)) = 1) (h : ∀ L ∈ totallyRamifiedOfDegree K n, ∫⁻ (a : Fin n → K) in eisensteinSet K n, ↑(L.rootCount a) ∂μ = 1 / ↑(Nat.card (IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer)) ^ (L.discriminantExponent + 1) * (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 = ↑n

Theorem 1 from the root-count integrals: if, for Haar measure normalized on the integer box, the root count of each L ∈ σ_K(n) integrates over the Eisenstein region to Serre's value q ^ (-(d(L) + 1)) (1 - q⁻¹), then ∑ q ^ (-c(L)) = n.