Almost every Eisenstein polynomial is separable

Over a nonarchimedean local field, the nonseparable Eisenstein polynomials form a null set for additive Haar measure on coefficient space. An Eisenstein polynomial is irreducible; when its linear coefficient is nonzero, its derivative is nonzero and it is separable. The exceptional coordinate hyperplane is null inside the integer box, since boxes with one coordinate in deeper powers of the maximal ideal have volumes tending to zero.

The linear case is separable everywhere. The result also applies in equal characteristic, where inseparable Eisenstein polynomials do exist and must be discarded in root counting.

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, equation (3).
• The linear-coefficient separability argument is adapted from separable_toPoly and ae_separable in MassFormula/First.lean of 0stellensatz/MassFormula, Apache-2.0.

theorem TauCeti.separable_monicOfCoeff_of_mem_eisensteinSet_of_coeff_one_ne_zero {K : Type u_1} [Field K] [ValuativeRel K] {n : ℕ} [IsDiscreteValuationRing ↥(ValuativeRel.valuation K).integer] (hn : 1 < n) {a : Fin n → K} (ha : a ∈ eisensteinSet K n) (h1 : a ⟨1, hn⟩ ≠ 0) : (Polynomial.monicOfCoeff a).Separable

An Eisenstein polynomial with nonzero linear coefficient is separable, including in positive characteristic.

theorem TauCeti.ae_separable_monicOfCoeff_restrict_eisensteinSet {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {n : ℕ} (hn : 0 < n) [MeasurableSpace (Fin n → K)] [BorelSpace (Fin n → K)] (μ : MeasureTheory.Measure (Fin n → K)) [μ.IsAddHaarMeasure] : ∀ᵐ (a : Fin n → K) ∂μ.restrict (eisensteinSet K n), (Polynomial.monicOfCoeff a).Separable

Almost every Eisenstein polynomial of positive degree is separable. No normalization of the additive Haar measure is needed.