Measurability of root counts over a nonarchimedean local field

Let L / K be an extension of nonarchimedean local fields. A monic polynomial of degree n over K is its coefficient vector a : Fin n → K, through TauCeti.Polynomial.monicOfCoeff. This file proves that the number of roots of monicOfCoeff a in L, counted with multiplicity, is a measurable function of a on the integer box 𝒪[K] ^ n: for every k, the integral coefficient vectors whose polynomial has at least k roots in L form a compact set.

This is what lets root counts be integrated over coefficient space, as in Serre's proof of his mass formula, where the root count in each totally ramified extension is integrated over the Eisenstein polynomials. The statement holds at every integral coefficient vector, separable or not: at an inseparable polynomial the root count need not be locally constant, but it is still measurable.

Main results

• TauCeti.isCompact_setOf_le_card_aroots: the integral coefficient vectors whose polynomial has at least k roots in L form a compact subset of Fin n → K.
• TauCeti.aemeasurable_card_aroots: the root count in L is almost everywhere measurable for every measure carried by the integer box.
• IntermediateField.aemeasurable_rootCount: the same for the root count IntermediateField.rootCount in a finite intermediate field of any extension of K.

Implementation notes

The roots in L of a monic polynomial p over 𝒪[K] lie in 𝒪[L] (TauCeti.aroots_eq_map_roots_integerRing), and p has at least k of them exactly when it factors over 𝒪[L] as ∏ j, (X - x j) * q with q monic of degree n - k. The tuples (x, q, p) satisfying this form a closed subset of a product of copies of 𝒪[L] and 𝒪[K], which is compact, and the set of the statement is its image under the projection to p.

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, §2.

theorem TauCeti.isCompact_setOf_le_card_aroots {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (L : Type u_2) [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] (n k : ℕ) : IsCompact {a : Fin n → K | a ∈ integerBox K (Fin n) ∧ k ≤ ((Polynomial.monicOfCoeff a).aroots L).card}

The superlevel sets of the root count are compact. For an extension L / K of nonarchimedean local fields, the coefficient vectors a in the integer box 𝒪[K] ^ n whose monic polynomial monicOfCoeff a has at least k roots in L, counted with multiplicity, form a compact subset of Fin n → K.

theorem TauCeti.aemeasurable_card_aroots {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (L : Type u_2) [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] {n : ℕ} [MeasurableSpace (Fin n → K)] [OpensMeasurableSpace (Fin n → K)] {ν : MeasureTheory.Measure (Fin n → K)} (hν : ∀ᵐ (a : Fin n → K) ∂ν, a ∈ integerBox K (Fin n)) : AEMeasurable (fun (a : Fin n → K) => ((Polynomial.monicOfCoeff a).aroots L).card) ν

The root count is measurable on the integer box. For an extension L / K of nonarchimedean local fields and a measure ν on Fin n → K carried by the integer box 𝒪[K] ^ n, the number of roots in L of monicOfCoeff a, counted with multiplicity, is an almost everywhere measurable function of a.

theorem IntermediateField.aemeasurable_rootCount {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {Ω : Type u_2} [Field Ω] [Algebra K Ω] (L : IntermediateField K Ω) [FiniteDimensional K ↥L] {n : ℕ} [MeasurableSpace (Fin n → K)] [OpensMeasurableSpace (Fin n → K)] {ν : MeasureTheory.Measure (Fin n → K)} (hν : ∀ᵐ (a : Fin n → K) ∂ν, a ∈ TauCeti.integerBox K (Fin n)) : AEMeasurable (fun (a : Fin n → K) => L.rootCount a) ν

The root count in a finite subextension is measurable on the integer box. For a finite intermediate field L of an extension Ω / K and a measure ν on Fin n → K carried by the integer box 𝒪[K] ^ n, the root count L.rootCount a is an almost everywhere measurable function of a. No topology or valuation on Ω is needed: L carries its canonical structure of a nonarchimedean local field.