Auxiliary file: the linear Haar scaling law

Lemma 3 of the paper, in the form §3 consumes it: an integral matrix M with nonzero determinant scales the Haar measure of the coefficient space by 1 / q ^ k, where k is the π-adic order of M.det ([Serre 1978, Lemma 3, p.1033][Serre1978]). The lemma is the volume input of the change of variables along the parametrization of equations (11)–(13), where M is the Jacobian of the minimal-polynomial map and k is d L.

The route is uniqueness-free—no appeal to the uniqueness of Haar measure, hence no second-countability or regularity side conditions. Everything reduces to lattices, that is to the images of the integer box under M:

• The index. card_quotient_range: the quotient of the integer box by its image under M has exactly q ^ k elements. Mathlib's Smith normal form over the principal ideal ring 𝒪[K] (Submodule.quotientEquivPiSpan) splits the quotient into a product of the residue rings of the diagonal coefficients a i, whose product is associated to M.det (LinearMap.associated_det_comp_equiv), and each factor is q to the order of a i because 𝒪[K] is a discrete valuation ring with residue cardinality q.
• The volume. measure_integerBox_eq_pow_mul: the image lattice is a compact subgroup of the integer box of index q ^ k, so the box is the disjoint union of its q ^ k translates and has q ^ k times its volume.
• The box form. measure_box_eq_inv_pow: the lattice of a diagonal matrix is the coordinate box whose i-th factor is π ^ e i times 𝒪[K] (imageLattice_diagonal), so a box has volume 1 / q ^ (∑ i, e i) once the measure is normalized on the integer box. This is what a ball of integers L becomes in the coordinates of a power basis, and the only other volume the assembly of equation (13) needs.
• The ball form. measure_ball_eq_pow_mul: a ball is itself a translate of the lattice of the box of constant radii π ^ m, and the image of a ball is a translate of the lattice of the matrix π ^ m • M, whose determinant has order m * n + k—so the scaling factor q ^ k appears as a ratio of two lattice volumes, with no scaling law for general sets needed.

Modeling decisions, local to this file:

• The scaling exponent is carried by the hypothesis Associated M.det (π ^ k)—the π-adic order of the determinant, stated through associates so that no ℤ-valued valuation or choice of normalization enters. associated_pow_of_valuation converts a valuation-level hypothesis (the form Lemma 2 of the paper produces) into it.
• The coefficient space, its measure muCoeff, and the integer box are those of First.lean; the box and the balls are restated here as integerBox and ball to keep this file independent of that one.

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.

The π-adic order of an element of 𝒪[K], through associates

theorem MassFormula.associated_pow_of_valuation {K : Type u_1} [Field K] [ValuativeRel K] [UniformSpace K] [IsNonarchimedeanLocalField K] {π : ↥(ValuativeRel.valuation K).integer} (hπ : Irreducible π) {a : ↥(ValuativeRel.valuation K).integer} {k : ℕ} (hval : (ValuativeRel.valuation K) ↑a = (ValuativeRel.valuation K) ↑π ^ k) : Associated a (π ^ k)

The valuation-level form of the order hypothesis: an integral element whose valuation is the k-th power of the valuation of π is associated to π ^ k—the bridge from the shape a valuation computation produces to the Associated hypothesis of the scaling law below ([Serre 1978, Lemma 2, p.1033][Serre1978]).

The index of an image lattice

theorem MassFormula.card_quotient_range {K : Type u_1} [Field K] [ValuativeRel K] [UniformSpace K] [IsNonarchimedeanLocalField K] {n : ℕ} (M : Matrix (Fin n) (Fin n) ↥(ValuativeRel.valuation K).integer) (hdet : M.det ≠ 0) {π : ↥(ValuativeRel.valuation K).integer} (hπ : Irreducible π) {k : ℕ} (hk : Associated M.det (π ^ k)) : Nat.card ((Fin n → ↥(ValuativeRel.valuation K).integer) ⧸ M.mulVecLin.range) = q K ^ k

The index of an image lattice: the quotient of the integer box by its image under M has exactly q ^ k elements, where k is the π-adic order of M.det. Mathlib's Smith normal form over the principal ideal ring 𝒪[K] presents the quotient as a product of the residue rings of the diagonal coefficients a i; their product is associated to M.det because the two embeddings of the integer box into itself with image the lattice—the one through M and the one through the Smith bases—differ by an automorphism, and LinearMap.associated_det_comp_equiv makes their determinants associated.

The integer box, its lattices, and the balls

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

The integer box of the coefficient space—the normalizing set of the paper's measure, which gives 𝒪[K] volume 1 coordinatewise ([Serre 1978, p.1032][Serre1978]).

Equations

• MassFormula.integerBox K n = Set.univ.pi fun (x : Fin n) => ↑(ValuativeRel.valuation K).integer

