Clean up immediately upstreamable prerequisites

PFR.lean

@@ -31,13 +31,18 @@ import PFR.HundredPercent
 import PFR.ImprovedPFR
 import PFR.Kullback
 import PFR.Main
+import PFR.Mathlib.Algebra.AddTorsor
 import PFR.Mathlib.Algebra.Group.Pointwise.Set.Basic
+import PFR.Mathlib.Algebra.Group.Prod
+import PFR.Mathlib.Algebra.Module.ZMod
 import PFR.Mathlib.Analysis.SpecialFunctions.NegMulLog
-import PFR.Mathlib.Data.Set.Pointwise.Finite
 import PFR.Mathlib.Data.Set.Pointwise.SMul
+import PFR.Mathlib.GroupTheory.PGroup
+import PFR.Mathlib.LinearAlgebra.AffineSpace.AffineSubspace
 import PFR.Mathlib.LinearAlgebra.Basis.VectorSpace
+import PFR.Mathlib.LinearAlgebra.Dimension.Finrank
 import PFR.Mathlib.MeasureTheory.Constructions.Pi
-import PFR.Mathlib.MeasureTheory.Integral.Bochner
+import PFR.Mathlib.MeasureTheory.Integral.IntegrableOn
 import PFR.Mathlib.MeasureTheory.Integral.Lebesgue
 import PFR.Mathlib.MeasureTheory.Integral.SetIntegral
 import PFR.Mathlib.MeasureTheory.Measure.NullMeasurable

PFR/ApproxHomPFR.lean

@@ -2,7 +2,7 @@ import Mathlib.Combinatorics.Additive.Energy
 import Mathlib.Analysis.Normed.Lp.PiLp
 import Mathlib.Analysis.InnerProductSpace.PiL2
 import LeanAPAP.Extras.BSG
-import PFR.Mathlib.Data.Set.Pointwise.Finite
+import PFR.Mathlib.Algebra.Group.Prod
 import PFR.HomPFR
 
 /-!
