diff --git a/LeanAPAP.lean b/LeanAPAP.lean
index 9881d40d2a..69c32b9a5c 100644
--- a/LeanAPAP.lean
+++ b/LeanAPAP.lean
@@ -1,8 +1,6 @@
 import LeanAPAP.Extras.BSG
 import LeanAPAP.FiniteField
 import LeanAPAP.Integer
-import LeanAPAP.Mathlib.MeasureTheory.Function.LpSpace
-import LeanAPAP.Mathlib.MeasureTheory.Integral.Bochner
 import LeanAPAP.Physics.AlmostPeriodicity
 import LeanAPAP.Physics.DRC
 import LeanAPAP.Physics.Unbalancing
diff --git a/LeanAPAP/FiniteField.lean b/LeanAPAP/FiniteField.lean
index 2fd03ee82c..8d6bdc4849 100644
--- a/LeanAPAP/FiniteField.lean
+++ b/LeanAPAP/FiniteField.lean
@@ -461,8 +461,8 @@ theorem ff (hq₃ : 3 ≤ q) (hq : q.Prime) (hA₀ : A.Nonempty) (hA : ThreeAPFr
       (B.dens < (65 / 64 : ℝ) ^ i * α →
         2⁻¹ ≤ card V * ⟪μ_[ℝ] B ∗ μ B, μ (B.image (2 • ·))⟫_[ℝ]) := by
     induction' i with i ih hi
-    · exact ⟨G, inferInstance, inferInstance, inferInstance, inferInstance, A, by simp, hA,
-        by simp, by simp [α, nnratCast_dens, Fintype.card_subtype, subset_iff]⟩
+    · exact ⟨G, inferInstance, inferInstance, inferInstance, inferInstance, A, by simp [n], hA,
+        by simp [α], by simp [α, nnratCast_dens, Fintype.card_subtype, subset_iff]⟩
     obtain ⟨V, _, _, _, _, B, hV, hB, hαβ, hBV⟩ := ih
     obtain hB' | hB' := le_or_lt 2⁻¹ (card V * ⟪μ_[ℝ] B ∗ μ B, μ (B.image (2 • ·))⟫_[ℝ])
     · exact ⟨V, inferInstance, inferInstance, inferInstance, inferInstance, B,
@@ -486,7 +486,7 @@ theorem ff (hq₃ : 3 ≤ q) (hq : q.Prime) (hA₀ : A.Nonempty) (hA : ThreeAPFr
         _ ≤ ‖(𝟭_[ℝ] B ∗ μ (V' : Set V).toFinset) x‖ := hx
         _ = B'.dens := ?_
       rw [mu, conv_smul, Pi.smul_apply, indicate_conv_indicate_eq_card_vadd_inter_neg,
-        norm_of_nonneg (by positivity), nnratCast_dens, card_preimage, smul_eq_mul, inv_mul_eq_div]
+        Real.norm_of_nonneg (by positivity), nnratCast_dens, card_preimage, smul_eq_mul, inv_mul_eq_div]
       congr 2
       · congr 1 with x
         simp
diff --git a/LeanAPAP/Mathlib/MeasureTheory/Function/LpSpace.lean b/LeanAPAP/Mathlib/MeasureTheory/Function/LpSpace.lean
deleted file mode 100644
index 0a3127129c..0000000000
--- a/LeanAPAP/Mathlib/MeasureTheory/Function/LpSpace.lean
+++ /dev/null
@@ -1,8 +0,0 @@
-import Mathlib.MeasureTheory.Function.LpSpace
-
-namespace MeasureTheory.Memℒp
-variable {α E : Type*} {m0 : MeasurableSpace α} {μ : Measure α} [IsFiniteMeasure μ]
-  [NormedAddCommGroup E] {p q : ENNReal} {f : α → E}
-
-lemma mono_exponent (hpq : p ≤ q) (hfq : Memℒp f q μ) : Memℒp f p μ :=
-  hfq.memℒp_of_exponent_le_of_measure_support_ne_top (by simp) (measure_ne_top _ .univ) hpq
diff --git a/LeanAPAP/Mathlib/MeasureTheory/Integral/Bochner.lean b/LeanAPAP/Mathlib/MeasureTheory/Integral/Bochner.lean
deleted file mode 100644
index e65b38a511..0000000000
--- a/LeanAPAP/Mathlib/MeasureTheory/Integral/Bochner.lean
+++ /dev/null
@@ -1,9 +0,0 @@
-import Mathlib.MeasureTheory.Integral.Bochner
-
-namespace MeasureTheory
-variable {α : Type*} {m : MeasurableSpace α} {μ : Measure α} {f : α → ℝ}
-
-lemma abs_integral_le_integral_abs : |∫ a, f a ∂μ| ≤ ∫ a, |f a| ∂μ :=
-  norm_integral_le_integral_norm f
-
-end MeasureTheory
diff --git a/LeanAPAP/Physics/AlmostPeriodicity.lean b/LeanAPAP/Physics/AlmostPeriodicity.lean
index f7db7df333..e37de5b215 100644
--- a/LeanAPAP/Physics/AlmostPeriodicity.lean
+++ b/LeanAPAP/Physics/AlmostPeriodicity.lean
@@ -138,7 +138,7 @@ lemma lemma28_part_one (hm : 1 ≤ m) (x : G) :
     simp only [boole_mul, indicate_apply]
     rw [← sum_filter, filter_mem_eq_inter, univ_inter, sub_self, smul_zero]
   congr with a : 1
-  simp only [sum_sub_distrib, Pi.smul_apply, sum_const, card_fin]
+  simp only [sum_sub_distrib, Pi.smul_apply, sum_const, card_fin, f']
 
 lemma big_shifts_step2 (L : Finset (Fin k → G)) (hk : k ≠ 0) :
     (∑ x ∈ L + S.piDiag (Fin k), ∑ l ∈ L, ∑ s ∈ S.piDiag (Fin k), ite (l + s = x) (1 : ℝ) 0) ^ 2
diff --git a/LeanAPAP/Physics/DRC.lean b/LeanAPAP/Physics/DRC.lean
index 1b45359474..9f1fc3a60d 100644
--- a/LeanAPAP/Physics/DRC.lean
+++ b/LeanAPAP/Physics/DRC.lean
@@ -128,7 +128,7 @@ lemma drc (hp₂ : 2 ≤ p) (f : G → ℝ≥0) (hf : ∃ x, x ∈ B₁ - B₂ 
     refine ⟨(lt_of_mul_lt_mul_left (hs.trans_eq' ?_) $ hg s).le, this.trans $ mul_le_of_le_one_right
       ?_ $ div_le_one_of_le₀ ?_ ?_, this.trans $ mul_le_of_le_one_left ?_ $ div_le_one_of_le₀ ?_ ?_⟩
     · simp_rw [A₁, A₂, g, ← card_smul_mu, smul_dconv, dconv_smul, ← Nat.cast_smul_eq_nsmul ℝ,
-        wInner_smul_left, smul_eq_mul, star_trivial, mul_assoc]
+        wInner_smul_left, smul_eq_mul, star_trivial, mul_assoc, A₁, A₂]
     any_goals positivity
     all_goals exact Nat.cast_le.2 $ card_mono inter_subset_left
   rw [← sum_mul, lemma_0, nsmul_eq_mul, Nat.cast_mul, ← sum_mul, mul_right_comm, ← hgB,
@@ -156,7 +156,7 @@ lemma drc (hp₂ : 2 ≤ p) (f : G → ℝ≥0) (hf : ∃ x, x ∈ B₁ - B₂ 
         := sum_lt_sum_of_nonempty ⟨s, mem_filter.2 ⟨mem_univ _, hs.symm⟩⟩ ?_
     _ ≤ ∑ s, M * sqrt (g s) := sum_le_univ_sum_of_nonneg fun s ↦ by positivity
     _ = M * (∑ s, sqrt #(A₁ s) * sqrt #(A₂ s))
-        := by simp_rw [mul_sum, sqrt_mul $ Nat.cast_nonneg _]
+        := by simp_rw [mul_sum, g, sqrt_mul $ Nat.cast_nonneg _]
     _ ≤ M * (sqrt (∑ s, #(A₁ s)) * sqrt (∑ s, #(A₂ s))) := by
       gcongr; exact sum_sqrt_mul_sqrt_le _ fun i ↦ by positivity fun i ↦ by positivity
     _ = _ := ?_
diff --git a/LeanAPAP/Prereqs/Chang.lean b/LeanAPAP/Prereqs/Chang.lean
index 737425e76a..043b30aba4 100644
--- a/LeanAPAP/Prereqs/Chang.lean
+++ b/LeanAPAP/Prereqs/Chang.lean
@@ -170,7 +170,7 @@ lemma chang (hf : f ≠ 0) (hη : 0 < η) :
       #Δ ≤ ⌈changConst * exp 1 * ⌈𝓛 ↑(‖f‖_[1] ^ 2 / ‖f‖_[2] ^ 2 / card G)⌉₊ / η ^ 2⌉₊ ∧
       largeSpec f η ⊆ Δ.addSpan := by
   refine exists_subset_addSpan_card_le_of_forall_addDissociated fun Δ hΔη hΔ ↦ ?_
-  obtain hΔ' | hΔ' := @eq_zero_or_pos _ _ #Δ
+  obtain hΔ' | hΔ' := eq_zero_or_pos #Δ
   · simp [hΔ']
   let α := ‖f‖_[1] ^ 2 / ‖f‖_[2] ^ 2 / card G
   have : 0 < α := by positivity
diff --git a/LeanAPAP/Prereqs/MarcinkiewiczZygmund.lean b/LeanAPAP/Prereqs/MarcinkiewiczZygmund.lean
index 7ed8dd2b6a..1c1de1996f 100644
--- a/LeanAPAP/Prereqs/MarcinkiewiczZygmund.lean
+++ b/LeanAPAP/Prereqs/MarcinkiewiczZygmund.lean
@@ -27,7 +27,7 @@ private lemma step_one (hA : A.Nonempty) (f : ι → ℝ) (a : Fin n → ι)
   calc
     |∑ i, f (a i)| ^ (m + 1)
       = |∑ i, (f (a i) - (∑ b ∈ B, f (b i)) / #B)| ^ (m + 1) := by
-      simp only [hf, sub_zero, zero_div]
+      simp only [B, hf, sub_zero, zero_div]
     _ = |(∑ b ∈ B, ∑ i, (f (a i) - f (b i))) / #B| ^ (m + 1) := by
       simp only [sum_sub_distrib]
       rw [sum_const, sub_div, sum_comm, sum_div, nsmul_eq_mul, card_piFinset, prod_const,
@@ -72,18 +72,18 @@ private lemma step_two_aux (A : Finset ι) (f : ι → ℝ) (ε : Fin n → ℝ)
     intro xy
     exact (fun i ↦ if ε i = 1 then xy.1 i else xy.2 i, fun i ↦ if ε i = 1 then xy.2 i else xy.1 i)
   have h₁ : ∀ a ∈ (A ^^ n) ×ˢ (A ^^ n), swapper a ∈ (A ^^ n) ×ˢ (A ^^ n) := by
-    simp only [mem_product, and_imp, mem_piFinset, ← forall_and]
+    simp only [mem_product, and_imp, mem_piFinset, ← forall_and, swapper]
     intro a h i
     split_ifs
     · exact h i
     · exact (h i).symm
   have h₂ : ∀ a ∈ (A ^^ n) ×ˢ (A ^^ n), swapper (swapper a) = a := fun a _ ↦ by
-    ext <;> simp only <;> split_ifs <;> rfl
+    ext <;> simp only [swapper] <;> split_ifs <;> rfl
   refine sum_nbij' swapper swapper h₁ h₁ h₂ h₂ ?_
   · rintro ⟨a, b⟩ _
     congr with i : 1
-    simp only [Pi.mul_apply, Pi.sub_apply, Function.comp_apply]
     simp only [mem_piFinset, mem_insert, mem_singleton] at hε
+    simp only [Pi.mul_apply, Pi.sub_apply, Function.comp_apply, swapper]
     split_ifs with h
     · simp [h]
     rw [(hε i).resolve_right h]
@@ -171,6 +171,7 @@ private lemma end_step {f : ι → ℝ} (hm : 1 ≤ m) (hA : A.Nonempty) :
         add_assoc, Nat.sub_add_cancel hm, pow_add, ← mul_pow, ← mul_pow, card_piFinset, prod_const,
         Finset.card_univ, Fintype.card_fin, Nat.cast_pow, mul_div_cancel_left₀]
       norm_num
+      dsimp [B]
       positivity
 
 namespace Real
diff --git a/LeanAPAP/Prereqs/NewMarcinkiewiczZygmund.lean b/LeanAPAP/Prereqs/NewMarcinkiewiczZygmund.lean
index e9c36ab8f5..1e90914b72 100644
--- a/LeanAPAP/Prereqs/NewMarcinkiewiczZygmund.lean
+++ b/LeanAPAP/Prereqs/NewMarcinkiewiczZygmund.lean
@@ -5,7 +5,6 @@ Authors: Yaël Dillies, Bhavik Mehta
 -/
 import Mathlib.Data.Nat.Choose.Multinomial
 import Mathlib.Probability.IdentDistrib
-import LeanAPAP.Mathlib.MeasureTheory.Integral.Bochner
 
 /-!
 # The Marcinkiewicz-Zygmund inequality
diff --git a/docbuild/lake-manifest.json b/docbuild/lake-manifest.json
index f58587e66b..6d0b2ec52a 100644
--- a/docbuild/lake-manifest.json
+++ b/docbuild/lake-manifest.json
@@ -5,10 +5,10 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover",
-   "rev": "0291556f04e89d46cd2999f0f4c1164c81778207",
+   "rev": "e9d995eaa95a4e3c880ffe94c416c34113e0f251",
    "name": "«doc-gen4»",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.15.0",
+   "inputRev": "main",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"type": "path",
@@ -32,7 +32,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "470c41643209208d325a5a7315116f293c7443fb",
+   "rev": "b64b8eab8cfcf24c398e84b11c77b6555b61095a",
    "name": "UnicodeBasic",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -42,7 +42,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "46376bc3c8f46ac1a1fd7712856b0f7bd6166098",
+   "rev": "9e99cb8cd9ba6906472634e6973c7e27482a70bb",
    "name": "BibtexQuery",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -52,7 +52,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "f8ed91f3a9d806648ae6a03ab98c8b87e8bedc7e",
+   "rev": "26b1d510d9b5238d36b521d5367c707146fecd9d",
    "name": "MD4Lean",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -62,7 +62,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "9082fa7b9f7bcad5b4b6052a629eb9347580073a",
+   "rev": "1844f029a2fd418595badb7be8d8967e20f65570",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,
@@ -72,10 +72,10 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "8e5cb8d424df462f84997dd68af6f40e347c3e35",
+   "rev": "1622a8693b31523c8f82db48e01b14c74bc1f155",
    "name": "plausible",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.15.0-rc1",
+   "inputRev": "v4.16.0-rc1",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/LeanSearchClient",
@@ -92,47 +92,47 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "ed3b856bd8893ade75cafe13e8544d4c2660f377",
+   "rev": "f72319c9686788305a8ab059f3c4d8c724785c83",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.15.0-rc1",
+   "inputRev": "main",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/ProofWidgets4",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "2b000e02d50394af68cfb4770a291113d94801b5",
+   "rev": "07f60e90998dfd6592688a14cd67bd4e384b77b2",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.48",
+   "inputRev": "v0.0.50",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "a4a08d92be3de00def5298059bf707c72dfd3c66",
+   "rev": "79402ad9ab4be9a2286701a9880697e2351e4955",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "master",
+   "inputRev": "v4.16.0-rc1",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/quote4",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "ad942fdf0b15c38bface6acbb01d63855a2519ac",
+   "rev": "f0c584bcb14c5adfb53079781eeea75b26ebbd32",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.14.0",
+   "inputRev": "v4.15.0",
    "inherited": true,
-   "configFile": "lakefile.lean"},
+   "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/batteries",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "f007bfe46ea8fb801ec907df9ab540054abcc5fd",
+   "rev": "5b23a1297aba9683f231c4b1a7ab4076af4ad53d",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
diff --git a/docbuild/lakefile.toml b/docbuild/lakefile.toml
index cea023c197..6da197f74d 100644
--- a/docbuild/lakefile.toml
+++ b/docbuild/lakefile.toml
@@ -10,4 +10,4 @@ path = "../"
 [[require]]
 scope = "leanprover"
 name = "doc-gen4"
-rev = "v4.15.0"
+rev = "main"
diff --git a/docbuild/lean-toolchain b/docbuild/lean-toolchain
index cf25a9816f..2ffc30ceba 100644
--- a/docbuild/lean-toolchain
+++ b/docbuild/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.15.0-rc1
+leanprover/lean4:v4.16.0-rc2
\ No newline at end of file
diff --git a/lake-manifest.json b/lake-manifest.json
index c03bcbc0fb..ebf51cf4bb 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -5,20 +5,20 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "9837ca9d65d9de6fad1ef4381750ca688774e608",
+   "rev": "1844f029a2fd418595badb7be8d8967e20f65570",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.15.0",
+   "inputRev": null,
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/plausible",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "2c57364ef83406ea86d0f78ce3e342079a2fece5",
+   "rev": "1622a8693b31523c8f82db48e01b14c74bc1f155",
    "name": "plausible",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.15.0",
+   "inputRev": "v4.16.0-rc1",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/LeanSearchClient",
@@ -35,30 +35,30 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "9a0b533c2fbd6195df067630be18e11e4349051c",
+   "rev": "f72319c9686788305a8ab059f3c4d8c724785c83",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.15.0",
+   "inputRev": "main",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/ProofWidgets4",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "2b000e02d50394af68cfb4770a291113d94801b5",
+   "rev": "07f60e90998dfd6592688a14cd67bd4e384b77b2",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.48",
+   "inputRev": "v0.0.50",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "2689851f387bb2cef351e6825fe94a56a304ca13",
+   "rev": "79402ad9ab4be9a2286701a9880697e2351e4955",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.15.0",
+   "inputRev": "v4.16.0-rc1",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/quote4",
@@ -75,10 +75,10 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "e8dc5fc16c625fc4fe08f42d625523275ddbbb4b",
+   "rev": "5b23a1297aba9683f231c4b1a7ab4076af4ad53d",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.15.0",
+   "inputRev": "main",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover/lean4-cli",
@@ -91,5 +91,5 @@
    "inputRev": "main",
    "inherited": true,
    "configFile": "lakefile.toml"}],
- "name": "LeanCamCombi",
+ "name": "LeanAPAP",
  "lakeDir": ".lake"}
diff --git a/lean-toolchain b/lean-toolchain
index d0eb99ff68..2ffc30ceba 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.15.0
+leanprover/lean4:v4.16.0-rc2
\ No newline at end of file