noncomputable def MassFormula.imageLattice {K : Type u_1} [Field K] [ValuativeRel K] {n : ℕ} (M : Matrix (Fin n) (Fin n) ↥(ValuativeRel.valuation K).integer) : Set (Fin n → K)

The image lattice M · 𝒪^n of an integral matrix, inside the coefficient space.

Equations

• MassFormula.imageLattice M = (M.map ⇑(algebraMap (↥(ValuativeRel.valuation K).integer) K)).mulVec '' MassFormula.integerBox K n

def MassFormula.ball {K : Type u_1} [Field K] [ValuativeRel K] {n : ℕ} (x : Fin n → K) (π : ↥(ValuativeRel.valuation K).integer) (m : ℕ) : Set (Fin n → K)

The coordinatewise closed ball around x of radius the m-th power of the valuation of π.

Equations

• MassFormula.ball x π m = {y : Fin n → K | ∀ (i : Fin n), (ValuativeRel.valuation K) (y i - x i) ≤ (ValuativeRel.valuation K) ↑π ^ m}

def MassFormula.box {K : Type u_1} [Field K] [ValuativeRel K] {n : ℕ} (π : ↥(ValuativeRel.valuation K).integer) (e : Fin n → ℕ) : Set (Fin n → K)

The coordinatewise box around the origin whose i-th radius is the e i-th power of the valuation of π—the lattice whose i-th factor is π ^ e i times 𝒪[K], which is what a ball of integers L becomes in the coordinates of a power basis (le_addVal_mul_iff_coords).

Equations

• MassFormula.box π e = Set.univ.pi fun (i : Fin n) => {z : K | (ValuativeRel.valuation K) z ≤ (ValuativeRel.valuation K) ↑π ^ e i}

def MassFormula.toCoeff {K : Type u_1} [Field K] [ValuativeRel K] {n : ℕ} : (Fin n → ↥(ValuativeRel.valuation K).integer) →+ Fin n → K

The coordinatewise inclusion of the integer box into the coefficient space, as an additive monoid homomorphism—the integral picture of the box.

Equations

• MassFormula.toCoeff = { toFun := fun (y : Fin n → ↥(ValuativeRel.valuation K).integer) (i : Fin n) => ↑(y i), map_zero' := ⋯, map_add' := ⋯ }

theorem MassFormula.toCoeff_apply {K : Type u_1} [Field K] [ValuativeRel K] {n : ℕ} (y : Fin n → ↥(ValuativeRel.valuation K).integer) (i : Fin n) : toCoeff y i = ↑(y i)

theorem MassFormula.toCoeff_injective {K : Type u_1} [Field K] [ValuativeRel K] {n : ℕ} : Function.Injective ⇑toCoeff

theorem MassFormula.range_toCoeff {K : Type u_1} [Field K] [ValuativeRel K] {n : ℕ} : Set.range ⇑toCoeff = integerBox K n

The integer box is exactly the range of the integral picture.

theorem MassFormula.imageLattice_eq_image_range {K : Type u_1} [Field K] [ValuativeRel K] {n : ℕ} (M : Matrix (Fin n) (Fin n) ↥(ValuativeRel.valuation K).integer) : imageLattice M = ⇑toCoeff '' ↑M.mulVecLin.range

The image lattice is the integral picture of the range submodule.

theorem MassFormula.toCoeff_mem_imageLattice_iff {K : Type u_1} [Field K] [ValuativeRel K] {n : ℕ} (M : Matrix (Fin n) (Fin n) ↥(ValuativeRel.valuation K).integer) (y : Fin n → ↥(ValuativeRel.valuation K).integer) : toCoeff y ∈ imageLattice M ↔ y ∈ M.mulVecLin.range

Membership in an image lattice, in the integral picture: an integral vector lies in the image of the integer box under M exactly when it lies in the range of M over 𝒪[K]—the integral picture being injective.

theorem MassFormula.isCompact_imageLattice {K : Type u_1} [Field K] [ValuativeRel K] [UniformSpace K] [IsNonarchimedeanLocalField K] {n : ℕ} (M : Matrix (Fin n) (Fin n) ↥(ValuativeRel.valuation K).integer) : IsCompact (imageLattice M)

The image lattice sits inside the integer box, and is compact—the continuous image of the compact box.

The volume of an image lattice

theorem MassFormula.measure_integerBox_eq_pow_mul {K : Type u_1} [Field K] [ValuativeRel K] [UniformSpace K] [IsUniformAddGroup K] [IsNonarchimedeanLocalField K] {n : ℕ} [MeasurableSpace (Fin n → K)] [BorelSpace (Fin n → K)] (μ : MeasureTheory.Measure (Fin n → K)) [μ.IsAddLeftInvariant] (M : Matrix (Fin n) (Fin n) ↥(ValuativeRel.valuation K).integer) (hdet : M.det ≠ 0) {π : ↥(ValuativeRel.valuation K).integer} (hπ : Irreducible π) {k : ℕ} (hk : Associated M.det (π ^ k)) : μ (integerBox K n) = ↑(q K) ^ k * μ (imageLattice M)

