Monic, projective and divisor cells

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.Assembly.TypeEvents7 8/-!9# Monic, projective and divisor cells10 11Residue-cell decompositions of spaces of polynomials over a complete DVR `O` with finite residue12field, and the laws of the factorization-type events on each cell, assuming the root cell law13`RootCellLaw`. Monic polynomials of degree `n` are partitioned into residue cells indexed by affine14divisors, primitive vectors into projective cells indexed by all divisors; each cell factors into15point cells and a cell at infinity, whose laws are descended from the root cell law.16 17## Main results18 19* `monic_cells_partition`, `projective_cells_partition`: the cell partitions.20* `product_law_of_factor_laws`: the law of a product of coprime cells.21* `point_cell_type_event`, `infinity_block_event_law`: laws of point cells and the cell at infinity.22* `divisor_form_cell_law`, `monic_cell_law`, `projective_cell_affine_type_event`: cell laws.23* `affine_type_event_primitive_density`: the primitive density of an affine type event.24 25Provenance: `Thm_SurfaceBlowupV2_{monic_cells_partition, point_chart_bijection,26product_cell_type_event_sets, product_cell_type_event_mass, product_law_of_factor_laws,27projective_divisor_count, projective_divisor_of_residue_vector, projective_cells_partition,28zero_cell_scaled, zero_cell_type_event_mass, point_cell_type_event, irreducible_cell_type_event,29infinity_block_event_law, divisor_form_cell_law, monic_cell_law,30projective_cell_affine_type_event, affine_type_event_primitive_density}`.31-/32 33namespace SurfaceBlowup34 35open scoped BigOperators ENNReal36 37/-! ### Normalized cell measures -/38 39/-- On a measurable cell `S` of finite positive mass, the coefficient measure of `E ∩ S` is the40mass of `S` times the normalized cell measure of `E`. -/41private theorem coefficientMeasure_inter_eq_mul (O : Type) [CommRing O] [IsDomain O]42    [TopologicalSpace O] [IsTopologicalRing O] [CompactSpace O] [T2Space O]43    [SecondCountableTopology O] [MeasurableSpace O] [BorelSpace O] {n : ℕ} {S : Set (Fin n → O)}44    (hS : MeasurableSet S) (h0 : coefficientMeasure O n S ≠ 0)45    (htop : coefficientMeasure O n S ≠ ⊤) (E : Set (Fin n → O)) :46    coefficientMeasure O n (E ∩ S) = coefficientMeasure O n S * cellMeasure O n S E := by47  rw [cellMeasure_apply_of_measurableSet O n S hS E, ← mul_assoc, ENNReal.mul_inv_cancel h0 htop,48    one_mul]49 50/-- If the cells `cell D` (`D ∈ S`) are measurable subsets of `P` and every point of `P` lies in51exactly one of them, then the measure of `E ∩ P` is the sum of the measures of `E ∩ cell D`. -/52private theorem measure_inter_eq_sum_cells {α ι : Type} [MeasurableSpace α]53    (μ : MeasureTheory.Measure α) {p : ι → Prop} (S : Finset ι) (hS : ∀ D, D ∈ S ↔ p D)54    (cell : ι → Set α) (P : Set α) (huniq : ∀ a ∈ P, ∃! D, p D ∧ a ∈ cell D)55    (hsub : ∀ D, p D → cell D ⊆ P) (hmeas : ∀ D, p D → MeasurableSet (cell D)) {E : Set α}56    (hE : MeasurableSet E) : μ (E ∩ P) = ∑ D ∈ S, μ (E ∩ cell D) := by57  have heq : E ∩ P = ⋃ D ∈ S, E ∩ cell D := by58    ext a59    simp only [Set.mem_inter_iff, Set.mem_iUnion, exists_prop, hS]60    refine ⟨fun ⟨haE, ha⟩ ↦ ?_, fun ⟨D, hD, haE, hc⟩ ↦ ⟨haE, hsub D hD hc⟩⟩61    obtain ⟨D, hD, -⟩ := huniq a ha62    exact ⟨D, hD.1, haE, hD.2⟩63  rw [heq]64  refine MeasureTheory.measure_biUnion_finset (fun D hD D' hD' hne ↦ Set.disjoint_left.2 ?_)65    fun D hD ↦ hE.inter (hmeas D ((hS D).1 hD))66  rintro a ⟨-, ha⟩ ⟨-, ha'⟩67  exact hne ((huniq a (hsub D ((hS D).1 hD) ha)).unique ⟨(hS D).1 hD, ha⟩ ⟨(hS D').1 hD', ha'⟩)68 69/-! ### Partitions into residue cells -/70 71/-- **Monic cell partition.** The monic polynomials of degree `n` over `O` are partitioned into the72residue cells of the affine divisors of degree `n` over the residue field: there are finitely many73such divisors, every coefficient vector lies in exactly one cell, each cell is measurable of mass74`q⁻ⁿ`, and the coefficient measure decomposes as a sum over cells. -/75theorem monic_cells_partition (O : Type) [CommRing O] [IsDomain O] [IsDiscreteValuationRing O]Lemma 7.176    [IsAdicComplete (IsLocalRing.maximalIdeal O) O] [Finite (IsLocalRing.ResidueField O)]77    [TopologicalSpace O] [IsTopologicalRing O] [CompactSpace O] [T2Space O]78    [SecondCountableTopology O] [MeasurableSpace O] [BorelSpace O]79    (htop : IsAdic (IsLocalRing.maximalIdeal O)) (n : ℕ) :80    (∃ S : Finset (ExceptionalDivisor (IsLocalRing.ResidueField O)), ∀ D, D ∈ S ↔ AffineDivisor81      (IsLocalRing.ResidueField O) n D) ∧ (∀ a : Fin n → O, ∃! D : ExceptionalDivisor82      (IsLocalRing.ResidueField O), AffineDivisor (IsLocalRing.ResidueField O) n D ∧ a ∈83      residueCell O n (divisorAffinePolynomial (IsLocalRing.ResidueField O) D)) ∧84      (∀ D : ExceptionalDivisor (IsLocalRing.ResidueField O), AffineDivisor85      (IsLocalRing.ResidueField O) n D → MeasurableSet (residueCell O n86      (divisorAffinePolynomial (IsLocalRing.ResidueField O) D)) ∧ coefficientMeasure O n87      (residueCell O n (divisorAffinePolynomial (IsLocalRing.ResidueField O) D)) =88      (Nat.card (IsLocalRing.ResidueField O) : ℝ≥0∞)⁻¹ ^ n ∧ ∀ E : Set (Fin n → O),89      coefficientMeasure O n (E ∩ residueCell O n90      (divisorAffinePolynomial (IsLocalRing.ResidueField O) D)) =91      (Nat.card (IsLocalRing.ResidueField O) : ℝ≥0∞)⁻¹ ^ n * cellMeasure O n92      (residueCell O n (divisorAffinePolynomial (IsLocalRing.ResidueField O) D)) E) ∧ ∀ S : Finset93      (ExceptionalDivisor (IsLocalRing.ResidueField O)),94      (∀ D, D ∈ S ↔ AffineDivisor (IsLocalRing.ResidueField O) n D) → ∀ E : Set (Fin n → O),95      MeasurableSet E → coefficientMeasure O n E = ∑ D ∈ S, coefficientMeasure O n96      (E ∩ residueCell O n (divisorAffinePolynomial (IsLocalRing.ResidueField O) D)) := by97  set k := IsLocalRing.ResidueField O98  have aux (D) (hD : AffineDivisor k n D) :99      (divisorAffinePolynomial k D).Monic ∧ (divisorAffinePolynomial k D).natDegree = n := by100    obtain ⟨hm, hn, -⟩ := divisor_vector_properties k n D hD.2101    exact ⟨hm, by rw [hn, hD.1, Nat.sub_zero]⟩102  -- unique cell103  have huniq : ∀ a : Fin n → O, ∃! D : ExceptionalDivisor k, AffineDivisor k n D ∧104      a ∈ residueCell O n (divisorAffinePolynomial k D) := by105    intro a106    obtain ⟨hm, hdeg, -, -⟩ := monic_poly_reconstruct O n a107    have hG : ((monicPolyO a).map (IsLocalRing.residue O)).Monic := hm.map _108    have hGn : ((monicPolyO a).map (IsLocalRing.residue O)).natDegree = n := by109      rw [hm.natDegree_map, hdeg]110    obtain ⟨D, ⟨hDa, hDp⟩, hDu⟩ := monic_polynomial_divisor k n _ hG hGn111    refine ⟨D, ⟨hDa, ?_⟩, ?_⟩112    · change _ = _; exact hDp.symm113    · rintro D' ⟨hD'a, hD'c⟩114      exact hDu D' ⟨hD'a, hD'c.symm⟩115  have hinj : ∀ D D' : ExceptionalDivisor k, AffineDivisor k n D → AffineDivisor k n D' →116      divisorAffinePolynomial k D = divisorAffinePolynomial k D' → D = D' := by117    intro D D' hD hD' h118    obtain ⟨hm, hn⟩ := aux D hD119    obtain ⟨E, -, hE⟩ := monic_polynomial_divisor k n _ hm hn120    exact (hE D ⟨hD, rfl⟩).trans (hE D' ⟨hD', h.symm⟩).symm121  have hcell : ∀ D : ExceptionalDivisor k, AffineDivisor k n D →122      MeasurableSet (residueCell O n (divisorAffinePolynomial k D)) ∧123      coefficientMeasure O n (residueCell O n (divisorAffinePolynomial k D)) =124        (Nat.card k : ℝ≥0∞)⁻¹ ^ n := by125    intro D hD126    obtain ⟨hm, hn⟩ := aux D hD127    obtain ⟨h1, h2, -⟩ := residue_cell_mass O htop n _ hm hn128    exact ⟨h1, h2⟩129  refine ⟨?_, huniq, ?_, ?_⟩130  · have hfin : Set.Finite {D : ExceptionalDivisor k | AffineDivisor k n D} := by131      have hT : Finite {F : Polynomial k // F.Monic ∧ F.natDegree = n} := by132        apply Nat.finite_of_card_ne_zero133        rw [monic_residue_polynomial_count k n]134        exact pow_ne_zero _ Nat.card_pos.ne'135      have : Finite {D : ExceptionalDivisor k // AffineDivisor k n D} :=136        Finite.of_injective137          (fun D => (⟨divisorAffinePolynomial k D.1, aux D.1 D.2⟩ :138            {F : Polynomial k // F.Monic ∧ F.natDegree = n}))139          (fun D D' h => Subtype.ext (hinj D D' D.2 D'.2 (congrArg Subtype.val h)))140      exact Set.finite_coe_iff.mp this141    exact ⟨hfin.toFinset, fun D => by rw [Set.Finite.mem_toFinset]; rfl⟩142  · intro D hD143    obtain ⟨h1, h2⟩ := hcell D hD144    refine ⟨h1, h2, fun E ↦ h2 ▸ coefficientMeasure_inter_eq_mul O h1 ?_ ?_ E⟩145    · exact h2 ▸ pow_ne_zero _ (ENNReal.inv_ne_zero.2 (ENNReal.natCast_ne_top _))146    · exact h2 ▸ ENNReal.pow_ne_top (ENNReal.inv_ne_top.2 (by exact_mod_cast Nat.card_pos.ne'))147  · intro S hS E hE148    simpa using measure_inter_eq_sum_cells (coefficientMeasure O n) S hS _ Set.univ149      (fun a _ ↦ huniq a) (fun _ _ ↦ Set.subset_univ _) (fun D hD ↦ (hcell D hD).1) hE150 151/-- The point chart is a bijection from the residue cell of `(Φ mod π)^r` onto the zero cell over152`O[X]/(Φ)`, and it identifies the congruence filtrations on both sides. -/153private theorem point_chart_bijection (O : Type) [CommRing O] [IsDomain O]154    [IsDiscreteValuationRing O]155    [IsAdicComplete (IsLocalRing.maximalIdeal O) O] [Finite (IsLocalRing.ResidueField O)]156    (Φ : Polynomial O) (hΦ : IsUnramifiedLift O Φ) (r : ℕ) :157    Set.BijOn (pointChart O Φ r) (residueCell O (Φ.natDegree * r) (residuePoly O Φ ^ r))158      (zeroCell O Φ r) ∧ ∀ (L : ℕ), ∀ a ∈ residueCell O (Φ.natDegree * r) (residuePoly O Φ ^ r),159      ∀ a' ∈ residueCell O (Φ.natDegree * r) (residuePoly O Φ ^ r),160      (∀ j, a j - a' j ∈ (IsLocalRing.maximalIdeal O) ^ L) ↔ ∀ j,161      pointChart O Φ r a j - pointChart O Φ r a' j ∈ (baseIdeal O Φ) ^ L := by162  have h1 := block_descent_bijection O Φ hΦ r163  have h2 := block_translation O Φ hΦ r164  refine ⟨h2.1.comp h1.1, fun L a ha a' ha' => ?_⟩165  exact (block_descent_congruence_iff O Φ hΦ r L a a' ha ha').trans166    (h2.2 L _ _)167 168/-! ### Product cells -/169 170/-- A point of a product of coprime residue cells has type `σ` after multiplying out iff its171factors have types `τ j` with `σ = ∑ j, τ j`. -/172private theorem factorProduct_mem_typeEvent_iff (O : Type) [CommRing O] [IsDomain O]173    [IsDiscreteValuationRing O] [IsAdicComplete (IsLocalRing.maximalIdeal O) O]174    [Finite (IsLocalRing.ResidueField O)] (L : ℕ)175    (g : Fin L → Polynomial (IsLocalRing.ResidueField O))176    (hc : ∀ i j, i ≠ j → IsCoprime (g i) (g j)) (σ : FactorType) (a : ∀ j, Fin (g j).natDegree → O)177    (ha : a ∈ Set.pi Set.univ fun j ↦ residueCell O (g j).natDegree (g j)) :178    factorProduct (fun j ↦ (g j).natDegree) a ∈ typeEvent O (∑ j, (g j).natDegree) σ ↔179      ∃ τ : Fin L → FactorType, (∀ j, a j ∈ typeEvent O (g j).natDegree (τ j)) ∧180        σ = ∑ j, τ j := by181  set d : Fin L → ℕ := fun j ↦ (g j).natDegree182  have hmon : ∀ j, (monicPolyO (a j)).Monic := fun j ↦ (monic_poly_reconstruct O (d j) (a j)).1183  have hprod : monicPolynomial O (factorProduct d a) = ∏ j, monicPolynomial O (a j) := by184    have hdeg : (∏ j, monicPolyO (a j)).natDegree = ∑ j, d j := by185      rw [Polynomial.natDegree_prod_of_monic _ _ fun j _ ↦ hmon j]186      exact Finset.sum_congr rfl fun j _ ↦ (monic_poly_reconstruct O (d j) (a j)).2.1187    rw [← monicPolyO_map_fraction,188      show monicPolyO (factorProduct d a) = ∏ j, monicPolyO (a j) from189      (monic_poly_reconstruct O _ (factorProduct d a)).2.2.2 _190        (Polynomial.monic_prod_of_monic _ _ fun j _ ↦ hmon j) hdeg, Polynomial.map_prod]191    exact Finset.prod_congr rfl fun j _ ↦ monicPolyO_map_fraction O (a j)192  refine (congrArg (HasPolynomialTypeF O · σ) hprod).to_iff.trans193    (coprime_family_type_iff O (Fin L) _ (fun j ↦ (monic_polynomial_degree O (d j) (a j)).1)194      (fun i j hij ↦ ?_) σ)195  rw [← monicPolyO_map_fraction, ← monicPolyO_map_fraction]196  refine coprime_of_coprime_residue_dvr O (BaseField O) _ _ (hmon i) (hmon j) ?_197  rw [show (monicPolyO (a i)).map (IsLocalRing.residue O) = g i from ha i (Set.mem_univ _),198    show (monicPolyO (a j)).map (IsLocalRing.residue O) = g j from ha j (Set.mem_univ _)]199  exact hc i j hij200 201/-- The trace on the product of coprime residue cells of the preimage of the type event `σ` is202the finite union, over factor types `τ ∈ W` adding up to `σ`, of products of factor events. -/203private theorem factorProduct_preimage_typeEvent_eq (O : Type) [CommRing O] [IsDomain O]204    [IsDiscreteValuationRing O] [IsAdicComplete (IsLocalRing.maximalIdeal O) O]205    [Finite (IsLocalRing.ResidueField O)] (L : ℕ)206    (g : Fin L → Polynomial (IsLocalRing.ResidueField O)) (hg : ∀ j, (g j).Monic)207    (hc : ∀ i j, i ≠ j → IsCoprime (g i) (g j)) (W : Fin L → Finset FactorType)208    (hW : ∀ j τ, (residueCell O (g j).natDegree (g j) ∩ typeEvent O (g j).natDegree209      τ).Nonempty → τ ∈ W j) (σ : FactorType) :210    factorProduct (fun j ↦ (g j).natDegree) ⁻¹' (residueCell O (∑ j, (g j).natDegree) (∏ j, g j) ∩211      typeEvent O (∑ j, (g j).natDegree) σ) ∩212        Set.pi Set.univ (fun j ↦ residueCell O (g j).natDegree (g j)) =213      ⋃ τ ∈ (Fintype.piFinset W).filter (fun τ : Fin L → FactorType ↦ σ = ∑ j, τ j),214        Set.pi Set.univ fun j ↦ residueCell O (g j).natDegree (g j) ∩215          typeEvent O (g j).natDegree (τ j) :=216  preimage_inter_pi_eq_biUnion _ _ _ _ (factor_product_bijection O (Fin L) g hg hc).mapsTo217    (fun j ↦ typeEvent O (g j).natDegree) W hW σ (factorProduct_mem_typeEvent_iff O L g hc σ · ·) _218    fun _ ↦ by rw [Finset.mem_filter, Fintype.mem_piFinset]219 220/-- A type event in a product of coprime residue cells is measurable. -/221private theorem measurableSet_product_cell_typeEvent (O : Type) [CommRing O] [IsDomain O]222    [IsDiscreteValuationRing O] [IsAdicComplete (IsLocalRing.maximalIdeal O) O]223    [Finite (IsLocalRing.ResidueField O)] [TopologicalSpace O] [IsTopologicalRing O]224    [CompactSpace O] [T2Space O] [SecondCountableTopology O] [MeasurableSpace O] [BorelSpace O]225    (htop : IsAdic (IsLocalRing.maximalIdeal O)) (L : ℕ)226    (g : Fin L → Polynomial (IsLocalRing.ResidueField O)) (hg : ∀ j, (g j).Monic)227    (hc : ∀ i j, i ≠ j → IsCoprime (g i) (g j)) (W : Fin L → Finset FactorType)228    (hW : ∀ j τ, (residueCell O (g j).natDegree (g j) ∩ typeEvent O (g j).natDegree229      τ).Nonempty → τ ∈ W j)230    (hmeas : ∀ j τ, MeasurableSet (residueCell O (g j).natDegree (g j) ∩ typeEvent O231      (g j).natDegree τ)) (σ : FactorType) :232    MeasurableSet (residueCell O (∑ j, (g j).natDegree) (∏ j, g j) ∩233      typeEvent O (∑ j, (g j).natDegree) σ) := by234  set d : Fin L → ℕ := fun j ↦ (g j).natDegree235  have hbij := factor_product_bijection O (Fin L) g hg hc236  choose c hcmem using fun j ↦ (residue_cell_cylinder O (d j) (g j)).2.1 (hg j) rfl237  have hclosed : IsClosed (Set.pi Set.univ fun j ↦ residueCell O (d j) (g j)) := by238    convert (coordinate_cylinder_clopen O (IsLocalRing.maximalIdeal O) htop 1).2.2 (Fin L) d c239      using 3 with j240    rw [pow_one]; exact (residue_cell_cylinder O (d j) (g j)).1 (c j) (hcmem j)241  exact measurableSet_inter_of_bijOn hclosed242    (factor_product_continuous O (Fin L) d).1.continuousOn hbij243    (factorProduct_preimage_typeEvent_eq O L g hg hc W hW σ ▸244      Finset.measurableSet_biUnion _ fun (τ : Fin L → FactorType) _ ↦245        .univ_pi fun j ↦ hmeas j (τ j))246 247/-- **Product law.** If the coprime factor cells have laws `Dl j`, then the product cell has law248`lawProd (List.ofFn Dl)`. -/249theorem product_law_of_factor_laws (O : Type) [CommRing O] [IsDomain O] [IsDiscreteValuationRing O]250    [IsAdicComplete (IsLocalRing.maximalIdeal O) O] [Finite (IsLocalRing.ResidueField O)]251    [TopologicalSpace O] [IsTopologicalRing O] [CompactSpace O] [T2Space O]252    [SecondCountableTopology O] [MeasurableSpace O] [BorelSpace O]253    (htop : IsAdic (IsLocalRing.maximalIdeal O)) (L : ℕ)254    (g : Fin L → Polynomial (IsLocalRing.ResidueField O)) (hg : ∀ j, (g j).Monic)255    (hc : ∀ i j, i ≠ j → IsCoprime (g i) (g j)) (Dl : Fin L → Law)256    (hnn : ∀ (j : Fin L) (τ : FactorType), 0 ≤ (lawCoeff (Dl j) τ).eval257      (Nat.card (IsLocalRing.ResidueField O)))258    (hlaw : ∀ (j : Fin L) (τ : FactorType), MeasurableSet259      (residueCell O (g j).natDegree (g j) ∩ typeEvent O (g j).natDegree τ) ∧ cellMeasure O260      (g j).natDegree (residueCell O (g j).natDegree (g j)) (typeEvent O (g j).natDegree τ) =261      densityValue (lawCoeff (Dl j) τ) (Nat.card (IsLocalRing.ResidueField O))) (σ : FactorType) :262    MeasurableSet (residueCell O (∑ j, (g j).natDegree) (∏ j, g j) ∩ typeEvent O263      (∑ j, (g j).natDegree) σ) ∧ cellMeasure O (∑ j, (g j).natDegree)264      (residueCell O (∑ j, (g j).natDegree) (∏ j, g j)) (typeEvent O (∑ j, (g j).natDegree) σ) =265      densityValue (lawCoeff (lawProd (List.ofFn Dl)) σ)266      (Nat.card (IsLocalRing.ResidueField O)) := by267  let W : Fin L → Finset FactorType := fun j =>268    (finite_types_of_degree (g j).natDegree).toFinset ∪ ((Dl j).map Prod.fst).toFinset269  have hW : ∀ j τ, (residueCell O (g j).natDegree (g j) ∩ typeEvent O (g j).natDegree τ).Nonempty →270      τ ∈ W j := by271    intro j τ ⟨a, _, ha⟩272    have h1 := polynomial_type_degree O _ τ ha273    have h2 := (monic_polynomial_degree O _ a).2274    simp only [W, Finset.mem_union, Set.Finite.mem_toFinset, Set.mem_ofPred_eq]275    exact Or.inl ⟨h1.1, h1.2.trans h2⟩276  have hmeas := fun j τ ↦ (hlaw j τ).1277  have hcell := fun j ↦ residue_cell_mass O htop _ (g j) (hg j) rfl278  have : ∀ j, MeasureTheory.IsProbabilityMeasure279      (cellMeasure O _ (residueCell O (g j).natDegree (g j))) := fun j ↦ (hcell j).2.2280  have hE := measurableSet_product_cell_typeEvent O htop L g hg hc W hW hmeas σ281  refine ⟨hE, ?_⟩282  rw [← cellMeasure_cell_inter (residue_cell_mass O htop _ (∏ j, g j)283      (Polynomial.monic_prod_of_monic _ _ fun j _ ↦ hg j)284      (Polynomial.natDegree_prod_of_monic _ _ fun j _ ↦ hg j)).1,285    measure_eq_sum_prod_of_preimage _ (factor_cells_measure_preserving O htop (Fin L) g hg hc) _286      (factor_cell_product_measure O htop (Fin L) g hg).2.1287      (fun j ↦ cellMeasure_cell_inter (hcell j).1) _ hmeas288      (fun _ _ _ _ h1 h2 ↦ polynomial_type_unique O _ _ _ h1 h2) hE _289      (factorProduct_preimage_typeEvent_eq O L g hg hc W hW σ),290    Finset.sum_congr rfl fun τ _ ↦ Finset.prod_congr rfl fun j _ ↦ (hlaw j (τ j)).2]291  exact sum_prod_densityValue_eq_lawProd Dl _ hnn W (fun _ ↦ Finset.subset_union_right) σ292 293/-! ### Projective cells -/294 295/-- The number of divisors of degree `n` with array `m` is `divisorCount 1 m` evaluated at the296residue field size. -/297private theorem projective_divisor_count (k : Type) [Field k] [Finite k] (n : ℕ) (m : Pattern n)298    (hm : m ∈ residuePatterns n) :299    Finite {D : ExceptionalDivisor k // exceptionalDegree k D = n ∧ HasArray k n D m} ∧300      ((Nat.card {D : ExceptionalDivisor k // exceptionalDegree k D = n ∧ HasArray k n D m} : ℕ) :301      ℚ) = (divisorCount 1 m).eval (Nat.card k) := by302  have hpt : ∀ δ : ℕ, 0 < δ → ((Nat.card {Q : ClosedDirection k // directionDegree k Q = δ} : ℕ) :303      ℚ) = (availablePoints 1 δ).eval (Nat.card k) := by304    intro δ hδ305    have h915 := nonboundary_direction_count k (State.single 1 1) δ hδ306    simp only at h915307    by_cases h1 : δ = 1308    · subst h1309      have hq : (Nat.card k : ℚ) ≠ 0 := by310        have : 0 < Nat.card k := Nat.card_pos311        exact_mod_cast this.ne'312      have hB :313          ((Nat.card {Q : ClosedDirection k // Q ∉ boundaryDirections k (State.single 1 1) ∧314          directionDegree k Q = 1} : ℕ) : ℚ) = Nat.card k := by315        rw [h915]; simp [availablePoints, Expr.eval]316      have hne : Nat.card {Q : ClosedDirection k // Q ∉ boundaryDirections k (State.single 1 1) ∧317          directionDegree k Q = 1} ≠ 0 := by318        intro h; rw [h] at hB; exact hq (by simpa using hB.symm)319      have := Nat.finite_of_card_ne_zero hne320      have e : {Q : ClosedDirection k // directionDegree k Q = 1} ≃ Option321          {Q : ClosedDirection k // Q ∉ boundaryDirections k (State.single 1 1) ∧ directionDegree k322          Q = 1} :=323        { toFun := fun Q => match Q with324            | ⟨none, _⟩ => none325            | ⟨some φ, h⟩ => some ⟨some φ, by simp [boundaryDirections, infinityDirection], h⟩326          invFun := fun o => match o with327            | none => ⟨none, rfl⟩328            | some Q => ⟨Q.1, Q.2.2⟩329          left_inv := by330            rintro ⟨Q, h⟩331            cases Q <;> rfl332          right_inv := by333            rintro (_ | ⟨Q, h⟩)334            · rfl335            · cases Q <;> simp [boundaryDirections, infinityDirection] at h ⊢ }336      rw [Nat.card_congr e, Nat.card_congr (Equiv.optionEquivSumPUnit.{0} _), Nat.card_sum,337          Nat.card_eq_fintype_card (α := PUnit), Fintype.card_punit, Nat.cast_add, hB]338      simp [availablePoints, Expr.eval]339    · have : ∀ Q : ClosedDirection k, directionDegree k Q = δ → Q ∉ boundaryDirections k340        (State.single 1 1) := by341        intro Q hQ hb342        obtain rfl : Q = infinityDirection k := hb343        exact h1 hQ.symm344      have e : Nat.card {Q : ClosedDirection k // directionDegree k Q = δ} = Nat.card345          {Q : ClosedDirection k // Q ∉ boundaryDirections k (State.single 1 1) ∧ directionDegree k346          Q = δ} :=347        Nat.card_congr (Equiv.subtypeEquivRight fun Q => ⟨fun h => ⟨this Q h, h⟩, fun h => h.2⟩)348      rw [e, h915]349      simp [availablePoints, h1]350  have hc : ∀ δ : ℕ, 0 < δ → ((Nat.card {Q : ClosedDirection k // Q ∈351      (Set.univ : Set (ClosedDirection k)) ∧ directionDegree k Q = δ} : ℕ) : ℚ) =352      (availablePoints 1 δ).eval (Nat.card k) := by353    intro δ hδ354    simpa only [Set.mem_univ, true_and] using hpt δ hδ355  have h := divisor_count_eval_of_point_count k Set.univ 1 hc n m hm356  have e : ∀ D : ExceptionalDivisor k, ((∀ Q, D Q ≠ 0 → Q ∈ (Set.univ : Set (ClosedDirection k))) ∧357      exceptionalDegree k D = n ∧ HasArray k n D m) ↔358      (exceptionalDegree k D = n ∧ HasArray k n D m) := by359    intro D; simp360  have eq := Equiv.subtypeEquivRight e361  have := h.1362  exact ⟨Finite.of_equiv _ eq, by rw [← Nat.card_congr eq, h.2]⟩363 364section365 366open Polynomial367 368private lemma formPoly_coeff {A : Type} [CommRing A] {n : ℕ} (v : Fin (n + 1) → A) (j : ℕ) :369    (formPoly v).coeff j = if h : j < n+1 then v ⟨j, h⟩ else 0 := by370  unfold formPoly371  rw [Polynomial.finsetSum_coeff]372  simp only [Polynomial.coeff_C_mul, Polynomial.coeff_X_pow]373  split_ifs with h374  · rw [Finset.sum_eq_single ⟨j, h⟩]375    · simp376    · intro b _ hb377      have : j ≠ (b : ℕ) := fun e => hb (Fin.ext e.symm)378      simp [this]379    · simp380  · apply Finset.sum_eq_zero381    intro b _382    have : j ≠ (b : ℕ) := by omega383    simp [this]384 385private lemma formPoly_smul (k : Type) [Field k] {n : ℕ} (c : k) (w : Fin (n + 1) → k) :386    formPoly (c • w) = C c * formPoly w := by387  unfold formPoly388  rw [Finset.mul_sum]389  refine Finset.sum_congr rfl fun i _ => ?_390  simp [Pi.smul_apply, smul_eq_mul, C_mul, mul_assoc]391 392private lemma exceptionalDegree_add (k : Type) [Field k] (A B : ExceptionalDivisor k) :393    exceptionalDegree k (A + B) = exceptionalDegree k A + exceptionalDegree k B := by394  unfold exceptionalDegree395  exact Finsupp.sum_add_index' (fun _ => by simp) (fun _ _ _ => by ring)396 397private lemma divisorAffinePolynomial_add (k : Type) [Field k] (A B : ExceptionalDivisor k) :398    divisorAffinePolynomial k (A + B) = divisorAffinePolynomial k A *399      divisorAffinePolynomial k B := by400  unfold divisorAffinePolynomial401  refine Finsupp.prod_add_index' (fun P => ?_) (fun P r s => ?_)402  · cases P <;> simp403  · cases P <;> simp [pow_add]404 405private lemma exceptionalDegree_single_none (k : Type) [Field k] (m : ℕ) :406    exceptionalDegree k (Finsupp.single (none : ClosedDirection k) m) = m := by407  unfold exceptionalDegree408  rw [Finsupp.sum_single_index] <;> simp [directionDegree]409 410private lemma divisorAffinePolynomial_single_none (k : Type) [Field k] (m : ℕ) :411    divisorAffinePolynomial k (Finsupp.single (none : ClosedDirection k) m) = 1 := by412  unfold divisorAffinePolynomial413  rw [Finsupp.prod_single_index]; simp414 415private lemma eq_erase_none_add_single (k : Type) [Field k] (D : ExceptionalDivisor k) :416    D = D.erase none + Finsupp.single none (D none) := by417  ext P418  cases P <;> simp419 420end421 422open Polynomial in423/-- Every nonzero residue vector is, up to scaling, the divisor vector of a unique divisor of424degree `n`. -/425private theorem projective_divisor_of_residue_vector (k : Type) [Field k] (n : ℕ)426    (v : Fin (n + 1) → k)427    (hv : v ≠ 0) :428    ∃! D : ExceptionalDivisor k, exceptionalDegree k D = n ∧ v ∈ scalarClass429      (divisorVector k n D) := by430  set H := formPoly v with hHdef431  have hvH : ∀ i : Fin (n+1), v i = H.coeff i := fun i => by432    rw [hHdef, formPoly_coeff, dif_pos i.isLt]433  have hH0 : H ≠ 0 := by434    intro h0; apply hv; funext i; rw [hvH i, h0]; simp435  have hdle : H.natDegree ≤ n := formPoly_natDegree_le v436  set c := H.leadingCoeff with hcdef437  have hc : c ≠ 0 := leadingCoeff_ne_zero.mpr hH0438  set H₀ := C c⁻¹ * H with hH₀def439  have hmon : H₀.Monic := monic_C_mul_of_mul_leadingCoeff_eq_one (inv_mul_cancel₀ hc)440  have hH₀deg : H₀.natDegree = H.natDegree := natDegree_C_mul (inv_ne_zero hc)441  obtain ⟨D₀, ⟨hD₀aff, hD₀P⟩, hD₀u⟩ := monic_polynomial_divisor k _ H₀ hmon hH₀deg442  refine ⟨D₀ + Finsupp.single none (n - H.natDegree), ⟨?_, ?_⟩, ?_⟩443  · rw [exceptionalDegree_add, hD₀aff.2, exceptionalDegree_single_none]; omega444  · refine ⟨c, hc, funext fun i => ?_⟩445    simp only [Pi.smul_apply, smul_eq_mul, divisorVector, divisorAffinePolynomial_add,446        divisorAffinePolynomial_single_none, mul_one, hD₀P,447      hH₀def, coeff_C_mul]448    rw [hvH i, ← mul_assoc, mul_inv_cancel₀ hc, one_mul]449  · rintro D' ⟨hdeg, c', hc', hv'⟩450    obtain ⟨hAmon, hAdeg, hinf, hform, -⟩ := divisor_vector_properties k n D' hdeg451    have hHA : H = C c' * divisorAffinePolynomial k D' := by452      rw [hHdef, hv', formPoly_smul, hform]453    have hcc : c = c' := by454      rw [hcdef, hHA, leadingCoeff_mul, leadingCoeff_C, hAmon.leadingCoeff, mul_one]455    have hH₀A : H₀ = divisorAffinePolynomial k D' := by456      rw [hH₀def, hHA, ← mul_assoc, ← C_mul, hcc, inv_mul_cancel₀ hc', C_1, one_mul]457    have hnone : D' none = n - H.natDegree := by458      have h1 := hAdeg459      rw [← hH₀A, hH₀deg] at h1460      change H.natDegree = n - D' none at h1461      have h3 : D' none ≤ n := hinf462      omega463    have hdec := eq_erase_none_add_single k D'464    have hE : AffineDivisor k H.natDegree (D'.erase none) := by465      refine ⟨Finsupp.erase_same, ?_⟩466      have h2 := hdeg467      rw [hdec, exceptionalDegree_add, exceptionalDegree_single_none] at h2468      omega469    have hEP : divisorAffinePolynomial k (D'.erase none) = H₀ := by470      rw [hH₀A]471      conv_rhs => rw [hdec]472      rw [divisorAffinePolynomial_add, divisorAffinePolynomial_single_none, mul_one]473    have := hD₀u _ ⟨hE, hEP⟩474    rw [hdec, this, hnone]475 476/-- **Projective cell partition.** The primitive coefficient vectors of length `n + 1` are477partitioned into the projective cells of the divisors of degree `n`, each measurable with an478explicit mass, and the coefficient measure decomposes as a sum over cells. -/479theorem projective_cells_partition (O : Type) [CommRing O] [IsDomain O] [IsDiscreteValuationRing O]Lemma 7.1480    [IsAdicComplete (IsLocalRing.maximalIdeal O) O] [Finite (IsLocalRing.ResidueField O)]481    [TopologicalSpace O] [IsTopologicalRing O] [CompactSpace O] [T2Space O]482    [SecondCountableTopology O] [MeasurableSpace O] [BorelSpace O]483    (htop : IsAdic (IsLocalRing.maximalIdeal O)) (n : ℕ) :484    (∃ S : Finset (ExceptionalDivisor (IsLocalRing.ResidueField O)), ∀ D, D ∈ S ↔ exceptionalDegree485      (IsLocalRing.ResidueField O) D = n) ∧ (∀ a : Fin (n+1) → O, primitive O a → ∃! D :486      ExceptionalDivisor (IsLocalRing.ResidueField O), exceptionalDegree487      (IsLocalRing.ResidueField O) D = n ∧ a ∈ projectiveCell O n488      (divisorVector (IsLocalRing.ResidueField O) n D)) ∧489      (∀ D : ExceptionalDivisor (IsLocalRing.ResidueField O), exceptionalDegree490      (IsLocalRing.ResidueField O) D = n → MeasurableSet491      (projectiveCell O n (divisorVector (IsLocalRing.ResidueField O) n D)) ∧ coefficientMeasure O492      (n+1) (projectiveCell O n (divisorVector (IsLocalRing.ResidueField O) n D)) =493      ((Nat.card (IsLocalRing.ResidueField O) : ℝ≥0∞) - 1) *494      (Nat.card (IsLocalRing.ResidueField O) : ℝ≥0∞)⁻¹ ^ (n+1) ∧ ∀ E : Set (Fin (n+1) → O),495      coefficientMeasure O (n+1) (E ∩ projectiveCell O n496      (divisorVector (IsLocalRing.ResidueField O) n D)) = coefficientMeasure O (n+1)497      (projectiveCell O n (divisorVector (IsLocalRing.ResidueField O) n D)) * cellMeasure O (n+1)498      (projectiveCell O n (divisorVector (IsLocalRing.ResidueField O) n D)) E) ∧ ∀ S : Finset499      (ExceptionalDivisor (IsLocalRing.ResidueField O)),500      (∀ D, D ∈ S ↔ exceptionalDegree (IsLocalRing.ResidueField O) D = n) → ∀ E : Set501      (Fin (n+1) → O), MeasurableSet E → coefficientMeasure O (n+1)502      (E ∩ {a : Fin (n+1) → O | primitive O a}) = ∑ D ∈ S, coefficientMeasure O (n+1)503      (E ∩ projectiveCell O n (divisorVector (IsLocalRing.ResidueField O) n D)) := by504  set k := IsLocalRing.ResidueField O505  have hprob := coefficient_measure_probability O htop (n+1)506  -- unique cell507  have huniq : ∀ a : Fin (n+1) → O, primitive O a → ∃! D : ExceptionalDivisor k,508      exceptionalDegree k D = n ∧ a ∈ projectiveCell O n (divisorVector k n D) := by509    intro a ha510    have hv := (primitive_iff_residue_ne_zero O n a).1 ha511    obtain ⟨D, ⟨hD1, hD2⟩, hDu⟩ := projective_divisor_of_residue_vector k n _ hv512    refine ⟨D, ⟨hD1, ha, hD2⟩, ?_⟩513    rintro D' ⟨h1, _, h2⟩514    exact hDu D' ⟨h1, h2⟩515  have hcell : ∀ D : ExceptionalDivisor k, exceptionalDegree k D = n →516      MeasurableSet (projectiveCell O n (divisorVector k n D)) ∧517      coefficientMeasure O (n+1) (projectiveCell O n (divisorVector k n D)) =518        ((Nat.card k : ℝ≥0∞) - 1) * (Nat.card k : ℝ≥0∞)⁻¹ ^ (n+1) := by519    intro D hD520    exact projective_cell_mass O htop n _521      (divisor_vector_properties k n D hD).2.2.2.2.2.2522  refine ⟨?_, huniq, ?_, ?_⟩523  · have hfin : {D : ExceptionalDivisor k | exceptionalDegree k D = n}.Finite := by524      refine Set.Finite.subset (Set.finite_univ.biUnion (t := fun m : Pattern n =>525        {D : ExceptionalDivisor k | exceptionalDegree k D = n ∧ HasArray k n D m ∧526          m ∈ residuePatterns n}) ?_) ?_527      · intro m _528        by_cases hm : m ∈ residuePatterns n529        · have := (projective_divisor_count k n m hm).1530          refine Set.Finite.subset (Set.finite_coe_iff.1 this) ?_531          intro D hD532          exact ⟨hD.1, hD.2.1⟩533        · refine Set.Finite.subset Set.finite_empty ?_534          intro D hD535          exact absurd hD.2.2 hm536      · intro D hD537        obtain ⟨m, hm1, hm2⟩ := (divisor_array_exists_unique k n D hD).1538        exact Set.mem_biUnion (Set.mem_univ m) ⟨hD, hm1, hm2⟩539    exact ⟨hfin.toFinset, fun D => by simp; rfl⟩540  · intro D hD541    obtain ⟨hmeas, hmass⟩ := hcell D hD542    refine ⟨hmeas, hmass,543      coefficientMeasure_inter_eq_mul O hmeas ?_ (MeasureTheory.measure_ne_top _ _)⟩544    have hq : 1 < Nat.card k := Finite.one_lt_card545    rw [hmass]546    refine mul_ne_zero (tsub_pos_of_lt (by exact_mod_cast hq)).ne'547      (pow_ne_zero _ (ENNReal.inv_ne_zero.2 (ENNReal.natCast_ne_top _)))548  · exact fun S hS E hE ↦ measure_inter_eq_sum_cells _ S hS _ _ huniq (fun _ _ _ ha ↦ ha.1)549      (fun D hD ↦ (hcell D hD).1) hE550 551/-! ### Point cells -/552 553/-- The zero cell over `O[X]/(Φ)` is the image of scaling by `π`; under this scaling its type554events are root events, and it is the first congruence neighbourhood of `0`. -/555private theorem zero_cell_scaled (O : Type) [CommRing O] [IsDomain O] [IsDiscreteValuationRing O]556    [IsAdicComplete (IsLocalRing.maximalIdeal O) O] [Finite (IsLocalRing.ResidueField O)]557    (Φ : Polynomial O) [IsDomain (AdjoinRoot Φ)] (pi : O) (hpi : Irreducible pi) (r : ℕ)558    (τ : FactorType) :559    zeroCell O Φ r = (fun z : Fin r → AdjoinRoot Φ => algebraMap O (AdjoinRoot Φ) pi • z) ''560      Set.univ ∧ zeroCell O Φ r ∩ typeEvent (AdjoinRoot Φ) r τ =561      (fun z : Fin r → AdjoinRoot Φ => algebraMap O (AdjoinRoot Φ) pi • z) '' rootEvent562      (AdjoinRoot Φ) (algebraMap O (AdjoinRoot Φ) pi) r τ ∧563      (∀ b : Fin r → AdjoinRoot Φ, b ∈ zeroCell O Φ r ↔ ∀ j, b j - 0 ∈ (baseIdeal O Φ) ^ 1) := by564  have hI : baseIdeal O Φ = Ideal.span {algebraMap O (AdjoinRoot Φ) pi} := by565    unfold baseIdeal566    rw [(IsDiscreteValuationRing.irreducible_iff_uniformizer pi).1 hpi, Ideal.map_span,567      Set.image_singleton]568    rfl569  have hcyl : ∀ b : Fin r → AdjoinRoot Φ, b ∈ zeroCell O Φ r ↔ ∀ j, b j ∈ baseIdeal O Φ := by570    intro b571    have h601 := (monic_poly_reconstruct (AdjoinRoot Φ) r b)572    obtain ⟨-, hdeg, hco, -⟩ := h601573    have h605 := (polynomial_congruence_and_product (AdjoinRoot Φ) (baseIdeal O Φ)).1574    change (monicPolyO b).map (baseReduce O Φ) = Polynomial.X ^ r ↔ _575    have : (Polynomial.X ^ r : Polynomial (residueExtension O Φ)) =576        (Polynomial.X ^ r : Polynomial (AdjoinRoot Φ)).map (baseReduce O Φ) := by simp577    rw [this]578    change (monicPolyO b).map (Ideal.Quotient.mk (baseIdeal O Φ)) =579        (Polynomial.X ^ r : Polynomial (AdjoinRoot Φ)).map (Ideal.Quotient.mk (baseIdeal O Φ)) ↔ _580    rw [h605]581    have hm : (monicPolyO b).Monic := (monic_poly_reconstruct (AdjoinRoot Φ) r b).1582    constructor583    · intro h j584      have := h j585      rw [hco j, Polynomial.coeff_X_pow] at this586      simpa [Fin.val_ne_iff.mp, j.2.ne] using this587    · intro h j588      by_cases hj : j < r589      · have := h ⟨j, hj⟩590        have e := hco ⟨j, hj⟩591        rw [e, Polynomial.coeff_X_pow, if_neg hj.ne]592        simpa using this593      · rcases (not_lt.1 hj).eq_or_lt with hr | hr594        · subst hr595          have h1 : (monicPolyO b).coeff r = 1 := by596            have := hm.coeff_natDegree597            rwa [hdeg] at this598          rw [Polynomial.coeff_X_pow, if_pos rfl, h1]599          simp600        · rw [Polynomial.coeff_eq_zero_of_natDegree_lt (by rw [hdeg]; exact hr),601            Polynomial.coeff_X_pow, if_neg hr.ne']602          simp603  have himg : ∀ b : Fin r → AdjoinRoot Φ, b ∈ zeroCell O Φ r ↔ ∃ z : Fin r → AdjoinRoot Φ,604      algebraMap O (AdjoinRoot Φ) pi • z = b := by605    intro b606    rw [hcyl]607    simp_rw [hI, Ideal.mem_span_singleton']608    constructor609    · intro h610      choose z hz using h611      exact ⟨z, funext fun j => by simp [mul_comm, ← hz j]⟩612    · rintro ⟨z, rfl⟩ j613      exact ⟨z j, by simp [mul_comm]⟩614  refine ⟨?_, ?_, ?_⟩615  · ext b; simp [himg b]616  · ext b617    constructor618    · rintro ⟨hb, ht⟩619      obtain ⟨z, rfl⟩ := (himg b).1 hb620      exact ⟨z, ht, rfl⟩621    · rintro ⟨z, hz, rfl⟩622      exact ⟨(himg _).2 ⟨z, rfl⟩, hz⟩623  · intro b624    rw [hcyl]; simp625 626/-- The zero cell over `O[X]/(Φ)` is measurable of mass `q^{-r deg Φ}`, and assuming the root cell627law its type events have the law of the single state `(1, r)` at the residue size `q^{deg Φ}`. -/628private theorem zero_cell_type_event_mass (hroot : RootCellLaw) (O : Type) [CommRing O] [IsDomain O]629    [IsDiscreteValuationRing O] [IsAdicComplete (IsLocalRing.maximalIdeal O) O]630    [Finite (IsLocalRing.ResidueField O)] [TopologicalSpace O] [IsTopologicalRing O]631    [CompactSpace O] [T2Space O] [SecondCountableTopology O] [MeasurableSpace O] [BorelSpace O]632    (htop : IsAdic (IsLocalRing.maximalIdeal O)) (Φ : Polynomial O) (hΦ : IsUnramifiedLift O Φ)633    [TopologicalSpace (AdjoinRoot Φ)] [MeasurableSpace (AdjoinRoot Φ)]634    (hτ : ‹TopologicalSpace (AdjoinRoot Φ)› = unramifiedTopology O Φ hΦ.1)635    (hmeas : ‹MeasurableSpace (AdjoinRoot Φ)› = unramifiedMeasurableSpace O Φ hΦ.1)636    [IsDomain (AdjoinRoot Φ)] [IsTopologicalRing (AdjoinRoot Φ)] [CompactSpace (AdjoinRoot Φ)]637    [T2Space (AdjoinRoot Φ)] [SecondCountableTopology (AdjoinRoot Φ)] [BorelSpace (AdjoinRoot Φ)]638    (pi : O) (hpi : Irreducible pi) (r : ℕ) (hr : 0 < r) (τ : FactorType) :639    MeasurableSet (zeroCell O Φ r) ∧ coefficientMeasure (AdjoinRoot Φ) r (zeroCell O Φ r) =640      (Nat.card (IsLocalRing.ResidueField O) : ℝ≥0∞)⁻¹ ^ (Φ.natDegree * r) ∧ MeasurableSet641      (zeroCell O Φ r ∩ typeEvent (AdjoinRoot Φ) r τ) ∧ cellMeasure (AdjoinRoot Φ) r642      (zeroCell O Φ r) (typeEvent (AdjoinRoot Φ) r τ) = densityValue643      (lawCoeff (stateLaw (State.single 1 r)) τ) (Nat.card (IsLocalRing.ResidueField O) ^644      Φ.natDegree) := by645  obtain ⟨_, hloc, hcz, hdvr, hcomp, hfin, hcard, -, -, -, -, -, hadic⟩ :=646    unramified_extension_measure_package O htop Φ hΦ hτ hmeas647  obtain ⟨_, _, -, -, hirr, -⟩ := unramified_is_dvr O Φ hΦ648  have hpi' : Irreducible (algebraMap O (AdjoinRoot Φ) pi) := hirr pi hpi649  clear hirr650  have := hloc651  have := hcz652  have := hdvr653  have := hcomp654  have := hfin655  obtain ⟨hR1, hR2⟩ := hroot (AdjoinRoot Φ) hadic _ hpi' r hr τ656  obtain ⟨hz1, hz2, -⟩ := zero_cell_scaled O Φ pi hpi r τ657  obtain ⟨hU1, hU2⟩ := scaling_image_borel_mass (AdjoinRoot Φ) hadic _ hpi' r Set.univ658      MeasurableSet.univ659  obtain ⟨hT1, hT2⟩ := scaling_image_borel_mass (AdjoinRoot Φ) hadic _ hpi' r _ hR1660  have := coefficient_measure_probability (AdjoinRoot Φ) hadic r661  have hq : (Nat.card (IsLocalRing.ResidueField (AdjoinRoot Φ)) : ℝ≥0∞)⁻¹ ^ r662      = (Nat.card (IsLocalRing.ResidueField O) : ℝ≥0∞)⁻¹ ^ (Φ.natDegree * r) := by663    rw [hcard, pow_mul, Nat.cast_pow, ENNReal.inv_pow]664  have hne0 : (Nat.card (IsLocalRing.ResidueField (AdjoinRoot Φ)) : ℝ≥0∞)⁻¹ ^ r ≠ 0 :=665    pow_ne_zero _ (ENNReal.inv_ne_zero.2 (ENNReal.natCast_ne_top _))666  have hpos : Nat.card (IsLocalRing.ResidueField (AdjoinRoot Φ)) ≠ 0 := Nat.card_pos.ne'667  have hnet : (Nat.card (IsLocalRing.ResidueField (AdjoinRoot Φ)) : ℝ≥0∞)⁻¹ ^ r ≠ ⊤ :=668    ENNReal.pow_ne_top (ENNReal.inv_ne_top.2 (by exact_mod_cast hpos))669  rw [← hz1] at hU1 hU2670  unfold rootEvent at hz2671  rw [← hz2] at hT1 hT2672  refine ⟨hU1, ?_, hT1, ?_⟩673  · rw [hU2, MeasureTheory.measure_univ, mul_one, hq]674  · unfold cellMeasure675    rw [MeasureTheory.Measure.smul_apply, MeasureTheory.Measure.restrict_apply' hU1, smul_eq_mul,676      Set.inter_comm, hT2, hU2, MeasureTheory.measure_univ, mul_one, ← mul_assoc,677          ENNReal.inv_mul_cancel hne0 hnet,678      one_mul]679    rw [hR2, hcard]680 681/-- On the residue cell of `(Φ mod π)^r`, the type event of a scaled type `scaleType (deg Φ) τ₀`682is the preimage under the point chart of the type event `τ₀` of the zero cell. -/683private theorem point_cell_typeEvent_scaleType_eq (O : Type) [CommRing O] [IsDomain O]684    [IsDiscreteValuationRing O] [IsAdicComplete (IsLocalRing.maximalIdeal O) O]685    [Finite (IsLocalRing.ResidueField O)] (Φ : Polynomial O) (hΦ : IsUnramifiedLift O Φ)686    [IsDomain (AdjoinRoot Φ)] (r : ℕ) (τ₀ : FactorType) :687    typeEvent O (Φ.natDegree * r) (scaleType Φ.natDegree τ₀) ∩688        residueCell O (Φ.natDegree * r) (residuePoly O Φ ^ r) =689      pointChart O Φ r ⁻¹' (zeroCell O Φ r ∩ typeEvent (AdjoinRoot Φ) r τ₀) ∩690        residueCell O (Φ.natDegree * r) (residuePoly O Φ ^ r) := by691  have hδ : 0 < Φ.natDegree := hΦ.1.natDegree_map (IsLocalRing.residue O) ▸692    Polynomial.natDegree_pos_iff_degree_pos.2 (Polynomial.degree_pos_of_irreducible hΦ.2)693  have hinj := (scale_type_valid_degree_iff Φ.natDegree r hδ τ₀).2694  ext a695  simp only [Set.mem_inter_iff, Set.mem_preimage]696  constructor697  · rintro ⟨h1, h2⟩698    obtain ⟨τ, hτ, he⟩ := (descended_block_type_iff O Φ hΦ r a h2 _).1 h1699    rw [hinj he]700    exact ⟨⟨(point_chart_bijection O Φ hΦ r).1.mapsTo h2, hτ⟩, h2⟩701  · rintro ⟨⟨-, h1⟩, h2⟩702    exact ⟨(descended_block_type_iff O Φ hΦ r a h2 _).2 ⟨τ₀, h1, rfl⟩, h2⟩703 704/-- On the residue cell of `(Φ mod π)^r`, the type event of a type that is not of the form705`scaleType (deg Φ) τ` is empty. -/706private theorem point_cell_inter_typeEvent_eq_empty (O : Type) [CommRing O] [IsDomain O]707    [IsDiscreteValuationRing O] [IsAdicComplete (IsLocalRing.maximalIdeal O) O]708    [Finite (IsLocalRing.ResidueField O)] (Φ : Polynomial O) (hΦ : IsUnramifiedLift O Φ)709    [IsDomain (AdjoinRoot Φ)] (r : ℕ) (σ : FactorType)710    (hσ : ∀ τ, σ ≠ scaleType Φ.natDegree τ) :711    residueCell O (Φ.natDegree * r) (residuePoly O Φ ^ r) ∩ typeEvent O (Φ.natDegree * r) σ =712      ∅ := by713  refine Set.eq_empty_of_forall_notMem fun a ⟨ha, h⟩ ↦ ?_714  obtain ⟨τ, -, he⟩ := (descended_block_type_iff O Φ hΦ r a ha _).1 h715  exact hσ τ he716 717/-- **Point cell law.** Assuming the root cell law, the residue cell of `(Φ mod π)^r` has the law718`lawDescend (deg Φ) (stateLaw (single 1 r))`. -/719theorem point_cell_type_event (hroot : RootCellLaw) (O : Type) [CommRing O] [IsDomain O]720    [IsDiscreteValuationRing O] [IsAdicComplete (IsLocalRing.maximalIdeal O) O]721    [Finite (IsLocalRing.ResidueField O)] [TopologicalSpace O] [IsTopologicalRing O]722    [CompactSpace O] [T2Space O] [SecondCountableTopology O] [MeasurableSpace O] [BorelSpace O]723    (htop : IsAdic (IsLocalRing.maximalIdeal O)) (Φ : Polynomial O) (hΦ : IsUnramifiedLift O Φ)724    (r : ℕ) (hr : 0 < r) (n : ℕ) (hn : Φ.natDegree * r = n) (σ : FactorType) :725    MeasurableSet (residueCell O n (residuePoly O Φ ^ r) ∩ typeEvent O n σ) ∧ cellMeasure O n726      (residueCell O n (residuePoly O Φ ^ r)) (typeEvent O n σ) = densityValue727      (lawCoeff (lawDescend Φ.natDegree (stateLaw (State.single 1 r))) σ)728      (Nat.card (IsLocalRing.ResidueField O)) := by729  -- strategy: transport cell measures along the point chart onto the zero cell over `O[X]/(Φ)`,730  -- where the root cell law applies; non-scaled types have empty events731  subst hn732  let tτ : TopologicalSpace (AdjoinRoot Φ) := unramifiedTopology O Φ hΦ.1733  let tm : MeasurableSpace (AdjoinRoot Φ) := unramifiedMeasurableSpace O Φ hΦ.1734  obtain ⟨hdom, hloc, hchar, hdvr, hcomp, hfin, hcard, htr, hcpt, ht2, hsc, hbor, hadic⟩ :=735    unramified_extension_measure_package O htop Φ hΦ rfl rfl736  obtain ⟨pi, hpi⟩ := IsDiscreteValuationRing.exists_irreducible O737  have hδ : 0 < Φ.natDegree := hΦ.1.natDegree_map (IsLocalRing.residue O) ▸738    Polynomial.natDegree_pos_iff_degree_pos.2 (Polynomial.degree_pos_of_irreducible hΦ.2)739  have hφmon : (residuePoly O Φ ^ r).Monic := (hΦ.1.map _).pow r740  have hφdeg : (residuePoly O Φ ^ r).natDegree = Φ.natDegree * r := by741    rw [(hΦ.1.map _).natDegree_pow, hΦ.1.natDegree_map, mul_comm]742  have hqinv0 : (Nat.card (IsLocalRing.ResidueField O) : ℝ≥0∞)⁻¹ ≠ 0 :=743    ENNReal.inv_ne_zero.2 (ENNReal.natCast_ne_top _)744  obtain ⟨hCm, hCμ, -⟩ := residue_cell_mass O htop (Φ.natDegree * r) _ hφmon hφdeg745  obtain ⟨hZm, hZμ, -, -⟩ := zero_cell_type_event_mass hroot O htop Φ hΦ rfl rfl pi hpi r hr σ746  obtain ⟨hbij, hcong⟩ := point_chart_bijection O Φ hΦ r747  have hmax : IsLocalRing.maximalIdeal (AdjoinRoot Φ) = baseIdeal O Φ :=748    (unramified_is_dvr O Φ hΦ).2.2.2.1749  set C := residueCell O (Φ.natDegree * r) (residuePoly O Φ ^ r) with hC750  set Z := zeroCell O Φ r with hZ751  set T := pointChart O Φ r with hT752  have hmass : ∀ (L : ℕ), 1 ≤ L → ∀ a ∈ C,753      cellMeasure O (Φ.natDegree * r) C {a' | ∀ j, a' j - a j ∈ (IsLocalRing.maximalIdeal O) ^ L}754        = cellMeasure (AdjoinRoot Φ) r Z755            {b | ∀ j, b j - T a j ∈ (IsLocalRing.maximalIdeal (AdjoinRoot Φ)) ^ L} := by756    intro L hL a ha757    have hsub1 : {a' : Fin (Φ.natDegree * r) → O | ∀ j, a' j - a j ∈ (IsLocalRing.maximalIdeal O) ^758        L} ⊆ C := fun a' ha' ↦ by759      rw [hC, (residue_cell_cylinder O _ _).1 a ha]760      exact fun i ↦ Ideal.pow_le_self (by omega) (ha' i)761    have hsub2 : {b : Fin r → AdjoinRoot Φ | ∀ j, b j - T a j ∈762        (IsLocalRing.maximalIdeal (AdjoinRoot Φ)) ^ L} ⊆ Z := fun b hb ↦ by763      have h3 := (zero_cell_scaled O Φ pi hpi r σ).2.2764      have hTa := (h3 _).1 (hbij.mapsTo ha)765      refine (h3 b).2 fun j ↦ ?_766      have hbj := Ideal.pow_le_self (by omega : L ≠ 0) (hb j)767      rw [hmax] at hbj768      rw [show b j - 0 = (b j - T a j) + (T a j - 0) by ring, pow_one]769      exact Ideal.add_mem _ hbj (pow_one (baseIdeal O Φ) ▸ hTa j)770    rw [cellMeasure_apply_of_measurableSet _ _ _ hCm, cellMeasure_apply_of_measurableSet _ _ _ hZm,771      Set.inter_eq_left.mpr hsub1, Set.inter_eq_left.mpr hsub2, hCμ, hZμ,772      coefficient_cylinder_mass O htop, coefficient_cylinder_mass (AdjoinRoot Φ) hadic, hcard]773    congr 1774    rw [residueCard, Nat.cast_pow, ENNReal.inv_pow, ← pow_mul, ← mul_assoc]775  have htrans := cell_transport_preimage O htop (AdjoinRoot Φ) hadic (Φ.natDegree * r) r C Z776    hCm hZm (by rw [hCμ]; exact pow_ne_zero _ hqinv0) (by rw [hZμ]; exact pow_ne_zero _ hqinv0) T777    hbij (by rw [hmax]; exact hcong) hmass778  by_cases hσ : ∃ τ₀, σ = scaleType Φ.natDegree τ₀779  · obtain ⟨τ₀, rfl⟩ := hσ780    obtain ⟨-, -, hZTm, hZTμ⟩ := zero_cell_type_event_mass hroot O htop Φ hΦ rfl rfl pi hpi r hr τ₀781    have hset := point_cell_typeEvent_scaleType_eq O Φ hΦ r τ₀782    obtain ⟨hm1, hm2⟩ := htrans _ hZTm783    refine ⟨?_, ?_⟩784    · rw [Set.inter_comm, hset, Set.inter_comm]; exact hm1785    · rw [cellMeasure_apply_of_measurableSet _ _ _ hCm, hset, ←786        cellMeasure_apply_of_measurableSet _ _ _ hCm, hm2,787        cellMeasure_apply_of_measurableSet _ _ _ hZm]788      have e : zeroCell O Φ r ∩ typeEvent (AdjoinRoot Φ) r τ₀ ∩ Z = typeEvent (AdjoinRoot Φ) r τ₀ ∩789          Z := by790        rw [hZ]; ext x; simp only [Set.mem_inter_iff]; tauto791      rw [e, ← cellMeasure_apply_of_measurableSet _ _ _ hZm, hZTμ]792      simp only [densityValue]793      rw [(law_coeff_descend Φ.natDegree hδ _ τ₀ _).1]794      push_cast795      rfl796  · push Not at hσ797    have hset := point_cell_inter_typeEvent_eq_empty O Φ hΦ r σ hσ798    refine ⟨by rw [hset]; exact MeasurableSet.empty, ?_⟩799    rw [cellMeasure_apply_of_measurableSet _ _ _ hCm, Set.inter_comm, hset]800    simp only [densityValue]801    rw [(law_coeff_descend Φ.natDegree hδ _ σ _).2 σ hσ]802    simp803 804/-- The point cell law for a monic irreducible residue polynomial `φ`, obtained by lifting `φ` to805an unramified `Φ`. -/806private theorem irreducible_cell_type_event (hroot : RootCellLaw) (O : Type) [CommRing O]807    [IsDomain O]808    [IsDiscreteValuationRing O] [IsAdicComplete (IsLocalRing.maximalIdeal O) O]809    [Finite (IsLocalRing.ResidueField O)] [TopologicalSpace O] [IsTopologicalRing O]810    [CompactSpace O] [T2Space O] [SecondCountableTopology O] [MeasurableSpace O] [BorelSpace O]811    (htop : IsAdic (IsLocalRing.maximalIdeal O)) (φ : Polynomial (IsLocalRing.ResidueField O))812    (hφ : φ.Monic) (hirr : Irreducible φ) (r : ℕ) (hr : 0 < r) (n : ℕ) (hn : φ.natDegree * r = n)813    (σ : FactorType) :814    MeasurableSet (residueCell O n (φ ^ r) ∩ typeEvent O n σ) ∧ cellMeasure O n815      (residueCell O n (φ ^ r)) (typeEvent O n σ) = densityValue816      (lawCoeff (lawDescend φ.natDegree (stateLaw (State.single 1 r))) σ)817      (Nat.card (IsLocalRing.ResidueField O)) := by818  obtain ⟨Φ, hΦ, hres, hdeg⟩ := exists_unramified_lift O φ hφ hirr819  subst hres820  rw [← hdeg] at hn ⊢821  exact point_cell_type_event hroot O htop Φ hΦ r hr n hn σ822 823open Polynomial in824private theorem formPoly_eq_reverse {O : Type} [CommRing O] [Nontrivial O] (r : ℕ) (b : Fin r → O) :825    formPoly (insertOne (0 : Fin (r+1)) b) = (monicPolyO (b ∘ Fin.rev)).reverse := by826  obtain ⟨hm, hd, hc, -⟩ := monic_poly_reconstruct O r (b ∘ Fin.rev)827  ext i828  rw [formPoly_coeff, coeff_reverse, hd]829  by_cases hi : i ≤ r830  · rw [dif_pos (by omega), revAt_le hi]831    rcases Nat.eq_zero_or_pos i with h0 | hpos832    · subst h0833      simp only [Nat.sub_zero]834      have h1 : (monicPolyO (b ∘ Fin.rev)).coeff r = 1 := by835        have := hm.coeff_natDegree; rwa [hd] at this836      rw [h1]; rfl837    · have := hc ⟨r - i, by omega⟩838      simp only at this839      rw [this]840      obtain ⟨k, rfl⟩ : ∃ k, i = k + 1 := ⟨i - 1, by omega⟩841      have e : (⟨k+1, by omega⟩ : Fin (r+1)) = (⟨k, by omega⟩ : Fin r).succ := rfl842      rw [e, insertOne, Fin.insertNth_zero', Fin.cons_succ]843      simp only [Function.comp_apply]844      congr 1; ext; simp [Fin.rev]; omega845  · rw [dif_neg (by omega)]846    have : revAt r i = i := by simp only [revAt]; exact if_neg hi847    rw [this, coeff_eq_zero_of_natDegree_lt (by omega)]848 849open Polynomial in850private theorem infinityBlockEvent_eq_preimage (O : Type) [CommRing O] [IsDomain O]851    [IsDiscreteValuationRing O] [IsAdicComplete (IsLocalRing.maximalIdeal O) O]852    [Finite (IsLocalRing.ResidueField O)] (r : ℕ) (hr : 0 < r) (σ : FactorType) :853    infinityBlockEvent O r σ = (fun b : Fin r → O => b ∘ Fin.rev) ⁻¹'854      ({b' | b' ⟨0, hr⟩ ≠ 0} ∩ typeEvent O r σ) := by855  ext b856  obtain ⟨hm, hd, hc, -⟩ := monic_poly_reconstruct O r (b ∘ Fin.rev)857  set P := monicPolyO (b ∘ Fin.rev) with hP858  set ι := algebraMap O (BaseField O)859  have hF := formPoly_eq_reverse r b860  have hFr : (formPoly (insertOne (0 : Fin (r+1)) b)).coeff r = (b ∘ Fin.rev) ⟨0, hr⟩ := by861    rw [hF, coeff_reverse, hd, revAt_le le_rfl, Nat.sub_self]862    exact hc ⟨0, hr⟩863  have hmap : (formPoly (insertOne (0 : Fin (r+1)) b)).map ι = (P.map ι).reverse := by864    ext i865    rw [coeff_map, coeff_reverse, hm.natDegree_map, hd, coeff_map, hF, coeff_reverse, ← hP, hd]866  have h0 : (P.map ι).coeff 0 = ι ((b ∘ Fin.rev) ⟨0, hr⟩) := by867    rw [coeff_map]; exact congrArg ι (hc ⟨0, hr⟩)868  have hinj : Function.Injective ι := IsFractionRing.injective O (BaseField O)869  simp only [infinityBlockEvent, typeEvent, Set.mem_ofPred_eq, Set.mem_preimage, Set.mem_inter_iff]870  rw [hFr, hmap, ← monicPolyO_map_fraction]871  constructor872  · rintro ⟨hne, ht⟩873    refine ⟨hne, ?_⟩874    have hne' : (P.map ι).coeff 0 ≠ 0 := by875      rw [h0]; exact fun e => hne (hinj (by rw [e, map_zero]))876    rw [reverse_polynomial_type_iff O (P.map ι) (hm.map ι) hne', h0]877    exact ht878  · rintro ⟨hne, ht⟩879    refine ⟨hne, ?_⟩880    have hne' : (P.map ι).coeff 0 ≠ 0 := by881      rw [h0]; exact fun e => hne (hinj (by rw [e, map_zero]))882    rw [reverse_polynomial_type_iff O (P.map ι) (hm.map ι) hne', h0] at ht883    exact ht884 885open MeasureTheory in886open MeasureTheory in887/-- Assuming the root cell law, the reduced form cell at infinity has law888`lawDescend 1 (stateLaw (single 1 r))` for its infinity block events. -/889theorem infinity_block_event_law (hroot : RootCellLaw) (O : Type) [CommRing O] [IsDomain O]890    [IsDiscreteValuationRing O] [IsAdicComplete (IsLocalRing.maximalIdeal O) O]891    [Finite (IsLocalRing.ResidueField O)] [TopologicalSpace O] [IsTopologicalRing O]892    [CompactSpace O] [T2Space O] [SecondCountableTopology O] [MeasurableSpace O] [BorelSpace O]893    (htop : IsAdic (IsLocalRing.maximalIdeal O)) (r : ℕ) (hr : 0 < r) (σ : FactorType) :894    MeasurableSet (reducedFormCell O r (0 : Fin (r+1))895      (Pi.single (0 : Fin (r+1)) (1 : IsLocalRing.ResidueField O)) ∩ infinityBlockEvent O r σ) ∧896      cellMeasure O r (reducedFormCell O r (0 : Fin (r+1))897      (Pi.single (0 : Fin (r+1)) (1 : IsLocalRing.ResidueField O))) (infinityBlockEvent O r σ) =898      densityValue (lawCoeff (lawDescend 1 (stateLaw (State.single 1 r))) σ)899      (Nat.card (IsLocalRing.ResidueField O)) := by900  set Z := reducedFormCell O r (0 : Fin (r+1)) (Pi.single (0 : Fin (r+1))901      (1 : IsLocalRing.ResidueField O)) with hZdef902  set CX := residueCell O r (Polynomial.X ^ r) with hCXdef903  set R : (Fin r → O) → (Fin r → O) := fun b => b ∘ Fin.rev with hRdef904  have hR : Measurable R := measurable_pi_iff.mpr fun j => measurable_pi_apply _905  have hZ : MeasurableSet Z :=906    (normalized_form_cell_cylinder_mass O htop r 0 _ (Pi.single_eq_same _ _)).2.2.2.1907  obtain ⟨-, hbij, -, hmp⟩ := form_cell_monic_identification O htop r908  have hRR : ∀ b, R (R b) = b := fun b => by909    funext j; simp [hRdef]910  have hCX : CX = R ⁻¹' Z := by911    ext b; constructor912    · intro hb913      obtain ⟨z, hz, rfl⟩ := hbij.surjOn hb914      change R (R z) ∈ Z915      rw [hRR]; exact hz916    · intro hb917      have : R (R b) ∈ CX := hbij.mapsTo hb918      rwa [hRR] at this919  have hCXm : MeasurableSet CX := hCX ▸ hR hZ920  obtain ⟨hT, hlaw⟩ := irreducible_cell_type_event hroot O htop Polynomial.X Polynomial.monic_X921    Polynomial.irreducible_X r hr r (by rw [Polynomial.natDegree_X, one_mul]) σ922  rw [Polynomial.natDegree_X] at hlaw923  obtain ⟨hHm0, hH0⟩ := coordinate_hyperplane_null O htop r ⟨0, hr⟩924  set H : Set (Fin r → O) := {b' | b' ⟨0, hr⟩ ≠ 0} with hHdef925  have hHm : MeasurableSet H := hHm0.compl926  set A := CX ∩ typeEvent O r σ ∩ H with hAdef927  have hA : MeasurableSet A := hT.inter hHm928  have hkey : infinityBlockEvent O r σ ∩ Z = R ⁻¹' A ∩ Z := by929    rw [infinityBlockEvent_eq_preimage O r hr σ]930    ext b931    simp only [Set.mem_inter_iff, Set.mem_preimage, hAdef]932    constructor933    · rintro ⟨⟨h1, h2⟩, hb⟩; exact ⟨⟨⟨hbij.mapsTo hb, h2⟩, h1⟩, hb⟩934    · rintro ⟨⟨⟨-, h2⟩, h1⟩, hb⟩; exact ⟨⟨h1, h2⟩, hb⟩935  refine ⟨?_, ?_⟩936  · rw [Set.inter_comm, hkey]; exact (hR hA).inter hZ937  rw [← cellMeasure_cell_inter hZ, Set.inter_comm Z, hkey, Set.inter_comm _ Z,938    cellMeasure_cell_inter hZ,939    hmp.measure_preimage hA.nullMeasurableSet, ← hlaw]940  have hnull : cellMeasure O r CX {b : Fin r → O | b ⟨0, hr⟩ = 0} = 0 := by941    have : (coefficientMeasure O r).restrict CX {b : Fin r → O | b ⟨0, hr⟩ = 0} = 0 :=942      le_antisymm ((Measure.restrict_le_self _).trans hH0.le) (zero_le)943    simp [cellMeasure, this]944  rw [← cellMeasure_cell_inter hCXm (typeEvent O r σ), Set.inter_comm CX,945    ← measure_inter_add_sdiff (typeEvent O r σ ∩ CX) hHm]946  have hdiff : cellMeasure O r CX (SDiff.sdiff (typeEvent O r σ ∩ CX) H) = 0 :=947    measure_mono_null (fun b hb => by simpa [hHdef] using hb.2) hnull948  rw [hdiff, add_zero, hAdef, Set.inter_comm CX]949 950section951variable {k : Type} [Field k]952 953private noncomputable def blockPoly : ClosedDirection k → ℕ → Polynomial k954  | none, _ => 1955  | some φ, r => φ.val ^ r956 957private def blockDeg : ClosedDirection k → ℕ → ℕ958  | none, r => r959  | some φ, r => φ.val.natDegree * r960 961private def blockNu : (Q : ClosedDirection k) → (r : ℕ) → Fin (blockDeg Q r + 1)962  | none, _ => 0963  | some _, _ => Fin.last _964 965private noncomputable def blockG (Q : ClosedDirection k) (r : ℕ) : Fin (blockDeg Q r + 1) → k :=966  fun i => (blockPoly Q r).coeff i967 968private lemma blockDeg_eq_mul (Q : ClosedDirection k) (r : ℕ) :969    blockDeg Q r = directionDegree k Q * r := by970  cases Q <;> simp [blockDeg, directionDegree]971 972private lemma blockPoly_natDegree_le (Q : ClosedDirection k) (r : ℕ) :973    (blockPoly Q r).natDegree ≤ blockDeg Q r := by974  cases Q with975  | none => simp [blockPoly]976  | some φ => simp [blockPoly, blockDeg, φ.2.1.natDegree_pow, mul_comm]977 978private lemma formPoly_coeff_eq_self (n : ℕ) (P : Polynomial k) (h : P.natDegree ≤ n) :979    formPoly (fun i : Fin (n+1) => P.coeff i) = P := by980  unfold formPoly981  rw [Fin.sum_univ_eq_sum_range (fun i => Polynomial.C (P.coeff i) * Polynomial.X ^ i) (n+1)]982  conv_rhs => rw [P.as_sum_range' (n+1) (by omega)]983  simp [Polynomial.C_mul_X_pow_eq_monomial]984 985private lemma formPoly_blockG (Q : ClosedDirection k) (r : ℕ) :986    formPoly (blockG Q r) = blockPoly Q r :=987  formPoly_coeff_eq_self _ _ (blockPoly_natDegree_le Q r)988 989private lemma blockPoly_isCoprime (a b : ClosedDirection k) (ra rb : ℕ) (hne : a ≠ b) :990    IsCoprime (blockPoly a ra) (blockPoly b rb) := by991  cases a with992  | none => simp [blockPoly, isCoprime_one_left]993  | some φ =>994    cases b with995    | none => simp [blockPoly, isCoprime_one_right]996    | some ψ =>997      exact (distinct_monic_irreducible_coprime k φ.1 ψ.1 φ.2.1 ψ.2.1 φ.2.2 ψ.2.2998        (fun h => hne (congrArg some (Subtype.ext h)))).pow999 1000private lemma blockPoly_some_natDegree (φ : AffineDirection k) (r : ℕ) :1001    (blockPoly (some φ) r).natDegree = blockDeg (some φ) r := by1002  simp [blockPoly, blockDeg, φ.2.1.natDegree_pow, mul_comm]1003 1004private lemma blockPoly_natDegree_or (a b : ClosedDirection k) (ra rb : ℕ) (hne : a ≠ b) :1005    (blockPoly a ra).natDegree = blockDeg a ra ∨ (blockPoly b rb).natDegree = blockDeg b rb := by1006  cases a with1007  | none =>1008    cases b with1009    | none => exact absurd rfl hne1010    | some ψ => exact Or.inr (blockPoly_some_natDegree ψ rb)1011  | some φ => exact Or.inl (blockPoly_some_natDegree φ ra)1012 1013private lemma blockG_single (r : ℕ) : blockG (none : ClosedDirection k) r = Pi.single 0 1 := by1014  funext i1015  simp only [blockG, blockPoly, Polynomial.coeff_one, Pi.single_apply]1016  by_cases h : i = 01017  · subst h; simp1018  · have : (i : ℕ) ≠ 0 := fun h' => h (Fin.ext h')1019    simp [h, this]1020 1021private lemma blockG_nu (a : ClosedDirection k) (r : ℕ) : blockG a r (blockNu a r) = 1 := by1022  cases a with1023  | none => rw [blockG_single]; simp [blockNu]1024  | some φ =>1025    simp only [blockG, blockNu, Fin.val_last]1026    rw [← blockPoly_some_natDegree φ r]1027    exact (φ.2.1.pow r)1028 1029private lemma block_class (a : ClosedDirection k) (r : ℕ) :1030    if a.isNone = true then (blockNu a r = 0 ∧ blockG a r = Pi.single 0 1) else blockNu a r =1031      Fin.last _ := by1032  cases a with1033  | none => simp [blockNu, blockG_single]1034  | some φ => simp [blockNu]1035 1036end1037 1038private lemma block_law (hroot : RootCellLaw) (O : Type) [CommRing O] [IsDomain O]1039    [IsDiscreteValuationRing O] [IsAdicComplete (IsLocalRing.maximalIdeal O) O]1040    [Finite (IsLocalRing.ResidueField O)] [TopologicalSpace O] [IsTopologicalRing O]1041    [CompactSpace O] [T2Space O] [SecondCountableTopology O] [MeasurableSpace O] [BorelSpace O]1042    (htop : IsAdic (IsLocalRing.maximalIdeal O)) (a : ClosedDirection (IsLocalRing.ResidueField O))1043    (r : ℕ) (hr : 0 < r) (τ : FactorType) :1044    MeasurableSet (reducedFormCell O (blockDeg a r) (blockNu a r) (blockG a r) ∩1045      (if a.isNone = true then infinityBlockEvent O (blockDeg a r) τ else typeEvent O1046      (blockDeg a r) τ)) ∧ cellMeasure O (blockDeg a r) (reducedFormCell O (blockDeg a r)1047      (blockNu a r) (blockG a r)) (if a.isNone = true then infinityBlockEvent O (blockDeg a r) τ1048      else typeEvent O (blockDeg a r) τ) = densityValue (lawCoeff1049      (lawDescend (directionDegree _ a) (stateLaw (State.single 1 r))) τ)1050      (Nat.card (IsLocalRing.ResidueField O)) := by1051  cases a with1052  | none =>1053    simp only [Option.isNone_none, if_true]1054    rw [blockG_single]1055    exact infinity_block_event_law hroot O htop r hr τ1056  | some φ =>1057    simp only [Option.isNone_some, Bool.false_eq_true, if_false]1058    have hcell := (form_cell_monic_identification O htop 0).1 (blockDeg (some φ) r)1059        (blockG (some φ) r)1060    rw [formPoly_blockG] at hcell1061    change MeasurableSet (reducedFormCell O _ (Fin.last _) _ ∩ _) ∧ cellMeasure O _1062        (reducedFormCell O _ (Fin.last _) _) _ = _1063    rw [hcell]1064    exact irreducible_cell_type_event hroot O htop φ.1 φ.2.1 φ.2.2 r hr _ rfl τ1065 1066private lemma block_law_coeff_nonneg (k : Type) [Field k] [Finite k] (a : ClosedDirection k) (r : ℕ)1067    (hr : 0 < r) (τ : FactorType) :1068    0 ≤ (lawCoeff (lawDescend (directionDegree _ a) (stateLaw (State.single 1 r))) τ).eval1069      (Nat.card k) :=1070  (state_law_coeff_nonneg _ (finite_field_card_primePower k) (State.single 1 r) ⟨one_pos, hr⟩ τ).21071    _ (directionDegree_pos _ a)1072 1073/-! ### Divisor cells -/1074 1075/-- **Divisor cell law.** Assuming the root cell law, the reduced form cell of a divisor `D` with1076array `m` has law `arrayLaw m`. -/1077theorem divisor_form_cell_law (hroot : RootCellLaw) (O : Type) [CommRing O] [IsDomain O]1078    [IsDiscreteValuationRing O] [IsAdicComplete (IsLocalRing.maximalIdeal O) O]1079    [Finite (IsLocalRing.ResidueField O)] [TopologicalSpace O] [IsTopologicalRing O]1080    [CompactSpace O] [T2Space O] [SecondCountableTopology O] [MeasurableSpace O] [BorelSpace O]1081    (htop : IsAdic (IsLocalRing.maximalIdeal O)) (n : ℕ)1082    (D : ExceptionalDivisor (IsLocalRing.ResidueField O))1083    (hD : exceptionalDegree (IsLocalRing.ResidueField O) D = n) (m : Pattern n)1084    (hm : HasArray (IsLocalRing.ResidueField O) n D m) (σ : FactorType) :1085    MeasurableSet (reducedFormCell O n1086      (⟨n - D (infinityDirection (IsLocalRing.ResidueField O)),1087        Nat.lt_succ_of_le (Nat.sub_le _ _)⟩ : Fin (n+1))1088      (divisorVector (IsLocalRing.ResidueField O) n D) ∩ insertOne1089      (⟨n - D (infinityDirection (IsLocalRing.ResidueField O)),1090        Nat.lt_succ_of_le (Nat.sub_le _ _)⟩ : Fin (n+1)) ⁻¹'1091      affineTypeEvent O n σ) ∧ cellMeasure O n (reducedFormCell O n1092      (⟨n - D (infinityDirection (IsLocalRing.ResidueField O)),1093        Nat.lt_succ_of_le (Nat.sub_le _ _)⟩ : Fin (n+1))1094      (divisorVector (IsLocalRing.ResidueField O) n D)) (insertOne1095      (⟨n - D (infinityDirection (IsLocalRing.ResidueField O)),1096        Nat.lt_succ_of_le (Nat.sub_le _ _)⟩ : Fin (n+1)) ⁻¹'1097      affineTypeEvent O n σ) = densityValue (lawCoeff (arrayLaw m) σ)1098      (Nat.card (IsLocalRing.ResidueField O)) := by1099  obtain ⟨e, he⟩ := array_enumeration (IsLocalRing.ResidueField O) n D hD m hm1100  let Q : Fin (otherChildren 1 m).length → ClosedDirection (IsLocalRing.ResidueField O) :=1101    fun j => (e j).val1102  have hQinj : Function.Injective Q := fun i j h => e.injective (Subtype.ext h)1103  have hr : ∀ j, 0 < D (Q j) := fun j => Nat.pos_of_ne_zero (Finsupp.mem_support_iff.mp (e j).2)1104  let d : Fin (otherChildren 1 m).length → ℕ := fun j => blockDeg (Q j) (D (Q j))1105  let ν : ∀ j, Fin (d j + 1) := fun j => blockNu (Q j) (D (Q j))1106  let g : ∀ j, Fin (d j + 1) → IsLocalRing.ResidueField O := fun j => blockG (Q j) (D (Q j))1107  have hsum : ∑ j, d j = n := by1108    refine Eq.trans ?_ hD1109    unfold exceptionalDegree Finsupp.sum1110    rw [← Finset.sum_coe_sort D.support]1111    rw [← Equiv.sum_comp e]1112    simp only [d, Q, blockDeg_eq_mul]1113  have hpoly : ∏ j, formPoly (g j) = divisorAffinePolynomial (IsLocalRing.ResidueField O) D := by1114    have : divisorAffinePolynomial (IsLocalRing.ResidueField O) D = D.prod1115        (fun P r => blockPoly P r) := by1116      unfold divisorAffinePolynomial1117      congr 1; funext P r; cases P <;> rfl1118    rw [this]1119    unfold Finsupp.prod1120    rw [← Finset.prod_coe_sort D.support, ← Equiv.prod_comp e]1121    simp only [g, formPoly_blockG, Q]1122  have hprod : formProd d g = divisorVector (IsLocalRing.ResidueField O) (∑ j, d j) D := by1123    funext i1124    simp only [formProd, divisorVector, hpoly]1125  have hD' : exceptionalDegree (IsLocalRing.ResidueField O) D = ∑ j, d j := hD.trans hsum.symm1126  have hμ : formProd d g ⟨(∑ j, d j) - D (infinityDirection (IsLocalRing.ResidueField O)),1127      Nat.lt_succ_of_le (Nat.sub_le _ _)⟩ = 1 := by1128    rw [hprod]1129    exact (divisor_vector_properties _ _ D hD').2.2.2.2.11130  have hc : FormsCoprime d g := by1131    constructor1132    · intro i j hij1133      simp only [g, formPoly_blockG]1134      exact blockPoly_isCoprime _ _ _ _ (fun h => hij (hQinj h))1135    · intro i j hij1136      simp only [g, d, formPoly_blockG]1137      exact blockPoly_natDegree_or _ _ _ _ (fun h => hij (hQinj h))1138  let Dl : Fin (otherChildren 1 m).length → Law := fun j =>1139    lawDescend (directionDegree _ (Q j)) (stateLaw (State.single 1 (D (Q j))))1140  have R := form_product_type_event_law O htop _ d ν g (fun j => blockG_nu _ _) hc _ hμ1141    (fun j => (Q j).isNone) (fun j => block_class _ _)1142    (fun i j hi hj => hQinj (by1143      simp only [Option.isNone_iff_eq_none] at hi hj; rw [hi, hj]))1144    Dl (fun j τ => block_law_coeff_nonneg _ _ _ (hr j) τ)1145        (fun j τ => block_law hroot O htop _ _ (hr j) τ) σ1146  have hlist : List.ofFn Dl = (otherChildren 1 m).map fun z => lawDescend z.1 (stateLaw z.2) := by1147    conv_rhs => rw [← List.ofFn_get (otherChildren 1 m), List.map_ofFn]1148    exact congrArg List.ofFn (funext fun j ↦ by simp only [Function.comp_apply, he j, Dl, Q])1149  rwa [hlist, hprod, hsum] at R1150 1151/-- **Monic cell law.** Assuming the root cell law, the residue cell of an affine divisor with1152array `m` has law `arrayLaw m`. -/1153theorem monic_cell_law (hroot : RootCellLaw) (O : Type) [CommRing O] [IsDomain O]Lemma 7.11154    [IsDiscreteValuationRing O] [IsAdicComplete (IsLocalRing.maximalIdeal O) O]1155    [Finite (IsLocalRing.ResidueField O)] [TopologicalSpace O] [IsTopologicalRing O]1156    [CompactSpace O] [T2Space O] [SecondCountableTopology O] [MeasurableSpace O] [BorelSpace O]1157    (htop : IsAdic (IsLocalRing.maximalIdeal O)) (n : ℕ)1158    (D : ExceptionalDivisor (IsLocalRing.ResidueField O))1159    (hD : AffineDivisor (IsLocalRing.ResidueField O) n D) (m : Pattern n)1160    (hm : HasArray (IsLocalRing.ResidueField O) n D m) (σ : FactorType) :1161    MeasurableSet (residueCell O n (divisorAffinePolynomial (IsLocalRing.ResidueField O) D) ∩1162      typeEvent O n σ) ∧ cellMeasure O n (residueCell O n1163      (divisorAffinePolynomial (IsLocalRing.ResidueField O) D)) (typeEvent O n σ) = densityValue1164      (lawCoeff (arrayLaw m) σ) (Nat.card (IsLocalRing.ResidueField O)) := by1165  set k := IsLocalRing.ResidueField O1166  obtain ⟨e, he⟩ := array_enumeration k n D hD.2 m hm1167  have hsome : ∀ j, ∃ a : AffineDirection k, (e j).val = some a := fun j ↦1168    Option.ne_none_iff_exists'.1 fun h ↦ Finsupp.mem_support_iff.1 (h ▸ (e j).2 :1169      none ∈ D.support) hD.11170  choose φ hφ using hsome1171  have hr : ∀ j, 0 < D (e j) := fun j ↦ Nat.pos_of_ne_zero (Finsupp.mem_support_iff.1 (e j).2)1172  let g : Fin (otherChildren 1 m).length → Polynomial k := fun j => (φ j).val ^ D (e j)1173  let Dl : Fin (otherChildren 1 m).length → Law := fun j => lawDescend (φ j).val.natDegree1174      (stateLaw (State.single 1 (D (e j))))1175  have hg : ∀ j, (g j).Monic := fun j => (φ j).property.1.pow _1176  have hc : ∀ i j, i ≠ j → IsCoprime (g i) (g j) := by1177    intro i j hij1178    have hne : (φ i).val ≠ (φ j).val := fun h ↦1179      hij (e.injective (Subtype.ext (by rw [hφ i, hφ j, Subtype.ext h])))1180    exact (distinct_monic_irreducible_coprime k _ _ (φ i).property.1 (φ j).property.11181      (φ i).property.2 (φ j).property.2 hne).pow1182  have hnn : ∀ (j : Fin (otherChildren 1 m).length) (τ : FactorType), 0 ≤ (lawCoeff (Dl j) τ).eval1183      (Nat.card k) := by1184    intro j τ1185    exact (state_law_coeff_nonneg _ (finite_field_card_primePower k) (State.single 1 (D (e j)))1186        (show 0 < 1 ∧ 0 < D (e j) from ⟨Nat.one_pos, hr j⟩) τ).2 _1187      (Polynomial.natDegree_pos_iff_degree_pos.mpr1188          (Polynomial.degree_pos_of_irreducible (φ j).property.2))1189  have hlaw : ∀ (j : Fin (otherChildren 1 m).length) (τ : FactorType), MeasurableSet1190      (residueCell O (g j).natDegree (g j) ∩ typeEvent O (g j).natDegree τ) ∧ cellMeasure O1191      (g j).natDegree (residueCell O (g j).natDegree (g j)) (typeEvent O (g j).natDegree τ) =1192      densityValue (lawCoeff (Dl j) τ) (Nat.card k) := by1193    intro j τ1194    exact irreducible_cell_type_event hroot O htop (φ j).val (φ j).property.1 (φ j).property.21195      (D (e j)) (hr j) (g j).natDegree (by simp only [g, Polynomial.natDegree_pow]; ring) τ1196  have hprod : ∏ j, g j = divisorAffinePolynomial k D := by1197    unfold divisorAffinePolynomial Finsupp.prod1198    rw [← Finset.prod_coe_sort D.support, ← e.prod_comp]1199    refine Finset.prod_congr rfl fun j _ => ?_1200    simp only [g, hφ j]1201  have hsum : ∑ j, (g j).natDegree = n := by1202    refine Eq.trans ?_ hD.21203    unfold exceptionalDegree Finsupp.sum1204    rw [← Finset.sum_coe_sort D.support, ← e.sum_comp]1205    refine Finset.sum_congr rfl fun j _ => ?_1206    simp only [g, hφ j, directionDegree, Polynomial.natDegree_pow]1207    ring1208  have hlist : List.ofFn Dl = (otherChildren 1 m).map fun z => lawDescend z.1 (stateLaw z.2) := by1209    conv_rhs => rw [← List.ofFn_get (otherChildren 1 m), List.map_ofFn]1210    exact congrArg List.ofFn (funext fun j ↦ by1211      simp only [Function.comp_apply, he j, Dl, hφ, directionDegree])1212  have key := product_law_of_factor_laws O htop _ g hg hc Dl hnn hlaw σ1213  rwa [hprod, hsum, hlist] at key1214 1215/-- Assuming the root cell law, the projective cell of a divisor with array `m` has law1216`arrayLaw m` for affine type events. -/1217theorem projective_cell_affine_type_event (hroot : RootCellLaw) (O : Type) [CommRing O] [IsDomain O]1218    [IsDiscreteValuationRing O] [IsAdicComplete (IsLocalRing.maximalIdeal O) O]1219    [Finite (IsLocalRing.ResidueField O)] [TopologicalSpace O] [IsTopologicalRing O]1220    [CompactSpace O] [T2Space O] [SecondCountableTopology O] [MeasurableSpace O] [BorelSpace O]1221    (htop : IsAdic (IsLocalRing.maximalIdeal O)) (n : ℕ)1222    (D : ExceptionalDivisor (IsLocalRing.ResidueField O))1223    (hD : exceptionalDegree (IsLocalRing.ResidueField O) D = n) (m : Pattern n)1224    (hm : HasArray (IsLocalRing.ResidueField O) n D m) (σ : FactorType) :1225    MeasurableSet (projectiveCell O n (divisorVector (IsLocalRing.ResidueField O) n D) ∩1226      affineTypeEvent O n σ) ∧ cellMeasure O (n+1) (projectiveCell O n1227      (divisorVector (IsLocalRing.ResidueField O) n D)) (affineTypeEvent O n σ) = densityValue1228      (lawCoeff (arrayLaw m) σ) (Nat.card (IsLocalRing.ResidueField O)) := by1229  obtain ⟨_, _, _, _, hGμ, _, hG0⟩ := divisor_vector_properties (IsLocalRing.ResidueField O) n D hD1230  set G := divisorVector (IsLocalRing.ResidueField O) n D with hG1231  set μ : Fin (n+1) := ⟨n - D (infinityDirection (IsLocalRing.ResidueField O)), by omega⟩ with hμ1232  obtain ⟨hPCm, _⟩ := projective_cell_mass O htop n G hG01233  obtain ⟨hmaps, _, _, hmp⟩ := projective_cell_normalization_pushforward O htop n G μ hGμ1234  obtain ⟨hEm, hEv⟩ := divisor_form_cell_law hroot O htop n D hD m hm σ1235  have hscale := (affine_type_event_unit_scaling O n σ).2 G μ hGμ1236  have hset : projectiveCell O n G ∩ affineTypeEvent O n σ1237      = projectiveCell O n G ∩ (projectiveNormalize O n G μ ⁻¹'1238          (reducedFormCell O n μ G ∩ insertOne μ ⁻¹' affineTypeEvent O n σ)) := by1239    ext a1240    simp only [Set.mem_inter_iff, Set.mem_preimage]1241    constructor1242    · rintro ⟨ha, hb⟩1243      exact ⟨ha, hmaps ha, (hscale a ha).2 hb⟩1244    · rintro ⟨ha, _, hb⟩1245      exact ⟨ha, (hscale a ha).1 hb⟩1246  refine ⟨?_, ?_⟩1247  · rw [hset]1248    exact hPCm.inter (hmp.measurable hEm)1249  · have hDc := (normalized_form_cell_cylinder_mass O htop n μ G hGμ).2.2.2.11250    rw [← cellMeasure_cell_inter hPCm, hset, cellMeasure_cell_inter hPCm,1251      hmp.measure_preimage hEm.nullMeasurableSet, cellMeasure_cell_inter hDc]1252    exact hEv1253 1254/-- **Primitive density.** Assuming the root cell law, the relative density of the affine type1255event `σ` among primitive coefficient vectors is `densityValue (projectiveExpr n σ) q`. -/1256theorem affine_type_event_primitive_density (hroot : RootCellLaw) (O : Type) [CommRing O]1257    [IsDomain O] [IsDiscreteValuationRing O] [IsAdicComplete (IsLocalRing.maximalIdeal O) O]1258    [Finite (IsLocalRing.ResidueField O)] [TopologicalSpace O] [IsTopologicalRing O]1259    [CompactSpace O] [T2Space O] [SecondCountableTopology O] [MeasurableSpace O] [BorelSpace O]1260    (htop : IsAdic (IsLocalRing.maximalIdeal O)) (n : ℕ) (σ : FactorType) :1261    MeasurableSet (affineTypeEvent O n σ ∩ {a : Fin (n+1) → O | primitive O a}) ∧1262      coefficientMeasure O (n+1) (affineTypeEvent O n σ ∩ {a : Fin (n+1) → O | primitive O a}) /1263      coefficientMeasure O (n+1) {a : Fin (n+1) → O | primitive O a} = densityValue1264      (projectiveExpr n σ) (Nat.card (IsLocalRing.ResidueField O)) := by1265  classical1266  set k := IsLocalRing.ResidueField O1267  set q := Nat.card k1268  set μ := coefficientMeasure O (n+1)1269  set A := affineTypeEvent O n σ1270  set Pr := {a : Fin (n+1) → O | primitive O a}1271  obtain ⟨⟨S, hS⟩, hpart, hcell, hsum⟩ := projective_cells_partition O htop n1272  set PC : ExceptionalDivisor k → Set (Fin (n+1) → O) := fun D ↦1273    projectiveCell O n (divisorVector k n D)1274  have hPCsub : ∀ D, PC D ⊆ Pr := fun D a ha ↦ ha.11275  have hlawD := fun D (hD : D ∈ S) m hm ↦1276    projective_cell_affine_type_event hroot O htop n D ((hS D).1 hD) m hm σ1277  have hmeas : MeasurableSet (A ∩ Pr) := by1278    have hunion : A ∩ Pr = ⋃ D ∈ S, PC D ∩ A := by1279      ext a1280      simp only [Set.mem_inter_iff, Set.mem_iUnion]1281      refine ⟨fun ⟨hA, hP⟩ ↦ ?_, fun ⟨D, _, ha, hA⟩ ↦ ⟨hA, hPCsub D ha⟩⟩1282      obtain ⟨D, ⟨hD, ha⟩, -⟩ := hpart a hP1283      exact ⟨D, (hS D).2 hD, ha, hA⟩1284    rw [hunion]1285    refine Finset.measurableSet_biUnion S fun D hD ↦ ?_1286    obtain ⟨⟨m, hm, -⟩, -⟩ := divisor_array_exists_unique k n D ((hS D).1 hD)1287    exact (hlawD D hD m hm).11288  refine ⟨hmeas, ?_⟩1289  -- the measure side: a sum over arrays weighted by divisor counts1290  let c : Pattern n → ℝ≥0∞ := fun m ↦ densityValue (lawCoeff (arrayLaw m) σ) q1291  set ν := densityValue (Expr.inv (projectiveNormalizer n)) q1292  have hcellD : ∀ D ∈ S, μ (A ∩ Pr ∩ PC D) * (μ Pr)⁻¹ =1293      ν * ∑ m ∈ residuePatterns n, if HasArray k n D m then c m else 0 := by1294    intro D hD1295    obtain ⟨⟨m₀, hm₀, hm₀R⟩, huniq⟩ := divisor_array_exists_unique k n D ((hS D).1 hD)1296    rw [Finset.sum_eq_single_of_mem m₀ hm₀R fun m _ hne ↦ if_neg fun h ↦ hne (huniq _ _ h hm₀),1297      if_pos hm₀, Set.inter_assoc, Set.inter_eq_right.2 (hPCsub D),1298      (hcell D ((hS D).1 hD)).2.2 A, (hlawD D hD m₀ hm₀).2, mul_right_comm, ← div_eq_mul_inv,1299      projective_cell_conditional_density O htop n (divisorVector k n D)1300        (divisor_vector_properties k n D ((hS D).1 hD)).2.2.2.2.2.2]1301  have hmass : μ (A ∩ Pr) / μ Pr =1302      ν * ∑ m ∈ residuePatterns n, ((S.filter fun D ↦ HasArray k n D m).card : ℝ≥0∞) * c m := by1303    have := hsum S hS (A ∩ Pr) hmeas1304    rw [Set.inter_assoc, Set.inter_self] at this1305    rw [div_eq_mul_inv, this, Finset.sum_mul, Finset.sum_congr rfl hcellD, ← Finset.mul_sum,1306      Finset.sum_comm]1307    refine congrArg (ν * ·) (Finset.sum_congr rfl fun m _ ↦ ?_)1308    rw [← Finset.sum_filter, Finset.sum_const, nsmul_eq_mul]1309  have hcard : ∀ m ∈ residuePatterns n, ((S.filter fun D ↦ HasArray k n D m).card : ℚ) =1310      (divisorCount 1 m).eval (q : ℚ) := by1311    intro m hm1312    rw [← (projective_divisor_count k n m hm).2,1313      Nat.subtype_card (S.filter fun D ↦ HasArray k n D m) fun D ↦ by rw [Finset.mem_filter, hS]]1314  -- the law side1315  have hlaw : (projectiveExpr n σ).eval (q : ℚ) = (Expr.inv (projectiveNormalizer n)).eval (q : ℚ) *1316      ∑ m ∈ residuePatterns n, (divisorCount 1 m).eval (q : ℚ) *1317        (lawCoeff (arrayLaw m) σ).eval (q : ℚ) := by1318    rw [projectiveExpr, globalLaw, law_coeff_scale, (law_coeff_flatMap _ _ _ [] [] σ _).2.2,1319      ← Finset.sum_map_toList]1320    simp only [if_true]1321    congr 21322    exact List.map_congr_left fun m _ ↦ by rw [law_coeff_scale]; rfl1323  have hPN : 0 ≤ (Expr.inv (projectiveNormalizer n)).eval (q : ℚ) := by1324    change 0 ≤ ((projectiveNormalizer n).eval (q : ℚ))⁻¹1325    rw [(projective_normalizer_eval _ n).1]1326    positivity1327  have hl : ∀ m : Pattern n, 0 ≤ (lawCoeff (arrayLaw m) σ).eval (q : ℚ) := by1328    refine fun m ↦ (law_coeff_nonneg_closure (q : ℚ)).2.2.1 _ (fun L hL τ ↦ ?_) σ1329    simp only [List.mem_map, otherChildren, List.mem_flatMap, List.mem_replicate] at hL1330    obtain ⟨z, ⟨ij, -, -, rfl⟩, rfl⟩ := hL1331    exact (state_law_coeff_nonneg q (finite_field_card_primePower k) _1332      (show State.Valid (.single 1 _) from ⟨Nat.one_pos, Nat.succ_pos _⟩) τ).2 _ (Nat.succ_pos _)1333  rw [hmass]1334  change ν * _ = ENNReal.ofReal (((projectiveExpr n σ).eval (q : ℚ) : ℚ) : ℝ)1335  rw [hlaw, Rat.cast_mul, ENNReal.ofReal_mul (by exact_mod_cast hPN), Rat.cast_sum,1336    ENNReal.ofReal_sum_of_nonneg fun m hm ↦ by1337      have := hl m; rw [← hcard m hm]; push_cast; positivity]1338  refine congrArg (ν * ·) (Finset.sum_congr rfl fun m hm ↦ ?_)1339  rw [← hcard m hm, Rat.cast_mul, ENNReal.ofReal_mul (by positivity), Rat.cast_natCast,1340    ENNReal.ofReal_natCast]1341 1342end SurfaceBlowup