The étale convention for the type densities

1/-2Copyright (c) 2026 Asvin G, Claude (Anthropic), GPT-6-Astra (OpenAI). All rights reserved.3Released under Apache 2.0 license as described in the file LICENSE.4Authors: Asvin G, Claude (Anthropic), GPT-6-Astra (OpenAI)5-/6import SurfaceBlowup.Basic7 8/-!9# The étale convention for the type densities10 11The published densities `monicDensity`, `projectiveDensity` (in `SurfaceBlowup.Basic`) define the12type of a polynomial through finite integral closures (the reduced-algebra convention). This file13defines the densities under the étale convention, where the event is restricted to separable14polynomials (étale algebras `K[X]/(f_a)`), resp. to binary forms with finite étale zero scheme.15 16## Main definitions17 18* `SurfaceBlowup.IsEtaleForm`19* `SurfaceBlowup.etaleMonicDensity`, `SurfaceBlowup.etaleProjectiveDensity`20-/21 22open MeasureTheory23open scoped ENNReal24 25namespace SurfaceBlowup26 27section EtaleForm28 29variable (O : Type) [CommRing O] [IsDomain O]30 31/-- The binary form `F_a` is étale of degree `n` (its zero scheme in `ℙ¹_K` is finite étale of32degree `n`): nonzero, degree drop at most one (so the point at infinity has multiplicity at most33one), and separable dehomogenization `F_a(X,1)`. -/34def IsEtaleForm {n : ℕ} (a : Fin (n + 1) → O) : Prop :=Remark 1.335  affinePolynomial O a ≠ 0 ∧ n - (affinePolynomial O a).natDegree ≤ 1 ∧36    (affinePolynomial O a).Separable37 38end EtaleForm39 40section EtaleMeasure41 42variable (O : Type) [CommRing O] [IsDomain O]43  [TopologicalSpace O] [IsTopologicalRing O] [CompactSpace O] [T2Space O]44  [SecondCountableTopology O]45  [MeasurableSpace O] [BorelSpace O]46 47/-- The monic probability of type `σ` under the étale convention: the event is restricted to48separable polynomials, i.e. to étale algebras `K[X]/(f_a)`. -/49noncomputable def etaleMonicDensity (n : ℕ) (σ : FactorType) : ℝ≥0∞ :=50  coefficientMeasure O n51    {a | (monicPolynomial O a).Separable ∧ HasPolynomialType O (monicPolynomial O a) σ}52 53/-- The projective probability of type `σ` under the étale convention. -/54noncomputable def etaleProjectiveDensity (n : ℕ) (σ : FactorType) : ℝ≥0∞ :=55  coefficientMeasure O (n+1) {a | primitive O a ∧ IsEtaleForm O a ∧ HasBinaryType O a σ} /56    coefficientMeasure O (n+1) {a | primitive O a}57 58end EtaleMeasure59 60end SurfaceBlowup