diff --git a/LeanAPAP.lean b/LeanAPAP.lean
index 3bd7563418..b12821c7d8 100644
--- a/LeanAPAP.lean
+++ b/LeanAPAP.lean
@@ -1,7 +1,6 @@
 import LeanAPAP.Extras.BSG
 import LeanAPAP.FiniteField
 import LeanAPAP.Integer
-import LeanAPAP.Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar
 import LeanAPAP.Mathlib.MeasureTheory.Function.LpSeminorm.Basic
 import LeanAPAP.Mathlib.Probability.ConditionalProbability
 import LeanAPAP.Mathlib.Probability.UniformOn
@@ -9,8 +8,6 @@ import LeanAPAP.Mathlib.Tactic.Positivity
 import LeanAPAP.Physics.AlmostPeriodicity
 import LeanAPAP.Physics.DRC
 import LeanAPAP.Physics.Unbalancing
-import LeanAPAP.Prereqs.AddChar.Basic
-import LeanAPAP.Prereqs.AddChar.PontryaginDuality
 import LeanAPAP.Prereqs.Bohr.Arc
 import LeanAPAP.Prereqs.Bohr.Basic
 import LeanAPAP.Prereqs.Bohr.Regular
@@ -25,10 +22,10 @@ import LeanAPAP.Prereqs.Energy
 import LeanAPAP.Prereqs.FourierTransform.Compact
 import LeanAPAP.Prereqs.FourierTransform.Convolution
 import LeanAPAP.Prereqs.FourierTransform.Discrete
+import LeanAPAP.Prereqs.Function.Dilate
 import LeanAPAP.Prereqs.Function.Indicator.Basic
 import LeanAPAP.Prereqs.Function.Indicator.Complex
 import LeanAPAP.Prereqs.Function.Indicator.Defs
-import LeanAPAP.Prereqs.Function.Translate
 import LeanAPAP.Prereqs.Inner.Function
 import LeanAPAP.Prereqs.Inner.Hoelder.Compact
 import LeanAPAP.Prereqs.Inner.Hoelder.Discrete
@@ -39,5 +36,4 @@ import LeanAPAP.Prereqs.LpNorm.Discrete.Defs
 import LeanAPAP.Prereqs.LpNorm.Weighted
 import LeanAPAP.Prereqs.MarcinkiewiczZygmund
 import LeanAPAP.Prereqs.NNLpNorm
-import LeanAPAP.Prereqs.Randomisation
 import LeanAPAP.Prereqs.Rudin
diff --git a/LeanAPAP/Mathlib/Analysis/SpecialFunctions/Complex/CircleAddChar.lean b/LeanAPAP/Mathlib/Analysis/SpecialFunctions/Complex/CircleAddChar.lean
deleted file mode 100644
index c7d8182a2c..0000000000
--- a/LeanAPAP/Mathlib/Analysis/SpecialFunctions/Complex/CircleAddChar.lean
+++ /dev/null
@@ -1,39 +0,0 @@
-import Mathlib.Algebra.EuclideanDomain.Basic
-import Mathlib.Algebra.EuclideanDomain.Field
-import Mathlib.Analysis.SpecialFunctions.Complex.Circle
-
-open AddChar Multiplicative Real
-open scoped ComplexConjugate Real
-
-namespace Circle
-variable {r s : ℝ}
-
-noncomputable def e : AddChar ℝ Circle where
-  toFun r := exp (2 * π * r)
-  map_zero_eq_one' := by simp
-  map_add_eq_mul' := by simp [mul_add, Complex.exp_add]
-
-lemma e_apply (r : ℝ) : e r = exp (2 * π * r) := rfl
-
-@[simp, norm_cast] lemma coe_e (r : ℝ) : ↑(e r) = Complex.exp ((2 * π * r : ℝ) * Complex.I) := rfl
-
-@[simp] lemma e_int (z : ℤ) : e z = 1 := exp_two_pi_mul_int _
-@[simp] lemma e_one : e 1 = 1 := by simpa using e_int 1
-@[simp] lemma e_add_int {z : ℤ} : e (r + z) = e r := by rw [map_add_eq_mul, e_int, mul_one]
-@[simp] lemma e_sub_int {z : ℤ} : e (r - z) = e r := by rw [map_sub_eq_div, e_int, div_one]
-@[simp] lemma e_fract (r : ℝ) : e (Int.fract r) = e r := by rw [Int.fract, e_sub_int]
-
-@[simp] lemma e_mod_div {m : ℤ} {n : ℕ} : e ((m % n : ℤ) / n) = e (m / n) := by
-  obtain hn | hn := eq_or_ne (n : ℝ) 0
-  · rw [hn, div_zero, div_zero]
-  · rw [Int.emod_def, Int.cast_sub, sub_div, Int.cast_mul, Int.cast_natCast,
-      mul_div_cancel_left₀ _ hn, e_sub_int]
-
-lemma e_eq_one : e r = 1 ↔ ∃ n : ℤ, r = n := by
-  simp [e_apply, exp_eq_one, mul_comm (2 * π), pi_ne_zero]
-
-lemma e_inj : e r = e s ↔ r ≡ s [PMOD 1] := by
-  simp [AddCommGroup.ModEq, ← e_eq_one, div_eq_one, map_sub_eq_div, eq_comm (b := 1),
-    eq_comm (a := e r)]
-
-end Circle
diff --git a/LeanAPAP/Physics/AlmostPeriodicity.lean b/LeanAPAP/Physics/AlmostPeriodicity.lean
index 8f8fdc9d79..31d834701c 100644
--- a/LeanAPAP/Physics/AlmostPeriodicity.lean
+++ b/LeanAPAP/Physics/AlmostPeriodicity.lean
@@ -1,6 +1,7 @@
 import Mathlib.Algebra.Order.Chebyshev
 import Mathlib.Combinatorics.Additive.DoublingConst
 import Mathlib.Data.Complex.ExponentialBounds
+import Mathlib.Tactic.Bound
 import LeanAPAP.Prereqs.Convolution.Discrete.Basic
 import LeanAPAP.Prereqs.Convolution.Norm
 import LeanAPAP.Prereqs.Inner.Hoelder.Discrete
@@ -11,7 +12,7 @@ import LeanAPAP.Prereqs.MarcinkiewiczZygmund
 -/
 
 open MeasureTheory
-open scoped Pointwise Combinatorics.Additive
+open scoped Pointwise Combinatorics.Additive translate
 
 namespace Finset
 variable {α : Type*} [DecidableEq α] {s : Finset α} {k : ℕ}
@@ -246,7 +247,7 @@ lemma lemma28_markov (hε : 0 < ε) (hm : 1 ≤ m)
   refine this.trans_eq ?_
   rw [l]
   congr with a : 3
-  refine pow_le_pow_iff_left ?_ ?_ ?_ <;> positivity
+  refine pow_le_pow_iff_left₀ ?_ ?_ ?_ <;> positivity
 
 variable [DiscreteMeasurableSpace G]
 
