Auxiliary file: tsum_one_div_q_pow_c—Theorem 1, the mass formula (§3, pp.1032–1033)

This file follows Serre's first proof (§3) in a root-counting variant. The paper partitions the Eisenstein region into classes indexed by the isomorphism classes of representatives, proves Theorem 2, and recovers Theorem 1 through Remark 3°. Here, instead, each individual L in sigma K n gets the counting function rootCount L—the number of roots of f lying in L—and the same change-of-variables computation along the parametrization of equations (5)–(13) evaluates its integral over the Eisenstein region as (1 / q ^ (d L + 1)) * (1 - 1 / q). Since a.e. f is separable (equation (3)) with each of its n roots generating exactly one member of sigma K n, the counts sum to n a.e., and integrating gives Theorem 1 directly—no quotient by isomorphism, no w L. This is the paper's computation reassembled, and is the more direct route to the sum indexed by sigma K n; Theorem 2 is recovered from the same core ([Serre 1978, §3, pp.1032–1033][Serre1978]).

Modeling decisions, local to this file:

• A monic polynomial of degree n is its coefficient vector a : Fin n → K, with a i the coefficient of X ^ i (toPoly)—the paper's identification of the space of such polynomials with a subspace of the coefficient space.
• The paper's measure, the product of the coordinate measures normalized so that 𝒪[K] has volume 1, is realized in one stroke as the Haar measure of the additive group Fin n → K normalized on the positive compact integer box (muCoeff). By uniqueness of Haar measure this is the product of the normalized coordinate measures, but the product structure is only ever needed inside the volume computations, so neither Measure.pi nor any σ-finiteness enters the statements.
• The Borel structure [MeasurableSpace (Fin n → K)] [BorelSpace (Fin n → K)] is a per-lemma hypothesis of the machinery; the concluding theorem introduces it via borel, so its statement requires no measurable-space parameter.
• The Eisenstein condition of equation (1) is stated multiplicatively: every coefficient lies in the open unit ball, and the constant term has the largest valuation below 1—that of a uniformizer.
• rootCount L a counts the roots of toPoly a in L with multiplicity (Multiset.card of aroots); on the full-measure separable locus all multiplicities are 1, so the count agrees with the paper's fiber count of the parametrization ([Serre 1978, Lemma 1, p.1033][Serre1978]).

The file contains the volume of the Eisenstein region (muCoeff_eisensteinSet, with its coset-counting helpers), the Eisenstein irreducibility and separability facts, the a.e. reduction of the root-count identity (tsum_rootCount, via the null hyperplane a 1 = 0), the counting combinatorics of tsum_rootCount_of_separable, the ramification core isTotallyRamified_adjoin_root (via EisensteinMonogenic.lean), the bound sub_one_le_d, the local constancy rootCount_eventuallyEq of the root count on the separable locus (via the Newton lifting of RootLifting.lean), the a.e. measurability aemeasurable_rootCount of the root count (from that local constancy), the countability countable_sigma of sigma K n (positive masses with bounded finite subsums), the change-of-variables identity lintegral_rootCount (assembled from the box decomposition below on top of UniformizerParam.lean and HaarScaling.lean), and the assembly of Theorem 1 (tsum_one_div_q_pow_c).

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.
• [Serre1979] J-P. Serre, Local fields, Graduate Texts in Mathematics 67, Springer, 1979.

The coefficient space, its measure, and the counting functions

noncomputable def MassFormula.toPoly {K : Type u_1} [Field K] {n : ℕ} (a : Fin n → K) : Polynomial K

The monic polynomial of degree n encoded by a coefficient vector a : Fin n → K, with a i the coefficient of X ^ i—the paper's identification of monic polynomials of degree n with points of the coefficient space ([Serre 1978, p.1032][Serre1978]).

Equations

• MassFormula.toPoly a = Polynomial.X ^ n + ∑ i : Fin n, Polynomial.C (a i) * Polynomial.X ^ ↑i

