Adic congruences, adic perturbations and transport of cylinder measures

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.AdicCylinders7 8/-!9# Adic congruences, adic perturbations and transport of cylinder measures10 11Let `I` be an ideal of `R` and `M` an `R`-module. Congruence modulo `I^j M` is an equivalence12relation, adic cylinders form a π-system, and perturbing by a map `r` that raises adic order13preserves and reflects these congruences. If `M` is `I`-adically complete, the adic perturbation14`x ↦ x + r x` is a bijection, is measurable for the adic cylinder15σ-algebra, and preserves every invariant probability measure with finite adic quotients. Also:16finite measures agreeing on adic cylinders are equal, and an invariant probability measure gives17each fibre of a surjection onto a finite group mass `1/|Q|`.18 19## Main results20 21* `SurfaceBlowup.adic_congruence_rules`, `SurfaceBlowup.adic_cylinders_intersection`,22  `SurfaceBlowup.adic_perturb_congruence_iff`23* `SurfaceBlowup.chart_image_measurable_chart_sigma`24* `SurfaceBlowup.adic_perturb_bijective`, `SurfaceBlowup.adic_perturb_measurable`,25  `SurfaceBlowup.adic_perturb_measure_preserving`26* `SurfaceBlowup.finite_measures_from_cylinders`27* `SurfaceBlowup.finite_quotient_fiber_mass`, `SurfaceBlowup.finite_quotient_event_mass`28 29Provenance: `Thm_SurfaceBlowupV2_{adic_congruence_rules, adic_cylinders_intersection,30adic_perturb_congruence_iff, chart_image_measurable_chart_sigma, digit_iter_successive,31digit_iter_cauchy, digit_iter_limit, digit_limit_solves, adic_perturb_bijective,32adic_perturb_cylinder_preimage, adic_perturb_measurable, finite_measures_from_cylinders,33finite_quotient_fiber_mass, adic_perturb_measure_preserving, finite_quotient_event_mass}` (moved34from `Blowup/Charts.lean` and `Blowup/CurveOrders.lean`).35-/36 37namespace SurfaceBlowup38 39open scoped ENNReal40 41/-! ### Adic congruences -/42 43/-- Congruence modulo `I^j M` is an equivalence relation, coarser for smaller `j`, and trivial44for `j = 0`. -/45theorem adic_congruence_rules (R M : Type) [CommRing R] [AddCommGroup M] [Module R M] (I : Ideal R)46    :47    (∀ j (x : M), adicCongr I j x x) ∧ (∀ j (x y : M), adicCongr I j x y → adicCongr I j y x) ∧48        (∀ j (x y z : M), adicCongr I j x y → adicCongr I j y z → adicCongr I j x z) ∧49        (∀ i j (x y : M), i ≤ j → adicCongr I j x y → adicCongr I i x y) ∧50        (∀ x y : M, adicCongr I 0 x y) := by51  unfold adicCongr52  exact ⟨fun _ _ => by simp, fun _ _ _ h => by simpa using neg_mem h,53    fun _ _ _ _ h1 h2 => by simpa using add_mem h1 h2,54    fun _ _ _ _ hij h => Submodule.smul_mono_left (Ideal.pow_le_pow_right hij) h, fun _ _ => by55        simp⟩56 57/-- Adic cylinders form a π-system. -/58theorem adic_cylinders_intersection (R M : Type) [CommRing R] [AddCommGroup M] [Module R M]59    (I : Ideal R) :60    IsPiSystem (adicCylinders I M) := by61  have mono : ∀ i j : ℕ, i ≤ j → (I ^ j • ⊤ : Submodule R M) ≤ I ^ i • ⊤ :=62    fun i j h => Submodule.smul_mono_left (Ideal.pow_le_pow_right h)63  have key : ∀ (i j : ℕ) (x x' z : M), i ≤ j → adicCongr I i z x → adicCongr I j z x' →64      {y | adicCongr I i y x} ∩ {y | adicCongr I j y x'} = {y | adicCongr I j y z} := by65    intro i j x x' z hij hx hx'66    unfold adicCongr at *67    ext y68    simp only [Set.mem_inter_iff, Set.mem_ofPred_eq]69    exact ⟨fun ⟨_, h2⟩ => by simpa using sub_mem h2 hx',70      fun h => ⟨by simpa using add_mem (mono i j hij h) hx, by simpa using add_mem h hx'⟩⟩71  rintro s hs t ht ⟨z, hzs, hzt⟩72  rcases hs with rfl | ⟨i, x, rfl⟩73  · simp at hzs74  rcases ht with rfl | ⟨j, x', rfl⟩75  · simp at hzt76  right77  rcases le_total i j with h | h78  · exact ⟨j, z, key i j x x' z h hzs hzt⟩79  · refine ⟨i, z, ?_⟩80    rw [Set.inter_comm]81    exact key j i x' x z h hzt hzs82 83/-- Perturbing by a map that raises adic order preserves and reflects congruence modulo84`I^j M`. -/85theorem adic_perturb_congruence_iff (R M : Type) [CommRing R] [AddCommGroup M] [Module R M]86    (I : Ideal R) (r : M → M) (hr : RaisesAdicOrder I r) (j : ℕ) (x y : M) :87    adicCongr I j (adicPerturb r x) (adicPerturb r y) ↔ adicCongr I j x y := by88  have mono : ∀ k, (I ^ (k+1) • ⊤ : Submodule R M) ≤ I ^ k • ⊤ := fun k =>89    Submodule.smul_mono_left (Ideal.pow_le_pow_right (Nat.le_succ k))90  have eq : adicPerturb r x - adicPerturb r y = (x - y) + (r x - r y) := by91    simp only [adicPerturb]; abel92  constructor93  · intro h94    induction j with95    | zero => simp [adicCongr]96    | succ k ih =>97      have h' : adicCongr I k (adicPerturb r x) (adicPerturb r y) := mono k h98      have hk := hr k x y (ih h')99      unfold adicCongr at h hk ⊢100      rw [eq] at h101      simpa using sub_mem h hk102  · intro h103    have hk := mono j (hr j x y h)104    unfold adicCongr at h hk ⊢105    rw [eq]106    exact Submodule.add_mem _ h hk107 108/-- The image of a measurable set of coordinates under a division chart is measurable for109the chart σ-algebra on ideals. -/110theorem chart_image_measurable_chart_sigma (O R : Type) [CommRing O] [CommRing R] [Algebra O R]111    [MeasurableSpace O] (pi : O) (n : ℕ) (f : R) (b : Fin n → R)112    (hchart : IsDivisionChart O R pi f b) (S : Set (Fin n → O)) (hS : MeasurableSet S) :113    @MeasurableSet (Ideal R) (idealChartSigma O R pi) (coordinateIdeal pi f b '' S) :=114  MeasurableSpace.measurableSet_generateFrom ⟨n, f, b, S, hchart, hS, rfl⟩115/-! ### Adic perturbations and measures -/116 117/-- Successive digit iterates are congruent modulo `I^j M`. -/118private theorem digit_iter_successive (R M : Type) [CommRing R] [AddCommGroup M] [Module R M]119    (I : Ideal R)120    (r : M → M) (hr : RaisesAdicOrder I r) (y : M) :121    ∀ j, adicCongr I j (digitIter r y (j+1)) (digitIter r y j) := by122  intro j123  induction j with124  | zero => simp [adicCongr]125  | succ n ih =>126    have h := hr n _ _ ih127    unfold adicCongr at h ⊢128    have e : digitIter r y (n + 1 + 1) - digitIter r y (n + 1)129        = -(r (digitIter r y (n + 1)) - r (digitIter r y n)) := by130      change (y - r (digitIter r y (n + 1))) - (y - r (digitIter r y n)) = _131      abel132    rw [e]133    exact neg_mem h134 135/-- The digit iterates form an `I`-adic Cauchy sequence. -/136private theorem digit_iter_cauchy (R M : Type) [CommRing R] [AddCommGroup M] [Module R M]137    (I : Ideal R)138    (r : M → M) (hr : RaisesAdicOrder I r) (y : M) :139    ∀ i j, i ≤ j → adicCongr I i (digitIter r y i) (digitIter r y j) := by140  obtain ⟨hrefl, hsymm, htrans, hmono, -⟩ := adic_congruence_rules R M I141  intro i j hij142  induction j, hij using Nat.le_induction with143  | base => exact hrefl _ _144  | succ j hij ih =>145    exact htrans _ _ _ _ ih146      (hsymm _ _ _ (hmono _ _ _ _ hij147        (digit_iter_successive R M I r hr y j)))148 149/-- In an `I`-adically complete module the digit iterates converge. -/150private theorem digit_iter_limit (R M : Type) [CommRing R] [AddCommGroup M] [Module R M]151    (I : Ideal R)152    (r : M → M) (hr : RaisesAdicOrder I r) [IsAdicComplete I M] (y : M) :153    ∃ x : M, ∀ j, adicCongr I j (digitIter r y j) x := by154  obtain ⟨L, hL⟩ := IsPrecomplete.prec (I := I) (M := M) (f := digitIter r y) inferInstance155    (fun {m n} hmn => SModEq.sub_mem.mpr156      (digit_iter_cauchy R M I r hr y m n hmn))157  exact ⟨L, fun j => SModEq.sub_mem.mp (hL j)⟩158 159/-- The limit of the digit iterates of `y` solves `x + r x = y`. -/160private theorem digit_limit_solves (R M : Type) [CommRing R] [AddCommGroup M] [Module R M]161    (I : Ideal R)162    (r : M → M) (hr : RaisesAdicOrder I r) [IsAdicComplete I M] (y x : M)163    (hx : ∀ j, adicCongr I j (digitIter r y j) x) :164    adicPerturb r x = y := by165  rw [IsHausdorff.eq_iff_smodEq (I := I)]166  intro j167  rw [SModEq.sub_mem]168  have hmono : (I ^ (j+1) • ⊤ : Submodule R M) ≤ I ^ j • ⊤ :=169    Submodule.smul_mono_left (Ideal.pow_le_pow_right (Nat.le_succ j))170  have h1 := hmono (hx (j+1))171  have h2 := hmono (hr j _ _ (hx j))172  unfold adicCongr at *173  have key : adicPerturb r x - y174      = -((digitIter r y (j+1) - x) + (r (digitIter r y j) - r x)) := by175    simp only [adicPerturb, digitIter]; abel176  rw [key]177  exact neg_mem (add_mem h1 h2)178 179/-- On an `I`-adically complete module, `x ↦ x + r x` is bijective when `r` raises adic order. -/180theorem adic_perturb_bijective (R M : Type) [CommRing R] [AddCommGroup M] [Module R M] (I : Ideal R)181    (r : M → M) (hr : RaisesAdicOrder I r) [IsAdicComplete I M] :182    Function.Bijective (adicPerturb r) := by183  refine ⟨fun x y hxy => ?_, fun y => ?_⟩184  · have h : ∀ j, adicCongr I j x y := fun j =>185      (adic_perturb_congruence_iff R M I r hr j x y).1 (by186        rw [hxy]; simp [adicCongr])187    exact sub_eq_zero.1 <| IsHausdorff.haus (IsAdicComplete.toIsHausdorff (I := I) (M := M))188      (x - y) fun n => by rw [SModEq.sub_mem, sub_zero]; exact h n189  · obtain ⟨x, hx⟩ := digit_iter_limit R M I r hr y190    exact ⟨x, digit_limit_solves R M I r hr y x hx⟩191 192/-- The preimage of an adic cylinder under an adic perturbation is an adic cylinder. -/193private theorem adic_perturb_cylinder_preimage (R M : Type) [CommRing R] [AddCommGroup M]194    [Module R M]195    (I : Ideal R) (r : M → M) (hr : RaisesAdicOrder I r) [IsAdicComplete I M] (j : ℕ) (z : M) :196    ∃ x : M, adicPerturb r x = z ∧ (adicPerturb r) ⁻¹' {w | adicCongr I j w z} =197        {y | adicCongr I j y x} := by198  obtain ⟨x, hx⟩ := (adic_perturb_bijective R M I r hr).2 z199  refine ⟨x, hx, ?_⟩200  ext y201  simp only [Set.mem_preimage, Set.mem_ofPred_eq]202  rw [← hx]203  exact adic_perturb_congruence_iff R M I r hr j y x204 205/-- An adic perturbation is measurable for the adic cylinder σ-algebra. -/206theorem adic_perturb_measurable (R M : Type) [CommRing R] [AddCommGroup M] [Module R M]207    (I : Ideal R) (r : M → M) (hr : RaisesAdicOrder I r) [IsAdicComplete I M] [MeasurableSpace M]208    (hgen : ‹MeasurableSpace M› = adicCylinderSpace I M) :209    Measurable (adicPerturb r) := by210  subst hgen211  let : MeasurableSpace M := adicCylinderSpace I M212  apply measurable_generateFrom213  rintro s (rfl | ⟨j, z, rfl⟩)214  · simp215  · obtain ⟨x, -, hx⟩ :=216      adic_perturb_cylinder_preimage R M I r hr j z217    rw [hx]218    exact MeasurableSpace.measurableSet_generateFrom (Or.inr ⟨j, x, rfl⟩)219 220/-- Two finite measures that agree on adic cylinders are equal, if the cylinders generate. -/221theorem finite_measures_from_cylinders (R M : Type) [CommRing R] [AddCommGroup M] [Module R M]222    (I : Ideal R) [MeasurableSpace M] (mu nu : MeasureTheory.Measure M)223    [MeasureTheory.IsFiniteMeasure mu] (hgen : ‹MeasurableSpace M› = adicCylinderSpace I M)224    (heq : ∀ j x, mu {y | adicCongr I j y x} = nu {y | adicCongr I j y x}) :225    mu = nu := by226  refine MeasureTheory.ext_of_generate_finite (adicCylinders I M) hgen227    (adic_cylinders_intersection R M I) ?_ ?_228  · rintro s (rfl | ⟨j, x, rfl⟩)229    · simp230    · exact heq j x231  · have h : {y : M | adicCongr I 0 y 0} = Set.univ := by ext; simp [adicCongr]232    exact h ▸ heq 0 0233 234/-- Under an invariant probability measure, each fibre of a surjection onto a finite group235has mass `1/|Q|`. -/236theorem finite_quotient_fiber_mass (G Q : Type) [AddCommGroup G] [AddCommGroup Q] [Finite Q]237    [MeasurableSpace G] [MeasurableAdd G] (mu : MeasureTheory.Measure G)238    [MeasureTheory.IsProbabilityMeasure mu] [MeasureTheory.Measure.IsAddLeftInvariant mu]239    (pi : G →+ Q) (hpi : Function.Surjective pi) (hm : ∀ a, MeasurableSet {x | pi x = a}) (a : Q) :240    mu {x | pi x = a} = (Nat.card Q : ℝ≥0∞)⁻¹ := by241  have hfib : ∀ b, mu {x | pi x = b} = mu {x | pi x = a} := by242    intro b243    obtain ⟨t, ht⟩ := hpi (a - b)244    have : {x | pi x = b} = (fun h => t + h) ⁻¹' {x | pi x = a} := by245      ext x; simp only [Set.mem_ofPred_eq, Set.mem_preimage, map_add, ht]246      constructor247      · intro h; rw [h]; abel248      · intro h249        have h2 : pi x = a - (a - b) := eq_sub_of_add_eq' h250        rw [h2]; abel251    rw [this, MeasureTheory.measure_preimage_add]252  have := Fintype.ofFinite Q253  have hU : (⋃ b : Q, {x | pi x = b}) = Set.univ := by254    ext x; simp255  have hsum : mu Set.univ = ∑ b : Q, mu {x | pi x = b} := by256    rw [← hU, MeasureTheory.measure_iUnion _ hm, tsum_fintype]257    intro i j hij258    exact Set.disjoint_left.mpr fun x hi hj => hij (hi.symm.trans hj)259  simp only [hfib, MeasureTheory.measure_univ, Finset.sum_const, Finset.card_univ,260    nsmul_eq_mul] at hsum261  rw [Nat.card_eq_fintype_card]262  have hpos : (Fintype.card Q : ℝ≥0∞) ≠ 0 := by simp263  rw [← one_mul (mu _), ← ENNReal.inv_mul_cancel hpos (by simp), mul_assoc, ← hsum, mul_one]264 265/-- An adic perturbation preserves an invariant probability measure with finite adic266quotients. -/267theorem adic_perturb_measure_preserving (R M : Type) [CommRing R] [AddCommGroup M] [Module R M]268    (I : Ideal R) (r : M → M) (hr : RaisesAdicOrder I r) [IsAdicComplete I M] [MeasurableSpace M]269    [MeasurableAdd M] (mu : MeasureTheory.Measure M) [MeasureTheory.IsProbabilityMeasure mu]270    [MeasureTheory.Measure.IsAddLeftInvariant mu] (hgen : ‹MeasurableSpace M› = adicCylinderSpace I271    M) (hfinite : ∀ j, Finite (AdicQuotient I M j)) :272    MeasureTheory.MeasurePreserving (adicPerturb r) mu mu := by273  have hmeas : Measurable (adicPerturb r) :=274    adic_perturb_measurable R M I r hr hgen275  have hball : ∀ j (x : M), MeasurableSet {y | adicCongr I j y x} := by276    intro j x277    rw [hgen]278    exact MeasurableSpace.measurableSet_generateFrom (Or.inr ⟨j, x, rfl⟩)279  have hfib : ∀ j (x : M),280      {y | (adicReduce I j : M →ₗ[R] AdicQuotient I M j).toAddMonoidHom y281        = (adicReduce I j : M →ₗ[R] AdicQuotient I M j) x} = {y | adicCongr I j y x} := by282    intro j x283    ext y284    simp only [Set.mem_ofPred_eq, adicReduce, adicCongr, LinearMap.toAddMonoidHom_coe,285      Submodule.mkQ_apply]286    exact Submodule.Quotient.eq _287  have hmass : ∀ j (x : M), mu {y | adicCongr I j y x}288      = (Nat.card (AdicQuotient I M j) : ℝ≥0∞)⁻¹ := by289    intro j x290    have := hfinite j291    rw [← hfib j x]292    refine finite_quotient_fiber_mass M (AdicQuotient I M j) mu293      (adicReduce I j : M →ₗ[R] AdicQuotient I M j).toAddMonoidHom294      (Submodule.mkQ_surjective _) ?_ _295    intro a296    obtain ⟨x', rfl⟩ := Submodule.mkQ_surjective (I ^ j • ⊤ : Submodule R M) a297    have := hfib j x'298    simp only [adicReduce] at this ⊢299    rw [this]300    exact hball j x'301  refine ⟨hmeas, finite_measures_from_cylinders R M I _ _ hgen fun j z => ?_⟩302  obtain ⟨x, -, hx⟩ := adic_perturb_cylinder_preimage R M I r hr j z303  rw [MeasureTheory.Measure.map_apply hmeas (hball j z), hx, hmass, hmass]304 305/-- Under an invariant probability measure, the preimage of `S ⊆ Q` under a surjection onto a306finite group has mass `|S|/|Q|`. -/307theorem finite_quotient_event_mass (G Q : Type) [AddCommGroup G] [AddCommGroup Q] [Finite Q]308    [MeasurableSpace G] [MeasurableAdd G] (mu : MeasureTheory.Measure G)309    [MeasureTheory.IsProbabilityMeasure mu] [MeasureTheory.Measure.IsAddLeftInvariant mu]310    (pi : G →+ Q) (hpi : Function.Surjective pi) (hm : ∀ a, MeasurableSet {x | pi x = a})311    (S : Set Q) :312    mu (pi ⁻¹' S) = (Nat.card S : ℝ≥0∞) / Nat.card Q := by313  have hS : S.Finite := Set.toFinite S314  have hU : pi ⁻¹' S = ⋃ a ∈ hS.toFinset, {x | pi x = a} := by315    ext x; simp316  rw [hU, MeasureTheory.measure_biUnion_finset]317  · simp_rw [finite_quotient_fiber_mass G Q mu pi hpi hm]318    rw [Finset.sum_const, nsmul_eq_mul, div_eq_mul_inv, Nat.card_eq_card_finite_toFinset hS]319  · intro a _ b _ hab320    exact Set.disjoint_left.mpr (fun x hx hy => hab (hx.symm.trans hy))321  · intro a _; exact hm a322 323end SurfaceBlowup