diff --git a/LeanAPAP.lean b/LeanAPAP.lean
index 4b76501882..d92e87adf4 100644
--- a/LeanAPAP.lean
+++ b/LeanAPAP.lean
@@ -1,14 +1,11 @@
 import LeanAPAP.Extras.BSG
 import LeanAPAP.FiniteField.Basic
-import LeanAPAP.Mathlib.Algebra.Algebra.Rat
 import LeanAPAP.Mathlib.Algebra.Group.AddChar
 import LeanAPAP.Mathlib.Algebra.Order.Group.Unbundled.Basic
 import LeanAPAP.Mathlib.Algebra.Star.Rat
 import LeanAPAP.Mathlib.Analysis.Complex.Basic
-import LeanAPAP.Mathlib.Analysis.Normed.Field.Basic
 import LeanAPAP.Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar
 import LeanAPAP.Mathlib.Analysis.SpecialFunctions.Pow.NNReal
-import LeanAPAP.Mathlib.Data.Real.Sqrt
 import LeanAPAP.Mathlib.MeasureTheory.Function.EssSup
 import LeanAPAP.Mathlib.MeasureTheory.Function.LpSeminorm.Basic
 import LeanAPAP.Mathlib.Order.ConditionallyCompleteLattice.Basic
@@ -50,4 +47,5 @@ import LeanAPAP.Prereqs.LpNorm.Discrete.Inner
 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/Algebra/Algebra/Rat.lean b/LeanAPAP/Mathlib/Algebra/Algebra/Rat.lean