noncomputable def MassFormula.rootCount {K : Type u_1} [Field K] (L : IntermediateField K (SeparableClosure K)) {n : ℕ} (a : Fin n → K) : ℕ

The counting function implicit in Lemma 1: the number of roots of toPoly a lying in the subextension L, with multiplicity. On the separable locus this is the fiber count of the parametrization over f, that is the number of uniformizers of L with minimal polynomial f ([Serre 1978, Lemma 1, p.1033][Serre1978]).

Equations

• MassFormula.rootCount L a = ((MassFormula.toPoly a).aroots ↥L).card

def MassFormula.eisensteinSet (K : Type u_1) [Field K] [ValuativeRel K] (n : ℕ) : Set (Fin n → K)

The Eisenstein region of equation (1), as a set of coefficient vectors: every coefficient lies in the open unit ball, and the constant term has the largest valuation below 1, that of a uniformizer ([Serre 1978, eq. (1), p.1032][Serre1978]).

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MassFormula.integerPositiveCompacts (K : Type u_1) [Field K] [ValuativeRel K] [UniformSpace K] [IsNonarchimedeanLocalField K] (n : ℕ) : TopologicalSpace.PositiveCompacts (Fin n → K)

The integer box in the coefficient space, compact with nonempty interior—the normalizing set of the measure below, giving 𝒪[K] volume 1 coordinatewise ([Serre 1978, p.1032][Serre1978]).

Equations

• MassFormula.integerPositiveCompacts K n = { carrier := Set.univ.pi fun (x : Fin n) => ↑(ValuativeRel.valuation K).integer, isCompact' := ⋯, interior_nonempty' := ⋯ }

noncomputable def MassFormula.muCoeff (K : Type u_1) [Field K] [ValuativeRel K] [UniformSpace K] [IsNonarchimedeanLocalField K] (n : ℕ) [MeasurableSpace (Fin n → K)] [BorelSpace (Fin n → K)] : MeasureTheory.Measure (Fin n → K)

The paper's measure on the coefficient space: the Haar measure of the locally compact additive group Fin n → K, normalized so that the integer box has volume 1 ([Serre 1978, p.1032][Serre1978]).

Equations

• MassFormula.muCoeff K n = MeasureTheory.Measure.addHaarMeasure (MassFormula.integerPositiveCompacts K n)

The X^n + ∑ C (c i) X^i coefficient shape, over any commutative ring

Haar-measure helpers: residue representatives, the uniformizer, and coset counting

The box-volume computations below implement the coset counting behind equation (2): the integer box has volume 1 by normalization; it is the disjoint union of q ^ n translates of the open-unit-ball box, indexed by vectors of residues; and the unit-ball box is in turn the disjoint union of q translates of the box whose 0-coordinate is shrunk one valuation level, indexed by residues via a uniformizer ([Serre 1978, eq. (2), p.1032][Serre1978]).

instance MassFormula.muCoeff_isAddLeftInvariant {K : Type u_1} [Field K] [ValuativeRel K] [UniformSpace K] [IsNonarchimedeanLocalField K] (n : ℕ) [MeasurableSpace (Fin n → K)] [BorelSpace (Fin n → K)] : (muCoeff K n).IsAddLeftInvariant

muCoeff is translation-invariant, being a Haar measure.

instance MassFormula.muCoeff_isOpenPosMeasure {K : Type u_1} [Field K] [ValuativeRel K] [UniformSpace K] [IsNonarchimedeanLocalField K] (n : ℕ) [MeasurableSpace (Fin n → K)] [BorelSpace (Fin n → K)] : (muCoeff K n).IsOpenPosMeasure

muCoeff is positive on nonempty open sets, being a Haar measure on the locally compact group Fin n → K.

The Eisenstein region: set identity, measurability, irreducibility, separability

These are the deterministic facts behind equation (3) and Lemma 1: the region is a difference of boxes (hence measurable), every point has an irreducible polynomial by the Eisenstein criterion over 𝒪[K] and Gauss's lemma, and the inseparable points lie on the null hyperplane where the X ^ 1-coefficient vanishes ([Serre 1978, eq. (3), p.1032; Lemma 1, p.1033][Serre1978]).