The volume of an image lattice: the integer box is the disjoint union of the q ^ k translates of its image under M, so the box has q ^ k times the volume of that image—for any translation-invariant measure, no normalization needed. The index q ^ k is card_quotient_range; the decomposition is the coset decomposition of the integer box modulo the lattice, transported along the integral picture toCoeff, and the lattice is measurable because it is compact.

The scaling law on boxes and on balls

theorem MassFormula.mem_box_iff {K : Type u_1} [Field K] [ValuativeRel K] {n : ℕ} (π : ↥(ValuativeRel.valuation K).integer) (e : Fin n → ℕ) (w : Fin n → K) : w ∈ box π e ↔ ∀ (i : Fin n), (ValuativeRel.valuation K) (w i) ≤ (ValuativeRel.valuation K) ↑π ^ e i

Membership in a box, coordinate by coordinate.

theorem MassFormula.imageLattice_diagonal {K : Type u_1} [Field K] [ValuativeRel K] {n : ℕ} {π : ↥(ValuativeRel.valuation K).integer} (hπ : Irreducible π) (e : Fin n → ℕ) : imageLattice (Matrix.diagonal fun (i : Fin n) => π ^ e i) = box π e

The lattice of a diagonal matrix is a box: multiplication by π ^ e i in the i-th coordinate has image π ^ e i times 𝒪[K] there, so the image lattice of a diagonal integral matrix of powers is the coordinate box of the corresponding radii.

theorem MassFormula.measure_imageLattice_eq_inv_pow {K : Type u_1} [Field K] [ValuativeRel K] [UniformSpace K] [IsUniformAddGroup K] [IsNonarchimedeanLocalField K] {n : ℕ} [MeasurableSpace (Fin n → K)] [BorelSpace (Fin n → K)] (μ : MeasureTheory.Measure (Fin n → K)) [μ.IsAddLeftInvariant] (hnorm : μ (integerBox K n) = 1) (M : Matrix (Fin n) (Fin n) ↥(ValuativeRel.valuation K).integer) (hdet : M.det ≠ 0) {π : ↥(ValuativeRel.valuation K).integer} (hπ : Irreducible π) {k : ℕ} (hk : Associated M.det (π ^ k)) : μ (imageLattice M) = (↑(q K))⁻¹ ^ k

The volume of an image lattice: for a measure normalized on the integer box—the paper's normalization giving 𝒪[K] volume 1, coordinatewise—the lattice of a matrix whose determinant has π-adic order k has volume 1 / q ^ k ([Serre 1978, p.1032][Serre1978]).

theorem MassFormula.measure_box_eq_inv_pow {K : Type u_1} [Field K] [ValuativeRel K] [UniformSpace K] [IsUniformAddGroup K] [IsNonarchimedeanLocalField K] {n : ℕ} [MeasurableSpace (Fin n → K)] [BorelSpace (Fin n → K)] (μ : MeasureTheory.Measure (Fin n → K)) [μ.IsAddLeftInvariant] (hnorm : μ (integerBox K n) = 1) {π : ↥(ValuativeRel.valuation K).integer} (hπ : Irreducible π) (e : Fin n → ℕ) : μ (box π e) = (↑(q K))⁻¹ ^ ∑ i : Fin n, e i

The volume of a coordinate box: the diagonal case of the lattice volume, the box of radii π ^ e i having volume 1 / q ^ (∑ i, e i).

theorem MassFormula.measure_ball_eq_pow_mul {K : Type u_1} [Field K] [ValuativeRel K] [UniformSpace K] [IsUniformAddGroup K] [IsNonarchimedeanLocalField K] {n : ℕ} [MeasurableSpace (Fin n → K)] [BorelSpace (Fin n → K)] (μ : MeasureTheory.Measure (Fin n → K)) [μ.IsAddLeftInvariant] (M : Matrix (Fin n) (Fin n) ↥(ValuativeRel.valuation K).integer) (hdet : M.det ≠ 0) {π : ↥(ValuativeRel.valuation K).integer} (hπ : Irreducible π) {k : ℕ} (hk : Associated M.det (π ^ k)) (x : Fin n → K) (m : ℕ) : μ (ball x π m) = ↑(q K) ^ k * μ ((M.map ⇑(algebraMap (↥(ValuativeRel.valuation K).integer) K)).mulVec '' ball x π m)

The form the change of variables consumes: an integral matrix whose determinant has π-adic order k shrinks the volume of every ball by exactly q ^ k. Both the ball and its image are translates of lattices—of the integer box scaled by π ^ m, and of its image under M, of determinant orders m * n and m * n + k—so the two applications of measure_integerBox_eq_pow_mul differ by the factor q ^ k, which is all that survives after the common factor q ^ (m * n) is cancelled.