deleted file mode 100644
index 83976519bd..0000000000
--- a/LeanAPAP/Mathlib/Algebra/Algebra/Rat.lean
+++ /dev/null
@@ -1,30 +0,0 @@
-import Mathlib.Algebra.Algebra.Rat
-import Mathlib.Algebra.Module.Basic
-
-variable {α β : Type*}
-
-instance [Monoid α] [AddCommMonoid β] [Module ℚ≥0 β] [DistribMulAction α β] :
-    SMulCommClass ℚ≥0 α β where
-  smul_comm q a b := by
-    rw [← q.num_div_den, div_eq_mul_inv]
-    simp_rw [mul_smul, inv_natCast_smul_comm, Nat.cast_smul_eq_nsmul]
-    rw [smul_comm a q.num]
-
-instance [Monoid α] [AddCommMonoid β] [Module ℚ≥0 β] [DistribMulAction α β] :
-    SMulCommClass α ℚ≥0 β := .symm ..
-
-instance [Semiring α] [Module ℚ≥0 α] : IsScalarTower ℚ≥0 α α where
-  smul_assoc q a b := sorry
-
-instance [Monoid α] [AddCommGroup β] [Module ℚ β] [DistribMulAction α β] :
-    SMulCommClass ℚ α β where
-  smul_comm q a b := by
-    rw [← q.num_div_den, div_eq_mul_inv]
-    simp_rw [mul_smul, inv_natCast_smul_comm, Int.cast_smul_eq_zsmul]
-    rw [smul_comm a q.num]
-
-instance [Monoid α] [AddCommGroup β] [Module ℚ β] [DistribMulAction α β] : SMulCommClass α ℚ β :=
-  .symm ..
-
-instance [Ring α] [Module ℚ α] : IsScalarTower ℚ α α where
-  smul_assoc q a b := sorry
diff --git a/LeanAPAP/Mathlib/Analysis/Normed/Field/Basic.lean b/LeanAPAP/Mathlib/Analysis/Normed/Field/Basic.lean
deleted file mode 100644
index 68d51f52ba..0000000000
--- a/LeanAPAP/Mathlib/Analysis/Normed/Field/Basic.lean
+++ /dev/null
@@ -1,18 +0,0 @@
-import Mathlib.Analysis.Normed.Field.Basic
-
-variable {R : Type*} [SeminormedRing R] {a b c : R}
-
-lemma norm_one_sub_mul (ha : ‖a‖ ≤ 1) : ‖c - a * b‖ ≤ ‖c - a‖ + ‖1 - b‖ :=
-  calc
-    _ ≤ ‖c - a‖ + ‖a * (1 - b)‖ := by
-        simpa [mul_one_sub] using norm_sub_le_norm_sub_add_norm_sub c a (a * b)
-    _ ≤ ‖c - a‖ + ‖a‖ * ‖1 - b‖ := by gcongr; exact norm_mul_le ..
-    _ ≤ ‖c - a‖ + 1 * ‖1 - b‖ := by gcongr
-    _ = ‖c - a‖ + ‖1 - b‖ := by simp
-
-lemma norm_one_sub_mul' (hb : ‖b‖ ≤ 1) : ‖c - a * b‖ ≤ ‖1 - a‖ + ‖c - b‖ := by
-  rw [add_comm]; exact norm_one_sub_mul (R := Rᵐᵒᵖ) hb
-
-lemma nnnorm_one_sub_mul (ha : ‖a‖₊ ≤ 1) : ‖c - a * b‖₊ ≤ ‖c - a‖₊ + ‖1 - b‖₊ := norm_one_sub_mul ha
-lemma nnnorm_one_sub_mul' (hb : ‖b‖₊ ≤ 1) : ‖c - a * b‖₊ ≤ ‖1 - a‖₊ + ‖c - b‖₊ :=
-  norm_one_sub_mul' hb
diff --git a/LeanAPAP/Mathlib/Data/Real/Sqrt.lean b/LeanAPAP/Mathlib/Data/Real/Sqrt.lean
deleted file mode 100644
index a17c6c4a35..0000000000
--- a/LeanAPAP/Mathlib/Data/Real/Sqrt.lean
+++ /dev/null
@@ -1,7 +0,0 @@
-import Mathlib.Data.Real.Sqrt
-
-namespace Real
-
-attribute [simp] sqrt_nonneg
-
-end Real
diff --git a/LeanAPAP/Physics/AlmostPeriodicity.lean b/LeanAPAP/Physics/AlmostPeriodicity.lean
index 48cf2f151e..4a526b6834 100644
--- a/LeanAPAP/Physics/AlmostPeriodicity.lean
+++ b/LeanAPAP/Physics/AlmostPeriodicity.lean
@@ -4,6 +4,7 @@ import Mathlib.Data.Complex.ExponentialBounds
 import LeanAPAP.Prereqs.Convolution.Discrete.Basic
 import LeanAPAP.Prereqs.Convolution.Norm
 import LeanAPAP.Prereqs.Curlog
+import LeanAPAP.Prereqs.Expect.Complex
 import LeanAPAP.Prereqs.MarcinkiewiczZygmund
 
 /-!
diff --git a/LeanAPAP/Physics/Unbalancing.lean b/LeanAPAP/Physics/Unbalancing.lean
index 9ec716ad89..d9c8f2c394 100644
--- a/LeanAPAP/Physics/Unbalancing.lean
+++ b/LeanAPAP/Physics/Unbalancing.lean
@@ -1,6 +1,6 @@
 import Mathlib.Algebra.Order.Group.PosPart
 import Mathlib.Data.Complex.ExponentialBounds
-import LeanAPAP.Prereqs.Convolution.Discrete.Basic
+import LeanAPAP.Prereqs.Convolution.Discrete.Defs
 import LeanAPAP.Prereqs.LpNorm.Discrete.Inner
 import LeanAPAP.Prereqs.LpNorm.Weighted
 
diff --git a/LeanAPAP/Prereqs/Bohr/Basic.lean b/LeanAPAP/Prereqs/Bohr/Basic.lean
index 2e315007b3..08b05818d0 100644
--- a/LeanAPAP/Prereqs/Bohr/Basic.lean
+++ b/LeanAPAP/Prereqs/Bohr/Basic.lean
@@ -1,6 +1,5 @@
 import Mathlib.Analysis.Complex.Basic
 import LeanAPAP.Prereqs.AddChar.PontryaginDuality