Local constancy of the root count on the separable locus

theorem MassFormula.rootCount_eventuallyEq (K : Type u_1) [Field K] [ValuativeRel K] [UniformSpace K] [IsUniformAddGroup K] [IsNonarchimedeanLocalField K] (n : ℕ) (hn : 0 < n) (L : IntermediateField K (SeparableClosure K)) (hL : L ∈ sigma K n) {a : Fin n → K} (ha : a ∈ eisensteinSet K n) (hsep : (toPoly a).Separable) : ∀ᶠ (b : Fin n → K) in nhds a, rootCount L b = rootCount L a

Local constancy of the root count at a separable point of the Eisenstein region: for every L in sigma K n, all coefficient vectors near a have the same number of roots in L as a itself. The quantitative content is card_aroots_eq—Newton lifting over the complete ring of integers of L—whose modulus, the T-th power of 𝓂[K], this statement converts into the neighborhood of a of coordinatewise radius the T-th power of the valuation of π. This is the shared analytic input of aemeasurable_rootCount, countable_sigma, and lintegral_rootCount.

The core lemmas

theorem MassFormula.muCoeff_eisensteinSet (K : Type u_1) [Field K] [ValuativeRel K] [UniformSpace K] [IsNonarchimedeanLocalField K] (n : ℕ) (hn : 0 < n) [MeasurableSpace (Fin n → K)] [BorelSpace (Fin n → K)] : (muCoeff K n) (eisensteinSet K n) = (↑(q K))⁻¹ ^ n * (1 - (↑(q K))⁻¹)

The Eisenstein region has volume (1 / q ^ n) * (1 - 1 / q). It is a difference of two boxes—the box of radius π minus the sub-box where the constant term lies in π ^ 2 * 𝒪[K]—of indices q ^ n and q ^ (n + 1) in the integer box; translation invariance and the coset count give the volumes 1 / q ^ n and 1 / q ^ (n + 1) ([Serre 1978, eq. (2), p.1032][Serre1978]).

theorem MassFormula.aemeasurable_rootCount (K : Type u_1) [Field K] [ValuativeRel K] [UniformSpace K] [IsUniformAddGroup K] [IsNonarchimedeanLocalField K] (n : ℕ) (hn : 0 < n) [MeasurableSpace (Fin n → K)] [BorelSpace (Fin n → K)] (L : IntermediateField K (SeparableClosure K)) (hL : L ∈ sigma K n) : AEMeasurable (fun (a : Fin n → K) => ↑(rootCount L a)) ((muCoeff K n).restrict (eisensteinSet K n))

Away from the measure-zero discriminant locus the root count is locally constant—Krasner's lemma, or continuity of the roots—hence a.e. measurable on the Eisenstein region. The local constancy is rootCount_eventuallyEq; it makes the root count continuous on the separable part of the region, and for 2 ≤ n the inseparable part sits on the null hyperplane a 1 = 0, so restricting the measure there changes nothing ([Serre 1978, eq. (3), p.1032][Serre1978]).

The change-of-variables core

The assembly of equations (5)–(13) on top of UniformizerParam.lean and HaarScaling.lean. Fix an Eisenstein generator ξ of integers L (exists_eisenstein_generator) and a radius ρ with d L + n ≤ n * ρ; the classes of integers L modulo π ^ ρ times integers L whose representative is a uniformizer index a family of boxes in the coefficient space—the box of the class of η being the coefficient vector of the monic annihilator of η, translated by the lattice of multiplication by π ^ ρ times the derivative of that annihilator at η, in the chart at η. By the local fiber count (existsUnique_isRoot_iff), a.e. polynomial of the Eisenstein region lies in exactly rootCount many boxes; each box has volume 1 / q ^ (n * ρ + d L) (measure_imageLattice_eq_inv_pow through det_leftMulMatrix and addVal_norm); and the corresponding cubes of the chart at ξ partition the set of uniformizers, of volume (1 / q) * (1 - 1 / q) (equation (5), measure_image_coord_uniformizers)—so the number of classes cancels between the two sums and the integral is (1 / q ^ d L) * (1 / q) * (1 - 1 / q).

