Measure of member boxes

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.NullBridges7 8/-!9# Measure of member boxes10 11Near the center of a cell of a concrete member, the strict transform identifies a box of the parent12coordinate space with a box of the product of child coordinate spaces, scaling Haar measure by13`q^(-tri(cellDegree))`. Summing over the coset decomposition of a cell, we show that the box14`{z ∈ cell : strict transform ∈ Π G_j}` is measurable and compute its measure in terms of the child15state measures.16 17## Main results18 19* `member_cell_box_measurable`: the set of ideals of a cell whose strict transforms lie in a20  measurable box `Π G_j` is measurable.21* `member_cell_box_measure`: its measure is `q^(-tri(cellDegree)) ∏ μ_j(G_j)`.22 23## Implementation notes24 25All results share the long list of hypotheses describing a cell and its children, which is26declared once as section variables; the local notation `cellStrict` abbreviates the strict-transform27map `J ↦ (strictTransformIdeal (alpha j) (e j) (cellDegree c) J)_j` of the cell, and further local28notations (`𝒪`, `ℛ`, `𝔫`, `ϖ`, `𝔡`, `𝒥`, `𝒱`, `𝐪`, `𝒞`) abbreviate the recurring parent data.29Both public results are obtained chart by chart from the private lemma `member_cell_chart_box`,30which sums the center computation `member_center_box_measure` over the coset decomposition of the31cell.32 33Provenance: member_center_translate_measure_data, member_center_box_measure,34member_cell_box_measurable, member_cell_box_measure.35-/36 37open MeasureTheory38open scoped BigOperators ENNReal39 40namespace SurfaceBlowup41 42/-! ### Auxiliary facts -/43 44/-- Scaling the coordinates by `π^k` maps measurable sets to measurable sets. -/45private theorem measurableSet_coordinateScale_image {O : Type} [CommRing O] {n : ℕ} (pi : O)46    [MeasurableSpace (Fin n → O)]47    (hgen : ‹MeasurableSpace (Fin n → O)› = adicCylinderSpace (Ideal.span {pi}) (Fin n → O))48    (hinj : Function.Injective (fun w : Fin n → O => pi • w)) (k : ℕ) (S : Set (Fin n → O))49    (hS : MeasurableSet S) :50    MeasurableSet (coordinateScale pi k '' S) := by51  induction k with52  | zero =>53    have h0 : (coordinateScale pi 0 : (Fin n → O) → (Fin n → O)) = id := by54      funext w; simp [coordinateScale]55    rwa [h0, Set.image_id]56  | succ k ih =>57    have : coordinateScale pi (k+1) '' S =58        (fun w : Fin n → O => pi • w) '' (coordinateScale pi k '' S) := by59      rw [Set.image_image]; congr 1; funext w; simp [coordinateScale, pow_succ', mul_smul]60    rw [this]; exact measurableSet_smul_image pi hgen hinj _ ih61 62/-- `q^n · q⁻¹^n = 1` for the (finite, nonzero) residue cardinality `q` of a member. -/63private theorem concreteMember_q_pow_mul_inv_pow (m : ConcreteMember) (n : ℕ) :64    (m.toMeasured.q : ℝ≥0∞) ^ n * (m.toMeasured.q : ℝ≥0∞)⁻¹ ^ n = 1 := by65  rw [← mul_pow, ENNReal.mul_inv_cancel (Nat.cast_ne_zero.mpr Nat.card_pos.ne')66    (ENNReal.natCast_ne_top _), one_pow]67 68/-- If `φ ⁻¹' C` is the union of the cosets `Cos z₀` (`z₀ ∈ F`), each a translate `z₀ + D`, and69  `φ (z₀ + w) = ψ z₀ w`, then `φ ⁻¹' (C ∩ Z)` is the union of the translates70  `z₀ + (ψ z₀ ⁻¹' Z ∩ D)`. -/71private theorem preimage_inter_eq_biUnion_translate {V I : Type} [Add V] (φ : V → I)72    (ψ : V → V → I) (C Z : Set I) (D : Set V) (F : Finset V) (Cos : V → Set V)73    (htr : ∀ z₀ w, φ (z₀ + w) = ψ z₀ w) (hcos : ∀ z₀, Cos z₀ = (fun w => z₀ + w) '' D)74    (hdec : φ ⁻¹' C = ⋃ z₀ ∈ F, Cos z₀) :75    φ ⁻¹' (C ∩ Z) = ⋃ z₀ ∈ F, (fun w => z₀ + w) '' (ψ z₀ ⁻¹' Z ∩ D) := by76  ext z77  rw [Set.mem_iUnion₂]78  constructor79  · rintro ⟨hzC, hzZ⟩80    have hz : z ∈ φ ⁻¹' C := hzC81    rw [hdec] at hz82    obtain ⟨z₀, hz₀, hzc⟩ := Set.mem_iUnion₂.mp hz83    rw [hcos] at hzc84    obtain ⟨w, hw, rfl⟩ := hzc85    exact ⟨z₀, hz₀, w, ⟨by rw [Set.mem_preimage, ← htr]; exact hzZ, hw⟩, rfl⟩86  · rintro ⟨z₀, hz₀, w, ⟨hwZ, hw⟩, rfl⟩87    have hzC : z₀ + w ∈ φ ⁻¹' C := by88      rw [hdec]; exact Set.mem_iUnion₂.mpr ⟨z₀, hz₀, by rw [hcos]; exact ⟨w, hw, rfl⟩⟩89    refine ⟨hzC, ?_⟩90    beta_reduce91    rw [htr]92    exact hwZ93 94/-- If finitely many sets `P p` (`p ∈ T`) partition `C` and `Φ` maps `C` bijectively onto `S`, then95  the measures of the pieces `Y ∩ Φ '' P p` add up to `ν (Y ∩ S)`. -/96private theorem sum_measure_inter_image_of_partition {α β ι : Type} [MeasurableSpace β]97    (ν : MeasureTheory.Measure β) {Φ : α → β} {C : Set α} {S : Set β} (hbij : Set.BijOn Φ C S)98    (T : Finset ι) (P : ι → Set α) (hsub : ∀ p ∈ T, P p ⊆ C) (hcov : C ⊆ ⋃ p ∈ T, P p)99    (hdisj : (T : Set ι).PairwiseDisjoint P) (Y : Set β)100    (hmeas : ∀ p ∈ T, MeasurableSet (Y ∩ Φ '' P p)) :101    ∑ p ∈ T, ν (Y ∩ Φ '' P p) = ν (Y ∩ S) := by102  rw [← MeasureTheory.measure_biUnion_finset _ hmeas]103  · congr 1104    ext y105    simp only [Set.mem_iUnion, Set.mem_inter_iff, exists_prop]106    constructor107    · rintro ⟨p, hp, hyY, J, hJ, rfl⟩108      exact ⟨hyY, hbij.mapsTo (hsub p hp hJ)⟩109    · rintro ⟨hyY, hyS⟩110      obtain ⟨J, hJ, rfl⟩ := hbij.surjOn hyS111      obtain ⟨p, hp, hJP⟩ := Set.mem_iUnion₂.mp (hcov hJ)112      exact ⟨p, hp, hyY, J, hJP, rfl⟩113  · intro p hp p' hp' hne114    refine Disjoint.mono Set.inter_subset_right Set.inter_subset_right ?_115    rw [Set.disjoint_left]116    rintro y ⟨J, hJ, rfl⟩ ⟨J', hJ', hJJ⟩117    obtain rfl := hbij.injOn (hsub _ hp' hJ') (hsub _ hp hJ) hJJ118    exact Set.disjoint_left.mp (hdisj hp hp' hne) hJ hJ'119 120/-- The `i`-th chart `z ↦ (f_i + π Σ zₖ b_{i,k})` of the atlas of a concrete member. -/121private noncomputable def memberChart (m : ConcreteMember) (i : m.atlas.ι) :122    (Fin m.toMeasured.s.degree → m.toMeasured.O) → Ideal m.toMeasured.R :=123  coordinateIdeal m.S.pi (m.atlas.chart i).f (m.atlas.chart i).b124 125/-- Every ideal of a cell of a concrete member lies in the range of one of the atlas charts. -/126private theorem member_cell_mem_chart_range (m : ConcreteMember) (c : m.toMeasured.cellIndex)127    (J : Ideal m.toMeasured.R) (hJ : J ∈ m.toMeasured.cell c) :128    ∃ i, J ∈ Set.range (memberChart m i) := by129  have hJs : J ∈ surfaceStateSet m.O m.R m.S m.s := hJ.1130  rw [m.atlas.cover] at hJs131  obtain ⟨i, hi⟩ := Set.mem_iUnion.mp hJs132  exact ⟨i, (concrete_member_charts m i).2.1 ▸ hi⟩133 134/-! ### Boxes in a cell -/135 136section CellBoxes137 138variable (m : ConcreteMember) (c : m.toMeasured.cellIndex)139    (mc : m.toMeasured.childIdx c → ConcreteMember)140 141/- Local abbreviations for the parent data: coefficient ring `𝒪`, ring `ℛ`, state degree `𝔫`,142uniformizer `ϖ`, cell degree `𝔡`, child index type `𝒥`, coordinate space `𝒱 = 𝒪^𝔫`, residue143cardinality `𝐪` (as an extended real), and the product `𝒞 = Π R_j` of the child rings. -/144local notation "𝒪" => m.toMeasured.O145local notation "ℛ" => m.toMeasured.R146local notation "𝔫" => m.toMeasured.s.degree147local notation "ϖ" => m.toMeasured.S.pi148local notation "𝔡" => m.toMeasured.cellDegree c149local notation "𝒥" => m.toMeasured.childIdx c150local notation "𝒱" => Fin 𝔫 → 𝒪151local notation "𝐪" => (m.toMeasured.q : ℝ≥0∞)152set_option quotPrecheck false153local notation "𝒞" => ∀ j, (mc j).toMeasured.R154set_option quotPrecheck true155 156/-- For a scaled normalization whose linear part has a scaled inverse `Q`, the child coordinate map157  `childCoordinateMap π a b E H` on `O^deg` has measurable range and measurable preimages. -/158private theorem member_childCoordinateMap_measurable {R : Type} [CommRing R] [Algebra 𝒪 R] (a : ℕ)159    (b : Fin 𝔫 → R) (E : R ≃ₗ[𝒪] (𝒱 × R)) [IsAdicComplete (Ideal.span {ϖ}) (𝒱 × R)]160    (H : 𝒱 →ₗ[𝒪] R) (k : ℕ) (hk : k < a) (Q : 𝒱 →ₗ[𝒪] 𝒱)161    (hQ : ∀ w, normalizationLinearPart E H (Q w) = (ϖ ^ k) • w) :162    MeasurableSet (Set.range (childCoordinateMap ϖ a b E H)) ∧163      ∀ T, MeasurableSet T → MeasurableSet (childCoordinateMap ϖ a b E H ⁻¹' T) := by164  have hpiIrr : Irreducible ϖ := m.toMeasured.S.pi_irreducible165  have hOc : IsAdicComplete (Ideal.span {ϖ}) 𝒪 := dvr_isAdicComplete_span_uniformizer _ _ hpiIrr166  have hOn : IsAdicComplete (Ideal.span {ϖ}) 𝒱 := finite_free_adic_complete _ _ _167  obtain ⟨hgen, -, -, -, hcontall⟩ :=168    coefficient_space_strict_instances 𝒪 m.toMeasured.htop ϖ hpiIrr 𝔫169  have hinj : Function.Injective (fun w : 𝒱 => ϖ • w) := smul_right_injective _ hpiIrr.ne_zero170  obtain ⟨-, hrange, hpre⟩ := child_coordinate_map_scaled _ _ _ _ a b E H (by omega) hinj171  refine ⟨?_, fun T hT ↦ ?_⟩172  · rw [← Set.preimage_image_eq (Set.range _) hinj, ← hrange,173      strict_normalizer_lattice_image _ _ _ _ a b E _ _ hk Q hQ]174    exact (continuous_const_smul _).measurable175      (isCompact_range (hcontall a _)).isClosed.measurableSet176  · rw [← hpre]177    exact scaled_strict_map_measurable _ _ _ _ a b E _ _ hk Q hQ hgen (hcontall a _)178      (measurableSet_smul_image _ hgen hinj T hT)179 180variable [∀ j, Algebra m.toMeasured.O (mc j).toMeasured.O]181    [∀ j, Algebra m.toMeasured.O (mc j).toMeasured.R]182    [∀ j, IsScalarTower m.toMeasured.O (mc j).toMeasured.O (mc j).toMeasured.R]183    (pc : ∀ j, (mc j).toMeasured.O ≃ₗ[m.toMeasured.O]184      (Fin (m.toMeasured.childDelta c j) → m.toMeasured.O))185    (hpc : ∀ j, Measurable (pc j)) (hpc' : ∀ j, Measurable (pc j).symm)186    (hcard : ∀ j, (mc j).toMeasured.q = m.toMeasured.q ^ m.toMeasured.childDelta c j)187    (hpiO : ∀ j, algebraMap m.toMeasured.O (mc j).toMeasured.O m.toMeasured.S.pi =188      (mc j).toMeasured.S.pi)189    (hdeg : ∑ j, m.toMeasured.childDelta c j * (mc j).toMeasured.s.degree = m.toMeasured.s.degree)190    (alpha : ∀ j, m.toMeasured.R →ₐ[m.toMeasured.O] (mc j).toMeasured.R)191    (e : ∀ j, (mc j).toMeasured.R) (he : ∀ j, e j = (mc j).toMeasured.S.t)192    (hvert : ∀ j, ∃ (s : ℕ) (cj : (mc j).toMeasured.R),193      algebraMap m.toMeasured.O (mc j).toMeasured.R m.toMeasured.S.pi ^ s =194      e j ^ m.toMeasured.cellDegree c * cj)195    (hbij : Set.BijOn196      (fun (J : Ideal m.toMeasured.R) (j : m.toMeasured.childIdx c) => strictTransformIdeal197      (alpha j) (e j) (m.toMeasured.cellDegree c) J) (m.toMeasured.cell c)198      (Set.pi Set.univ fun j => (mc j).toMeasured.stateSet))199    (hstrict : ∀ f : m.toMeasured.R, Ideal.span {f} ∈ m.toMeasured.cell c →200      ∃ g : (∀ j, (mc j).toMeasured.R), ∀ j, alpha j f = e j ^ m.toMeasured.cellDegree c * g j)201    (hindex : ∀ f : m.toMeasured.R, Ideal.span {f} ∈ m.toMeasured.cell c →202      ∀ g : (∀ j, (mc j).toMeasured.R), (∀ j, alpha j f = e j ^ m.toMeasured.cellDegree c * g j) →203      ∀ iota : (m.toMeasured.R ⧸ Ideal.span {f}) →ₗ[m.toMeasured.O]204      ((∀ j, (mc j).toMeasured.R) ⧸ Ideal.span {g}),205      (∀ h : m.toMeasured.R, iota (Ideal.Quotient.mk (Ideal.span {f}) h) =206      Ideal.Quotient.mk (Ideal.span {g}) (fun j => alpha j h)) → Function.Injective iota ∧207      Module.length m.toMeasured.O208      (((∀ j, (mc j).toMeasured.R) ⧸ Ideal.span {g}) ⧸ LinearMap.range iota) =209      (chooseTwo (m.toMeasured.cellDegree c) : ℕ∞))210    (hsum : ∑ j, m.toMeasured.childDelta c j * (mc j).toMeasured.s.firstContact =211      m.toMeasured.cellDegree c)212 213/-- The strict-transform map of the cell `c`, sending an ideal to its tuple of child strict214  transforms. -/215local notation "cellStrict" => fun (J : Ideal ℛ) (j : 𝒥) => strictTransformIdeal (alpha j) (e j) 𝔡 J216 217/-- The box of parent coordinates divisible by `π^k`, the domain of the recentred chart. -/218local notation "centerBox" k => Set.range (coordinateScale ϖ k)219 220include he hpiO in221/-- The parameter `π` lies in the Jacobson radical of `Π R_j`, and the tuple `e = (t_j)_j` of child222  parameters is a nonzerodivisor of `Π R_j`. -/223private theorem member_children_jacobson_regular :224    algebraMap 𝒪 𝒞 ϖ ∈ Ideal.jacobson (⊥ : Ideal 𝒞) ∧ Function.Injective (fun z : 𝒞 => e * z) := by225  refine pi_algebraMap_mem_jacobson_bot 𝒪 _ _ _ (fun j => ?_) e226    fun j => concrete_member_mul_t_injective (he j)227  rw [IsScalarTower.algebraMap_apply 𝒪 (mc j).toMeasured.O, hpiO j]228  exact (surface_vertical_parameter _ _ (mc j).toMeasured.S).2229 230include hpiO in231/-- The product `Π R_j` of the child surfaces is `π`-adically complete. -/232private theorem member_children_isAdicComplete : IsAdicComplete (Ideal.span {ϖ}) 𝒞 := by233  have hRj : ∀ j, IsAdicComplete (Ideal.span {ϖ}) (mc j).toMeasured.R := fun j => by234    rw [← IsAdicComplete.map_algebraMap_iff (S := (mc j).toMeasured.O), Ideal.map_span,235      Set.image_singleton, hpiO j]236    change IsAdicComplete (Ideal.span {(mc j).S.pi})237      (ConcreteSurface (mc j).O (mc j).pi (mc j).u (mc j).a (mc j).b)238    rw [(mc j).hS_pi]239    exact concrete_surface_isAdicComplete_span_pi_base _ _ (mc j).hpi _ _ _ (mc j).ha240  exact isAdicComplete_pi _ _ _ _241 242omit [∀ j, Algebra 𝒪 (mc j).toMeasured.R]243  [∀ j, IsScalarTower 𝒪 (mc j).toMeasured.O (mc j).toMeasured.R] in244/-- Given division charts `E' j` at state generators `g j` of the children and a measurable245  coordinate splitting `ρ`, the child chart map `w ↦ (coordinateIdeal (g j) (ρ w)_j)_j` is246  measurable. -/247private theorem child_chart_map_measurable (g : 𝒞)248    (hgj : ∀ j, Ideal.span {g j} ∈ (mc j).toMeasured.stateSet)249    (bc' : ∀ j, Fin (mc j).toMeasured.s.degree → (mc j).toMeasured.R)250    (E' : ∀ j, (mc j).toMeasured.R ≃ₗ[(mc j).toMeasured.O]251      ((Fin (mc j).toMeasured.s.degree → (mc j).toMeasured.O) × (mc j).toMeasured.R))252    (hE' : ∀ j w, (E' j).symm w = divisionMap (g j) (bc' j) w)253    (ρ : 𝒱 ≃ₗ[𝒪] (∀ j, Fin (mc j).toMeasured.s.degree → (mc j).toMeasured.O))254    (hρ : Measurable ρ) :255    Measurable fun (w : 𝒱) (j : 𝒥) =>256      coordinateIdeal (mc j).toMeasured.S.pi (g j) (bc' j) (ρ w j) := by257  rw [measurable_pi_iff]; intro j258  have := concrete_member_division_module_isAdicComplete (mc j)259  obtain ⟨hp0, hpm⟩ :=260    surface_vertical_parameter (mc j).toMeasured.O (mc j).toMeasured.R (mc j).toMeasured.S261  exact (coordinate_ideal_measurable_chart_sigma _ (mc j).toMeasured.htop _ _262    (mc j).toMeasured.S.pi_irreducible hp0 hpm _ (g j) (bc' j)263    ⟨⟨E' j, hE' j⟩, (concrete_member_state_generator_regular (mc j) (g j) (hgj j)).2.2⟩).comp264    ((measurable_pi_apply j).comp hρ)265 266include hcard hpiO he hbij hindex hsum267 268/-- At the center of a cell, the box of parent coordinates whose strict transforms lie in `Π G_j`269  has Haar measure `q^(-tri(cellDegree))` times the measure of the corresponding set of child270  coordinates. -/271private theorem member_center_translate_measure_data272    (s : ℕ) (hs : tri 𝔡 ≤ s) (cc : 𝒞) (hcc : (algebraMap 𝒪 𝒞 ϖ) ^ s = e ^ 𝔡 * cc)273    (f : ℛ) (b : Fin 𝔫 → ℛ) (E₀ : ℛ ≃ₗ[𝒪] (𝒱 × ℛ)) (hE₀ : ∀ w, E₀.symm w = divisionMap f b w)274    (hf : Ideal.span {f} ∈ m.toMeasured.cell c)275    (g : 𝒞) (hg : ∀ j, alpha j f = e j ^ 𝔡 * g j)276    (hgj : ∀ j, Ideal.span {g j} ∈ (mc j).toMeasured.stateSet)277    (bc' : ∀ j, Fin (mc j).toMeasured.s.degree → (mc j).toMeasured.R)278    (E' : ∀ j, (mc j).toMeasured.R ≃ₗ[(mc j).toMeasured.O]279      ((Fin (mc j).toMeasured.s.degree → (mc j).toMeasured.O) × (mc j).toMeasured.R))280    (hE' : ∀ j w, (E' j).symm w = divisionMap (g j) (bc' j) w)281    (ρ : 𝒱 ≃ₗ[𝒪] (∀ j, Fin (mc j).toMeasured.s.degree → (mc j).toMeasured.O))282    (hρ : Measurable ρ) (bc : Fin 𝔫 → 𝒞)283    (hcompat : ∀ (w : 𝒱) (j : 𝒥), coordinateLift bc w j = coordinateLift (bc' j) (ρ w j))284    (a : ℕ) (ha : a = s * 𝔫 - tri 𝔡 + 1) :285    letI : Module 𝒪 𝒞 := Algebra.toModule286    ∀ (E : 𝒞 ≃ₗ[𝒪] (𝒱 × 𝒞)), (∀ w, E.symm w = divisionMap g bc w) →287      ∀ (G : ∀ j, Set (Ideal (mc j).toMeasured.R)), (∀ j, MeasurableSet (G j)) →288      MeasurableSet (Set.range (childCoordinateMap ϖ a bc E289        (pulledVariation (AlgHom.pi alpha) cc b))) ∧290      MeasurableSet (coordinateIdeal ϖ f b ⁻¹' (cellStrict ⁻¹' Set.pi Set.univ G) ∩291        centerBox (s + a - 1)) ∧292      cellStrict '' (coordinateIdeal ϖ f b '' centerBox (s + a - 1)) =293        (fun (w : 𝒱) (j : 𝒥) => coordinateIdeal (mc j).toMeasured.S.pi (g j) (bc' j) (ρ w j)) ''294          Set.range (childCoordinateMap ϖ a bc E (pulledVariation (AlgHom.pi alpha) cc b)) ∧295      coefficientMeasure 𝒪 𝔫296        (coordinateIdeal ϖ f b ⁻¹' (cellStrict ⁻¹' Set.pi Set.univ G) ∩ centerBox (s + a - 1)) =297        𝐪⁻¹ ^ tri 𝔡 * coefficientMeasure 𝒪 𝔫298          ((fun (w : 𝒱) (j : 𝒥) => coordinateIdeal (mc j).toMeasured.S.pi (g j) (bc' j) (ρ w j))299            ⁻¹' Set.pi Set.univ G ∩300            Set.range (childCoordinateMap ϖ a bc E (pulledVariation (AlgHom.pi alpha) cc b))) := by301  -- the strict transform intertwines the parent chart on the center box with the child charts302  -- along the child coordinate map; transport measurability and measure along this square303  intro E hE G hG304  set Φ := fun (J : Ideal ℛ) (j : 𝒥) => strictTransformIdeal (alpha j) (e j) 𝔡 J305  set Ψ := fun (w : 𝒱) (j : 𝒥) => coordinateIdeal (mc j).toMeasured.S.pi (g j) (bc' j) (ρ w j)306  set ch := childCoordinateMap ϖ a bc E (pulledVariation (AlgHom.pi alpha) cc b)307  set sc := coordinateScale (n := 𝔫) ϖ (s + a - 1)308  have hpiIrr : Irreducible ϖ := m.toMeasured.S.pi_irreducible309  have hf' : AlgHom.pi alpha f = e ^ 𝔡 * g := by310    funext j; simp [AlgHom.pi_apply, hg j]311  obtain ⟨hjac, heC⟩ := member_children_jacobson_regular m c mc hpiO e he312  -- completeness of the coordinate modules313  have hOc : IsAdicComplete (Ideal.span {ϖ}) 𝒪 := dvr_isAdicComplete_span_uniformizer _ _ hpiIrr314  have hOn : IsAdicComplete (Ideal.span {ϖ}) 𝒱 := finite_free_adic_complete _ _ _315  have hC := member_children_isAdicComplete m c mc hpiO316  have hprod : IsAdicComplete (Ideal.span {ϖ}) (𝒱 × 𝒞) := isAdicComplete_prod _ _ _ _317  -- product chart and linear part318  obtain ⟨hproj, -, hinjP⟩ := product_chart_projection 𝒪 𝒥 (fun j => (mc j).toMeasured.O)319    (fun j => (mc j).toMeasured.R) (fun j => (mc j).toMeasured.s.degree) _ ρ bc' bc hcompat g _ _320    hpiO321  have hΨ : Function.Injective (coordinateIdeal ϖ g bc) := hinjP fun j =>322    (concrete_member_division_chart_measure (mc j) (g j) (hgj j) (bc' j) (E' j) (hE' j)).1323  obtain ⟨Q, hQ, hD, hkl⟩ := member_center_linear_part m c mc hcard alpha e he hbij hindex hsum324    s hs cc hcc f b E₀ hE₀ hf g hg bc E hE325  have htri : tri 𝔡 ≤ s * 𝔫 :=326    le_trans hs (Nat.le_mul_of_pos_right s (concrete_member_one_le_degree m))327  obtain ⟨hgen, hHaar, hProb, hfinite, hcontall⟩ :=328    coefficient_space_strict_instances 𝒪 m.toMeasured.htop ϖ hpiIrr 𝔫329  have hk : s * 𝔫 - tri 𝔡 < a := by omega330  have hΨm : Measurable Ψ := child_chart_map_measurable m c mc g hgj bc' E' hE' ρ hρ331  set T := Ψ ⁻¹' Set.pi Set.univ G332  have hT : MeasurableSet T := hΨm (MeasurableSet.univ_pi hG)333  -- the strict transform commutes with the coordinate charts334  have hcomm : ∀ z, strictTransformIdeal (AlgHom.pi alpha) e 𝔡 (coordinateIdeal ϖ f b (sc z)) =335      coordinateIdeal ϖ g bc (ch z) :=336    strict_chart_coordinates_commute _ _ _ _ _ s a _ _ f g e cc b hf' hcc heC (by omega) hjac bc E337      hE338  have hcommC : ∀ z, Φ (coordinateIdeal ϖ f b (sc z)) = Ψ (ch z) := fun z => by339    funext j; simp only [Φ, Ψ]340    rw [← (pi_strict_transform_map_eval _ _ _ _ alpha e g _ _).2.2.2 j, hcomm z, hproj]341  have hL : coordinateIdeal ϖ f b ⁻¹' (Φ ⁻¹' Set.pi Set.univ G) ∩ Set.range sc =342      sc '' (ch ⁻¹' T) := by343    ext x; constructor344    · rintro ⟨hx, z, rfl⟩; exact ⟨z, (hcommC z ▸ hx : Ψ (ch z) ∈ Set.pi Set.univ G), rfl⟩345    · rintro ⟨z, hz, rfl⟩; exact ⟨(hcommC z ▸ hz : Φ _ ∈ Set.pi Set.univ G), z, rfl⟩346  obtain ⟨hrangeM, hpreM⟩ := member_childCoordinateMap_measurable m a bc E347    (pulledVariation (AlgHom.pi alpha) cc b) _ hk Q hQ348  have himgS : strictTransformIdeal (AlgHom.pi alpha) e 𝔡 '' (coordinateIdeal ϖ f b '' Set.range sc)349      = coordinateIdeal ϖ g bc '' Set.range ch := by350    rw [Set.image_image, ← Set.range_comp, ← Set.range_comp]351    exact congrArg Set.range (funext hcomm)352  refine ⟨hrangeM, ?_, ?_, ?_⟩353  · rw [hL]354    exact measurableSet_coordinateScale_image _ hgen (smul_right_injective _ hpiIrr.ne_zero) _ _355      (hpreM T hT)356  · rw [Set.image_image, ← Set.range_comp, ← Set.range_comp]357    exact congrArg Set.range (funext hcommC)358  · rw [hL, ← strict_chart_preimage_set_identity _ _ _ _ _ s a _ _ f g e cc b hf' hcc heC359      (by omega) hjac bc E hE hΨ T, strict_transform_translate_measure _ _ _ _ _ s a _ _ f g e cc b360      hf' hcc heC (by omega) hjac bc E hE hΨ _ hk Q hQ hD hpiIrr hkl hgen _ hfinite (hcontall a _)361      (fun k S _ => coordinate_scale_measure _ m.toMeasured.htop _ hpiIrr _ k S) htri rfl T hT,362      himgS, ← Set.image_inter hΨ, Set.preimage_image_eq _ hΨ]363 364include pc hpc hpc' hdeg hstrict in365/-- The coefficient measure of the center box of parent coordinates whose strict transforms lie in366  `Π G_j` is `q^(-tri(cellDegree)) q^(deg)` times the product child measure of the part of `Π G_j`367  reached from the center box. -/368private theorem member_center_box_measure369    (s : ℕ) (hs : tri 𝔡 ≤ s) (cc : 𝒞) (hcc : (algebraMap 𝒪 𝒞 ϖ) ^ s = e ^ 𝔡 * cc)370    (f : ℛ) (b : Fin 𝔫 → ℛ) (E₀ : ℛ ≃ₗ[𝒪] (𝒱 × ℛ)) (hE₀ : ∀ w, E₀.symm w = divisionMap f b w)371    (hf : Ideal.span {f} ∈ m.toMeasured.cell c) (a : ℕ) (ha : a = s * 𝔫 - tri 𝔡 + 1)372    (G : ∀ j, Set (Ideal (mc j).toMeasured.R)) (hG : ∀ j, MeasurableSet (G j)) :373    MeasurableSet (coordinateIdeal ϖ f b ⁻¹' (cellStrict ⁻¹' Set.pi Set.univ G) ∩374      centerBox (s + a - 1)) ∧375    MeasurableSet (cellStrict '' (coordinateIdeal ϖ f b '' centerBox (s + a - 1))) ∧376    coefficientMeasure 𝒪 𝔫377      (coordinateIdeal ϖ f b ⁻¹' (cellStrict ⁻¹' Set.pi Set.univ G) ∩ centerBox (s + a - 1)) =378      𝐪⁻¹ ^ tri 𝔡 * 𝐪 ^ 𝔫 * Measure.pi (fun j => (mc j).toMeasured.μ)379        (Set.pi Set.univ G ∩ cellStrict '' (coordinateIdeal ϖ f b '' centerBox (s + a - 1))) := by380  obtain ⟨g, hg⟩ := hstrict f hf381  have hgj : ∀ j, Ideal.span {g j} ∈ (mc j).toMeasured.stateSet := fun j => by382    simpa [strict_transform_ideal_of_generator _ _ _ (alpha j) (e j) (g j) _ f (hg j)383      (concrete_member_mul_t_injective (he j))] using hbij.mapsTo hf j (Set.mem_univ _)384  choose bc' E' hE' using fun j => concrete_member_state_generator_division (mc j) (g j) (hgj j)385  obtain ⟨ρ, bc, hρ, hρ', hcompat⟩ := product_coordinates_exist 𝒪 𝒥 (fun j => (mc j).toMeasured.O)386    (fun j => (mc j).toMeasured.R) (m.toMeasured.childDelta c) (fun j => (mc j).toMeasured.s.degree)387    pc hpc hpc' 𝔫 hdeg bc'388  obtain ⟨E, hE⟩ := product_division_equiv 𝒪 𝒥 (fun j => (mc j).toMeasured.O)389    (fun j => (mc j).toMeasured.R) (fun j => (mc j).toMeasured.s.degree) 𝔫 ρ bc' bc hcompat g E' hE'390  obtain ⟨h1, h2, h3, h4⟩ := member_center_translate_measure_data m c mc hcard hpiO alpha e he391    hbij hindex hsum s hs cc hcc f b E₀ hE₀ hf g hg hgj bc' E' hE' ρ hρ bc hcompat a ha E hE G hG392  obtain ⟨hemb, hpush⟩ := member_product_chart_pushforward 𝒥 mc g hgj bc' E' hE'393  set T := Set.range (childCoordinateMap ϖ a bc E (pulledVariation (AlgHom.pi alpha) cc b))394  set Ψ := fun (w : ∀ j, Fin (mc j).toMeasured.s.degree → (mc j).toMeasured.O) (j : 𝒥) =>395    coordinateIdeal (mc j).toMeasured.S.pi (g j) (bc' j) (w j)396  have hρT : MeasurableSet (ρ '' T) := by397    rw [LinearEquiv.image_eq_preimage_symm]; exact hρ' h1398  have himg : (fun (w : 𝒱) (j : 𝒥) => coordinateIdeal (mc j).toMeasured.S.pi (g j) (bc' j)399      (ρ w j)) '' T = Ψ '' (ρ '' T) := by400    rw [Set.image_image]401  refine ⟨h2, ?_, ?_⟩402  · rw [h3, himg]; exact hemb.measurableSet_image' hρT403  · rw [h4, h3, himg]404    set Y := ρ '' T ∩ Ψ ⁻¹' Set.pi Set.univ G405    have hYm : MeasurableSet Y := hρT.inter (hemb.measurable (MeasurableSet.univ_pi hG))406    have hpre : (fun (w : 𝒱) (j : 𝒥) => coordinateIdeal (mc j).toMeasured.S.pi (g j) (bc' j)407        (ρ w j)) ⁻¹' Set.pi Set.univ G ∩ T = ρ ⁻¹' Y := by408      rw [Set.preimage_inter, Set.preimage_image_eq _ ρ.injective, Set.inter_comm]; rfl409    have hC : (∏ j, ((mc j).toMeasured.q : ℝ≥0∞)⁻¹ ^ (mc j).toMeasured.s.degree) = 𝐪⁻¹ ^ 𝔫 := by410      simp_rw [hcard, Nat.cast_pow, ENNReal.inv_pow, ← pow_mul]411      rw [Finset.prod_pow_eq_pow_sum, hdeg]412    rw [hpre, ← Measure.map_apply hρ hYm,413      member_coefficient_measure_map_product_coordinates m c mc ρ hρ,414      ← Set.inter_comm, ← Set.image_inter_preimage, hpush Y hYm, hC, mul_assoc,415      ← mul_assoc (𝐪 ^ _), concreteMember_q_pow_mul_inv_pow, one_mul]416 417open scoped Classical in418include pc hpc hpc' hdeg hstrict in419/-- In the chart `i` of a cell, given coset representatives `reps` of level `s + a - 1`, the chart420  preimage of the box `{J ∈ cell : cellStrict J ∈ Π G_j}` is measurable, and its measure is421  `q^(-tri(cellDegree)) q^deg` times the sum, over the representatives landing in the cell, of the422  child measures of the images of the corresponding cosets. -/423private theorem member_cell_chart_box (s : ℕ) (hs : tri 𝔡 ≤ s) (cc : 𝒞)424    (hcc : (algebraMap 𝒪 𝒞 ϖ) ^ s = e ^ 𝔡 * cc) (a : ℕ) (ha : a = s * 𝔫 - tri 𝔡 + 1)425    (reps : Finset 𝒱) (hrdisj : (reps : Set 𝒱).PairwiseDisjoint (coordinateCoset ϖ (s + a - 1)))426    (i : m.atlas.ι)427    (hdec : memberChart m i ⁻¹' m.toMeasured.cell c =428      ⋃ z₀ ∈ reps.filter (fun z₀ => memberChart m i z₀ ∈ m.toMeasured.cell c),429        coordinateCoset ϖ (s + a - 1) z₀)430    (G : ∀ j, Set (Ideal (mc j).toMeasured.R)) (hG : ∀ j, MeasurableSet (G j)) :431    MeasurableSet (memberChart m i ⁻¹' (m.toMeasured.cell c ∩ cellStrict ⁻¹' Set.pi Set.univ G)) ∧432    coefficientMeasure 𝒪 𝔫433        (memberChart m i ⁻¹' (m.toMeasured.cell c ∩ cellStrict ⁻¹' Set.pi Set.univ G)) =434      𝐪⁻¹ ^ tri 𝔡 * 𝐪 ^ 𝔫 *435        ∑ z₀ ∈ reps.filter (fun z₀ => memberChart m i z₀ ∈ m.toMeasured.cell c),436        Measure.pi (fun j => (mc j).toMeasured.μ) (Set.pi Set.univ G ∩437          cellStrict '' (memberChart m i '' coordinateCoset ϖ (s + a - 1) z₀)) ∧438    ∀ z₀ ∈ reps.filter (fun z₀ => memberChart m i z₀ ∈ m.toMeasured.cell c),439      MeasurableSet (cellStrict '' (memberChart m i '' coordinateCoset ϖ (s + a - 1) z₀)) := by440  set Φ := fun (J : Ideal ℛ) (j : 𝒥) => strictTransformIdeal (alpha j) (e j) 𝔡 J441  have := concrete_member_division_module_isAdicComplete m442  -- `Φi` is the chart, `F` the representatives of the cell in it, and `Φp z₀` the chart recentred443  -- at `z₀`; the chart preimage of the box is the union of the translated center boxes `A z₀`444  let fi : ℛ := (m.atlas.chart i).f445  let bi : Fin 𝔫 → ℛ := (m.atlas.chart i).b446  set Φi := memberChart m i447  set F := reps.filter (fun z₀ => Φi z₀ ∈ m.toMeasured.cell c)448  let Φp (z₀ : 𝒱) : 𝒱 → Ideal ℛ := coordinateIdeal ϖ (fi + ϖ • coordinateLift bi z₀) bi449  have Tr := fun z₀ => member_chart_translate m fi bi (s + a - 1) z₀450  set Y := Set.pi Set.univ G451  set Rg := Set.range (coordinateScale (n := 𝔫) ϖ (s + a - 1))452  let A (z₀ : 𝒱) : Set 𝒱 := (fun z => z₀ + z) '' (Φp z₀ ⁻¹' (Φ ⁻¹' Y) ∩ Rg)453  -- the center box measure applies at every representative454  have hC : ∀ z₀ ∈ F, MeasurableSet (Φp z₀ ⁻¹' (Φ ⁻¹' Y) ∩ Rg) ∧455      MeasurableSet (Φ '' (Φp z₀ '' Rg)) ∧456      coefficientMeasure 𝒪 𝔫 (Φp z₀ ⁻¹' (Φ ⁻¹' Y) ∩ Rg) =457        𝐪⁻¹ ^ tri 𝔡 * 𝐪 ^ 𝔫 *458          Measure.pi (fun j => (mc j).toMeasured.μ) (Y ∩ Φ '' (Φp z₀ '' Rg)) := by459    intro z₀ hz₀460    have hf : Ideal.span {fi + ϖ • coordinateLift bi z₀} ∈ m.toMeasured.cell c := by461      have h0 := (Tr z₀).1 0462      rw [add_zero] at h0463      have : coordinateIdeal ϖ fi bi z₀ = Ideal.span {fi + ϖ • coordinateLift bi z₀} := by464        rw [h0]465        simp [coordinateIdeal, normalizedIdeal, normalizedGenerator, coordinateLift]466      rw [← this]; exact (Finset.mem_filter.mp hz₀).2467    obtain ⟨E₀, hE₀⟩ := @division_data_vertical_perturbation 𝒪 ℛ _ _ _ 𝔫 ϖ fi bi468      (m.atlas.chart i).E (m.atlas.chart i).division this (coordinateLift bi z₀)469    exact member_center_box_measure m c mc pc hpc hpc' hcard hpiO hdeg alpha e he hbij470      hstrict hindex hsum s hs cc hcc _ bi E₀ hE₀ hf a ha G hG471  have hPeq (z₀) : Φp z₀ '' Rg = Φi '' coordinateCoset ϖ (s + a - 1) z₀ := by472    rw [(Tr z₀).2.1, Set.image_image]473    exact congrArg (· '' Rg) (funext fun w => ((Tr z₀).1 w).symm)474  have hXi : Φi ⁻¹' (m.toMeasured.cell c ∩ Φ ⁻¹' Y) = ⋃ z₀ ∈ F, A z₀ :=475    preimage_inter_eq_biUnion_translate Φi Φp _ _ Rg F _ (fun z₀ => (Tr z₀).1)476      (fun z₀ => (Tr z₀).2.1) hdec477  have hAdisj : (F : Set _).PairwiseDisjoint A := by478    intro z₀ hz z₀' hz' hne479    have hsub : ∀ z₁, A z₁ ⊆ coordinateCoset ϖ (s + a - 1) z₁ := fun z₁ => by480      rw [(Tr z₁).2.1]; exact Set.image_mono Set.inter_subset_right481    exact (hrdisj (Finset.mem_filter.mp hz).1 (Finset.mem_filter.mp hz').1 hne).mono (hsub z₀)482      (hsub z₀')483  have hAmeas : ∀ z₀ ∈ F, MeasurableSet (A z₀) := fun z₀ hz => ((Tr z₀).2.2 _).2 (hC z₀ hz).1484  refine ⟨?_, ?_, fun z₀ hz => hPeq z₀ ▸ (hC z₀ hz).2.1⟩485  · rw [hXi]; exact Finset.measurableSet_biUnion _ hAmeas486  · rw [hXi, measure_biUnion_finset hAdisj hAmeas, Finset.mul_sum]487    refine Finset.sum_congr rfl fun z₀ hz => ?_488    rw [← hPeq]489    exact ((Tr z₀).2.2 _).1.trans (hC z₀ hz).2.2490 491include pc hpc hpc' hdeg hvert hstrict in492/-- The set of ideals in a cell whose strict transforms lie in a measurable box `Π G_j` is493  measurable. -/494theorem member_cell_box_measurable :Theorem 5.1495    (letI : ∀ j, MeasurableSpace (Ideal (mc j).toMeasured.R) :=496      fun j => (mc j).toMeasured.measurableSpaceIdeal;497      letI : MeasurableSpace (Ideal ℛ) := m.toMeasured.measurableSpaceIdeal;498      ∀ (G : ∀ j, Set (Ideal (mc j).toMeasured.R)), (∀ j, MeasurableSet (G j)) →499      MeasurableSet (m.toMeasured.cell c ∩ (fun (J : Ideal ℛ) (j : 𝒥) =>500        strictTransformIdeal (alpha j) (e j) 𝔡 J) ⁻¹' Set.pi Set.univ G)) := by501  intro G hG502  classical503  obtain ⟨s, cc, hs, hcc⟩ := common_vertical_exponent 𝒪 𝒥 (fun j => (mc j).toMeasured.R) ϖ e 𝔡504    hvert (tri 𝔡)505  set a := s * 𝔫 - tri 𝔡 + 1 with ha506  have htri := tri_chooseTwo 𝔡507  obtain ⟨reps, -, -, hrdisj, hdec⟩ :=508    member_cell_chart_coset_decomposition m c (s + a - 1) (by omega)509  set X := m.toMeasured.cell c ∩ cellStrict ⁻¹' Set.pi Set.univ G510  -- `X` is the union of the images of its chart preimages, which are measurable511  have hX : X = ⋃ i, memberChart m i '' (memberChart m i ⁻¹' X) := by512    ext J513    simp only [Set.mem_iUnion, Set.image_preimage_eq_inter_range, Set.mem_inter_iff]514    constructor515    · intro h; obtain ⟨i, hi⟩ := member_cell_mem_chart_range m c J h.1; exact ⟨i, h, hi⟩516    · rintro ⟨-, h, -⟩; exact h517  rw [hX]518  exact MeasurableSet.iUnion fun i => chart_image_measurable_chart_sigma _ _ _ _ _ _519    (m.atlas.chart i).isDivisionChart _520    (member_cell_chart_box m c mc pc hpc hpc' hcard hpiO hdeg alpha e he hbij hstrict hindex hsum521      s hs cc hcc a ha reps hrdisj i (hdec i) G hG).1522 523include pc hpc hpc' hdeg hvert hstrict in524/-- The measure of the set of ideals in a cell whose strict transforms lie in a box `Π G_j` is525  `q^(-tri(cellDegree))` times the product of the child state measures of the `G_j`. -/526theorem member_cell_box_measure :(1.7)Theorem 5.1Proposition 6.1527    (letI : ∀ j, MeasurableSpace (Ideal (mc j).toMeasured.R) :=528      fun j => (mc j).toMeasured.measurableSpaceIdeal;529      letI : MeasurableSpace (Ideal ℛ) := m.toMeasured.measurableSpaceIdeal;530      ∀ (G : ∀ j, Set (Ideal (mc j).toMeasured.R)), (∀ j, MeasurableSet (G j)) →531      m.toMeasured.μ (m.toMeasured.cell c ∩ (fun (J : Ideal ℛ) (j : 𝒥) =>532        strictTransformIdeal (alpha j) (e j) 𝔡 J) ⁻¹' Set.pi Set.univ G) =533      𝐪⁻¹ ^ tri 𝔡 * ∏ j, (mc j).toMeasured.μ (G j)) := by534  -- sum the chart computations of `member_cell_chart_box` over the charts; the images of the535  -- cosets in the cell partition the cell, hence their strict transforms partition `Π stateSet_j`536  intro G hG537  classical538  obtain ⟨s, cc, hs, hcc⟩ := common_vertical_exponent 𝒪 𝒥 (fun j => (mc j).toMeasured.R) ϖ e _539    hvert (tri 𝔡)540  set a := s * 𝔫 - tri 𝔡 + 1 with ha541  have htri := tri_chooseTwo 𝔡542  obtain ⟨reps, -, -, hrdisj, hdec⟩ :=543    member_cell_chart_coset_decomposition m c (s + a - 1) (by omega)544  have hbox := fun i => member_cell_chart_box m c mc pc hpc hpc' hcard hpiO hdeg alpha e he hbij545    hstrict hindex hsum s hs cc hcc a ha reps hrdisj i (hdec i) G hG546  -- `F i` are the representatives of the cell in chart `i`, `P ⟨i, z₀⟩` the image of a coset547  let F (i : m.atlas.ι) := reps.filter (fun z₀ => memberChart m i z₀ ∈ m.toMeasured.cell c)548  let P (p : Σ _ : m.atlas.ι, 𝒱) := memberChart m p.1 '' coordinateCoset ϖ (s + a - 1) p.2549  have hdec' (i) : memberChart m i ⁻¹' m.toMeasured.cell c =550      ⋃ z₀ ∈ F i, coordinateCoset ϖ (s + a - 1) z₀ := hdec i551  have hPcell : ∀ p ∈ Finset.univ.sigma F, P p ⊆ m.toMeasured.cell c := by552    rintro ⟨i, z₀⟩ hp J ⟨z, hz, rfl⟩553    have : z ∈ memberChart m i ⁻¹' m.toMeasured.cell c := by554      rw [hdec']; exact Set.mem_biUnion (Finset.mem_sigma.mp hp).2 hz555    exact this556  have hPunion : m.toMeasured.cell c ⊆ ⋃ p ∈ Finset.univ.sigma F, P p := by557    intro J hJc558    obtain ⟨i, z, rfl⟩ := member_cell_mem_chart_range m c J hJc559    have hz : z ∈ memberChart m i ⁻¹' m.toMeasured.cell c := hJc560    rw [hdec'] at hz561    obtain ⟨z₀, hz₀, hzc⟩ := Set.mem_iUnion₂.mp hz562    exact Set.mem_iUnion₂.mpr ⟨⟨i, z₀⟩, Finset.mem_sigma.mpr ⟨Finset.mem_univ _, hz₀⟩, z, hzc, rfl⟩563  have hPdisj : ((Finset.univ.sigma F : Finset _) : Set _).PairwiseDisjoint P := by564    rintro ⟨i, z₀⟩ hp ⟨i', z₀'⟩ hp' hne565    have hz := (Finset.mem_sigma.mp hp).2566    have hz' := (Finset.mem_sigma.mp hp').2567    by_cases hii : i = i'568    · subst hii569      have hne' : z₀ ≠ z₀' := fun h => hne (h ▸ rfl)570      exact (Set.disjoint_image_iff (concrete_member_charts m i).1).mpr571        (hrdisj (Finset.mem_filter.mp hz).1 (Finset.mem_filter.mp hz').1 hne')572    · have h := m.atlas.disjoint hii573      simp only at h574      rw [← (concrete_member_charts m i).2.1, ← (concrete_member_charts m i').2.1] at h575      exact h.mono (Set.image_subset_range _ _) (Set.image_subset_range _ _)576  have : ∀ j, IsFiniteMeasure (mc j).toMeasured.μ := fun j =>577    (concrete_member_measure_finite_support (mc j)).1578  have hparts := sum_measure_inter_image_of_partition (Measure.pi fun j => (mc j).toMeasured.μ)579    hbij _ P hPcell hPunion hPdisj (Set.pi Set.univ G) fun p hp => (MeasurableSet.univ_pi hG).inter580      ((hbox p.1).2.2 p.2 (Finset.mem_sigma.mp hp).2)581  rw [Finset.sum_sigma, ← Set.pi_inter_distrib, Measure.pi_pi] at hparts582  -- the state measure is `q^(-deg)` times the sum of the chart measures583  rw [MeasuredSurface.μ, stateMeasure, Measure.smul_apply, Measure.finsetSum_apply, smul_eq_mul]584  have hmeas := member_cell_box_measurable m c mc pc hpc hpc' hcard hpiO hdeg alpha e he hvert hbij585    hstrict hindex hsum G hG586  calc _ = 𝐪⁻¹ ^ 𝔫 * ∑ i, 𝐪⁻¹ ^ tri 𝔡 * 𝐪 ^ 𝔫 *587        ∑ z₀ ∈ F i, Measure.pi (fun j => (mc j).toMeasured.μ)588          (Set.pi Set.univ G ∩ cellStrict '' P ⟨i, z₀⟩) := by589        congr 1590        refine Finset.sum_congr rfl fun i _ => ?_591        rw [chartMeasure]592        exact (Measure.map_apply (concrete_member_charts m i).2.2 hmeas).trans (hbox i).2.1593    _ = (𝐪 ^ 𝔫 * 𝐪⁻¹ ^ 𝔫) * (𝐪⁻¹ ^ tri 𝔡 * ∏ j, (mc j).toMeasured.μ (G j)) := by594        rw [← Finset.mul_sum, hparts, Finset.prod_congr rfl fun j _ =>595          ((concrete_member_measure_finite_support (mc j)).2 (G j)).symm]596        ring597    _ = _ := by rw [concreteMember_q_pow_mul_inv_pow, one_mul]598 599end CellBoxes600 601end SurfaceBlowup