-import LeanAPAP.Prereqs.Function.Translate
 
 open AddChar Function
 open scoped NNReal ENNReal
diff --git a/LeanAPAP/Prereqs/Convolution/Norm.lean b/LeanAPAP/Prereqs/Convolution/Norm.lean
index 317144285e..14f1d1e33a 100644
--- a/LeanAPAP/Prereqs/Convolution/Norm.lean
+++ b/LeanAPAP/Prereqs/Convolution/Norm.lean
@@ -1,8 +1,7 @@
 import Mathlib.Data.Real.StarOrdered
 import LeanAPAP.Prereqs.Convolution.Discrete.Defs
 import LeanAPAP.Prereqs.LpNorm.Discrete.Basic
-import LeanAPAP.Prereqs.Convolution.Order
-import LeanAPAP.Prereqs.LpNorm.Compact.Defs
+import LeanAPAP.Prereqs.LpNorm.Discrete.Inner
 
 /-!
 # Norm of a convolution
diff --git a/LeanAPAP/Prereqs/FourierTransform/Discrete.lean b/LeanAPAP/Prereqs/FourierTransform/Discrete.lean
index bd9aafe643..a2f98fefaf 100644
--- a/LeanAPAP/Prereqs/FourierTransform/Discrete.lean
+++ b/LeanAPAP/Prereqs/FourierTransform/Discrete.lean
@@ -1,8 +1,9 @@
 import LeanAPAP.Prereqs.AddChar.MeasurableSpace
 import LeanAPAP.Prereqs.AddChar.PontryaginDuality
+import LeanAPAP.Prereqs.Convolution.Discrete.Defs
+import LeanAPAP.Prereqs.Function.Indicator.Defs
 import LeanAPAP.Prereqs.LpNorm.Compact.Inner
 import LeanAPAP.Prereqs.LpNorm.Discrete.Inner
-import LeanAPAP.Prereqs.Convolution.Discrete.Defs
 
 /-!
 # Discrete Fourier transform
diff --git a/LeanAPAP/Prereqs/LpNorm/Compact/Defs.lean b/LeanAPAP/Prereqs/LpNorm/Compact/Defs.lean
index 412bb3f389..ecb654ec92 100644
--- a/LeanAPAP/Prereqs/LpNorm/Compact/Defs.lean
+++ b/LeanAPAP/Prereqs/LpNorm/Compact/Defs.lean
@@ -1,8 +1,7 @@
 import Mathlib.Data.Finset.Density
 import Mathlib.Probability.ConditionalProbability
-import LeanAPAP.Prereqs.LpNorm.Discrete.Basic
-import LeanAPAP.Prereqs.LpNorm.Discrete.Inner
 import LeanAPAP.Prereqs.Expect.Complex
+import LeanAPAP.Prereqs.NNLpNorm
 
 /-!
 # Normalised Lp norms
diff --git a/LeanAPAP/Prereqs/LpNorm/Compact/Inner.lean b/LeanAPAP/Prereqs/LpNorm/Compact/Inner.lean
index 5f07874414..492b40c819 100644
--- a/LeanAPAP/Prereqs/LpNorm/Compact/Inner.lean
+++ b/LeanAPAP/Prereqs/LpNorm/Compact/Inner.lean
@@ -1,8 +1,8 @@
 import Mathlib.Analysis.InnerProductSpace.PiL2
-import LeanAPAP.Mathlib.Algebra.Algebra.Rat
 import LeanAPAP.Mathlib.Algebra.Star.Rat
 import LeanAPAP.Prereqs.Expect.Complex
 import LeanAPAP.Prereqs.LpNorm.Compact.Defs
+import LeanAPAP.Prereqs.LpNorm.Discrete.Inner
 
 /-! # Inner product -/
 