Generic helpers over a discrete valuation ring

Additive-valuation converters on 𝒪[K]

The chart and the lattices at an arbitrary basis

Small ℕ∞ arithmetic helpers

The integral model of a coefficient vector

The annihilator package at an arbitrary uniformizer of integers L

The cubes decomposing the set of uniformizers are centered at arbitrary uniformizers η of integers L, each carrying its own chart (the coordinates in the powers of η, powersBasisIntegers) and its own monic annihilator; the definitions below bundle the two, with the monogenic basis basisOfEisenstein as the junk value on non-uniformizers so that families indexed by residue classes stay total.

The box of a uniformizer

The volume of a box, and the a.e. separability

theorem MassFormula.lintegral_rootCount (K : Type u_1) [Field K] [ValuativeRel K] [UniformSpace K] [IsUniformAddGroup K] [IsNonarchimedeanLocalField K] (n : ℕ) (hn : 0 < n) [MeasurableSpace (Fin n → K)] [BorelSpace (Fin n → K)] (L : IntermediateField K (SeparableClosure K)) (hL : L ∈ sigma K n) : ∫⁻ (a : Fin n → K) in eisensteinSet K n, ↑(rootCount L a) ∂muCoeff K n = (↑(q K))⁻¹ ^ (d L + 1) * (1 - (↑(q K))⁻¹)

The heart of §3, equations (5)–(13): for L in sigma K n, the integral of rootCount L over the Eisenstein region is (1 / q ^ (d L + 1)) * (1 - 1 / q), that is 1 / q ^ d L times the volume of the set of uniformizers. The route is the lattice form of the paper's change of variables (see the header of UniformizerParam.lean): fixing ρ = d L + 2, the classes of integers L modulo π ^ ρ times integers L whose representative is a uniformizer index a family of disjoint boxes in the coefficient space—the box of the class of η being the exact level set where the value at η has valuation at least n * ρ + d L (mem_boxAt_iff), of volume 1 / q ^ (n * ρ + d L) (measure_boxAt), contained in the region (boxAt_subset_eisensteinSet). A.e. f lies in exactly rootCount L f boxes—the fiber count existsUnique_isRoot_iff makes each root correspond to its class bijectively, every root of an Eisenstein polynomial being a uniformizer (irreducible_of_isRoot)—while the corresponding cubes of the chart partition the image of the set of uniformizers, of volume (1 / q) * (1 - 1 / q) (equation (5), measure_image_coord_uniformizers). So the number of classes cancels between the two sums, and the integral is (1 / q ^ d L) * (1 / q) * (1 - 1 / q)—Lemmas 1–3 with no Jacobian and no w L ([Serre 1978, §3, pp.1032–1033][Serre1978]).

theorem MassFormula.isTotallyRamified_adjoin_root (K : Type u_1) [Field K] [ValuativeRel K] [UniformSpace K] [IsNonarchimedeanLocalField K] {n : ℕ} (hn : 0 < n) {a : Fin n → K} (ha : a ∈ eisensteinSet K n) {x : SeparableClosure K} (hx : (Polynomial.aeval x) (toPoly a) = 0) : IsTotallyRamified K⟮x⟯

The ramification core: a root of an Eisenstein polynomial generates a totally ramified extension ([Serre 1979, Chap. I, §6, Prop. 17][Serre1979]). The minimal polynomial of the root over 𝒪[K] is identified with the integral Eisenstein model (minpoly_eq_of_root), and isTotallyRamified_adjoin computes ramificationIdx L = n through the monogenic presentation integers_eq_adjoin.