@@ -31,37 +31,31 @@ $|G|^2 / K$ pairs $(x,y) \in G^2$ such that $$ f(x+y) = f(x) + f(y).$$
 Then there exists a homomorphism $\phi : G \to G'$ and a constant $c \in G'$ such that
 $f(x) = \phi(x)+c$ for at least $|G| / (2 ^ {172} * K ^ {146})$ values of $x \in G$. -/
 theorem approx_hom_pfr (f : G → G') (K : ℝ) (hK : K > 0)
-    (hf : Nat.card {x : G × G | f (x.1 + x.2) = f x.1 + f x.2} ≥ Nat.card G ^ 2 / K) :
+    (hf : Nat.card G ^ 2 / K ≤ Nat.card {x : G × G | f (x.1 + x.2) = f x.1 + f x.2}) :
     ∃ (φ : G →+ G') (c : G'), Nat.card {x | f x = φ x + c} ≥ Nat.card G / (2 ^ 172 * K ^ 146) := by
   let A := (Set.univ.graphOn f).toFinite.toFinset
-
-  have h_cs : ((A ×ˢ A).filter (fun (a, a') ↦ a + a' ∈ A) |>.card : ℝ) ^ 2 ≤
-      Finset.card A * E[A] := by
-    norm_cast
-    convert card_sq_le_card_mul_addEnergy A A A
-  rewrite [← Nat.card_eq_finsetCard, ← Nat.card_eq_finsetCard,
-    Nat.card_congr (Set.equivFilterGraph f)] at h_cs
-
-  have hA : Nat.card A = Nat.card G := by
-    rw [← Nat.card_univ (α := G), ← Set.card_graphOn _ f, Nat.card_eq_finsetCard,
-      Set.Finite.card_toFinset]
-    simp
-  have hA_pos : 0 < (Nat.card A : ℝ) := Nat.cast_pos.mpr <| Nat.card_pos.trans_eq hA.symm
-  have : (Nat.card G ^2 / K)^2 ≤ Nat.card A * E[A] := LE.le.trans (by gcongr) h_cs
-  rewrite [← hA] at this
-  replace : E[A] ≥ (Finset.card A)^3 / K^2 := calc
-    _ ≥ (Nat.card A ^ 2 / K)^2 / Nat.card A := (div_le_iff₀' <| hA_pos).mpr this
-    _ = (Nat.card A ^ 4 / Nat.card A) / K^2 := by ring
-    _ = A.card ^ 3 / K ^ 2 := by
-      rw [pow_succ, mul_div_assoc, div_self (ne_of_gt hA_pos), mul_one,
-        Nat.card_eq_finsetCard]
+  have hA : #A = Nat.card G := by rw [Set.Finite.card_toFinset]; simp [← Nat.card_eq_fintype_card]
   have hA_nonempty : A.Nonempty := by simp [-Set.Finite.toFinset_setOf, A]
+  have hA_pos : 0 < #A := by positivity
+  have := calc
+    (#A ^ 3 / K ^ 2 : ℝ)
+      = (Nat.card G ^ 2 / K) ^ 2 / #A := by field_simp [hA]; ring
+    _ ≤ Nat.card {x : G × G | f (x.1 + x.2) = f x.1 + f x.2} ^ 2 / #A := by gcongr
+    _ = #{ab ∈ A ×ˢ A | ab.1 + ab.2 ∈ A} ^ 2 / #A := by
+      congr
+      rw [← Nat.card_eq_finsetCard, ← Finset.coe_sort_coe, Finset.coe_filter,
+        Set.Finite.toFinset_prod]
+      simp only [Set.Finite.mem_toFinset, A]
+      rw [Nat.card_congr (addMemGraphEquiv ..)]
+      simp
+    _ ≤ #A * E[A] / #A := by gcongr; exact mod_cast card_sq_le_card_mul_addEnergy ..
+    _ = E[A] := by field_simp
   obtain ⟨A', hA', hA'1, hA'2⟩ :=
     BSG_self' (sq_nonneg K) hA_nonempty (by simpa only [inv_mul_eq_div] using this)
-  clear h_cs hf this
+  clear hf this
   have hA'₀ : A'.Nonempty := Finset.card_pos.1 $ Nat.cast_pos.1 $ hA'1.trans_lt' $ by positivity
   let A'' := A'.toSet
-  have hA''_coe : Nat.card A'' = Finset.card A' := Nat.card_eq_finsetCard A'
+  have hA''_coe : Nat.card A'' = #A' := Nat.card_eq_finsetCard A'
   have hA''_pos : 0 < Nat.card A'' := by rw [hA''_coe]; exact hA'₀.card_pos
   have hA''_nonempty : Set.Nonempty A'' := nonempty_subtype.mp (Finite.card_pos_iff.mp hA''_pos)
   have : Finset.card (A' - A') = Nat.card (A'' + A'') := calc
@@ -146,7 +140,7 @@ theorem approx_hom_pfr (f : G → G') (K : ℝ) (hK : K > 0)
     · obtain ⟨ch, hch⟩ := Finset.mem_biUnion.mp hx
       exact ((Set.Finite.mem_toFinset _).mp hch.2).1
 
-  replace : ∑ __ in cH₁, ((2 ^ 4)⁻¹ * (K ^ 2)⁻¹ * A.card / cH₁.card : ℝ) ≤
+  replace : ∑ __ in cH₁, ((2 ^ 4)⁻¹ * (K ^ 2)⁻¹ * #A / cH₁.card : ℝ) ≤
       ∑ ch in cH₁, ((translate ch.1 ch.2).toFinite.toFinset.card : ℝ) := by
     rewrite [Finset.sum_const, nsmul_eq_mul, ← mul_div_assoc, mul_div_right_comm, div_self, one_mul]
     · apply hA'1.trans
@@ -155,7 +149,7 @@ theorem approx_hom_pfr (f : G → G') (K : ℝ) (hK : K > 0)
     · symm
       refine ne_of_lt <| Nat.cast_zero.symm.trans_lt <| Nat.cast_lt.mpr <| Finset.card_pos.mpr ?_
       exact (Set.Finite.toFinset_nonempty _).mpr h_nonempty
-  replace : ∃ c' : G × G', ∃ h : G', (2 ^ 4 : ℝ)⁻¹ * (K ^ 2)⁻¹ * A.card / cH₁.card ≤
+  replace : ∃ c' : G × G', ∃ h : G', (2 ^ 4 : ℝ)⁻¹ * (K ^ 2)⁻¹ * #A / cH₁.card ≤
       Nat.card { x : G | f x = φ x + (-φ c'.1 + c'.2 + h) } := by
     obtain ⟨ch, hch⟩ :=
       Finset.exists_le_of_sum_le ((Set.Finite.toFinset_nonempty _).mpr h_nonempty) this
@@ -168,12 +162,10 @@ theorem approx_hom_pfr (f : G → G') (K : ℝ) (hK : K > 0)
   use φ, -φ c'.1 + c'.2 + h
   refine le_trans ?_ hch
   unfold_let cH₁
-  rewrite [← Nat.card_eq_finsetCard, hA, ← mul_inv, inv_mul_eq_div, div_div]
+  rewrite [hA, ← mul_inv, inv_mul_eq_div, div_div]
   apply div_le_div (Nat.cast_nonneg _) le_rfl
   · apply mul_pos
-    · apply mul_pos
-      · norm_num
-      · exact sq_pos_of_pos hK
+    · positivity
     · rewrite [Nat.cast_pos, Finset.card_pos, Set.Finite.toFinset_nonempty _]
       exact h_nonempty
   rw [show 146 = 2 + 144 by norm_num, show 172 = 4 + 168 by norm_num, pow_add, pow_add,

PFR/Endgame.lean

@@ -393,7 +393,7 @@ lemma construct_good_prelim :
       simp only [integral_sub .of_finite .of_finite, integral_const, measure_univ,
         ENNReal.one_toReal, smul_eq_mul, one_mul, sub_left_inj, sum2]
       simp_rw [condRuzsaDist'_eq_sum hT₁ hT₃,
-        integral_eq_setIntegral (FiniteRange.null_of_compl _ T₃), setIntegral_eq_sum,
+        integral_eq_setIntegral (FiniteRange.null_of_compl _ T₃), integral_finset _ _ IntegrableOn.finset,
         Measure.map_apply hT₃ (.singleton _), smul_eq_mul]
 
     gcongr
@@ -404,7 +404,7 @@ lemma construct_good_prelim :
       simp only [integral_sub .of_finite .of_finite, integral_const, measure_univ,
         ENNReal.one_toReal, smul_eq_mul, one_mul, sub_left_inj, sum3]
       simp_rw [condRuzsaDist'_eq_sum hT₂ hT₃,
-        integral_eq_setIntegral (FiniteRange.null_of_compl _ T₃), setIntegral_eq_sum,
+        integral_eq_setIntegral (FiniteRange.null_of_compl _ T₃), integral_finset _ _ IntegrableOn.finset,
         Measure.map_apply hT₃ (.singleton _), smul_eq_mul]
     gcongr
     linarith [condRuzsaDist_le' ℙ ℙ p.hmeas2 hT₂ hT₃]
@@ -458,7 +458,7 @@ local notation3:max "δ'" => I[T₁ : T₂|R] + I[T₂ : T₃|R] + I[T₃ : T₁
 omit [AddCommGroup G] in
 lemma delta'_eq_integral :
     δ' = (Measure.map R ℙ)[fun r => δ[ℙ[|R⁻¹' {r}]]] := by
-  simp_rw [condMutualInfo_eq_integral_mutualInfo, integral_eq_sum, smul_add,
+  simp_rw [condMutualInfo_eq_integral_mutualInfo, integral_fintype _ .of_finite, smul_add,
     Finset.sum_add_distrib]
 
 include hT₁ hT₂ hT₃ hT h_min hR hX₁ hX₂ in
@@ -474,7 +474,7 @@ lemma cond_construct_good [IsProbabilityMeasure (ℙ : Measure Ω)] :
     k = (Measure.map R ℙ)[fun _r => k] := by
       rw [integral_const]; simp
     _ ≤ _ := ?_
-  simp_rw [integral_eq_sum]
+  simp_rw [integral_fintype _ .of_finite]
   apply Finset.sum_le_sum
   intro r _
   by_cases hr : ℙ (R⁻¹' {r}) = 0

PFR/ForMathlib/AffineSpaceDim.lean

@@ -1,23 +1,36 @@
-import Mathlib.LinearAlgebra.Dimension.Finrank
-import Mathlib.RingTheory.Finiteness
+import Mathlib.LinearAlgebra.Dimension.Constructions
+import Mathlib.LinearAlgebra.Dimension.Finite
+import PFR.Mathlib.LinearAlgebra.AffineSpace.AffineSubspace
+import PFR.Mathlib.LinearAlgebra.Dimension.Finrank
 
-variable {G : Type*} [AddCommGroup G]
+open scoped Pointwise
 
-/-- If G ≅ ℤᵈ then there is a subgroup H of G such that A lies in a coset of H. This is helpful to
-give the equivalent definition of `dimension`. Here this is stated in greated generality since the
-proof carries over automatically. -/
-lemma exists_coset_cover (A : Set G) :
-    ∃ (d : ℕ), ∃ (S : Submodule ℤ G) (v : G), Module.finrank ℤ S = d ∧ ∀ a ∈ A, a - v ∈ S :=
-  ⟨Module.finrank ℤ (⊤ : Submodule ℤ G), ⊤, by simp⟩
+namespace AffineSpace
+variable {k V P : Type*} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {s : Set P}
+  {S : Submodule k V}
 
--- TODO: Redefine as `Module.finrank ℤ (vectorSpan ℤ A)`
+variable (k) in
 open scoped Classical in
 /-- The dimension of the affine span over `ℤ` of a subset of an additive group. -/
-noncomputable def dimension (A : Set G) : ℕ := Nat.find (exists_coset_cover A)
+noncomputable def finrank (s : Set P) : ℕ := (vectorSpan k s).finrank
 
-lemma dimension_le_of_coset_cover (A : Set G) (S : Submodule ℤ G) (v : G)
-    (hA : ∀ a ∈ A, a - v ∈ S) : dimension A ≤ Module.finrank ℤ S := by
-  classical exact Nat.find_le ⟨S , v, rfl, hA⟩
+variable (k) in
+@[simp]
+lemma finrank_vadd_set (s : Set P) (v : V) : finrank k (v +ᵥ s) = AffineSpace.finrank k s := by
+  simp [finrank]
 
-lemma dimension_le_rank [Module.Finite ℤ G] (A : Set G) : dimension A ≤ Module.finrank ℤ G := by
-  simpa using dimension_le_of_coset_cover A ⊤ 0 (by simp)
+variable (k) in
+@[simp] lemma finrank_empty [Nontrivial k] : finrank k (∅ : Set P) = 0 := by simp [finrank]
+
+variable [StrongRankCondition k]
+
+lemma finrank_le_submoduleFinrank [Module.Finite k S] (q : P) (hs : ∀ p ∈ s, p -ᵥ q ∈ S) :
+    finrank k s ≤ S.finrank := by
+  refine Submodule.finrank_mono ?_
+  simpa [vectorSpan, Submodule.span_le, Set.vsub_subset_iff]
+    using fun a ha b hb ↦ S.sub_mem (hs _ ha) (hs _ hb)
+
+lemma finrank_le_moduleFinrank [Module.Finite k V] : finrank k s ≤ Module.finrank k V :=
+  (vectorSpan k s).finrank_le
+
+end AffineSpace

PFR/ForMathlib/Entropy/Basic.lean

@@ -446,15 +446,15 @@ lemma condEntropy_le_log_card [MeasurableSingletonClass S] [Fintype S]
 lemma condEntropy_eq_sum [MeasurableSingletonClass T] (X : Ω → S) (Y : Ω → T) (μ : Measure Ω)
     [IsFiniteMeasure μ] (hY : Measurable Y) [FiniteRange Y]:
     H[X | Y ; μ] = ∑ y in FiniteRange.toFinset Y, (μ.map Y {y}).toReal * H[X | Y ← y ; μ] := by
-  rw [condEntropy_def, integral_eq_setIntegral (full_measure_of_finiteRange hY), setIntegral_eq_sum]
+  rw [condEntropy_def, integral_eq_setIntegral (full_measure_of_finiteRange hY), integral_finset _ _ IntegrableOn.finset]
   simp_rw [smul_eq_mul]
 
 /-- `H[X|Y] = ∑_y P[Y=y] H[X|Y=y]`$.-/
 lemma condEntropy_eq_sum_fintype
     [MeasurableSingletonClass T] (X : Ω → S) (Y : Ω → T) (μ : Measure Ω)
     [IsFiniteMeasure μ] (hY : Measurable Y) [Fintype T] :
     H[X | Y ; μ] = ∑ y, (μ (Y ⁻¹' {y})).toReal * H[X | Y ← y ; μ] := by
-  rw [condEntropy_def, integral_eq_sum]
+  rw [condEntropy_def, integral_fintype _ .of_finite]
   simp_rw [smul_eq_mul, Measure.map_apply hY (.singleton _)]
 
 variable [MeasurableSingletonClass T]
@@ -828,7 +828,7 @@ lemma condMutualInfo_eq_kernel_mutualInfo
     I[X : Y | Z ; μ] = Ik[condDistrib (⟨X, Y⟩) Z μ, μ.map Z] := by
   rcases finiteSupport_of_finiteRange (μ := μ) (X := Z) with ⟨A, hA⟩
   simp_rw [condMutualInfo_def, entropy_def, Kernel.mutualInfo, Kernel.entropy,
-    integral_eq_setIntegral hA, setIntegral_eq_sum, smul_eq_mul, mul_sub, mul_add,
+    integral_eq_setIntegral hA, integral_finset _ _ IntegrableOn.finset, smul_eq_mul, mul_sub, mul_add,
     Finset.sum_sub_distrib, Finset.sum_add_distrib]
   congr with x
   · have h := condDistrib_fst_ae_eq hX hY hZ μ
@@ -857,7 +857,7 @@ lemma condMutualInfo_eq_sum [MeasurableSingletonClass U] [IsFiniteMeasure μ]
     I[X : Y | Z ; μ] = ∑ z in FiniteRange.toFinset Z,
       (μ (Z ⁻¹' {z})).toReal * I[X : Y ; (μ[|Z ← z])] := by
   rw [condMutualInfo_eq_integral_mutualInfo,
-    integral_eq_setIntegral (FiniteRange.null_of_compl _ Z), setIntegral_eq_sum]
+    integral_eq_setIntegral (FiniteRange.null_of_compl _ Z), integral_finset _ _ IntegrableOn.finset]
   congr 1 with z
   rw [map_apply hZ (MeasurableSet.singleton z)]
   rfl

PFR/ForMathlib/Entropy/Kernel/Basic.lean

@@ -1,6 +1,6 @@
 import Mathlib.MeasureTheory.Integral.Prod
 import PFR.ForMathlib.Entropy.Measure
-import PFR.Mathlib.MeasureTheory.Integral.Bochner
+import PFR.Mathlib.MeasureTheory.Integral.IntegrableOn
 import PFR.Mathlib.MeasureTheory.Integral.SetIntegral
 import PFR.Mathlib.Probability.Kernel.Disintegration
 
@@ -167,7 +167,8 @@ lemma entropy_comap [MeasurableSingletonClass T]
       exact MeasurableSet.compl (Finset.measurableSet A)
     exact ae_eq_univ.mp hf_range
   simp_rw [entropy]
-  simp_rw [integral_eq_setIntegral hA, integral_eq_setIntegral this, setIntegral_eq_sum,
+  simp_rw [integral_eq_setIntegral hA, integral_eq_setIntegral this,
+    integral_finset _ _ IntegrableOn.finset,
     Measure.comap_apply f hf.injective hf.measurableSet_image' _ (.singleton _)]
   simp only [Set.image_singleton, smul_eq_mul]
   simp_rw [comap_apply]
@@ -223,7 +224,7 @@ lemma entropy_compProd_aux [MeasurableSingletonClass S] [MeasurableSingletonClas
   · simp
   let A := μ.support
   have hsum (F : T → ℝ) : ∫ (t : T), F t ∂μ = ∑ t in A, (μ.real {t}) * (F t) := by
-    rw [integral_eq_setIntegral (measure_compl_support μ), setIntegral_eq_sum]
+    rw [integral_eq_setIntegral (measure_compl_support μ), integral_finset _ _ IntegrableOn.finset]
     congr with t ht
   simp_rw [entropy, hsum, ← Finset.sum_add_distrib]
   apply Finset.sum_congr rfl
@@ -246,7 +247,7 @@ lemma entropy_compProd_aux [MeasurableSingletonClass S] [MeasurableSingletonClas
       simp at hu ⊢
       exact hu hs
     exact MeasurableSet.compl (Finset.measurableSet _)
-  rw [measureEntropy_def_finite' hκη, measureEntropy_def_finite' (hB t ht), setIntegral_eq_sum,
+  rw [measureEntropy_def_finite' hκη, measureEntropy_def_finite' (hB t ht), integral_finset _ _ IntegrableOn.finset,
     ← Finset.sum_add_distrib, Finset.sum_product]
   apply Finset.sum_congr rfl
   intro s hs

PFR/ForMathlib/Entropy/Kernel/MutualInfo.lean

@@ -120,7 +120,7 @@ lemma mutualInfo_nonneg' {κ : Kernel T (S × U)} {μ : Measure T} [IsFiniteMeas
     [FiniteSupport μ] (hκ : FiniteKernelSupport κ) :
     0 ≤ Ik[κ, μ] := by
   simp_rw [mutualInfo, entropy, integral_eq_setIntegral (measure_compl_support μ),
-    setIntegral_eq_sum, smul_eq_mul]
+    integral_finset _ _ IntegrableOn.finset, smul_eq_mul]
   rw [← Finset.sum_add_distrib, ← Finset.sum_sub_distrib]
   refine Finset.sum_nonneg (fun x _ ↦ ?_)
   by_cases hx : μ {x} = 0

PFR/ForMathlib/Entropy/Kernel/RuzsaDist.lean

@@ -295,7 +295,7 @@ lemma rdist_triangle_aux1 (κ : Kernel T G) (η : Kernel T' G)
       (((μ.support ×ˢ μ''.support) ×ˢ μ'.support : Finset ((T × T'') × T')) : Set ((T × T'') × T'))ᶜ
       = 0 :=
     Measure.prod_of_full_measure_finset hAC (measure_compl_support μ')
-  simp_rw [entropy, integral_eq_setIntegral hAB, integral_eq_setIntegral hACB, setIntegral_eq_sum,
+  simp_rw [entropy, integral_eq_setIntegral hAB, integral_eq_setIntegral hACB, integral_finset _ _ IntegrableOn.finset,
     smul_eq_mul, Measure.prod_apply_singleton, Finset.sum_product, ENNReal.toReal_mul, mul_assoc,
     ← Finset.mul_sum]
   congr with x
@@ -326,7 +326,7 @@ lemma rdist_triangle_aux2 (η : Kernel T' G) (ξ : Kernel T'' G)
       (((μ.support ×ˢ μ''.support) ×ˢ μ'.support : Finset ((T × T'') × T')) : Set ((T × T'') × T'))ᶜ
       = 0 :=
     Measure.prod_of_full_measure_finset hAC (measure_compl_support μ')
-  simp_rw [entropy, integral_eq_setIntegral hACB, integral_eq_setIntegral hBC, setIntegral_eq_sum,
+  simp_rw [entropy, integral_eq_setIntegral hACB, integral_eq_setIntegral hBC, integral_finset _ _ IntegrableOn.finset,
     smul_eq_mul, Measure.prod_apply_singleton]
   conv_rhs => rw [Finset.sum_product_right]
   conv_lhs => rw [Finset.sum_product, Finset.sum_product_right]

PFR/ForMathlib/Entropy/RuzsaDist.lean

@@ -466,7 +466,7 @@ lemma condRuzsaDist_eq_sum' {X : Ω → G} {Z : Ω → S} {Y : Ω' → G} {W : 
     d[X | Z ; μ # Y | W ; μ']
       = ∑ z, ∑ w, (μ (Z ⁻¹' {z})).toReal * (μ' (W ⁻¹' {w})).toReal
           * d[X ; (μ[|Z ← z]) # Y ; (μ'[|W ← w])] := by
-  rw [condRuzsaDist_def, Kernel.rdist, integral_eq_sum]
+  rw [condRuzsaDist_def, Kernel.rdist, integral_fintype _ .of_finite]
   simp_rw [Measure.prod_apply_singleton, ENNReal.toReal_mul, smul_eq_mul, Fintype.sum_prod_type,
     Measure.map_apply hZ (.singleton _),
     Measure.map_apply hW (.singleton _)]
@@ -502,7 +502,7 @@ lemma condRuzsaDist_eq_sum {X : Ω → G} {Z : Ω → S} {Y : Ω' → G} {W : Ω
       simp [← FiniteRange.range]
       measurability
     }
-  rw [condRuzsaDist_def, Kernel.rdist, integral_eq_setIntegral this, setIntegral_eq_sum]
+  rw [condRuzsaDist_def, Kernel.rdist, integral_eq_setIntegral this, integral_finset _ _ IntegrableOn.finset]
   simp_rw [Measure.prod_apply_singleton, ENNReal.toReal_mul, smul_eq_mul, Finset.sum_product,
     Measure.map_apply hZ (.singleton _),
     Measure.map_apply hW (.singleton _)]
@@ -583,7 +583,7 @@ lemma condRuzsaDist'_eq_sum {X : Ω → G} {Y : Ω' → G} {W : Ω' → T} (hY :
     convert measure_empty (μ := μ)
     simp [← FiniteRange.range]
     measurability
-  rw [condRuzsaDist'_def, Kernel.rdist, integral_eq_setIntegral this, setIntegral_eq_sum]
+  rw [condRuzsaDist'_def, Kernel.rdist, integral_eq_setIntegral this, integral_finset _ _ IntegrableOn.finset]
   simp_rw [Measure.prod_apply_singleton, smul_eq_mul, Finset.sum_product]
   simp only [Finset.univ_unique, PUnit.default_eq_unit, MeasurableSpace.measurableSet_top,
     Measure.dirac_apply', Set.mem_singleton_iff, Set.indicator_of_mem, Pi.one_apply, one_mul,
@@ -680,9 +680,8 @@ lemma condRuzsaDist'_eq_integral (X : Ω → G) {Y : Ω' → G} {W : Ω' → T}
     convert measure_empty (μ := μ)
     simp [← FiniteRange.range]
     measurability
-  rw [integral_eq_setIntegral this]
-  convert symm $ setIntegral_eq_sum (μ'.map W) _ (fun w ↦ d[X ; μ # Y ; (μ'[|W ← w])])
-  rw [Measure.map_apply hW (MeasurableSet.singleton _)]
+  rw [integral_eq_setIntegral this, integral_finset _ _ IntegrableOn.finset]
+  simp [Measure.map_apply hW (MeasurableSet.singleton _)]
 
 section
 
@@ -832,8 +831,8 @@ lemma condRuzsaDist_of_copy {X : Ω → G} (hX : Measurable X) {Z : Ω → S} (h
       measurability
     }
   rw [condRuzsaDist_def, condRuzsaDist_def, Kernel.rdist, Kernel.rdist,
-    integral_eq_setIntegral hfull, integral_eq_setIntegral hfull', setIntegral_eq_sum,
-    setIntegral_eq_sum]
+    integral_eq_setIntegral hfull, integral_eq_setIntegral hfull', integral_finset _ _ IntegrableOn.finset,
+    integral_finset _ _ IntegrableOn.finset]
   have hZZ' : μ.map Z = μ''.map Z' := (h1.comp measurable_snd).map_eq
   have hWW' : μ'.map W = μ'''.map W' := (h2.comp measurable_snd).map_eq
   simp_rw [Measure.prod_apply_singleton, ENNReal.toReal_mul, ← hZZ', ← hWW',
@@ -904,8 +903,8 @@ lemma condRuzsaDist'_of_copy (X : Ω → G) {Y : Ω' → G} (hY : Measurable Y)
     simp [← FiniteRange.range]
     measurability
   rw [condRuzsaDist'_def, condRuzsaDist'_def, Kernel.rdist, Kernel.rdist,
-    integral_eq_setIntegral hfull, integral_eq_setIntegral hfull', setIntegral_eq_sum,
-    setIntegral_eq_sum]
+    integral_eq_setIntegral hfull, integral_eq_setIntegral hfull', integral_finset _ _ IntegrableOn.finset,
+    integral_finset _ _ IntegrableOn.finset]
   have hWW' : μ'.map W = μ'''.map W' := (h2.comp measurable_snd).map_eq
   simp_rw [Measure.prod_apply_singleton, ENNReal.toReal_mul, ← hWW',
     Measure.map_apply hW (.singleton _)]