@@ -374,13 +375,7 @@ lemma T_bound (hK₂ : 2 ≤ K) (Lc Sc Ac ASc Tc : ℕ) (hk : k = ⌈(64 : ℝ)
   rw [Nat.cast_add_one, ← le_sub_iff_add_le, hk']
   refine (Nat.ceil_lt_add_one ?_).le.trans ?_
   · positivity
-  have : (1 : ℝ) ≤ 128 * (m / ε ^ 2) := by
-    rw [div_eq_mul_one_div]
-    refine one_le_mul_of_one_le_of_one_le (by norm_num1) ?_
-    refine one_le_mul_of_one_le_of_one_le (Nat.one_le_cast.2 hm) ?_
-    refine one_le_one_div (by positivity) ?_
-    rw [sq_le_one_iff hε.le]
-    exact hε'
+  have : (1 : ℝ) ≤ 128 * (m / ε ^ 2) := by rw [div_eq_mul_one_div]; bound
   rw [mul_div_assoc, mul_div_assoc]
   linarith only [this]
 
diff --git a/LeanAPAP/Physics/DRC.lean b/LeanAPAP/Physics/DRC.lean
index 14137d6101..429770148e 100644
--- a/LeanAPAP/Physics/DRC.lean
+++ b/LeanAPAP/Physics/DRC.lean
@@ -214,9 +214,11 @@ lemma sifting (B₁ B₂ : Finset G) (hε : 0 < ε) (hε₁ : ε ≤ 1) (hδ : 0
       · exact Pi.le_def.1 (dconv_nonneg (R := ℝ) mu_nonneg mu_nonneg) x
       · exact dconv_nonneg indicate_nonneg indicate_nonneg _
       · simpa using hx
-    _ ≤ ∑ x, (μ B₁ ○ μ B₂) x * ((1 - ε) * ‖𝟭_[ℝ] A ○ 𝟭 A‖_[p, μ B₁ ○ μ B₂]) ^ p :=
-      sum_le_univ_sum_of_nonneg fun x ↦
-        mul_nonneg (dconv_nonneg (mu_nonneg (β := ℝ)) mu_nonneg _) $ hp.pow_nonneg _
+    _ ≤ ∑ x, (μ B₁ ○ μ B₂) x * ((1 - ε) * ‖𝟭_[ℝ] A ○ 𝟭 A‖_[p, μ B₁ ○ μ B₂]) ^ p := by
+      gcongr
+      · intros
+        exact mul_nonneg (dconv_nonneg (mu_nonneg (β := ℝ)) mu_nonneg _) $ hp.pow_nonneg _
+      · exact subset_univ _
     _ = ‖μ_[ℝ] B₁‖_[1] * ‖μ_[ℝ] B₂‖_[1] * ((1 - ε) ^ p * ‖𝟭_[ℝ] A ○ 𝟭 A‖_[p, μ B₁ ○ μ B₂] ^ p)
         := ?_
     _ ≤ _ :=
diff --git a/LeanAPAP/Prereqs/AddChar/Basic.lean b/LeanAPAP/Prereqs/AddChar/Basic.lean
deleted file mode 100644
index 1d4ae361a9..0000000000
--- a/LeanAPAP/Prereqs/AddChar/Basic.lean
+++ /dev/null
@@ -1,79 +0,0 @@
-import Mathlib.Algebra.BigOperators.Expect
-import Mathlib.Algebra.Group.AddChar
-import Mathlib.Analysis.RCLike.Inner
-
-open Finset hiding card
-open Fintype (card)
-open Function RCLike
-open scoped BigOperators ComplexConjugate DirectSum
-
-variable {G H R : Type*}
-
-namespace AddChar
-section AddGroup
-variable [AddGroup G]
-
-section Semifield
-variable [Fintype G] [Semifield R] [IsDomain R] [CharZero R] {ψ : AddChar G R}
-
-lemma expect_eq_ite (ψ : AddChar G R) : 𝔼 a, ψ a = if ψ = 0 then 1 else 0 := by
-  split_ifs with h
-  · simp [h, card_univ]
-  obtain ⟨x, hx⟩ := ne_one_iff.1 h
-  refine eq_zero_of_mul_eq_self_left hx ?_
-  rw [Finset.mul_expect]
-  exact Fintype.expect_equiv (Equiv.addLeft x) _ _ fun y ↦ (map_add_eq_mul _ _ _).symm
-
-lemma expect_eq_zero_iff_ne_zero : 𝔼 x, ψ x = 0 ↔ ψ ≠ 0 := by
-  rw [expect_eq_ite, one_ne_zero.ite_eq_right_iff]
-
-lemma expect_ne_zero_iff_eq_zero : 𝔼 x, ψ x ≠ 0 ↔ ψ = 0 := expect_eq_zero_iff_ne_zero.not_left
-
-end Semifield
-
-section RCLike
-variable [RCLike R] [Fintype G]
-
-lemma wInner_cWeight_self (ψ : AddChar G R) : ⟪(ψ : G → R), ψ⟫ₙ_[R] = 1 := by
-  simp [wInner_cWeight_eq_expect, ψ.norm_apply, RCLike.conj_mul]
-
-end RCLike
-end AddGroup
-
-section AddCommGroup
-variable [AddCommGroup G]
-
-section RCLike
-variable [RCLike R] {ψ₁ ψ₂ : AddChar G R}
-
-lemma wInner_cWeight_eq_boole [Fintype G] (ψ₁ ψ₂ : AddChar G R) :
-    ⟪(ψ₁ : G → R), ψ₂⟫ₙ_[R] = if ψ₁ = ψ₂ then 1 else 0 := by
-  split_ifs with h
-  · rw [h, wInner_cWeight_self]
-  have : ψ₁⁻¹ * ψ₂ ≠ 1 := by rwa [Ne, inv_mul_eq_one]
-  simp_rw [wInner_cWeight_eq_expect, RCLike.inner_apply, ← inv_apply_eq_conj]
-  simpa [map_neg_eq_inv] using expect_eq_zero_iff_ne_zero.2 this
-
-lemma wInner_cWeight_eq_zero_iff_ne [Fintype G] : ⟪(ψ₁ : G → R), ψ₂⟫ₙ_[R] = 0 ↔ ψ₁ ≠ ψ₂ := by
-  rw [wInner_cWeight_eq_boole, one_ne_zero.ite_eq_right_iff]
-
-lemma wInner_cWeight_eq_one_iff_eq [Fintype G] : ⟪(ψ₁ : G → R), ψ₂⟫ₙ_[R] = 1 ↔ ψ₁ = ψ₂ := by
-  rw [wInner_cWeight_eq_boole, one_ne_zero.ite_eq_left_iff]
-
-variable (G R)
-
-protected lemma linearIndependent [Finite G] : LinearIndependent R ((⇑) : AddChar G R → G → R) := by
-  cases nonempty_fintype G
-  exact linearIndependent_of_ne_zero_of_wInner_cWeight_eq_zero AddChar.coe_ne_zero fun ψ₁ ψ₂ ↦
-    wInner_cWeight_eq_zero_iff_ne.2
-
-noncomputable instance instFintype [Finite G] : Fintype (AddChar G R) :=
-  @Fintype.ofFinite _ (AddChar.linearIndependent G R).finite
-
-@[simp] lemma card_addChar_le [Fintype G] : card (AddChar G R) ≤ card G := by
-  simpa only [Module.finrank_fintype_fun_eq_card] using
-    (AddChar.linearIndependent G R).fintype_card_le_finrank
-
-end RCLike
-end AddCommGroup
-end AddChar
diff --git a/LeanAPAP/Prereqs/AddChar/PontryaginDuality.lean b/LeanAPAP/Prereqs/AddChar/PontryaginDuality.lean
deleted file mode 100644
index 2faf766cec..0000000000
--- a/LeanAPAP/Prereqs/AddChar/PontryaginDuality.lean
+++ /dev/null
@@ -1,232 +0,0 @@
-import Mathlib.Algebra.DirectSum.AddChar
-import Mathlib.GroupTheory.FiniteAbelian.Basic
-import LeanAPAP.Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar
-import LeanAPAP.Prereqs.AddChar.Basic
-
-/-!
-# Pontryagin duality for finite abelian groups
-
-This file proves the Pontryagin duality in case of finite abelian groups. This states that any
-finite abelian group is canonically isomorphic to its double dual (the space of complex-valued
-characters of its space of complex-valued characters).
-
-We first prove it for `ZMod n` and then extend to all finite abelian groups using the
-Structure Theorem.
--/
-
-noncomputable section
-
-open Circle Finset Function Multiplicative
-open Fintype (card)
-open scoped BigOperators DirectSum
-
-variable {α : Type*} [AddCommGroup α] {n : ℕ} {a b : α}
-
-namespace AddChar
-
-private def zmodAuxAux (n : ℕ) : ℤ →+ Additive Circle where
-  toFun x := Additive.ofMul (e $ x / n)
-  map_zero' := by dsimp; rw [Int.cast_zero, zero_div, ofMul_eq_zero, map_zero_eq_one]
-  map_add' x y := by rw [← ofMul_mul, Equiv.apply_eq_iff_eq, Int.cast_add, add_div, map_add_eq_mul]
-
-@[simp]
-lemma zmodAuxAux_apply (n : ℕ) (z : ℤ) : zmodAuxAux n z = Additive.ofMul (e $ z / n) := rfl
-
-/-- The character sending `k : ZMod n` to `e ^ (2 * π * i * k / n)`. -/
-private def zmodAux (n : ℕ) : AddChar (ZMod n) Circle :=
-  AddChar.toAddMonoidHomEquiv.symm $ ZMod.lift n ⟨zmodAuxAux n, by
-    obtain hn | hn := eq_or_ne (n : ℝ) 0 <;> simp [hn, zmodAuxAux]⟩
-
---TODO: Heavily generalise. Yaël's attempts at generalising failed :(
-@[simp] lemma aux (n : ℕ) (h) :
-    (⟨zmodAuxAux n, h⟩ : {f : ℤ →+ Additive Circle // f n = 0}) = zmodAuxAux n := rfl
-
-@[simp] lemma zmodAux_apply (n : ℕ) (z : ℤ) : zmodAux n z = e (z / n) := by simp [zmodAux]
-
--- probably an evil lemma
--- @[simp] lemma zmodAux_apply (n : ℕ) (x : ZMod n) : zmodAux n x = e (x / n) :=
--- by simp [zmodAux]
-
-lemma zmodAux_injective (hn : n ≠ 0) : Injective (zmodAux n) := by
-  replace hn : (n : ℝ) ≠ 0 := Nat.cast_ne_zero.2 hn
-  simp [zmodAux, ZMod.lift_injective, CharP.intCast_eq_zero_iff _ n, e_eq_one, div_eq_iff hn,
-    mul_comm _ (n : ℝ), -forall_exists_index]
-  norm_cast
-  exact fun _ ↦ id
-
-/-- Indexing of the complex characters of `ZMod n`. `AddChar.zmod n x` is the character sending `y`
-to `e ^ (2 * π * i * x * y / n)`. -/
-def zmod (n : ℕ) (x : ZMod n) : AddChar (ZMod n) Circle :=
-  (zmodAux n).compAddMonoidHom $ AddMonoidHom.mulLeft x
-
-@[simp] lemma zmod_apply (n : ℕ) (x y : ℤ) :
-    (zmod n x) (y : ZMod n) = e (x * y / n) := by
-  simp [zmod, ← Int.cast_mul x y, -Int.cast_mul]
-
-@[simp] lemma zmod_zero (n : ℕ) : zmod n 0 = 1 := by
-  refine DFunLike.ext _ _ ?_
-  rw [ZMod.intCast_surjective.forall]
-  rintro y
-  simpa using zmod_apply n 0 y
-
-@[simp] lemma zmod_add (n : ℕ) : ∀ x y : ZMod n, zmod n (x + y) = zmod n x * zmod n y := by
-  simp only [DFunLike.ext_iff, ZMod.intCast_surjective.forall, ← Int.cast_add, AddChar.mul_apply,
-    zmod_apply]
-  simp [add_mul, add_div, map_add_eq_mul]
-
--- probably an evil lemma
--- @[simp] lemma zmod_apply (n : ℕ) (x y : ZMod n) : zmod n x y = e (x * y / n) :=
--- by simp [addChar.zmod, ZMod.coe_mul]
-
-lemma zmod_injective (hn : n ≠ 0) : Injective (zmod n) := by
-  simp_rw [Injective, ZMod.intCast_surjective.forall]
-  rintro x y h
-  replace hn : (n : ℝ) ≠ 0 := by positivity
-  simpa only [Int.cast_one, mul_one, one_mul, e_inj, AddCommGroup.div_modEq_div hn,
-    AddCommGroup.intCast_modEq_intCast', AddCommGroup.modEq_iff_int_modEq,
-    CharP.intCast_eq_intCast (ZMod n) n] using (zmod_apply _ _ _).symm.trans $
-    (DFunLike.congr_fun h ((1 : ℤ) : ZMod n)).trans $ zmod_apply _ _ _
-
-@[simp] lemma zmod_inj (hn : n ≠ 0) {x y : ZMod n} : zmod n x = zmod n y ↔ x = y :=
-  (zmod_injective hn).eq_iff
-
-def zmodHom (n : ℕ) : AddChar (ZMod n) (AddChar (ZMod n) Circle) where
-  toFun := zmod n
-  map_zero_eq_one' := by simp
-  map_add_eq_mul' := by simp
-
-def mkZModAux {ι : Type} [DecidableEq ι] (n : ι → ℕ) (u : ∀ i, ZMod (n i)) :
-    AddChar (⨁ i, ZMod (n i)) Circle :=
-  AddChar.directSum fun i ↦ zmod (n i) (u i)
-
-lemma mkZModAux_injective {ι : Type} [DecidableEq ι] {n : ι → ℕ} (hn : ∀ i, n i ≠ 0) :
-    Injective (mkZModAux n) :=
-  AddChar.directSum_injective.comp fun f g h ↦ by simpa [funext_iff, hn] using h
-
-/-- The circle-valued characters of a finite abelian group are the same as its complex-valued
-characters. -/
-def circleEquivComplex [Finite α] : AddChar α Circle ≃+ AddChar α ℂ where
-  toFun ψ := toMonoidHomEquiv.symm $ coeHom.comp ψ.toMonoidHom
-  invFun ψ :=
-    { toFun := fun a ↦ (⟨ψ a, mem_sphere_zero_iff_norm.2 $ ψ.norm_apply _⟩ : Circle)
-      map_zero_eq_one' := by simp [Circle]
-      map_add_eq_mul' := fun a b ↦ by ext : 1; simp [map_add_eq_mul] }
-  left_inv ψ := by ext : 1; simp
-  right_inv ψ := by ext : 1; simp
-  map_add' ψ χ := rfl
-
-@[simp] lemma card_eq [Fintype α] : card (AddChar α ℂ) = card α := by
-  obtain ⟨ι, _, n, hn, ⟨e⟩⟩ := AddCommGroup.equiv_directSum_zmod_of_finite' α
-  classical
-  have hn' : ∀ i, n i ≠ 0 := fun i ↦ by have := hn i; positivity
-  let f : α → AddChar α ℂ := fun a ↦ coeHom.compAddChar ((mkZModAux n $ e a).compAddMonoidHom e)
-  have hf : Injective f := circleEquivComplex.injective.comp
-    ((compAddMonoidHom_injective_left _ e.surjective).comp $ (mkZModAux_injective hn').comp $
-      DFunLike.coe_injective.comp $ e.injective.comp Additive.ofMul.injective)
-  exact (card_addChar_le _ _).antisymm (Fintype.card_le_of_injective _ hf)
-
-/-- `ZMod n` is (noncanonically) isomorphic to its group of characters. -/
-def zmodAddEquiv (hn : n ≠ 0) : ZMod n ≃+ AddChar (ZMod n) ℂ := by
-  haveI : NeZero n := ⟨hn⟩
-  refine AddEquiv.ofBijective
-    (circleEquivComplex.toAddMonoidHom.comp $ AddChar.toAddMonoidHom $ zmodHom n) ?_
-  rw [Fintype.bijective_iff_injective_and_card, card_eq]
-  exact ⟨circleEquivComplex.injective.comp $ zmod_injective hn, rfl⟩
-
-@[simp] lemma zmodAddEquiv_apply [NeZero n] (x : ZMod n) :
-    zmodAddEquiv (NeZero.ne _) x = circleEquivComplex (zmod n x) := rfl
-
-section Finite
-variable (α) [Finite α]
-
-/-- Complex-valued characters of a finite abelian group `α` form a basis of `α → ℂ`. -/
-def complexBasis : Basis (AddChar α ℂ) ℂ (α → ℂ) :=
-  basisOfLinearIndependentOfCardEqFinrank (AddChar.linearIndependent _ _) $ by
-    cases nonempty_fintype α; rw [card_eq, Module.finrank_fintype_fun_eq_card]
-
-@[simp, norm_cast]
-lemma coe_complexBasis : ⇑(complexBasis α) = ((⇑) : AddChar α ℂ → α → ℂ) := by
-  rw [complexBasis, coe_basisOfLinearIndependentOfCardEqFinrank]
-
-variable {α}
-
-@[simp]
-lemma complexBasis_apply (ψ : AddChar α ℂ) : complexBasis α ψ = ψ := by rw [coe_complexBasis]
-
-lemma exists_apply_ne_zero : (∃ ψ : AddChar α ℂ, ψ a ≠ 1) ↔ a ≠ 0 := by
-  refine ⟨?_, fun ha ↦ ?_⟩
-  · rintro ⟨ψ, hψ⟩ rfl
-    exact hψ ψ.map_zero_eq_one
-  classical
-  by_contra! h
-  let f : α → ℂ := fun b ↦ if a = b then 1 else 0
-  have h₀ := congr_fun ((complexBasis α).sum_repr f) 0
-  have h₁ := congr_fun ((complexBasis α).sum_repr f) a
-  simp only [complexBasis_apply, Fintype.sum_apply, Pi.smul_apply, h, smul_eq_mul, mul_one,
-    map_zero_eq_one, if_pos rfl, if_neg ha, f] at h₀ h₁
-  exact one_ne_zero (h₁.symm.trans h₀)
-
-lemma forall_apply_eq_zero : (∀ ψ : AddChar α ℂ, ψ a = 1) ↔ a = 0 := by
-  simpa using exists_apply_ne_zero.not
-
-lemma doubleDualEmb_injective : Injective (doubleDualEmb : α → AddChar (AddChar α ℂ) ℂ) :=
-  doubleDualEmb.ker_eq_bot_iff.1 $ eq_bot_iff.2 fun a ha ↦
-    forall_apply_eq_zero.1 fun ψ ↦ by simpa using DFunLike.congr_fun ha (Additive.ofMul ψ)
-
-lemma doubleDualEmb_bijective : Bijective (doubleDualEmb : α → AddChar (AddChar α ℂ) ℂ) := by
-  cases nonempty_fintype α
-  exact (Fintype.bijective_iff_injective_and_card _).2
-    ⟨doubleDualEmb_injective, card_eq.symm.trans card_eq.symm⟩
-
-@[simp]
-lemma doubleDualEmb_inj : (doubleDualEmb a : AddChar (AddChar α ℂ) ℂ) = doubleDualEmb b ↔ a = b :=
-  doubleDualEmb_injective.eq_iff
-
-@[simp] lemma doubleDualEmb_eq_zero : (doubleDualEmb a : AddChar (AddChar α ℂ) ℂ) = 0 ↔ a = 0 := by
-  rw [← map_zero doubleDualEmb, doubleDualEmb_inj]
-
-lemma doubleDualEmb_ne_zero : (doubleDualEmb a : AddChar (AddChar α ℂ) ℂ) ≠ 0 ↔ a ≠ 0 :=
-  doubleDualEmb_eq_zero.not
-
-/-- The double dual isomorphism. -/
-def doubleDualEquiv : α ≃+ AddChar (AddChar α ℂ) ℂ :=
-  AddEquiv.ofBijective _ doubleDualEmb_bijective
-
-@[simp]
-lemma coe_doubleDualEquiv : ⇑(doubleDualEquiv : α ≃+ AddChar (AddChar α ℂ) ℂ) = doubleDualEmb := rfl
-
-@[simp] lemma doubleDualEmb_doubleDualEquiv_symm_apply (a : AddChar (AddChar α ℂ) ℂ) :
-    doubleDualEmb (doubleDualEquiv.symm a) = a :=
-  doubleDualEquiv.apply_symm_apply _
-
-@[simp] lemma doubleDualEquiv_symm_doubleDualEmb_apply (a : AddChar (AddChar α ℂ) ℂ) :
-    doubleDualEquiv.symm (doubleDualEmb a) = a := doubleDualEquiv.symm_apply_apply _
-
-end Finite
-
-lemma sum_apply_eq_ite [Fintype α] [DecidableEq α] (a : α) :
-    ∑ ψ : AddChar α ℂ, ψ a = if a = 0 then (Fintype.card α : ℂ) else 0 := by
-  simpa using sum_eq_ite (doubleDualEmb a : AddChar (AddChar α ℂ) ℂ)
-
-lemma expect_apply_eq_ite [Fintype α] [DecidableEq α] (a : α) :
-    𝔼 ψ : AddChar α ℂ, ψ a = if a = 0 then 1 else 0 := by
-  simpa using expect_eq_ite (doubleDualEmb a : AddChar (AddChar α ℂ) ℂ)
-
-lemma sum_apply_eq_zero_iff_ne_zero [Finite α] : ∑ ψ : AddChar α ℂ, ψ a = 0 ↔ a ≠ 0 := by
-  classical
-  cases nonempty_fintype α
-  rw [sum_apply_eq_ite, Ne.ite_eq_right_iff]
-  exact Nat.cast_ne_zero.2 Fintype.card_ne_zero
-
-lemma sum_apply_ne_zero_iff_eq_zero [Finite α] : ∑ ψ : AddChar α ℂ, ψ a ≠ 0 ↔ a = 0 :=
-  sum_apply_eq_zero_iff_ne_zero.not_left
-
-lemma expect_apply_eq_zero_iff_ne_zero [Finite α] : 𝔼 ψ : AddChar α ℂ, ψ a = 0 ↔ a ≠ 0 := by
-  classical
-  cases nonempty_fintype α
-  rw [expect_apply_eq_ite, one_ne_zero.ite_eq_right_iff]
-
-lemma expect_apply_ne_zero_iff_eq_zero [Finite α] : 𝔼 ψ : AddChar α ℂ, ψ a ≠ 0 ↔ a = 0 :=
-  expect_apply_eq_zero_iff_ne_zero.not_left
-
-end AddChar
diff --git a/LeanAPAP/Prereqs/Bohr/Arc.lean b/LeanAPAP/Prereqs/Bohr/Arc.lean
index 411f70f308..f34f95884b 100644
--- a/LeanAPAP/Prereqs/Bohr/Arc.lean
+++ b/LeanAPAP/Prereqs/Bohr/Arc.lean
@@ -1,5 +1,4 @@
 import Mathlib.Analysis.Complex.Angle
-import LeanAPAP.Prereqs.AddChar.PontryaginDuality
 import LeanAPAP.Prereqs.Bohr.Basic
 
 /- ### Arc Bohr sets -/
diff --git a/LeanAPAP/Prereqs/Bohr/Basic.lean b/LeanAPAP/Prereqs/Bohr/Basic.lean
index 9ee0f08479..7ca3a9adcb 100644
--- a/LeanAPAP/Prereqs/Bohr/Basic.lean
+++ b/LeanAPAP/Prereqs/Bohr/Basic.lean
@@ -1,5 +1,5 @@
 import Mathlib.Analysis.Complex.Basic
-import LeanAPAP.Prereqs.AddChar.PontryaginDuality
+import Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality
 
 open AddChar Function
 open scoped NNReal ENNReal Finset
diff --git a/LeanAPAP/Prereqs/Chang.lean b/LeanAPAP/Prereqs/Chang.lean
index b6dbc02282..f8d6715cd7 100644
--- a/LeanAPAP/Prereqs/Chang.lean
+++ b/LeanAPAP/Prereqs/Chang.lean
@@ -175,7 +175,7 @@ lemma chang (hf : f ≠ 0) (hη : 0 < η) :
   set β := ⌈𝓛 α⌉₊
   have hβ : 0 < β := Nat.ceil_pos.2 (curlog_pos (by positivity) $ α_le_one _)
   have : 0 < ‖f‖_[1] := by positivity
-  refine le_of_pow_le_pow_left hβ.ne' zero_le' $ Nat.cast_le.1 $ le_of_mul_le_mul_right ?_
+  refine le_of_pow_le_pow_left₀ hβ.ne' zero_le' $ Nat.cast_le.1 $ le_of_mul_le_mul_right ?_
     (by positivity : 0 < #Δ ^ β * (η ^ (2 * β) * α))
   push_cast
   rw [← mul_assoc, ← pow_add, ← two_mul]
diff --git a/LeanAPAP/Prereqs/Convolution/Compact.lean b/LeanAPAP/Prereqs/Convolution/Compact.lean
index 025cf85d6c..d933e9645e 100644
--- a/LeanAPAP/Prereqs/Convolution/Compact.lean
+++ b/LeanAPAP/Prereqs/Convolution/Compact.lean
@@ -30,7 +30,7 @@ point in time.
 -/
 
 open Finset Fintype Function
-open scoped BigOperators ComplexConjugate NNReal Pointwise
+open scoped BigOperators ComplexConjugate NNReal Pointwise translate
 
 local notation a " /ℚ " q => (q : ℚ≥0)⁻¹ • a
 
diff --git a/LeanAPAP/Prereqs/Convolution/Discrete/Basic.lean b/LeanAPAP/Prereqs/Convolution/Discrete/Basic.lean
index 1a343be73b..1f7c5e70ef 100644
--- a/LeanAPAP/Prereqs/Convolution/Discrete/Basic.lean
+++ b/LeanAPAP/Prereqs/Convolution/Discrete/Basic.lean
@@ -37,7 +37,7 @@ Multiplicativise? Probably ugly and not very useful.
 local notation:70 s:70 " ^^ " n:71 => Fintype.piFinset fun _ : Fin n ↦ s
 
 open Finset Fintype Function
-open scoped BigOperators ComplexConjugate NNReal Pointwise
+open scoped BigOperators ComplexConjugate NNReal Pointwise translate
 
 variable {G R γ : Type*} [Fintype G] [DecidableEq G] [AddCommGroup G]
 
diff --git a/LeanAPAP/Prereqs/Convolution/Discrete/Defs.lean b/LeanAPAP/Prereqs/Convolution/Discrete/Defs.lean
index 58c9e2baaa..e6b1e8cc8f 100644
--- a/LeanAPAP/Prereqs/Convolution/Discrete/Defs.lean
+++ b/LeanAPAP/Prereqs/Convolution/Discrete/Defs.lean
@@ -1,6 +1,6 @@
+import Mathlib.Algebra.Group.Translate
 import Mathlib.Algebra.Star.Conjneg
 import Mathlib.Analysis.Complex.Basic
-import LeanAPAP.Prereqs.Function.Translate
 
 /-!
 # Convolution
@@ -33,7 +33,7 @@ Multiplicativise? Probably ugly and not very useful.
 -/
 
 open Finset Fintype Function
-open scoped ComplexConjugate NNReal Pointwise NNRat
+open scoped ComplexConjugate NNReal Pointwise translate
 
 variable {G H R S : Type*} [DecidableEq G] [AddCommGroup G]
 
diff --git a/LeanAPAP/Prereqs/Convolution/Norm.lean b/LeanAPAP/Prereqs/Convolution/Norm.lean
index fb96931636..b31507e7ef 100644
--- a/LeanAPAP/Prereqs/Convolution/Norm.lean
+++ b/LeanAPAP/Prereqs/Convolution/Norm.lean
@@ -12,7 +12,7 @@ convolution inequality.
 -/
 
 open Finset Function MeasureTheory RCLike Real
-open scoped ComplexConjugate ENNReal NNReal Pointwise
+open scoped ComplexConjugate ENNReal NNReal Pointwise translate
 
 variable {ι 𝕜 : Type*} [Fintype ι] [DecidableEq ι] [AddCommGroup ι]
 
diff --git a/LeanAPAP/Prereqs/Energy.lean b/LeanAPAP/Prereqs/Energy.lean
index 4cab0bffed..5d4d108705 100644
--- a/LeanAPAP/Prereqs/Energy.lean
+++ b/LeanAPAP/Prereqs/Energy.lean
@@ -1,4 +1,3 @@
-import LeanAPAP.Prereqs.AddChar.Basic
 import LeanAPAP.Prereqs.Convolution.Discrete.Basic
 import LeanAPAP.Prereqs.FourierTransform.Discrete
 import LeanAPAP.Prereqs.Function.Indicator.Complex
diff --git a/LeanAPAP/Prereqs/FourierTransform/Compact.lean b/LeanAPAP/Prereqs/FourierTransform/Compact.lean
index e5ffd3fc1e..3872283903 100644
--- a/LeanAPAP/Prereqs/FourierTransform/Compact.lean
+++ b/LeanAPAP/Prereqs/FourierTransform/Compact.lean
@@ -52,7 +52,7 @@ lemma cft_apply (f : α → ℂ) (ψ : AddChar α ℂ) : cft f ψ = ⟪ψ, f⟫
 /-- **Parseval-Plancherel identity** for the discrete Fourier transform. -/
 @[simp] lemma dL2Norm_cft [MeasurableSpace α] [DiscreteMeasurableSpace α] (f : α → ℂ) :
     ‖cft f‖_[2] = ‖f‖ₙ_[2] :=
-  (sq_eq_sq (zero_le _) (zero_le _)).1 $ NNReal.coe_injective $ Complex.ofReal_injective $ by
+  (sq_eq_sq₀ (zero_le _) (zero_le _)).1 $ NNReal.coe_injective $ Complex.ofReal_injective $ by
     push_cast; simpa only [RCLike.wInner_cWeight_self, wInner_one_self] using wInner_one_cft f f
 
 /-- **Fourier inversion** for the discrete Fourier transform. -/
@@ -156,7 +156,7 @@ lemma cft_cdconv (f g : α → ℂ) : cft (f ○ₙ g) = cft f * conj (cft g) :=
 -- lemma dL2Norm_iterCconv (f : α → ℂ) (n : ℕ) : ‖f ∗^ₙ n‖ₙ_[2] = ‖f ^ n‖_[2] := by
 --   rw [← dL2Norm_cft, cft_iterCconv, ← ENNReal.coe_two, dLpNorm_pow]
 --   norm_cast
---   refine (sq_eq_sq (by positivity) $ by positivity).1 ?_
+--   refine (sq_eq_sq₀ (by positivity) $ by positivity).1 ?_
 --   rw [← ENNReal.coe_two, dLpNorm_pow, ← pow_mul', ← Complex.ofReal_inj]
 --   push_cast
 --   simp_rw [pow_mul, ← Complex.mul_conj', conj_iterConv_apply, mul_pow]
diff --git a/LeanAPAP/Prereqs/FourierTransform/Convolution.lean b/LeanAPAP/Prereqs/FourierTransform/Convolution.lean
index e43e869a2a..095d422cdd 100644
--- a/LeanAPAP/Prereqs/FourierTransform/Convolution.lean
+++ b/LeanAPAP/Prereqs/FourierTransform/Convolution.lean
@@ -1,4 +1,4 @@
-import LeanAPAP.Prereqs.AddChar.PontryaginDuality
+import Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality
 import LeanAPAP.Prereqs.Convolution.Compact
 import LeanAPAP.Prereqs.Function.Indicator.Defs
 import LeanAPAP.Prereqs.Inner.Hoelder.Compact
@@ -16,7 +16,7 @@ set_option pp.piBinderTypes false
 
 lemma cLpNorm_cconv_le_cLpNorm_cdconv (hn₀ : n ≠ 0) (hn : Even n) (f : G → ℂ) :
     ‖f ∗ₙ f‖ₙ_[n] ≤ ‖f ○ₙ f‖ₙ_[n] := by
-  refine le_of_pow_le_pow_left hn₀ (by positivity) ?_
+  refine le_of_pow_le_pow_left₀ hn₀ (by positivity) ?_
   obtain ⟨k, rfl⟩ := hn.two_dvd
   simp only [ne_eq, mul_eq_zero, OfNat.ofNat_ne_zero, false_or] at hn₀
   refine Complex.le_of_eq_sum_of_eq_sum_norm (fun ψ : (Fin k → AddChar G ℂ) × (Fin k → AddChar G ℂ)
diff --git a/LeanAPAP/Prereqs/FourierTransform/Discrete.lean b/LeanAPAP/Prereqs/FourierTransform/Discrete.lean
index 0a677f1897..94f156140e 100644
--- a/LeanAPAP/Prereqs/FourierTransform/Discrete.lean
+++ b/LeanAPAP/Prereqs/FourierTransform/Discrete.lean
@@ -1,7 +1,8 @@
 import Mathlib.Algebra.BigOperators.Balance
+import Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality
 import Mathlib.MeasureTheory.Constructions.AddChar
-import LeanAPAP.Prereqs.AddChar.PontryaginDuality
 import LeanAPAP.Prereqs.Convolution.Discrete.Defs
+import LeanAPAP.Prereqs.Function.Dilate
 import LeanAPAP.Prereqs.Function.Indicator.Defs
 import LeanAPAP.Prereqs.Inner.Hoelder.Compact
 
@@ -13,7 +14,7 @@ Fourier inversion formula for it.
 -/
 
 open AddChar Finset Fintype Function MeasureTheory RCLike
-open scoped BigOperators ComplexConjugate ComplexOrder
+open scoped BigOperators ComplexConjugate ComplexOrder translate
 
 variable {α γ : Type*} [AddCommGroup α] [Fintype α] {f : α → ℂ} {ψ : AddChar α ℂ} {n : ℕ}
 
@@ -53,7 +54,7 @@ lemma dft_smul {𝕝 : Type*} [CommSemiring 𝕝] [StarRing 𝕝] [Algebra 𝕝
 /-- **Parseval-Plancherel identity** for the discrete Fourier transform. -/
 @[simp] lemma cL2Norm_dft [MeasurableSpace α] [DiscreteMeasurableSpace α] (f : α → ℂ) :
     ‖dft f‖ₙ_[2] = ‖f‖_[2] :=
-  (sq_eq_sq (zero_le _) (zero_le _)).1 $ NNReal.coe_injective $ Complex.ofReal_injective $ by
+  (sq_eq_sq₀ (zero_le _) (zero_le _)).1 $ NNReal.coe_injective $ Complex.ofReal_injective $ by
     push_cast; simpa only [RCLike.wInner_cWeight_self, wInner_one_self] using wInner_cWeight_dft f f
 
 /-- **Fourier inversion** for the discrete Fourier transform. -/
diff --git a/LeanAPAP/Prereqs/Function/Dilate.lean b/LeanAPAP/Prereqs/Function/Dilate.lean
new file mode 100644
index 0000000000..945fdd0dab
--- /dev/null
+++ b/LeanAPAP/Prereqs/Function/Dilate.lean
@@ -0,0 +1,16 @@
+import Mathlib.Algebra.Star.SelfAdjoint
+import Mathlib.Data.ZMod.Basic
+
+/-!
+# Dilation operator
+-/
+
+variable {G 𝕜 : Type*} [AddCommGroup G]
+
+noncomputable def dilate (f : G → 𝕜) (n : ℕ) : G → 𝕜 :=
+  fun a ↦ f ((n⁻¹ : ZMod (Nat.card G)).val • a)
+
+variable [Star 𝕜] {f : G → 𝕜}
+
+protected lemma IsSelfAdjoint.dilate (hf : IsSelfAdjoint f) (n : ℕ) : IsSelfAdjoint (dilate f n) :=
+  Pi.isSelfAdjoint.2 fun _g ↦ hf.apply _
diff --git a/LeanAPAP/Prereqs/Function/Indicator/Basic.lean b/LeanAPAP/Prereqs/Function/Indicator/Basic.lean
index 2807a8554e..0bb463372b 100644
--- a/LeanAPAP/Prereqs/Function/Indicator/Basic.lean
+++ b/LeanAPAP/Prereqs/Function/Indicator/Basic.lean
@@ -1,14 +1,14 @@
 import Mathlib.Algebra.AddTorsor
 import Mathlib.Algebra.BigOperators.Expect
+import Mathlib.Algebra.Group.Translate
 import Mathlib.Algebra.Star.Conjneg
 import Mathlib.Data.Fintype.Lattice
 import Mathlib.Data.NNRat.Order
-import LeanAPAP.Prereqs.Function.Translate
 import LeanAPAP.Prereqs.Function.Indicator.Defs
 
 open Finset Function
 open Fintype (card)
-open scoped BigOperators ComplexConjugate Pointwise
+open scoped BigOperators ComplexConjugate Pointwise translate
 
 local notation a " /ℚ " q => (q : ℚ≥0)⁻¹ • a
 
diff --git a/LeanAPAP/Prereqs/Function/Translate.lean b/LeanAPAP/Prereqs/Function/Translate.lean
deleted file mode 100644
index d7f939aa0f..0000000000
--- a/LeanAPAP/Prereqs/Function/Translate.lean
+++ /dev/null
@@ -1,83 +0,0 @@
-import Mathlib.Algebra.BigOperators.Pi
-import Mathlib.Algebra.Star.SelfAdjoint
-import Mathlib.Data.ZMod.Basic
-
-/-!
-# Precomposition operators
--/
-
-open Function Set
-open scoped ComplexConjugate Pointwise
-
-/-! ### Translation operator -/
-
-section translate
-variable {ι α β γ : Type*} [AddCommGroup α]
-
-def translate (a : α) (f : α → β) : α → β := fun x ↦ f (x - a)
-
-notation "τ " => translate
-
-@[simp] lemma translate_apply (a : α) (f : α → β) (x : α) : τ a f x = f (x - a) := rfl
-@[simp] lemma translate_zero (f : α → β) : τ 0 f = f := by ext; simp
-
-lemma translate_translate (a b : α) (f : α → β) : τ a (τ b f) = τ (a + b) f := by
-  ext; simp [sub_sub]
-
-lemma translate_add (a b : α) (f : α → β) : τ (a + b) f = τ a (τ b f) := by ext; simp [sub_sub]
-
-lemma translate_add' (a b : α) (f : α → β) : τ (a + b) f = τ b (τ a f) := by
-  rw [add_comm, translate_add]
-
-lemma translate_comm (a b : α) (f : α → β) : τ a (τ b f) = τ b (τ a f) := by
-  rw [← translate_add, translate_add']
-
-@[simp] lemma comp_translate (a : α) (f : α → β) (g : β → γ) : g ∘ τ a f = τ a (g ∘ f) := rfl
-
-@[simp]
-lemma translate_smul_right [SMul γ β] (a : α) (f : α → β) (c : γ) : τ a (c • f) = c • τ a f := rfl
-
-section AddCommMonoid
-variable [AddCommMonoid β]
-
-@[simp] lemma translate_zero_right (a : α) : τ a (0 : α → β) = 0 := rfl
-
-lemma translate_add_right (a : α) (f g : α → β) : τ a (f + g) = τ a f + τ a g := rfl
-
-lemma translate_sum_right (a : α) (f : ι → α → β) (s : Finset ι) :
-    τ a (∑ i in s, f i) = ∑ i in s, τ a (f i) := by ext; simp
-
-lemma sum_translate [Fintype α] (a : α) (f : α → β) : ∑ b, τ a f b = ∑ b, f b :=
-  Fintype.sum_equiv (Equiv.subRight _) _ _ fun _ ↦ rfl
-
-end AddCommMonoid
-
-section AddCommGroup
-variable [AddCommGroup β]
-
-lemma translate_sub_right (a : α) (f g : α → β) : τ a (f - g) = τ a f - τ a g := rfl
-lemma translate_neg_right (a : α) (f : α → β) : τ a (-f) = -τ a f := rfl
-
-@[simp] lemma support_translate (a : α) (f : α → β) : support (τ a f) = a +ᵥ support f := by
-  ext; simp [mem_vadd_set_iff_neg_vadd_mem, sub_eq_neg_add]
-
-end AddCommGroup
-
-variable [CommRing β]
-
-lemma translate_prod_right (a : α) (f : ι → α → β) (s : Finset ι) :
-    τ a (∏ i in s, f i) = ∏ i in s, τ a (f i) := by ext; simp
-
-end translate
-
-open Fintype
-
-variable {α β G 𝕜 : Type*} [AddCommGroup G]
-
-noncomputable def dilate (f : G → 𝕜) (n : ℕ) : G → 𝕜 :=
-  fun a ↦ f ((n⁻¹ : ZMod (Nat.card G)).val • a)
-
-variable [Star 𝕜] {f : G → 𝕜}
-
-protected lemma IsSelfAdjoint.dilate (hf : IsSelfAdjoint f) (n : ℕ) : IsSelfAdjoint (dilate f n) :=
-  Pi.isSelfAdjoint.2 fun _g ↦ hf.apply _
diff --git a/LeanAPAP/Prereqs/LpNorm/Compact.lean b/LeanAPAP/Prereqs/LpNorm/Compact.lean
index 84641d613b..72f3f79f60 100644
--- a/LeanAPAP/Prereqs/LpNorm/Compact.lean
+++ b/LeanAPAP/Prereqs/LpNorm/Compact.lean
@@ -1,7 +1,7 @@
+import Mathlib.Algebra.Group.Translate
 import Mathlib.Algebra.Star.Conjneg
 import Mathlib.Data.Fintype.Order
 import LeanAPAP.Prereqs.Function.Indicator.Defs
-import LeanAPAP.Prereqs.Function.Translate
 import LeanAPAP.Prereqs.NNLpNorm
 
 /-!
@@ -11,7 +11,7 @@ import LeanAPAP.Prereqs.NNLpNorm
 open Finset hiding card
 open Function ProbabilityTheory Real
 open Fintype (card)
-open scoped BigOperators ComplexConjugate ENNReal NNReal
+open scoped BigOperators ComplexConjugate ENNReal NNReal translate
 
 local notation:70 s:70 " ^^ " n:71 => Fintype.piFinset fun _ : Fin n ↦ s
 
diff --git a/LeanAPAP/Prereqs/LpNorm/Discrete/Basic.lean b/LeanAPAP/Prereqs/LpNorm/Discrete/Basic.lean
index 610ebb43c4..4537d151f2 100644
--- a/LeanAPAP/Prereqs/LpNorm/Discrete/Basic.lean
+++ b/LeanAPAP/Prereqs/LpNorm/Discrete/Basic.lean
@@ -1,6 +1,6 @@
+import Mathlib.Algebra.Group.Translate
 import Mathlib.Algebra.Star.Conjneg
 import LeanAPAP.Prereqs.Function.Indicator.Defs
-import LeanAPAP.Prereqs.Function.Translate
 import LeanAPAP.Prereqs.LpNorm.Discrete.Defs
 
 /-!
@@ -8,7 +8,7 @@ import LeanAPAP.Prereqs.LpNorm.Discrete.Defs
 -/
 
 open Finset Function Real
-open scoped BigOperators ComplexConjugate ENNReal NNReal
+open scoped BigOperators ComplexConjugate ENNReal NNReal translate
 
 namespace MeasureTheory
 variable {ι G 𝕜 E R : Type*} [Fintype ι] {mι : MeasurableSpace ι} [DiscreteMeasurableSpace ι]
diff --git a/LeanAPAP/Prereqs/LpNorm/Weighted.lean b/LeanAPAP/Prereqs/LpNorm/Weighted.lean
index ab6de63804..6a039f90df 100644
--- a/LeanAPAP/Prereqs/LpNorm/Weighted.lean
+++ b/LeanAPAP/Prereqs/LpNorm/Weighted.lean
@@ -1,5 +1,5 @@
+import Mathlib.Algebra.Group.Translate
 import Mathlib.Algebra.Star.Conjneg
-import LeanAPAP.Prereqs.Function.Translate
 import LeanAPAP.Prereqs.LpNorm.Discrete.Defs
 
 /-!
@@ -7,7 +7,7 @@ import LeanAPAP.Prereqs.LpNorm.Discrete.Defs
 -/
 
 open Finset Function Real MeasureTheory
-open scoped ComplexConjugate ENNReal NNReal
+open scoped ComplexConjugate ENNReal NNReal translate
 
 variable {α 𝕜 E : Type*} [MeasurableSpace α]
 
diff --git a/LeanAPAP/Prereqs/Randomisation.lean b/LeanAPAP/Prereqs/Randomisation.lean
deleted file mode 100644
index a5a24e469d..0000000000
--- a/LeanAPAP/Prereqs/Randomisation.lean
+++ /dev/null
@@ -1,37 +0,0 @@
-import Mathlib.Combinatorics.Additive.Dissociation
-import LeanAPAP.Prereqs.AddChar.Basic
-
-/-!
-# Randomisation
--/
-
-open Finset
-open scoped BigOperators ComplexConjugate
-
-variable {α : Type*} [Fintype α] [AddCommGroup α] {p : ℕ}
-
-/-- A function of dissociated support can be randomised. -/
-lemma AddDissociated.randomisation (c : AddChar α ℂ → ℝ) (d : AddChar α ℂ → ℂ)
-    (hcd : AddDissociated {ψ | d ψ ≠ 0}) : 𝔼 a, ∏ ψ, (c ψ + (d ψ * ψ a).re) = ∏ ψ, c ψ := by
-  refine Complex.ofReal_injective ?_
-  push_cast
-  calc
-    _ = ∑ t, (𝔼 a, ∏ ψ ∈ t, ((d ψ * ψ a) + conj (d ψ * ψ a)) / 2) * ∏ ψ ∈ tᶜ, (c ψ : ℂ) := by
-        simp_rw [expect_mul, ← expect_sum_comm, ← Fintype.prod_add, add_comm,
-          Complex.re_eq_add_conj]
-    _ = (𝔼 a, ∏ ψ ∈ ∅, ((d ψ * ψ a) + conj (d ψ * ψ a)) / 2) * ∏ ψ ∈ ∅ᶜ, (c ψ : ℂ) :=
-        Fintype.sum_eq_single ∅ fun t ht ↦ mul_eq_zero_of_left ?_ _
-    _ = _ := by simp
-  simp only [map_mul, prod_div_distrib, prod_add, prod_const, ← expect_div, expect_sum_comm,
-    div_eq_zero_iff, pow_eq_zero_iff', OfNat.ofNat_ne_zero, ne_eq, card_eq_zero, compl_eq_empty_iff,
-    false_and, or_false]
-  refine sum_eq_zero fun u _ ↦ ?_
-  calc
-    𝔼 a, (∏ ψ ∈ u, d ψ * ψ a) * ∏ ψ ∈ t \ u, conj (d ψ) * conj (ψ a)
-      = ((∏ ψ ∈ u, d ψ) * ∏ ψ ∈ t \ u, conj (d ψ)) * 𝔼 a, (∑ ψ ∈ u, ψ - ∑ ψ ∈ t \ u, ψ) a := by
-        simp_rw [mul_expect, AddChar.sub_apply, AddChar.sum_apply, mul_mul_mul_comm,
-          ← prod_mul_distrib, AddChar.map_neg_eq_conj]
-    _ = 0 := ?_
-  rw [mul_eq_zero, AddChar.expect_eq_zero_iff_ne_zero, sub_ne_zero, or_iff_not_imp_left, ← Ne,
-    mul_ne_zero_iff, prod_ne_zero_iff, prod_ne_zero_iff]
-  exact fun h ↦ hcd.ne h.1 (by simpa only [map_ne_zero] using h.2) (sdiff_ne_right.2 $ .inl ht).symm
diff --git a/LeanAPAP/Prereqs/Rudin.lean b/LeanAPAP/Prereqs/Rudin.lean
index 405c8fc81e..fa95586b2c 100644
--- a/LeanAPAP/Prereqs/Rudin.lean
+++ b/LeanAPAP/Prereqs/Rudin.lean
@@ -1,7 +1,7 @@
 import Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
 import Mathlib.Analysis.SpecialFunctions.Trigonometric.Series
+import Mathlib.Combinatorics.Additive.Randomisation
 import LeanAPAP.Prereqs.FourierTransform.Compact
-import LeanAPAP.Prereqs.Randomisation
 
 /-!
 # Rudin's inequality
@@ -85,7 +85,7 @@ private lemma rudin_ineq_aux (hp : 2 ≤ p) (f : α → ℂ) (hf : AddDissociate
       _ ≤ 2 ^ p * exp (‖f‖ₙ_[2] ^ 2 / 2) := by gcongr; exact le_self_pow₀ one_le_two hp₀
       _ = (2 * exp 2⁻¹) ^ p := by
           rw [hfp, sq_sqrt, mul_pow, ← exp_nsmul, nsmul_eq_mul, div_eq_mul_inv]; positivity
-  refine le_of_pow_le_pow_left hp₀ (by positivity) ?_
+  refine le_of_pow_le_pow_left₀ hp₀ (by positivity) ?_
   rwa [hfp, mul_assoc, mul_self_sqrt, mul_pow, ← div_le_iff₀, ← div_pow]
   all_goals positivity
 
diff --git a/lake-manifest.json b/lake-manifest.json
index 633613a339..5a0fe5a20e 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "af731107d531b39cd7278c73f91c573f40340612",
+   "rev": "b100ff2565805e9f30a482788b3fc66937a7f38a",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -25,7 +25,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "5dfdc66e0d503631527ad90c1b5d7815c86a8662",
+   "rev": "de91b59101763419997026c35a41432ac8691f15",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -55,7 +55,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "ac7b989cbf99169509433124ae484318e953d201",
+   "rev": "b0b73e5bc33f1bc4d3c0f254630dd0e262cecc08",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -85,7 +85,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "62a2cc31bac6416736c17a57383a622c208f21cb",
+   "rev": "79635cf94d5bbd65851b5e47c0149c7e58f1b73a",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,
@@ -105,7 +105,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "b41bc9cec7f433d6e1d74ff3b59edaaf58ad2915",
+   "rev": "2905ab4ec3961d1fd68ddae0ab4083497e579014",
    "name": "UnicodeBasic",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -125,7 +125,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "e18c6c23dd7cb1f12d79d6304262351df943aa37",
+   "rev": "7b6a56e8e4fcf54d3834b225b9814a7c9e4d4bda",
    "name": "«doc-gen4»",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",