Measure-preserving maps between homogeneous 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.Measure.AdicTransport7import SurfaceBlowup.Unramified.FrobeniusDescent8 9/-!10# Measure-preserving maps between homogeneous cells11 12Over a complete discrete valuation ring `O` with finite residue field, the normalized Haar measures13on residue cells of monic polynomials, on reduced form cells and on projective cells are related by14explicit algebraic maps. This file shows that these maps are measure preserving.15 16## Main results17 18* `SurfaceBlowup.form_product_measurable`: the reduced form-product map is Borel measurable.19* `SurfaceBlowup.factor_cells_measure_preserving`: multiplying monic lifts of pairwise coprime20  residue factors pushes the product of the factor cell measures to the cell measure of the product.21* `SurfaceBlowup.form_cell_monic_identification`: reduced form cells normalized at the last22  coordinate are monic residue cells, and coordinate reversal identifies the form cell of `X ^ r`23  normalized at `0` with the monic residue cell of `X ^ r`, measure-preservingly.24* `SurfaceBlowup.form_cells_measure_preserving`: the homogeneous analogue of the first result for25  reduced form cells.26* `SurfaceBlowup.projective_cell_normalization_pushforward`: normalizing a primitive vector at a27  coordinate where its residue form is `1` pushes the projective cell measure to the reduced form28  cell measure.29 30## Implementation notes31 32The three measure-preservation proofs share one skeleton33(`measurePreserving_cellMeasure_of_balls`): both measures are finite and agree on the34generating `𝔪`-adic balls, which reduces to balls of radius `𝔪 ^ L`, `L ≥ 1`, centred in the35target cell (balls centred outside the cell miss it).36 37Provenance: `Thm_SurfaceBlowupV2_{form_product_measurable, factor_cells_measure_preserving,38form_cell_monic_identification, form_cells_measure_preserving,39projective_cell_normalization_pushforward}` (`form_product_measurable` moved from40`Unramified/LocalDescent.lean`).41-/42 43namespace SurfaceBlowup44 45open scoped BigOperators ENNReal46 47/-! ### A skeleton for measure preservation onto a cell -/48 49/-- A measurable map `f` sending `P`-almost every point into a measurable cell `D` (a single50residue class modulo `𝔪`, with `cellMeasure O N D` a probability measure) pushes the probability51measure `P` forward to `cellMeasure O N D` as soon as both measures agree on the `𝔪 ^ L`-balls52(`L ≥ 1`) centred in `D`. -/53private theorem measurePreserving_cellMeasure_of_balls (O : Type) [CommRing O] [IsDomain O]54    [IsDiscreteValuationRing O] [TopologicalSpace O] [IsTopologicalRing O] [CompactSpace O]55    [T2Space O] [SecondCountableTopology O] [MeasurableSpace O] [BorelSpace O]56    (htop : IsAdic (IsLocalRing.maximalIdeal O)) {α : Type} [MeasurableSpace α]57    (P : MeasureTheory.Measure α) [MeasureTheory.IsProbabilityMeasure P] (N : ℕ)58    (D : Set (Fin N → O)) (hDm : MeasurableSet D)59    [MeasureTheory.IsProbabilityMeasure (cellMeasure O N D)]60    (hDball : ∀ z ∈ D, D = {y | ∀ j, y j - z j ∈ IsLocalRing.maximalIdeal O})61    (f : α → Fin N → O) (hf : Measurable f) (S : Set α) (hS : P Sᶜ = 0)62    (hSD : Set.MapsTo f S D)63    (hball : ∀ L, 1 ≤ L → ∀ x ∈ D,64      P (f ⁻¹' {y | ∀ j, y j - x j ∈ IsLocalRing.maximalIdeal O ^ L}) =65        cellMeasure O N D {y | ∀ j, y j - x j ∈ IsLocalRing.maximalIdeal O ^ L}) :66    MeasureTheory.MeasurePreserving f P (cellMeasure O N D) := by67  set m := IsLocalRing.maximalIdeal O68  have hgen := finite_coordinate_borel_cylinders O m htop N69  refine ⟨hf, finite_measures_from_cylinders O (Fin N → O) m _ _ hgen fun L x => ?_⟩70  have hB : {y : Fin N → O | adicCongr m L y x} = {y | ∀ j, y j - x j ∈ m ^ L} := by71    ext y; exact finite_coordinate_adic_congruence O N m L y x72  have hBm : MeasurableSet {y : Fin N → O | ∀ j, y j - x j ∈ m ^ L} := by73    have h1 : @MeasurableSet _ (adicCylinderSpace m (Fin N → O)) {y | adicCongr m L y x} :=74      MeasurableSpace.measurableSet_generateFrom (Or.inr ⟨L, x, rfl⟩)75    rwa [← hgen, hB] at h176  rw [hB, MeasureTheory.Measure.map_apply hf hBm]77  rcases Nat.eq_zero_or_pos L with rfl | hL78  · have : {y : Fin N → O | ∀ j, y j - x j ∈ m ^ 0} = Set.univ := by ext y; simp79    rw [this, Set.preimage_univ, MeasureTheory.measure_univ, MeasureTheory.measure_univ]80  by_cases hx : x ∈ D81  · exact hball L hL x hx82  -- a ball around a point outside `D` misses `D`, so both sides vanish83  have hfar : ∀ y ∈ D, ¬ ∀ j, y j - x j ∈ m ^ L := fun y hy hyx => hx <| by84    rw [hDball y hy]85    exact fun j => by simpa only [neg_sub] using m.neg_mem (Ideal.pow_le_self (by omega) (hyx j))86  have h0 : cellMeasure O N D {y | ∀ j, y j - x j ∈ m ^ L} = 0 := by87    rw [cellMeasure, MeasureTheory.Measure.smul_apply, MeasureTheory.Measure.restrict_apply' hDm,88      show {y : Fin N → O | ∀ j, y j - x j ∈ m ^ L} ∩ D = ∅ from89        Set.eq_empty_of_forall_notMem fun y ⟨h1, h2⟩ => hfar y h2 h1]90    simp91  rw [h0]92  exact MeasureTheory.measure_mono_null (fun a ha haS => hfar _ (hSD haS) ha) hS93 94/-! ### Products of monic residue cells -/95 96/-- Multiplying monic lifts of pairwise coprime monic residue polynomials `g i` pushes the product97of the normalized cell measures forward to the normalized cell measure of `∏ i, g i`. -/98theorem factor_cells_measure_preserving (O : Type) [CommRing O] [IsDomain O]Lemma 7.199    [IsDiscreteValuationRing O] [IsAdicComplete (IsLocalRing.maximalIdeal O) O]100    [Finite (IsLocalRing.ResidueField O)] [TopologicalSpace O] [IsTopologicalRing O]101    [CompactSpace O] [T2Space O] [SecondCountableTopology O] [MeasurableSpace O] [BorelSpace O]102    (htop : IsAdic (IsLocalRing.maximalIdeal O)) (ι : Type) [Fintype ι]103    (g : ι → Polynomial (IsLocalRing.ResidueField O)) (hg : ∀ i, (g i).Monic)104    (hc : ∀ i j, i ≠ j → IsCoprime (g i) (g j))105    [hσ : ∀ i, MeasureTheory.SigmaFinite106      (cellMeasure O (g i).natDegree (residueCell O (g i).natDegree (g i)))] :107    MeasureTheory.MeasurePreserving (factorProduct (fun i => (g i).natDegree))108      (MeasureTheory.Measure.pi109        (fun i => cellMeasure O (g i).natDegree (residueCell O (g i).natDegree (g i))))110      (cellMeasure O (∑ i, (g i).natDegree)111        (residueCell O (∑ i, (g i).natDegree) (∏ i, g i))) := by112  set m := IsLocalRing.maximalIdeal O113  set n := ∑ i, (g i).natDegree114  set C := residueCell O n (∏ i, g i)115  set PC := Set.pi Set.univ (fun i => residueCell O (g i).natDegree (g i))116  set f := factorProduct (O := O) (fun i => (g i).natDegree)117  set q : ℝ≥0∞ := (Nat.card (IsLocalRing.ResidueField O) : ℝ≥0∞) with hq118  have hfm : Measurable f := (factor_product_continuous O ι (fun i => (g i).natDegree)).2119  have hGm : (∏ i, g i).Monic := Polynomial.monic_prod_of_monic _ _ (fun i _ => hg i)120  have hGn : (∏ i, g i).natDegree = n := Polynomial.natDegree_prod_of_monic _ _ (fun i _ => hg i)121  obtain ⟨hCm, hCmass, hρprob⟩ := residue_cell_mass O htop n (∏ i, g i) hGm hGn122  obtain ⟨hPprob, hPnull, hPball⟩ := factor_cell_product_measure O htop ι g hg123  have hbij := factor_product_bijection O ι g hg hc124  obtain ⟨pi, hpi⟩ := IsDiscreteValuationRing.exists_irreducible O125  have hq0 : q ≠ 0 := Nat.cast_ne_zero.2 Nat.card_pos.ne'126  have hqt : q ≠ ⊤ := by simp [hq]127  have hqi0 : q⁻¹ ^ n ≠ 0 := pow_ne_zero _ (ENNReal.inv_ne_zero.mpr hqt)128  have hqit : q⁻¹ ^ n ≠ ⊤ := ENNReal.pow_ne_top (ENNReal.inv_ne_top.mpr hq0)129  refine measurePreserving_cellMeasure_of_balls O htop _ n C hCm (residue_cell_cylinder O n _).1 f130    hfm PC hPnull hbij.mapsTo fun j hj x hx => ?_131  set B := {y : Fin n → O | ∀ i, y i - x i ∈ m ^ j} with hBdef132  have hmj : m ^ j ≤ m := Ideal.pow_le_self (by omega)133  obtain ⟨a', ha', hfa'⟩ := hbij.surjOn hx134  have hBC : B ⊆ C := fun y hy => by135    change y ∈ residueCell O n (∏ i, g i)136    rw [(residue_cell_cylinder O n _).1 x hx]137    exact fun i => hmj (hy i)138  have hpre : f ⁻¹' B ∩ PC = Set.pi Set.univ139      (fun i => {b : Fin (g i).natDegree → O | ∀ k, b k - a' i k ∈ m ^ j}) := by140    ext a141    constructor142    · rintro ⟨hfa, haP⟩143      simpa using (factor_product_congruence_iff O ι g hc j a a' haP ha').1144        fun k => by have h := hfa k; rw [← hfa'] at h; exact h145    · intro ha146      simp only [Set.mem_pi, Set.mem_univ, Set.mem_ofPred_eq, true_implies] at ha147      have haP : a ∈ PC := by148        simp only [PC, Set.mem_pi, Set.mem_univ, true_implies]149        intro i150        rw [(residue_cell_cylinder O _ _).1 _ (ha' i (Set.mem_univ i))]151        exact fun k => hmj (ha i k)152      refine ⟨?_, haP⟩153      change ∀ k, f a k - x k ∈ m ^ j154      rw [← hfa']155      exact (factor_product_congruence_iff O ι g hc j a a' haP ha').2 ha156  have hmass : coefficientMeasure O n B = q⁻¹ ^ (n * j) := by157    have := coefficient_uniformizer_cylinder_mass O htop n pi hpi j x158    rw [← hpi.maximalIdeal_eq] at this159    rw [← this]160    congr 1161    ext y; exact (finite_coordinate_adic_congruence O n m j y x).symm162  rw [← MeasureTheory.measure_inter_conull hPnull, hpre, hPball j hj a' ha', cellMeasure,163    MeasureTheory.Measure.smul_apply, smul_eq_mul, MeasureTheory.Measure.restrict_apply' hCm,164    Set.inter_eq_left.mpr hBC, hCmass, hmass]165  obtain ⟨k, rfl⟩ : ∃ k, j = k + 1 := ⟨j - 1, by omega⟩166  rw [Nat.add_sub_cancel, mul_add, mul_one, pow_add, ← mul_assoc, mul_comm _ (q⁻¹ ^ (n * k)),167    mul_assoc, ENNReal.inv_mul_cancel hqi0 hqit, mul_one]168 169/-! ### Reduced form cells versus monic residue cells -/170 171private theorem formPoly_coeff_fin {A : Type} [CommRing A] {n : ℕ} (a : Fin (n + 1) → A)172    (k : Fin (n + 1)) : (formPoly a).coeff (k : ℕ) = a k := by173  simp [formPoly, Polynomial.finsetSum_coeff, Polynomial.coeff_X_pow, Fin.val_inj]174 175private theorem formPoly_inj_fin {A : Type} [CommRing A] {n : ℕ} (a a' : Fin (n + 1) → A) :176    formPoly a = formPoly a' ↔ a = a' :=177  ⟨fun h => funext fun k => by rw [← formPoly_coeff_fin a k, ← formPoly_coeff_fin a' k, h],178    fun h => h ▸ rfl⟩179 180private theorem formPoly_map_fin {A B : Type} [CommRing A] [CommRing B] (f : A →+* B) {n : ℕ}181    (a : Fin (n + 1) → A) : (formPoly a).map f = formPoly (fun i => f (a i)) := by182  simp [formPoly, Polynomial.map_sum]183 184private theorem formPoly_insertOne_last_eq {A : Type} [CommRing A] {d : ℕ} (b : Fin d → A) :185    formPoly (insertOne (Fin.last d) b) = monicPolyO b := by186  unfold formPoly monicPolyO insertOne187  rw [Fin.sum_univ_castSucc]188  simp [add_comm]189 190private theorem reducedFormCell_last_eq (O : Type) [CommRing O] [IsLocalRing O] (d : ℕ)191    (g : Fin (d + 1) → IsLocalRing.ResidueField O) :192    reducedFormCell O d (Fin.last d) g = residueCell O d (formPoly g) := by193  ext b194  simp only [reducedFormCell, normalizedFormCell, residueCell, Set.mem_ofPred_eq]195  have h1 : insertOne (Fin.last d) b (Fin.last d) = 1 := by simp [insertOne]196  rw [← formPoly_insertOne_last_eq, formPoly_map_fin, formPoly_inj_fin]197  simp only [h1, true_and]198  rfl199 200private theorem insertOne_last_comp_rev {A : Type} [CommRing A] {r : ℕ} (b : Fin r → A) :201    insertOne (Fin.last r) (b ∘ Fin.rev) = insertOne 0 b ∘ Fin.rev := by202  funext i203  refine Fin.lastCases ?_ (fun j => ?_) i204  · simp [insertOne]205  · simp [insertOne, Fin.rev_castSucc]206 207private theorem mem_reducedFormCell_zero_iff (O : Type) [CommRing O] [IsLocalRing O] (r : ℕ)208    (b : Fin r → O) :209    b ∈ reducedFormCell O r 0 (Pi.single 0 1) ↔210      b ∘ Fin.rev ∈ residueCell O r (Polynomial.X ^ r) := by211  have hX : (Polynomial.X ^ r : Polynomial (IsLocalRing.ResidueField O))212      = formPoly (Pi.single (Fin.last r) 1) := by213    have h0 : monicPolyO (0 : Fin r → IsLocalRing.ResidueField O) = Polynomial.X ^ r := by214      simp [monicPolyO]215    rw [← h0, ← formPoly_insertOne_last_eq]216    congr 1217    funext i218    refine Fin.lastCases ?_ (fun j => ?_) i219    · simp [insertOne]220    · simp [insertOne, Fin.castSucc_ne_last]221  rw [hX, ← reducedFormCell_last_eq]222  simp only [reducedFormCell, normalizedFormCell, Set.mem_ofPred_eq, insertOne_last_comp_rev]223  have h0 : insertOne 0 b 0 = 1 := by simp [insertOne]224  simp only [Function.comp_apply, Fin.rev_last, h0, true_and]225  constructor226  · intro h; rw [← (show (Pi.single 0 1 : Fin (r+1) → IsLocalRing.ResidueField O) ∘ Fin.rev227        = Pi.single (Fin.last r) 1 from ?_), ← h]228    · rfl229    · funext i; simp [Pi.single_apply, Fin.rev_eq_iff]230  · intro h231    funext i232    have := congrFun h (Fin.rev i)233    simp only [residueVector, Function.comp_apply, Fin.rev_rev] at this ⊢234    rw [this]; simp [Pi.single_apply, Fin.rev_eq_iff]235 236private theorem comp_rev_comp_rev {A : Type} {r : ℕ} (b : Fin r → A) :237    (b ∘ Fin.rev) ∘ Fin.rev = b := by238  funext i; simp239 240/-- Reduced form cells normalized at the last coordinate are monic residue cells; coordinate241reversal is a bijection, compatible with congruences and measure preserving, from the reduced form242cell of `X ^ r` normalized at `0` onto the monic residue cell of `X ^ r`. -/243theorem form_cell_monic_identification (O : Type) [CommRing O] [IsDomain O]244    [IsDiscreteValuationRing O] [IsAdicComplete (IsLocalRing.maximalIdeal O) O]245    [Finite (IsLocalRing.ResidueField O)] [TopologicalSpace O] [IsTopologicalRing O]246    [CompactSpace O] [T2Space O] [SecondCountableTopology O] [MeasurableSpace O] [BorelSpace O]247    (htop : IsAdic (IsLocalRing.maximalIdeal O)) (r : ℕ) :248    (∀ (d : ℕ) (g : Fin (d+1) → IsLocalRing.ResidueField O),249      reducedFormCell O d (Fin.last d) g = residueCell O d (formPoly g)) ∧250    Set.BijOn (fun b : Fin r → O => b ∘ Fin.rev) (reducedFormCell O r 0 (Pi.single 0 1))251      (residueCell O r (Polynomial.X ^ r)) ∧252    (∀ (L : ℕ) (b b' : Fin r → O), (∀ j, b j - b' j ∈ (IsLocalRing.maximalIdeal O) ^ L) ↔253      ∀ j, (b ∘ Fin.rev) j - (b' ∘ Fin.rev) j ∈ (IsLocalRing.maximalIdeal O) ^ L) ∧254    MeasureTheory.MeasurePreserving (fun b : Fin r → O => b ∘ Fin.rev)255      (cellMeasure O r (reducedFormCell O r 0 (Pi.single 0 1)))256      (cellMeasure O r (residueCell O r (Polynomial.X ^ r))) := by257  have hcong : ∀ (L : ℕ) (b b' : Fin r → O),258      (∀ j, b j - b' j ∈ (IsLocalRing.maximalIdeal O) ^ L) ↔259        ∀ j, (b ∘ Fin.rev) j - (b' ∘ Fin.rev) j ∈ (IsLocalRing.maximalIdeal O) ^ L :=260    fun L b b' => ⟨fun h j => h _, fun h j => by simpa using h (Fin.rev j)⟩261  refine ⟨reducedFormCell_last_eq O, ?_, hcong, ?_⟩262  · refine ⟨fun b hb => (mem_reducedFormCell_zero_iff O r b).1 hb, ?_,263      fun b' hb' => ⟨b' ∘ Fin.rev, ?_, ?_⟩⟩264    · intro b _ b' _ h265      simpa [comp_rev_comp_rev] using congrArg (fun c : Fin r → O => c ∘ Fin.rev) h266    · rw [mem_reducedFormCell_zero_iff]; simpa [comp_rev_comp_rev] using hb'267    · simp [comp_rev_comp_rev]268  let R : (Fin r → O) ≃ᵐ (Fin r → O) :=269    { toFun := fun b => b ∘ Fin.rev270      invFun := fun b => b ∘ Fin.rev271      left_inv := comp_rev_comp_rev272      right_inv := comp_rev_comp_rev273      measurable_toFun := measurable_pi_iff.2 (fun j => measurable_pi_apply _)274      measurable_invFun := measurable_pi_iff.2 (fun j => measurable_pi_apply _) }275  have hR : ∀ b, R b = b ∘ Fin.rev := fun _ => rfl276  have hμ : MeasureTheory.MeasurePreserving R (coefficientMeasure O r)277      (coefficientMeasure O r) := by278    refine ⟨R.measurable, ?_⟩279    have huniv : coefficientMeasure O r Set.univ = 1 := by280      simpa using coefficient_cylinder_mass O htop r 0 0281    have : MeasureTheory.IsFiniteMeasure (coefficientMeasure O r) := ⟨by simp [huniv]⟩282    refine finite_measures_from_cylinders O (Fin r → O) (IsLocalRing.maximalIdeal O) _ _283      (finite_coordinate_borel_cylinders O _ htop r) fun j x => ?_284    have hset : ∀ z : Fin r → O, {y | adicCongr (IsLocalRing.maximalIdeal O) j y z}285        = {y | ∀ i, y i - z i ∈ (IsLocalRing.maximalIdeal O) ^ j} := fun z => by286      ext y; exact finite_coordinate_adic_congruence O r _ j y z287    rw [hset, R.map_apply]288    have hpre : R ⁻¹' {y | ∀ i, y i - x i ∈ (IsLocalRing.maximalIdeal O) ^ j}289        = {y | ∀ i, y i - (x ∘ Fin.rev) i ∈ (IsLocalRing.maximalIdeal O) ^ j} := by290      ext y291      simp only [Set.mem_preimage, Set.mem_ofPred_eq, hR]292      rw [hcong j y (x ∘ Fin.rev)]293      simp294    rw [hpre, coefficient_cylinder_mass O htop, coefficient_cylinder_mass O htop]295  have hpre : R ⁻¹' residueCell O r (Polynomial.X ^ r) = reducedFormCell O r 0 (Pi.single 0 1) := by296    ext b; simp [hR, mem_reducedFormCell_zero_iff]297  have h2 := hμ.restrict_preimage_emb R.measurableEmbedding (residueCell O r (Polynomial.X ^ r))298  have hmass := hμ.measure_preimage_emb R.measurableEmbedding (residueCell O r (Polynomial.X ^ r))299  rw [hpre] at h2 hmass300  refine ⟨R.measurable, ?_⟩301  unfold cellMeasure302  rw [MeasureTheory.Measure.map_smul, show (fun b : Fin r → O => b ∘ Fin.rev) = ⇑R from rfl,303    h2.map_eq, hmass]304 305/-! ### Measurability of form products -/306 307/-- The reduced form-product map is Borel measurable. -/308theorem form_product_measurable (O : Type) [CommRing O] [IsDomain O] [IsDiscreteValuationRing O]309    [IsAdicComplete (IsLocalRing.maximalIdeal O) O] [Finite (IsLocalRing.ResidueField O)]310    [TopologicalSpace O] [IsTopologicalRing O] [CompactSpace O] [T2Space O]311    [SecondCountableTopology O] [MeasurableSpace O] [BorelSpace O]312    (htop : IsAdic (IsLocalRing.maximalIdeal O)) (ι : Type) [Fintype ι] (d : ι → ℕ)313    (ν : ∀ i, Fin (d i + 1)) (g : ∀ i, Fin (d i + 1) → IsLocalRing.ResidueField O)314    (hgν : ∀ i, g i (ν i) = 1) (hc : FormsCoprime d g) (μ : Fin ((∑ i, d i) + 1))315    (hμ : formProd d g μ = 1) :316    Measurable (reducedFormProduct O d ν g μ) := by317  set m := IsLocalRing.maximalIdeal O318  set f := reducedFormProduct O d ν g μ319  set PC : Set (∀ i, Fin (d i) → O) :=320    Set.pi Set.univ (fun i ↦ reducedFormCell O (d i) (ν i) (g i))321  have hPC : MeasurableSet PC := MeasurableSet.univ_pi (fun i ↦322    (normalized_form_cell_cylinder_mass O htop (d i) (ν i) (g i) (hgν i)).2.2.2.1)323  have hoff : ∀ a, a ∉ PC → f a = 0 := fun a ha ↦ by324    simp only [f, reducedFormProduct]325    exact if_neg fun h ↦ ha fun i _ ↦ h i326  have hball : ∀ (k : ℕ) (L : ℕ) (x : Fin k → O),327      MeasurableSet {b : Fin k → O | ∀ j, b j - x j ∈ m ^ L} := fun k L x ↦ by328    have hk := finite_coordinate_borel_cylinders O m htop k329    have : @MeasurableSet _ (adicCylinderSpace m (Fin k → O)) {b | adicCongr m L b x} :=330      MeasurableSpace.measurableSet_generateFrom (Or.inr ⟨L, x, rfl⟩)331    rw [← hk] at this332    convert this using 1333    ext b334    exact (finite_coordinate_adic_congruence O k m L b x).symm335  have hk := finite_coordinate_borel_cylinders O m htop (∑ i, d i)336  change @Measurable _ _ _ (inferInstance : MeasurableSpace (Fin _ → O)) f337  rw [hk]338  refine measurable_generateFrom ?_339  rintro s (rfl | ⟨L, x, rfl⟩)340  · simp341  obtain ⟨_, hsymm, htrans, -, -⟩ := adic_congruence_rules O (Fin (∑ i, d i) → O) m342  by_cases hne : ∃ a₀ ∈ PC, adicCongr m L (f a₀) x343  · obtain ⟨a₀, ha₀, hfa₀⟩ := hne344    have heq : f ⁻¹' {y | adicCongr m L y x} =345        (PC ∩ Set.pi Set.univ (fun i ↦ {b : Fin (d i) → O | ∀ j, b j - a₀ i j ∈ m ^ L})) ∪346        (PCᶜ ∩ {_a | adicCongr m L (0 : Fin (∑ i, d i) → O) x}) := by347      ext a348      simp only [Set.mem_preimage, Set.mem_ofPred_eq, Set.mem_union, Set.mem_inter_iff,349        Set.mem_compl_iff, Set.mem_univ_pi]350      by_cases ha : a ∈ PC351      · simp only [ha, true_and, not_true_eq_false, false_and, or_false]352        constructor353        · intro h354          have h2 : adicCongr m L (f a) (f a₀) := htrans _ _ _ _ h (hsymm _ _ _ hfa₀)355          rw [finite_coordinate_adic_congruence] at h2356          exact form_product_congruence_reflects O ι d ν g hgν hc μ hμ a a₀ ha ha₀ L h2357        · intro h358          refine htrans _ _ _ _ ?_ hfa₀359          rw [finite_coordinate_adic_congruence]360          exact (form_product_maps_to_and_preserves O ι d ν g μ hμ a a₀ ha ha₀).2.2.2 L h361      · simp only [ha, false_and, false_or, not_false_eq_true, true_and, hoff a ha]362    rw [heq]363    exact (hPC.inter (MeasurableSet.univ_pi (fun i ↦ hball _ _ _))).union364      (hPC.compl.inter (MeasurableSet.const _))365  · push Not at hne366    have heq : f ⁻¹' {y | adicCongr m L y x} =367        PCᶜ ∩ {_a | adicCongr m L (0 : Fin (∑ i, d i) → O) x} := by368      ext a369      simp only [Set.mem_preimage, Set.mem_ofPred_eq, Set.mem_inter_iff, Set.mem_compl_iff]370      by_cases ha : a ∈ PC371      · simp only [ha, not_true_eq_false, false_and, iff_false]372        exact hne a ha373      · simp only [ha, not_false_eq_true, true_and, hoff a ha]374    rw [heq]375    exact hPC.compl.inter (MeasurableSet.const _)376 377/-! ### Products of reduced form cells -/378 379/-- The homogeneous analogue of `factor_cells_measure_preserving`: the reduced form product map380pushes the product of the normalized reduced form cell measures forward to the normalized reduced381form cell measure of the product form. -/382theorem form_cells_measure_preserving (O : Type) [CommRing O] [IsDomain O]Lemma 7.1383    [IsDiscreteValuationRing O] [IsAdicComplete (IsLocalRing.maximalIdeal O) O]384    [Finite (IsLocalRing.ResidueField O)] [TopologicalSpace O] [IsTopologicalRing O]385    [CompactSpace O] [T2Space O] [SecondCountableTopology O] [MeasurableSpace O] [BorelSpace O]386    (htop : IsAdic (IsLocalRing.maximalIdeal O)) (ι : Type) [Fintype ι] (d : ι → ℕ)387    (ν : ∀ i, Fin (d i + 1)) (g : ∀ i, Fin (d i + 1) → IsLocalRing.ResidueField O)388    (hgν : ∀ i, g i (ν i) = 1) (hc : FormsCoprime d g) (μ : Fin ((∑ i, d i) + 1))389    (hμ : formProd d g μ = 1)390    [hσ : ∀ i, MeasureTheory.SigmaFinite391      (cellMeasure O (d i) (reducedFormCell O (d i) (ν i) (g i)))] :392    MeasureTheory.MeasurePreserving (reducedFormProduct O d ν g μ)393      (MeasureTheory.Measure.pi394        (fun i => cellMeasure O (d i) (reducedFormCell O (d i) (ν i) (g i))))395      (cellMeasure O (∑ i, d i) (reducedFormCell O (∑ i, d i) μ (formProd d g))) := by396  let m := IsLocalRing.maximalIdeal O397  let f := reducedFormProduct O d ν g μ398  let P := MeasureTheory.Measure.pi399    (fun i => cellMeasure O (d i) (reducedFormCell O (d i) (ν i) (g i)))400  let PC := Set.pi Set.univ (fun i => reducedFormCell O (d i) (ν i) (g i))401  let D := reducedFormCell O (∑ i, d i) μ (formProd d g)402  have hfm : Measurable f := form_product_measurable O htop ι d ν g hgν hc μ hμ403  obtain ⟨hPprob, hPnull, hPball⟩ := form_cell_product_measure O htop ι d ν g hgν404  obtain ⟨-, hDball, -, hDmeas, -, hDprob, hDmass⟩ :=405    normalized_form_cell_cylinder_mass O htop (∑ i, d i) μ (formProd d g) hμ406  refine measurePreserving_cellMeasure_of_balls O htop P _ D hDmeas hDball f hfm PC hPnull407    (fun a ha => (form_product_maps_to_and_preserves O ι d ν g μ hμ a a ha ha).1)408    fun L hL x hx => ?_409  have hmL : m ^ L ≤ m := Ideal.pow_le_self (by omega)410  rw [hDmass L x hL hx]411  obtain ⟨a', ha', rfl⟩ := (form_product_bijection O ι d ν g hgν hc μ hμ).surjOn hx412  have hsub : Set.pi Set.univ (fun i => {b : Fin (d i) → O | ∀ j, b j - a' i j ∈ m ^ L}) ⊆413      PC := by414    intro a ha i _415    change a i ∈ reducedFormCell O (d i) (ν i) (g i)416    rw [(normalized_form_cell_cylinder_mass O htop (d i) (ν i) (g i) (hgν i)).2.1 (a' i)417      (ha' i trivial)]418    exact fun j => hmL (ha i trivial j)419  rw [← MeasureTheory.measure_inter_conull hPnull, ← hPball L hL a' ha']420  congr 1421  ext a422  constructor423  · rintro ⟨h1, h2⟩ i _ j424    exact form_product_congruence_reflects O ι d ν g hgν hc μ hμ a a' h2 ha' L h1 i j425  · exact fun ha => ⟨(form_product_maps_to_and_preserves O ι d ν g μ hμ a a' (hsub ha)426      ha').2.2.2 L (fun i j => ha i trivial j), hsub ha⟩427 428/-! ### Projective cells -/429 430/-- The number of residue classes modulo `𝔪 ^ L` of units is `q ^ L - q ^ (L - 1)`. -/431private theorem card_units_mod_pow (O : Type) [CommRing O] [IsDomain O]432    [IsDiscreteValuationRing O] [Finite (IsLocalRing.ResidueField O)] (L : ℕ) (hL : 1 ≤ L) :433    Nat.card {c : O ⧸ (IsLocalRing.maximalIdeal O)^L |434        ∃ y, Ideal.Quotient.mk _ y = c ∧ y ∉ IsLocalRing.maximalIdeal O}435      = Nat.card (IsLocalRing.ResidueField O) ^ L -436        Nat.card (IsLocalRing.ResidueField O) ^ (L-1) := by437  set m := IsLocalRing.maximalIdeal O438  have hle : m ^ L ≤ m := Ideal.pow_le_self (by omega)439  set J : Ideal (O ⧸ m ^ L) := m.map (Ideal.Quotient.mk (m ^ L))440  have hU : {c : O ⧸ m^L | ∃ y, Ideal.Quotient.mk _ y = c ∧ y ∉ m} =441      (J : Set (O ⧸ m^L))ᶜ := by442    ext c443    simp only [Set.mem_ofPred_eq, Set.mem_compl_iff, SetLike.mem_coe, J,444      Ideal.mem_map_iff_of_surjective _ Ideal.Quotient.mk_surjective]445    constructor446    · rintro ⟨y, rfl, hy⟩ ⟨z, hz, hzy⟩447      exact hy (by simpa using m.sub_mem hz (hle (Ideal.Quotient.eq.mp hzy)))448    · intro h449      obtain ⟨y, rfl⟩ := Ideal.Quotient.mk_surjective c450      exact ⟨y, rfl, fun hy => h ⟨y, hy, rfl⟩⟩451  have hQ := residue_quotient_card O L452  have hq0 : 0 < Nat.card (IsLocalRing.ResidueField O) := Nat.card_pos453  have hfin : Finite (O ⧸ m ^ L) := Nat.finite_of_card_ne_zero (by rw [hQ]; positivity)454  have hcard := Submodule.card_eq_card_quotient_mul_card J455  have hquot : Nat.card ((O ⧸ m ^ L) ⧸ J) = Nat.card (IsLocalRing.ResidueField O) :=456    Nat.card_congr (DoubleQuot.quotQuotEquivQuotOfLE hle).toEquiv457  rw [hquot, hQ] at hcard458  have hJ : Nat.card J = Nat.card (IsLocalRing.ResidueField O) ^ (L - 1) := by459    obtain ⟨k, rfl⟩ : ∃ k, L = k + 1 := ⟨L - 1, by omega⟩460    rw [pow_succ] at hcard461    simpa using (Nat.eq_of_mul_eq_mul_right hq0 hcard).symm462  rw [hU, Nat.card_coe_set_eq]463  have h2 := Set.ncard_add_ncard_compl (J : Set (O ⧸ m^L))464  have h3 : (J : Set (O ⧸ m^L)).ncard = Nat.card (IsLocalRing.ResidueField O) ^ (L - 1) := by465    rw [← hJ]; rfl466  rw [h3, hQ] at h2467  omega468 469/-- The set of vectors with unit `μ`-coordinate that are congruent modulo `𝔪 ^ L` to a multiple470of `bt` (with `bt μ = 1`) is measurable, of mass `(q ^ L - q ^ (L - 1)) / (q ^ L) ^ (n + 1)`. -/471private theorem unit_multiple_cylinder_mass (O : Type) [CommRing O] [IsDomain O]472    [IsDiscreteValuationRing O] [IsAdicComplete (IsLocalRing.maximalIdeal O) O]473    [Finite (IsLocalRing.ResidueField O)] [TopologicalSpace O] [IsTopologicalRing O]474    [CompactSpace O] [T2Space O] [SecondCountableTopology O] [MeasurableSpace O] [BorelSpace O]475    (htop : IsAdic (IsLocalRing.maximalIdeal O)) (n L : ℕ) (hL : 1 ≤ L) (μ : Fin (n + 1))476    (bt : Fin (n + 1) → O) (hb : bt μ = 1) :477    MeasurableSet {a : Fin (n+1) → O | a μ ∉ IsLocalRing.maximalIdeal O ∧478      ∀ j, a j - a μ * bt j ∈ (IsLocalRing.maximalIdeal O) ^ L} ∧479    coefficientMeasure O (n+1) {a : Fin (n+1) → O | a μ ∉ IsLocalRing.maximalIdeal O ∧480      ∀ j, a j - a μ * bt j ∈ (IsLocalRing.maximalIdeal O) ^ L}481      = ((Nat.card (IsLocalRing.ResidueField O) ^ L -482          Nat.card (IsLocalRing.ResidueField O) ^ (L-1) : ℕ) : ℝ≥0∞) /483        ((Nat.card (IsLocalRing.ResidueField O) ^ L) ^ (n+1) : ℕ) := by484  set m := IsLocalRing.maximalIdeal O485  have hle : m ^ L ≤ m := Ideal.pow_le_self (by omega)486  have hQ := residue_quotient_card O L487  have : Finite (O ⧸ m ^ L) :=488    Nat.finite_of_card_ne_zero (by rw [hQ]; exact (pow_pos Nat.card_pos L).ne')489  let mk := Ideal.Quotient.mk (m ^ L)490  let π : (Fin (n+1) → O) →+ (Fin (n+1) → O ⧸ m ^ L) :=491    (mk : O →+ O ⧸ m ^ L).compLeft (Fin (n+1))492  have hπ : ∀ a j, π a j = mk (a j) := fun _ _ => rfl493  set U := {c : O ⧸ m^L | ∃ y, mk y = c ∧ y ∉ m} with hUdef494  set S := (fun c : O ⧸ m^L => fun j => c * mk (bt j)) '' U with hSdef495  have hE : {a : Fin (n+1) → O | a μ ∉ m ∧ ∀ j, a j - a μ * bt j ∈ m ^ L} = π ⁻¹' S := by496    ext a497    simp only [Set.mem_ofPred_eq, Set.mem_preimage, hSdef, hUdef, Set.mem_image]498    constructor499    · rintro ⟨h1, h2⟩500      refine ⟨mk (a μ), ⟨a μ, rfl, h1⟩, funext fun j => ?_⟩501      rw [hπ, ← map_mul]502      exact (Ideal.Quotient.eq.mpr (h2 j)).symm503    · rintro ⟨c, ⟨y, rfl, hy⟩, hc⟩504      have hj : ∀ j, mk (a j) = mk y * mk (bt j) := fun j => by rw [← hπ, ← hc]505      have hμ' : mk (a μ) = mk y := by rw [hj μ, hb, map_one, mul_one]506      have hyμ : a μ - y ∈ m ^ L := Ideal.Quotient.eq.mp hμ'507      refine ⟨fun h => hy (by simpa using m.sub_mem h (hle hyμ)),508        fun j => Ideal.Quotient.eq.mp ?_⟩509      rw [map_mul, hj j, hμ']510  have hsurj : Function.Surjective π := fun v =>511    ⟨fun j => (Ideal.Quotient.mk_surjective (v j)).choose,512      funext fun j => (Ideal.Quotient.mk_surjective (v j)).choose_spec⟩513  have hball : ∀ x0 : Fin (n+1) → O,514      MeasurableSet {b' : Fin (n+1) → O | ∀ j, b' j - x0 j ∈ m ^ L} := by515    intro x0516    have : @MeasurableSet _ (adicCylinderSpace m (Fin (n+1) → O))517        {b' : Fin (n+1) → O | ∀ j, b' j - x0 j ∈ m ^ L} := by518      apply MeasurableSpace.measurableSet_generateFrom519      refine Or.inr ⟨L, x0, ?_⟩520      ext y521      simp only [Set.mem_ofPred_eq]522      rw [finite_coordinate_adic_congruence]523    rwa [← finite_coordinate_borel_cylinders O m htop (n+1)] at this524  have hfib : ∀ v, MeasurableSet {x | π x = v} := by525    intro v526    obtain ⟨x0, rfl⟩ := hsurj v527    convert hball x0 using 1528    ext x529    simp only [Set.mem_ofPred_eq]530    exact ⟨fun h j => Ideal.Quotient.eq.mp (by rw [← hπ, ← hπ, h]),531      fun h => funext fun j => Ideal.Quotient.eq.mpr (h j)⟩532  have := coefficient_measure_probability O htop (n+1)533  have : MeasureTheory.Measure.IsAddLeftInvariant (coefficientMeasure O (n+1)) := by534    unfold coefficientMeasure; infer_instance535  have hmeas : MeasurableSet (π ⁻¹' S) := by536    have : π ⁻¹' S = ⋃ s ∈ S, {x | π x = s} := by ext; simp537    rw [this]538    exact MeasurableSet.biUnion (Set.to_countable S) fun s _ => hfib s539  refine ⟨hE ▸ hmeas, ?_⟩540  rw [hE, finite_quotient_event_mass _ _ (coefficientMeasure O (n+1)) π hsurj hfib S]541  have hS : Nat.card S = Nat.card U :=542    Nat.card_image_of_injective (fun c c' h => by simpa [hb] using congrFun h μ) _543  rw [hS, card_units_mod_pow O L hL, Nat.card_fun, hQ, Nat.card_fin]544 545private theorem projective_mass_ratio (q n L : ℕ) (hq : 1 < q) (hL : 1 ≤ L) :546    (((q : ℝ≥0∞) - 1) * (q : ℝ≥0∞)⁻¹ ^ (n+1))⁻¹ *547        (((q ^ L - q ^ (L-1) : ℕ) : ℝ≥0∞) / ((q ^ L) ^ (n+1) : ℕ))548      = (q : ℝ≥0∞)⁻¹ ^ (n * (L-1)) := by549  obtain ⟨k, rfl⟩ : ∃ k, L = k + 1 := ⟨L - 1, by omega⟩550  simp only [Nat.add_sub_cancel]551  rw [show q ^ (k+1) - q ^ k = q ^ k * (q - 1) by rw [pow_succ, Nat.mul_sub, mul_one]]552  have hq0 : (q : ℝ≥0∞) ≠ 0 := by exact_mod_cast (by omega : q ≠ 0)553  have hqt : (q : ℝ≥0∞) ≠ ⊤ := ENNReal.natCast_ne_top q554  have hqr : (q : ℝ≥0∞) * (q : ℝ≥0∞)⁻¹ = 1 := ENNReal.mul_inv_cancel hq0 hqt555  have hq1 : ((q - 1 : ℕ) : ℝ≥0∞) = (q : ℝ≥0∞) - 1 := by556    rw [ENNReal.natCast_sub]; simp557  have hs0 : (q : ℝ≥0∞) - 1 ≠ 0 := by558    rw [← hq1]; exact_mod_cast (by omega : q - 1 ≠ 0)559  have hst : (q : ℝ≥0∞) - 1 ≠ ⊤ := ENNReal.sub_ne_top hqt560  push_cast561  rw [div_eq_mul_inv, ENNReal.mul_inv (Or.inl hs0) (Or.inl hst), ← pow_mul]562  simp only [ENNReal.inv_pow, inv_inv]563  set r := (q : ℝ≥0∞)⁻¹564  set Q := (q : ℝ≥0∞)565  set s := Q - 1566  have hss : s⁻¹ * s = 1 := ENNReal.inv_mul_cancel hs0 hst567  rw [show (k+1) * (n+1) = (n + 1 + k) + n * k by ring, pow_add r]568  have hpow : Q ^ (n+1+k) * r ^ (n+1+k) = 1 := by rw [← mul_pow, hqr, one_pow]569  calc s⁻¹ * Q ^ (n + 1) * (Q ^ k * s * (r ^ (n + 1 + k) * r ^ (n * k)))570      = (s⁻¹ * s) * (Q ^ (n+1+k) * r ^ (n+1+k)) * r ^ (n * k) := by ring571    _ = r ^ (n * k) := by rw [hss, hpow, one_mul, one_mul]572 573private theorem projectiveNormalize_alg (O : Type) [CommRing O] [IsLocalRing O] (n : ℕ)574    (G : Fin (n + 1) → IsLocalRing.ResidueField O) (μ : Fin (n + 1)) (hGμ : G μ = 1) :575    Set.MapsTo (projectiveNormalize O n G μ) (projectiveCell O n G) (reducedFormCell O n μ G) ∧576    Set.SurjOn (projectiveNormalize O n G μ) (projectiveCell O n G) (reducedFormCell O n μ G) ∧577    (∀ a ∈ projectiveCell O n G, ∀ a' ∈ projectiveCell O n G,578      projectiveNormalize O n G μ a = projectiveNormalize O n G μ a' ↔579        ∃ u : Oˣ, a' = (u : O) • a) := by580  set PC := projectiveCell O n G581  have hunit : ∀ a ∈ PC, ∃ v : Oˣ, a μ = v ∧582      residueVector O a = IsLocalRing.residue O (v : O) • G := by583    rintro a ⟨-, c, hc, hac⟩584    have hr : IsLocalRing.residue O (a μ) = c := by585      simpa [residueVector, hGμ] using congrFun hac μ586    have hu : IsUnit (a μ) := by587      rw [← IsLocalRing.notMem_maximalIdeal, ← IsLocalRing.residue_eq_zero_iff, hr]; exact hc588    exact ⟨hu.unit, rfl, by rw [hac]; simp [hr]⟩589  have hnorm : ∀ (a : Fin (n+1) → O) (v : Oˣ), a μ = v →590      normalizeAt μ a = ((v⁻¹ : Oˣ) : O) • a := fun a v hv => by591    simp only [normalizeAt, hv, Ring.inverse_unit]592  have hins : ∀ w : Fin (n+1) → O, w μ = 1 → insertOne μ (dropCoord μ w) = w := fun w hw => by593    simp only [insertOne, dropCoord]594    rw [← hw]; exact Fin.insertNth_self_removeNth μ w595  have hnm : ∀ a ∈ PC, projectiveNormalize O n G μ a = dropCoord μ (normalizeAt μ a) :=596    fun a ha => if_pos ha597  have hnμ : ∀ a ∈ PC, normalizeAt μ a μ = 1 := by598    intro a ha599    obtain ⟨v, hv, -⟩ := hunit a ha600    rw [hnorm a v hv]; simp [hv]601  have hinj : ∀ a ∈ PC, ∀ a' ∈ PC,602      projectiveNormalize O n G μ a = projectiveNormalize O n G μ a' ↔603        normalizeAt μ a = normalizeAt μ a' := by604    intro a ha a' ha'605    rw [hnm a ha, hnm a' ha']606    exact ⟨fun h => by rw [← hins _ (hnμ a ha), ← hins _ (hnμ a' ha'), h], fun h => by rw [h]⟩607  refine ⟨?_, ?_, ?_⟩608  · intro a ha609    obtain ⟨v, hv, hres⟩ := hunit a ha610    change insertOne μ (projectiveNormalize O n G μ a) ∈ normalizedFormCell O n μ G611    rw [hnm a ha, hins _ (hnμ a ha)]612    refine ⟨hnμ a ha, ?_⟩613    rw [hnorm a v hv]614    funext i615    have := congrFun hres i616    simp only [residueVector, Pi.smul_apply, smul_eq_mul, map_mul] at this ⊢617    rw [this, ← mul_assoc, ← map_mul, Units.inv_mul, map_one, one_mul]618  · intro b hb619    obtain ⟨h1, h2⟩ : insertOne μ b ∈ normalizedFormCell O n μ G := hb620    have hPC : insertOne μ b ∈ PC :=621      ⟨⟨μ, by rw [h1]; exact isUnit_one⟩, 1, one_ne_zero, by rw [h2, one_smul]⟩622    refine ⟨insertOne μ b, hPC, ?_⟩623    rw [hnm _ hPC]624    simp only [normalizeAt]625    rw [h1, Ring.inverse_one, one_smul]626    simp only [dropCoord, insertOne, Fin.removeNth_insertNth]627  · intro a ha a' ha'628    rw [hinj a ha a' ha']629    obtain ⟨v, hv, -⟩ := hunit a ha630    obtain ⟨v', hv', -⟩ := hunit a' ha'631    rw [hnorm a v hv, hnorm a' v' hv']632    constructor633    · intro h634      refine ⟨v' * v⁻¹, funext fun j => ?_⟩635      have := congrFun h j636      simp only [Pi.smul_apply, smul_eq_mul] at this ⊢637      calc a' j = (v' : O) * (((v'⁻¹ : Oˣ) : O) * a' j) := by638              rw [← mul_assoc, Units.mul_inv, one_mul]639        _ = _ := by rw [← this]; simp only [Units.val_mul]; ring640    · rintro ⟨u, rfl⟩641      obtain rfl : v' = u * v := by642        ext; rw [← hv', Units.val_mul, ← hv]; simp643      funext j644      simp only [Pi.smul_apply, smul_eq_mul, mul_inv_rev, Units.val_mul]645      rw [← mul_assoc, mul_assoc (v⁻¹ : Oˣ).val, Units.inv_mul, mul_one]646 647private theorem projectiveNormalize_preimage_ball (O : Type) [CommRing O] [IsLocalRing O]648    (n : ℕ) (G : Fin (n + 1) → IsLocalRing.ResidueField O) (μ : Fin (n + 1)) (L : ℕ) (hL : 1 ≤ L)649    (x : Fin n → O) (hx : x ∈ reducedFormCell O n μ G) :650    projectiveCell O n G ∩651        projectiveNormalize O n G μ ⁻¹' {y | ∀ j, y j - x j ∈ (IsLocalRing.maximalIdeal O) ^ L}652      = {a | a μ ∉ IsLocalRing.maximalIdeal O ∧653          ∀ j, a j - a μ * insertOne μ x j ∈ (IsLocalRing.maximalIdeal O) ^ L} := by654  set m := IsLocalRing.maximalIdeal O655  have hle : m ^ L ≤ m := Ideal.pow_le_self (by omega)656  obtain ⟨h1, h2⟩ : insertOne μ x ∈ normalizedFormCell O n μ G := hx657  have hxs : ∀ i, insertOne μ x (μ.succAbove i) = x i := fun i => by658    simp [insertOne, Fin.insertNth_apply_succAbove]659  ext a660  simp only [Set.mem_inter_iff, Set.mem_preimage, Set.mem_ofPred_eq]661  constructor662  · rintro ⟨⟨-, c, hc, hac⟩, hB⟩663    have hG : G μ = 1 := by simpa [residueVector, h1] using (congrFun h2 μ).symm664    have hr : IsLocalRing.residue O (a μ) = c := by simpa [residueVector, hG] using congrFun hac μ665    have hu : IsUnit (a μ) := by666      rw [← IsLocalRing.notMem_maximalIdeal, ← IsLocalRing.residue_eq_zero_iff, hr]; exact hc667    refine ⟨IsLocalRing.notMem_maximalIdeal.mpr hu, fun j => ?_⟩668    rw [projectiveNormalize, if_pos ⟨⟨μ, hu⟩, c, hc, hac⟩] at hB669    rcases Fin.eq_self_or_eq_succAbove μ j with rfl | ⟨i, rfl⟩670    · rw [h1, mul_one, sub_self]; exact Submodule.zero_mem _671    · have := hB i672      simp only [dropCoord, normalizeAt, Fin.removeNth, Pi.smul_apply, smul_eq_mul] at this673      rw [hxs]674      convert Ideal.mul_mem_left (m ^ L) (a μ) this using 1675      rw [mul_sub, ← mul_assoc, Ring.mul_inverse_cancel _ hu, one_mul]676  · rintro ⟨hμ, hj⟩677    have hu : IsUnit (a μ) := IsLocalRing.notMem_maximalIdeal.mp hμ678    have hres : residueVector O a = IsLocalRing.residue O (a μ) • G := by679      funext j680      have : IsLocalRing.residue O (a j) = IsLocalRing.residue O (a μ * insertOne μ x j) :=681        Ideal.Quotient.eq.mpr (hle (hj j))682      rw [← h2]683      simpa [residueVector, map_mul] using this684    have hPC : a ∈ projectiveCell O n G :=685      ⟨⟨μ, hu⟩, _, (hu.map (IsLocalRing.residue O)).ne_zero, hres⟩686    refine ⟨hPC, fun i => ?_⟩687    rw [projectiveNormalize, if_pos hPC]688    simp only [dropCoord, normalizeAt, Fin.removeNth, Pi.smul_apply, smul_eq_mul]689    have h3 := Ideal.mul_mem_left (m ^ L) (Ring.inverse (a μ)) (hj (μ.succAbove i))690    rw [hxs] at h3691    convert h3 using 1692    rw [mul_sub, ← mul_assoc, Ring.inverse_mul_cancel _ hu, one_mul]693 694/-- Normalizing a primitive vector at a coordinate `μ` with `G μ = 1` maps the projective cell of695`G` onto the reduced form cell of `G`, with fibres the unit multiples, and pushes the normalized696projective cell measure forward to the normalized reduced form cell measure. -/697theorem projective_cell_normalization_pushforward (O : Type) [CommRing O] [IsDomain O]698    [IsDiscreteValuationRing O] [IsAdicComplete (IsLocalRing.maximalIdeal O) O]699    [Finite (IsLocalRing.ResidueField O)] [TopologicalSpace O] [IsTopologicalRing O]700    [CompactSpace O] [T2Space O] [SecondCountableTopology O] [MeasurableSpace O] [BorelSpace O]701    (htop : IsAdic (IsLocalRing.maximalIdeal O)) (n : ℕ)702    (G : Fin (n + 1) → IsLocalRing.ResidueField O) (μ : Fin (n + 1)) (hGμ : G μ = 1) :703    Set.MapsTo (projectiveNormalize O n G μ) (projectiveCell O n G) (reducedFormCell O n μ G) ∧704    Set.SurjOn (projectiveNormalize O n G μ) (projectiveCell O n G) (reducedFormCell O n μ G) ∧705    (∀ a ∈ projectiveCell O n G, ∀ a' ∈ projectiveCell O n G,706      projectiveNormalize O n G μ a = projectiveNormalize O n G μ a' ↔707        ∃ u : Oˣ, a' = (u : O) • a) ∧708    MeasureTheory.MeasurePreserving (projectiveNormalize O n G μ)709      (cellMeasure O (n+1) (projectiveCell O n G)) (cellMeasure O n (reducedFormCell O n μ G)) := by710  obtain ⟨hmaps, hsurjOn, hfibre⟩ := projectiveNormalize_alg O n G μ hGμ711  refine ⟨hmaps, hsurjOn, hfibre, ?_⟩712  set m := IsLocalRing.maximalIdeal O713  set nm := projectiveNormalize O n G μ714  set PC := projectiveCell O n G715  set D := reducedFormCell O n μ G716  set q := Nat.card (IsLocalRing.ResidueField O)717  have hq1 : 1 < q := Finite.one_lt_card718  have hG0 : G ≠ 0 := fun h => by simp [h] at hGμ719  obtain ⟨hPCm, hPCmass⟩ := projective_cell_mass O htop n G hG0720  obtain ⟨-, hDball, -, hDmeas, -, hDprob, hDmass⟩ :=721    normalized_form_cell_cylinder_mass O htop n μ G hGμ722  have hgen := finite_coordinate_borel_cylinders O m htop n723  have hB : ∀ (L : ℕ) (x : Fin n → O),724      {y : Fin n → O | adicCongr m L y x} = {y | ∀ j, y j - x j ∈ m ^ L} := fun L x => by725    ext y; exact finite_coordinate_adic_congruence O n m L y x726  -- the preimage of a ball around a point outside `D` is empty727  have hkey : ∀ L (x : Fin n → O), 1 ≤ L → x ∉ D →728      PC ∩ nm ⁻¹' {y | ∀ j, y j - x j ∈ m ^ L} = ∅ := fun L x hL hx => by729    refine Set.eq_empty_of_forall_notMem fun a ⟨ha, hyx⟩ => hx ?_730    change x ∈ reducedFormCell O n μ G731    rw [hDball _ (hmaps ha)]732    exact fun j => by733      simpa only [neg_sub] using m.neg_mem (Ideal.pow_le_self (by omega : L ≠ 0) (hyx j))734  have hPCB : ∀ L (x : Fin n → O), MeasurableSet (PC ∩ nm ⁻¹' {y | ∀ j, y j - x j ∈ m ^ L}) := by735    intro L x736    rcases Nat.eq_zero_or_pos L with rfl | hL737    · have : {y : Fin n → O | ∀ j, y j - x j ∈ m ^ 0} = Set.univ := by ext y; simp738      rw [this, Set.preimage_univ, Set.inter_univ]; exact hPCm739    by_cases hx : x ∈ D740    · rw [projectiveNormalize_preimage_ball O n G μ L hL x hx]741      exact (unit_multiple_cylinder_mass O htop n L hL μ (insertOne μ x) (by simp [insertOne])).1742    · rw [hkey L x hL hx]; exact MeasurableSet.empty743  have hoff : ∀ a, a ∉ PC → nm a = 0 := fun a ha => if_neg ha744  have hnmm : Measurable nm := by745    change @Measurable _ _ _ (inferInstance : MeasurableSpace (Fin n → O)) nm746    rw [hgen]747    refine measurable_generateFrom ?_748    rintro s (rfl | ⟨L, x, rfl⟩)749    · simp750    rw [hB]751    have : nm ⁻¹' {y | ∀ j, y j - x j ∈ m ^ L} = (PC ∩ nm ⁻¹' {y | ∀ j, y j - x j ∈ m ^ L}) ∪752        (PCᶜ ∩ {_a | (0 : Fin n → O) ∈ {y : Fin n → O | ∀ j, y j - x j ∈ m ^ L}}) := by753      ext a754      by_cases ha : a ∈ PC755      · simp [ha]756      · simp [ha, hoff a ha]757    rw [this]758    exact (hPCB L x).union (hPCm.compl.inter (MeasurableSet.const _))759  have hμ0 : coefficientMeasure O (n+1) PC ≠ 0 := by760    rw [hPCmass]761    refine mul_ne_zero ?_ (pow_ne_zero _ (ENNReal.inv_ne_zero.mpr (ENNReal.natCast_ne_top _)))762    rw [← Nat.cast_one, ← ENNReal.natCast_sub]; exact_mod_cast (by omega : q - 1 ≠ 0)763  have hμt : coefficientMeasure O (n+1) PC ≠ ⊤ := by764    have := coefficient_measure_probability O htop (n+1)765    exact MeasureTheory.measure_ne_top _ _766  have : MeasureTheory.IsProbabilityMeasure (cellMeasure O (n+1) PC) := by767    constructor768    rw [cellMeasure, MeasureTheory.Measure.smul_apply,769      MeasureTheory.Measure.restrict_apply MeasurableSet.univ, Set.univ_inter, smul_eq_mul,770      ENNReal.inv_mul_cancel hμ0 hμt]771  refine measurePreserving_cellMeasure_of_balls O htop _ n D hDmeas hDball nm hnmm PC772    (by rw [cellMeasure, MeasureTheory.Measure.smul_apply,773      MeasureTheory.Measure.restrict_apply' hPCm, Set.compl_inter_self,774      MeasureTheory.measure_empty, smul_zero]) hmaps fun L hL x hx => ?_775  rw [cellMeasure, MeasureTheory.Measure.smul_apply, MeasureTheory.Measure.restrict_apply' hPCm,776    smul_eq_mul, Set.inter_comm, hDmass L x hL hx,777    projectiveNormalize_preimage_ball O n G μ L hL x hx,778    (unit_multiple_cylinder_mass O htop n L hL μ (insertOne μ x) (by simp [insertOne])).2, hPCmass]779  exact projective_mass_ratio q n L hq1 hL780 781end SurfaceBlowup