theorem MassFormula.tsum_rootCount_of_separable (K : Type u_1) [Field K] [ValuativeRel K] [UniformSpace K] [IsNonarchimedeanLocalField K] {n : ℕ} (hn : 0 < n) {a : Fin n → K} (ha : a ∈ eisensteinSet K n) (hsep : (toPoly a).Separable) : ∑' (L : ↑(sigma K n)), ↑(rootCount (↑L) a) = ↑n

The algebraic core of equation (3) and Lemma 1: a separable point of the Eisenstein region has root counts over sigma K n summing to n. The polynomial is irreducible with n distinct roots in SeparableClosure K; each root generates a member of sigma K n (of degree n via its minimal polynomial, totally ramified by isTotallyRamified_adjoin_root); a member of sigma K n contains a root exactly when the root generates it (equal finite degrees); so the root counts are the fiber counts of the map sending a root x to K⟮x⟯ on the n-element root set, and fiberwise counting sums them to n ([Serre 1978, eq. (3), p.1032; Lemma 1, p.1033][Serre1978]).

theorem MassFormula.tsum_rootCount (K : Type u_1) [Field K] [ValuativeRel K] [UniformSpace K] [IsUniformAddGroup K] [IsNonarchimedeanLocalField K] (n : ℕ) (hn : 0 < n) [MeasurableSpace (Fin n → K)] [BorelSpace (Fin n → K)] : ∀ᵐ (a : Fin n → K) ∂(muCoeff K n).restrict (eisensteinSet K n), ∑' (L : ↑(sigma K n)), ↑(rootCount (↑L) a) = ↑n

Almost every f in the Eisenstein region has nonzero discriminant—and such an f, irreducible by the Eisenstein criterion and separable, has exactly n roots in SeparableClosure K, each a uniformizer generating a totally ramified subextension of degree n. A root generating L lies in no other member of sigma K n (two members containing a common generator coincide), so the root counts over sigma K n sum to n ([Serre 1978, eq. (3), p.1032][Serre1978]).

theorem MassFormula.countable_sigma (K : Type u_1) [Field K] [ValuativeRel K] [UniformSpace K] [IsUniformAddGroup K] [IsNonarchimedeanLocalField K] (n : ℕ) (hn : 0 < n) : (sigma K n).Countable

sigma K n is countable—all the tsum–lintegral interchange of the assembly needs. Remarks 1° and 2° refine this (finiteness outside the equal-characteristic wild case, Krasner's counts), but countability is cheaper: the members of sigma K n carve the Eisenstein region into pieces of positive volume with bounded total. Concretely, each L in sigma K n owns a nonempty open subset of the Eisenstein region on which its root count is positive—a neighborhood, by the local constancy rootCount_eventuallyEq, of the coefficient vector of the minimal polynomial of an Eisenstein generator (exists_eisenstein_generator); the masses are positive (Haar), while any finitely many of them total at most n times the volume of the region because the root counts sum to n a.e. (equation (3)); a family of positive masses with bounded finite subsums has countable index.

The assembly

theorem MassFormula.tsum_one_div_q_pow_c (K : Type u_1) [Field K] [ValuativeRel K] [UniformSpace K] [IsUniformAddGroup K] [IsNonarchimedeanLocalField K] (n : ℕ) (hn : 0 < n) : ∑' (L : ↑(sigma K n)), 1 / ↑(q K) ^ c ↑L = ↑n

The sum of 1 / q ^ c L over L in sigma K n is n, assembled from the core lemmas above. Summing lintegral_rootCount over the countably many members of sigma K n and interchanging sum and integral turns the a.e. identity that the root counts sum to n into an identity between the sum of the (1 / q ^ (d L + 1)) * (1 - 1 / q) and n times the volume of the region, itself n * (1 / q ^ n) * (1 - 1 / q); cancelling 1 - 1 / q and multiplying through by q ^ n gives the mass formula, the bound n - 1 ≤ d L (sub_one_le_d) converting q ^ n * (1 / q ^ (d L + 1)) into 1 / q ^ c L ([Serre 1978, Theorem 1, p.1031][Serre1978]).