diff --git a/LeanAPAP/Prereqs/LpNorm/Weighted.lean b/LeanAPAP/Prereqs/LpNorm/Weighted.lean
index 65ede55cf5..76eb388e9f 100644
--- a/LeanAPAP/Prereqs/LpNorm/Weighted.lean
+++ b/LeanAPAP/Prereqs/LpNorm/Weighted.lean
@@ -1,4 +1,5 @@
-import LeanAPAP.Prereqs.LpNorm.Discrete.Basic
+import LeanAPAP.Prereqs.Function.Translate
+import LeanAPAP.Prereqs.LpNorm.Discrete.Defs
 
 /-!
 # Lp norms
diff --git a/LeanAPAP/Prereqs/Randomisation.lean b/LeanAPAP/Prereqs/Randomisation.lean
new file mode 100644
index 0000000000..ead086fdb0
--- /dev/null
+++ b/LeanAPAP/Prereqs/Randomisation.lean
@@ -0,0 +1,38 @@
+import Mathlib.Combinatorics.Additive.Dissociation
+import LeanAPAP.Prereqs.AddChar.Basic
+import LeanAPAP.Prereqs.Expect.Complex
+
+/-!
+# 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 8578f2a5fd..741539d354 100644
--- a/LeanAPAP/Prereqs/Rudin.lean
+++ b/LeanAPAP/Prereqs/Rudin.lean
@@ -1,9 +1,8 @@
 import Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
 import Mathlib.Analysis.SpecialFunctions.Trigonometric.Series
-import Mathlib.Combinatorics.Additive.Dissociation
 import LeanAPAP.Mathlib.Analysis.Complex.Basic
-import LeanAPAP.Mathlib.Data.Real.Sqrt
 import LeanAPAP.Prereqs.FourierTransform.Compact
+import LeanAPAP.Prereqs.Randomisation
 
 /-!
 # Rudin's inequality
@@ -19,32 +18,6 @@ open scoped BigOperators Nat NNReal ENNReal ComplexConjugate ComplexOrder
 
 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
-
 variable [MeasurableSpace α] [DiscreteMeasurableSpace α]
 
 /-- **Rudin's inequality**, exponential form. -/
diff --git a/lake-manifest.json b/lake-manifest.json
index 83746084ff..10f41a1d42 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "a7fd140a94bbbfa40cf10839227bbb9e8492be2d",
+   "rev": "9c6c2d647e57b2b7a0b42dd8080c698bd33a1b6f",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -15,7 +15,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "d38fb94558af9957b8f479e350841ce65a1ec42c",
+   "rev": "9d0bdd07bdfe53383567509348b1fe917fc08de4",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -25,7 +25,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "6c89b6765913a0d727c1066493c3f5dc51c9713e",
+   "rev": "deb279eb7be16848d0bc8387f80d6e41bcdbe738",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -55,7 +55,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "0a756018b736ef4f4bc3c9a45fc03cf97a0b1a0c",
+   "rev": "1ef0b288623337cb37edd1222b9c26b4b77c6620",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -65,7 +65,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "63cced2a6b7c4ed2afb8e6cdf7443d6dbcc975e0",
+   "rev": "00df099f8ed42c12b35cdedcfbf1fde6c7413662",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,
@@ -85,7 +85,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "9447739fe9714f8a091192bad5cd5e7b5a8ae1e4",
+   "rev": "929690af200efb291babee737b087d244a70c3c3",
    "name": "UnicodeBasic",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -105,7 +105,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "83f718b9055972dce4f92f5b3917426b91a0d2fe",
+   "rev": "e490631b72a43a6a82b4ddd3a2d020b2029491d0",
    "name": "«doc-gen4»",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
diff --git a/lean-toolchain b/lean-toolchain
index 28b8e55a50..5a9c76dc98 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.11.0-rc3
+leanprover/lean4:v4.11.0