diff --git a/LeanAPAP.lean b/LeanAPAP.lean
index 3b8e5a853f..3bd7563418 100644
--- a/LeanAPAP.lean
+++ b/LeanAPAP.lean
@@ -2,17 +2,15 @@ import LeanAPAP.Extras.BSG
 import LeanAPAP.FiniteField
 import LeanAPAP.Integer
 import LeanAPAP.Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar
-import LeanAPAP.Mathlib.Data.ENNReal.Basic
-import LeanAPAP.Mathlib.MeasureTheory.Function.EssSup
 import LeanAPAP.Mathlib.MeasureTheory.Function.LpSeminorm.Basic
+import LeanAPAP.Mathlib.Probability.ConditionalProbability
+import LeanAPAP.Mathlib.Probability.UniformOn
 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.MeasurableSpace
 import LeanAPAP.Prereqs.AddChar.PontryaginDuality
-import LeanAPAP.Prereqs.Balance.Complex
 import LeanAPAP.Prereqs.Bohr.Arc
 import LeanAPAP.Prereqs.Bohr.Basic
 import LeanAPAP.Prereqs.Bohr.Regular
@@ -34,7 +32,6 @@ import LeanAPAP.Prereqs.Function.Translate
 import LeanAPAP.Prereqs.Inner.Function
 import LeanAPAP.Prereqs.Inner.Hoelder.Compact
 import LeanAPAP.Prereqs.Inner.Hoelder.Discrete
-import LeanAPAP.Prereqs.Inner.Weighted
 import LeanAPAP.Prereqs.LargeSpec
 import LeanAPAP.Prereqs.LpNorm.Compact
 import LeanAPAP.Prereqs.LpNorm.Discrete.Basic
diff --git a/LeanAPAP/Extras/BSG.lean b/LeanAPAP/Extras/BSG.lean
index b40afd33a8..7e0944f75a 100644
--- a/LeanAPAP/Extras/BSG.lean
+++ b/LeanAPAP/Extras/BSG.lean
@@ -124,7 +124,7 @@ lemma claim_two :
     rw [Real.sq_sqrt]
     exact dconv_nonneg (R := ℝ) indicate_nonneg indicate_nonneg s -- why do I need the annotation??
   have := sum_mul_sq_le_sq_mul_sq univ f (fun s ↦ f s * (A ∩ (s +ᵥ B)).card)
-  refine div_le_of_nonneg_of_le_mul (by positivity) ?_ ?_
+  refine div_le_of_le_mul₀ (by positivity) ?_ ?_
   · refine sum_nonneg fun i _ ↦ ?_
     -- indicate nonneg should be a positivity lemma
     exact mul_nonneg (dconv_nonneg indicate_nonneg indicate_nonneg _) (by positivity)
diff --git a/LeanAPAP/FiniteField.lean b/LeanAPAP/FiniteField.lean
index 8fe1efaea8..7de83ce29c 100644
--- a/LeanAPAP/FiniteField.lean
+++ b/LeanAPAP/FiniteField.lean
@@ -1,5 +1,4 @@
 import Mathlib.FieldTheory.Finite.Basic
-import LeanAPAP.Prereqs.Balance.Complex
 import LeanAPAP.Prereqs.Chang
 import LeanAPAP.Prereqs.Convolution.ThreeAP
 import LeanAPAP.Prereqs.FourierTransform.Convolution
@@ -16,7 +15,7 @@ set_option linter.haveLet 0
 
 attribute [-simp] Real.log_inv
 
-open FiniteDimensional Fintype Function MeasureTheory RCLike Real
+open Fintype Function MeasureTheory Module RCLike Real
 open Finset hiding card
 open scoped ENNReal NNReal BigOperators Combinatorics.Additive Pointwise
 
@@ -28,13 +27,13 @@ local notation "𝓛" x:arg => 1 + log x⁻¹
 private lemma one_le_curlog (hx₀ : 0 ≤ x) (hx₁ : x ≤ 1) : 1 ≤ 𝓛 x := by
   obtain rfl | hx₀ := hx₀.eq_or_lt
   · simp
-  have : 0 ≤ log x⁻¹ := log_nonneg $ one_le_inv (by positivity) hx₁
+  have : 0 ≤ log x⁻¹ := log_nonneg $ (one_le_inv₀ (by positivity)).2 hx₁
   linarith
 
 private lemma curlog_pos (hx₀ : 0 ≤ x) (hx₁ : x ≤ 1) : 0 < 𝓛 x := by
   obtain rfl | hx₀ := hx₀.eq_or_lt
   · simp
-  have : 0 ≤ log x⁻¹ := log_nonneg $ one_le_inv (by positivity) hx₁
+  have : 0 ≤ log x⁻¹ := log_nonneg $ (one_le_inv₀ (by positivity)).2 hx₁
   positivity
 
 private lemma rpow_inv_neg_curlog_le (hx₀ : 0 ≤ x) (hx₁ : x ≤ 1) : x⁻¹ ^ (𝓛 x)⁻¹ ≤ exp 1 := by
@@ -42,7 +41,7 @@ private lemma rpow_inv_neg_curlog_le (hx₀ : 0 ≤ x) (hx₁ : x ≤ 1) : x⁻
   · simp; positivity
   obtain rfl | hx₁ := hx₁.eq_or_lt
   · simp
-  have hx := one_lt_inv hx₀ hx₁
+  have hx := (one_lt_inv₀ hx₀).2 hx₁
   calc
     x⁻¹ ^ (𝓛 x)⁻¹ ≤ x⁻¹ ^ (log x⁻¹)⁻¹ := by
       gcongr
@@ -59,11 +58,11 @@ private lemma curlog_mul_le (hx₀ : 0 < x) (hx₁ : x ≤ 1) (hy₀ : 0 < y) (h
   calc
     log x⁻¹ - (x⁻¹ - 1) ≤ 0 := sub_nonpos.2 $ log_le_sub_one_of_pos $ by positivity
     _ ≤ (x⁻¹ - 1) * log y⁻¹ :=
-      mul_nonneg (sub_nonneg.2 $ one_le_inv hx₀ hx₁) $ log_nonneg $ one_le_inv hy₀ hy₁
+      mul_nonneg (sub_nonneg.2 $ (one_le_inv₀ hx₀).2 hx₁) $ log_nonneg $ (one_le_inv₀ hy₀).2 hy₁
 
 private lemma curlog_div_le (hx₀ : 0 < x) (hx₁ : x ≤ 1) (hy : 1 ≤ y) :
     𝓛 (x / y) ≤ y * 𝓛 x := by
-  simpa [div_eq_inv_mul] using curlog_mul_le (by positivity) (inv_le_one hy) hx₀ hx₁
+  simpa [div_eq_inv_mul] using curlog_mul_le (by positivity) (inv_le_one_of_one_le₀ hy) hx₀ hx₁
 
 private lemma curlog_rpow_le' (hx₀ : 0 < x) (hx₁ : x ≤ 1) (hy₀ : 0 < y) (hy₁ : y ≤ 1) :
     𝓛 (x ^ y) ≤ y⁻¹ * 𝓛 x := by
@@ -71,9 +70,10 @@ private lemma curlog_rpow_le' (hx₀ : 0 < x) (hx₁ : x ≤ 1) (hy₀ : 0 < y)
     rw [← sub_nonneg] at h ⊢
     exact h.trans_eq (by rw [← inv_rpow, log_rpow]; ring; all_goals positivity)
   calc
-    1 - y⁻¹ ≤ 0 := sub_nonpos.2 $ one_le_inv hy₀ hy₁
+    1 - y⁻¹ ≤ 0 := sub_nonpos.2 $ (one_le_inv₀ hy₀).2 hy₁
     _ ≤ (y⁻¹ - y) * log x⁻¹ :=
-      mul_nonneg (sub_nonneg.2 $ hy₁.trans $ one_le_inv hy₀ hy₁) $ log_nonneg $ one_le_inv hx₀ hx₁
+      mul_nonneg (sub_nonneg.2 $ hy₁.trans $ (one_le_inv₀ hy₀).2 hy₁) $
+        log_nonneg $ (one_le_inv₀ hx₀).2 hx₁
 
 private lemma curlog_rpow_le (hx₀ : 0 < x) (hy : 1 ≤ y) : 𝓛 (x ^ y) ≤ y * 𝓛 x := by
   rw [← inv_rpow, log_rpow, mul_one_add]
@@ -91,7 +91,7 @@ lemma global_dichotomy [MeasurableSpace G] [DiscreteMeasurableSpace G] (hA : A.N
   set p := 2 * ⌈𝓛 γ⌉₊
   have hp : 1 < p :=
     Nat.succ_le_iff.1 (le_mul_of_one_le_right zero_le' $ Nat.ceil_pos.2 $ curlog_pos hγ.le hγ₁)
-  have hp' : (p⁻¹ : ℝ≥0) < 1 := inv_lt_one $ mod_cast hp
+  have hp' : (p⁻¹ : ℝ≥0) < 1 := inv_lt_one_of_one_lt₀ $ mod_cast hp
   have hp'' : (p : ℝ≥0).IsConjExponent _ := .conjExponent $ mod_cast hp
   rw [mul_comm, ← div_div, div_le_iff₀ (zero_lt_two' ℝ)]
   calc
@@ -115,7 +115,7 @@ lemma global_dichotomy [MeasurableSpace G] [DiscreteMeasurableSpace G] (hA : A.N
     congr
     any_goals positivity
     exact ENNReal.natCast_ne_top _
-  · have : 1 ≤ γ⁻¹ := one_le_inv hγ hγ₁
+  · have : 1 ≤ γ⁻¹ := (one_le_inv₀ hγ).2 hγ₁
     have : 0 ≤ log γ⁻¹ := log_nonneg this
     calc
       γ ^ (-(↑p)⁻¹ : ℝ) = √(γ⁻¹ ^ ((↑⌈1 + log γ⁻¹⌉₊)⁻¹ : ℝ)) := by
@@ -142,8 +142,9 @@ lemma ap_in_ff (hα₀ : 0 < α) (hα₂ : α ≤ 2⁻¹) (hε₀ : 0 < ε) (hε
   have hA₁ : A₁.Nonempty := by simpa using hα₀.trans_le hαA₁
   have hA₂ : A₂.Nonempty := by simpa using hα₀.trans_le hαA₂
   have hα₁ : α ≤ 1 := hαA₁.trans $ mod_cast A₁.dens_le_one
-  have : 0 ≤ log α⁻¹ := log_nonneg $ one_le_inv hα₀ hα₁
-  have : 0 ≤ log (ε * α)⁻¹ := log_nonneg $ one_le_inv (by positivity) $ mul_le_one hε₁ hα₀.le hα₁
+  have : 0 ≤ log α⁻¹ := log_nonneg $ (one_le_inv₀ hα₀).2 hα₁
+  have : 0 ≤ log (ε * α)⁻¹ :=
+    log_nonneg $ (one_le_inv₀ (by positivity)).2 $ mul_le_one₀ hε₁ hα₀.le hα₁
   obtain rfl | hS := S.eq_empty_or_nonempty
   · exact ⟨⊤, inferInstance, by simp [hε₀.le]; positivity⟩
   have hA₁ : σ[A₁, univ] ≤ α⁻¹ :=
@@ -156,7 +157,7 @@ lemma ap_in_ff (hα₀ : 0 < α) (hα₂ : α ≤ 2⁻¹) (hε₀ : 0 < ε) (hε
       ε * α / 4 ≤ ε * 1 / 4 := by gcongr
       _ ≤ 1 := by linarith
   obtain ⟨T, hTcard, hTε⟩ := AlmostPeriodicity.linfty_almost_periodicity_boosted ε hε₀ hε₁ k
-    (by positivity) ((le_inv (by positivity) (by positivity)).2 hα₂) hA₁ univ_nonempty S A₂ hS hA₂
+    (by positivity) (le_inv_of_le_inv₀ (by positivity) hα₂) hA₁ univ_nonempty S A₂ hS hA₂
   have hT : 0 < (T.card : ℝ) := hTcard.trans_lt' (by positivity)
   replace hT : T.Nonempty := by simpa using hT
   let Δ := largeSpec (μ T) 2⁻¹
@@ -186,7 +187,7 @@ lemma ap_in_ff (hα₀ : 0 < α) (hα₂ : α ≤ 2⁻¹) (hε₀ : 0 < ε) (hε
                 Nat.ceil_le_two_mul <| two_inv_lt_one.le.trans <| one_le_curlog (by positivity) sorry
               _ ≤ 2 * (4 * 𝓛 (ε * α)) := by
                 gcongr
-                exact curlog_div_le (by positivity) (mul_le_one hε₁ hα₀.le hα₁) (by norm_num)
+                exact curlog_div_le (by positivity) (mul_le_one₀ hε₁ hα₀.le hα₁) (by norm_num)
               _ = 2 ^ 3 * 𝓛 (ε * α) := by ring
         _ = 2 ^ 19 * 𝓛 α ^ 2 * 𝓛 (ε * α) ^ 2 * ε⁻¹ ^ 2 := by ring_nf
     calc
@@ -250,7 +251,7 @@ lemma di_in_ff [MeasurableSpace G] [DiscreteMeasurableSpace G] (hq₃ : 3 ≤ q)
     ∃ p' : ℕ, p' ≤ 2 ^ 10 * (ε / 2)⁻¹ ^ 2 * p ∧
       1 + ε / 2 / 2 ≤ ‖card G • (f ○ f) + 1‖_[p', μ univ] := by
     refine unbalancing _ (mul_ne_zero two_ne_zero (Nat.ceil_pos.2 $ curlog_pos hγ.le hγ₁).ne')
-      (ε / 2) (by positivity) (div_le_one_of_le (hε₁.le.trans $ by norm_num) $ by norm_num)
+      (ε / 2) (by positivity) (div_le_one_of_le₀ (hε₁.le.trans $ by norm_num) $ by norm_num)
       (card G • (balance (μ A) ○ balance (μ A))) (sqrt (card G) • balance (μ A)) (μ univ) ?_ ?_ ?_
     · ext a : 1
       simp [smul_dconv, dconv_smul, smul_smul, ← mul_assoc, ← sq, ← Complex.ofReal_pow]
@@ -268,7 +269,7 @@ lemma di_in_ff [MeasurableSpace G] [DiscreteMeasurableSpace G] (hq₃ : 3 ≤ q)
   have : 0 < log (64 / ε) := log_pos $ (one_lt_div hε₀).2 (by linarith)
   have : 1 ≤ 𝓛 γ := one_le_curlog hγ.le hγ₁
   have : 0 < q' := by positivity
-  have : 1 ≤ ε⁻¹ := one_le_inv hε₀ hε₁.le
+  have : 1 ≤ ε⁻¹ := (one_le_inv₀ hε₀).2 hε₁.le
   have :=
     calc
       (q' : ℝ) ≤ ↑(2 * ⌈2 ^ 10 * (ε / 2)⁻¹ ^ 2 * p + 2 ^ 8 * ε⁻¹ ^ 2 * (64 / ε)⌉₊) := by
@@ -288,7 +289,7 @@ lemma di_in_ff [MeasurableSpace G] [DiscreteMeasurableSpace G] (hq₃ : 3 ≤ q)
           (2⁻¹ : ℝ) ≤ 2 ^ 15 * 1 * 1 := by norm_num
           _ ≤ 2 ^ 15 * ε⁻¹ ^ 3 * 𝓛 γ := ?_
         gcongr
-        exact one_le_pow₀ (one_le_inv hε₀ hε₁.le)
+        exact one_le_pow₀ ((one_le_inv₀ hε₀).2 hε₁.le)
       _ = 2 ^ 17 * 𝓛 γ / ε ^ 3 := by ring
   obtain ⟨A₁, A₂, hA, hA₁, hA₂⟩ : ∃ (A₁ A₂ : Finset G),
       1 - ε / 32 ≤ ∑ x ∈ s q' (ε / 16) univ univ A, (μ A₁ ○ μ A₂) x ∧
@@ -301,7 +302,7 @@ lemma di_in_ff [MeasurableSpace G] [DiscreteMeasurableSpace G] (hq₃ : 3 ≤ q)
           gcongr
           · norm_num
           · norm_num
-          · exact one_le_inv hε₀ hε₁.le
+          · exact (one_le_inv₀ hε₀).2 hε₁.le
           · norm_num
         _ ≤ ⌈2 ^ 8 * ε⁻¹ ^ 2 * log (64 / ε)⌉₊ := Nat.le_ceil _
         _ = ↑(1 * ⌈0 + 2 ^ 8 * ε⁻¹ ^ 2 * log (64 / ε)⌉₊) := by rw [one_mul, zero_add]
@@ -362,12 +363,12 @@ lemma di_in_ff [MeasurableSpace G] [DiscreteMeasurableSpace G] (hq₃ : 3 ≤ q)
       _ ≤ 2 ^ 32 * (8 * q' * 𝓛 α) ^ 2 *
           (2 ^ 8 * q' * 𝓛 α / ε) ^ 2 * (ε / 32)⁻¹ ^ 2 := by
         have : α ^ (2 * q') ≤ 1 := pow_le_one₀ hα₀.le hα₁
-        have : 4⁻¹ * α ^ (2 * q') ≤ 1 := mul_le_one (by norm_num) (by positivity) ‹_›
-        have : ε / 32 * (4⁻¹ * α ^ (2 * q')) ≤ 1 := mul_le_one (by linarith) (by positivity) ‹_›
+        have : 4⁻¹ * α ^ (2 * q') ≤ 1 := mul_le_one₀ (by norm_num) (by positivity) ‹_›
+        have : ε / 32 * (4⁻¹ * α ^ (2 * q')) ≤ 1 := mul_le_one₀ (by linarith) (by positivity) ‹_›
         have : 0 ≤ log (ε / 32 * (4⁻¹ * α ^ (2 * q')))⁻¹ :=
-          log_nonneg $ one_le_inv (by positivity) ‹_›
-        have : 0 ≤ log (4⁻¹ * α ^ (2 * q'))⁻¹ := log_nonneg $ one_le_inv (by positivity) ‹_›
-        have : 0 ≤ log (α ^ (2 * q'))⁻¹ := log_nonneg $ one_le_inv (by positivity) ‹_›
+          log_nonneg $ (one_le_inv₀ (by positivity)).2 ‹_›
+        have : 0 ≤ log (4⁻¹ * α ^ (2 * q'))⁻¹ := log_nonneg $ (one_le_inv₀ (by positivity)).2 ‹_›
+        have : 0 ≤ log (α ^ (2 * q'))⁻¹ := log_nonneg $ (one_le_inv₀ (by positivity)).2 ‹_›
         have :=
           calc
             𝓛 (4⁻¹ * α ^ (2 * q')) ≤ 4⁻¹⁻¹ * 𝓛 (α ^ (2 * q')) :=
@@ -434,7 +435,7 @@ theorem ff (hq₃ : 3 ≤ q) (hq : q.Prime) (hA₀ : A.Nonempty) (hA : ThreeAPFr
   have : NeZero q := ⟨by positivity⟩
   have : Fact q.Prime := ⟨hq⟩
   have hq' : Odd q := hq.odd_of_ne_two $ by rintro rfl; simp at hq₃
-  have : 1 ≤ α⁻¹ := one_le_inv (by positivity) (by simp [α])
+  have : 1 ≤ α⁻¹ := (one_le_inv₀ (by positivity)).2 (by simp [α])
   have hα₀ : 0 < α := by positivity
   have : 0 ≤ log α⁻¹ := log_nonneg ‹_›
   have : 0 < 𝓛 α := by positivity
@@ -525,13 +526,13 @@ theorem ff (hq₃ : 3 ≤ q) (hq : q.Prime) (hA₀ : A.Nonempty) (hA : ThreeAPFr
     calc
       _ ≤ (1 : ℝ) := mod_cast dens_le_one
       _ < _ := ?_
-    rw [← inv_pos_lt_iff_one_lt_mul, lt_pow_iff_log_lt, ← div_lt_iff₀]
+    rw [← inv_lt_iff_one_lt_mul₀, lt_pow_iff_log_lt, ← div_lt_iff₀]
     calc
       log α⁻¹ / log (65 / 64)
         < ⌊log α⁻¹ / log (65 / 64)⌋₊ + 1 := Nat.lt_floor_add_one _
       _ = ⌊(log (65 / 64) + log α⁻¹) / log (65 / 64)⌋₊ := by
         rw [add_comm (log _), ← div_add_one aux.ne', Nat.floor_add_one, Nat.cast_succ]
-        exact div_nonneg (log_nonneg $ one_le_inv (by positivity) (by simp [α])) aux.le
+        exact div_nonneg (log_nonneg $ (one_le_inv₀ (by positivity)).2 (by simp [α])) aux.le
       _ ≤ ⌊𝓛 α / log (65 / 64)⌋₊ := by
         gcongr
         calc
@@ -555,7 +556,7 @@ theorem ff (hq₃ : 3 ≤ q) (hq : q.Prime) (hA₀ : A.Nonempty) (hA : ThreeAPFr
         _ = 2 ^ 148 * (log (65 / 64)) ⁻¹ * 𝓛 α ^ 9 := by ring
         _ ≤ 2 ^ 148 * 2 ^ 7 * 𝓛 α ^ 9 := by
           gcongr
-          rw [inv_le ‹_› (by positivity)]
+          refine inv_le_of_inv_le₀ (by positivity) ?_
           calc
             (2 ^ 7)⁻¹ ≤ 1 - (65 / 64)⁻¹ := by norm_num
             _ ≤ log (65 / 64) := one_sub_inv_le_log_of_pos (by positivity)
diff --git a/LeanAPAP/Mathlib/Data/ENNReal/Basic.lean b/LeanAPAP/Mathlib/Data/ENNReal/Basic.lean
deleted file mode 100644
index 4b0c8e2c35..0000000000
--- a/LeanAPAP/Mathlib/Data/ENNReal/Basic.lean
+++ /dev/null
@@ -1,32 +0,0 @@
-import Mathlib.Data.ENNReal.Basic
-
-namespace ENNReal
-
-@[simp] lemma ofNat_pos {n : ℕ} [n.AtLeastTwo] : 0 < (no_index OfNat.ofNat n : ℝ≥0∞) :=
-  Nat.cast_pos.2 Fin.size_pos'
-
-end ENNReal
-
-namespace Mathlib.Meta.Positivity
-open Lean Meta Qq Function ENNReal
-
-private lemma ennreal_one_pos : (0 : ℝ≥0∞) < 1 := zero_lt_one
-
-/-- The `positivity` extension which identifies expressions of the form `‖f‖_[p]`. -/
-@[positivity OfNat.ofNat _] def evalOfNatENNReal : PositivityExt where eval {u} α _z _p e := do
-  match u, α, e with
-  | 0, ~q(ℝ≥0∞), ~q(@OfNat.ofNat _ $n $instn) =>
-    try
-      let instn ← synthInstanceQ q(Nat.AtLeastTwo $n)
-      return Strictness.positive (q(@ofNat_pos $n $instn) : Expr)
-    catch _ => do
-      match n with
-      | ~q(1) => return .positive (q(ennreal_one_pos) : Expr)
-      | _ => throwError "not positive"
-  | _ => throwError "not `ENNReal`-valued `ofNat`"
-
-end Mathlib.Meta.Positivity
-
-open scoped ENNReal
-
-example : (0 : ℝ≥0∞) < 1 := by positivity
diff --git a/LeanAPAP/Mathlib/MeasureTheory/Function/EssSup.lean b/LeanAPAP/Mathlib/MeasureTheory/Function/EssSup.lean
deleted file mode 100644
index 2a8335967c..0000000000
--- a/LeanAPAP/Mathlib/MeasureTheory/Function/EssSup.lean
+++ /dev/null
@@ -1,40 +0,0 @@
-import Mathlib.MeasureTheory.Function.EssSup
-import Mathlib.Probability.ConditionalProbability
-
-open Filter MeasureTheory ProbabilityTheory
-open scoped ENNReal
-
-variable {α β : Type*} {m : MeasurableSpace α} [ConditionallyCompleteLattice β]
-  {μ : Measure α} {f : α → β}
-
-section SMul
-variable {R : Type*} [Zero R] [SMulWithZero R ℝ≥0∞] [IsScalarTower R ℝ≥0∞ ℝ≥0∞]
-  [NoZeroSMulDivisors R ℝ≥0∞] {c : ℝ≥0∞}
-
--- TODO: Replace in mathlib
-@[simp] lemma essSup_smul_measure' {f : α → β} {c : ℝ≥0∞} (hc : c ≠ 0) :
-    essSup f (c • μ) = essSup f μ := by simp_rw [essSup, Measure.ae_smul_measure_eq hc]
-
-end SMul
-
-variable [Nonempty α]
-
-lemma essSup_eq_ciSup (hμ : ∀ a, μ {a} ≠ 0) (hf : BddAbove (Set.range f)) :
-    essSup f μ = ⨆ a, f a := by rw [essSup, ae_eq_top.2 hμ, limsup_top_eq_ciSup hf]
-
-lemma essInf_eq_ciInf (hμ : ∀ a, μ {a} ≠ 0) (hf : BddBelow (Set.range f)) :
-    essInf f μ = ⨅ a, f a := by rw [essInf, ae_eq_top.2 hμ, liminf_top_eq_ciInf hf]
-
-variable [MeasurableSingletonClass α]
-
-@[simp] lemma essSup_count_eq_ciSup (hf : BddAbove (Set.range f)) :
-    essSup f .count = ⨆ a, f a := essSup_eq_ciSup (by simp) hf
-
-@[simp] lemma essInf_count_eq_ciInf (hf : BddBelow (Set.range f)) :
-    essInf f .count = ⨅ a, f a := essInf_eq_ciInf (by simp) hf
-
-@[simp] lemma essSup_cond_count_eq_ciSup [Finite α] (hf : BddAbove (Set.range f)) :
-    essSup f .count[|.univ] = ⨆ a, f a := essSup_eq_ciSup (by simp [cond_apply, Set.finite_univ]) hf
-
-@[simp] lemma essInf_cond_count_eq_ciInf [Finite α] (hf : BddBelow (Set.range f)) :
-    essInf f .count[|.univ] = ⨅ a, f a := essInf_eq_ciInf (by simp [cond_apply, Set.finite_univ]) hf
diff --git a/LeanAPAP/Mathlib/Probability/ConditionalProbability.lean b/LeanAPAP/Mathlib/Probability/ConditionalProbability.lean
new file mode 100644
index 0000000000..ed16872260
--- /dev/null
+++ b/LeanAPAP/Mathlib/Probability/ConditionalProbability.lean
@@ -0,0 +1,13 @@
+import Mathlib.Probability.ConditionalProbability
+
+open MeasureTheory
+open scoped ENNReal
+
+namespace ProbabilityTheory
+variable {Ω Ω' α : Type*} {m : MeasurableSpace Ω} {m' : MeasurableSpace Ω'} {μ : Measure Ω}
+  {s t : Set Ω}
+
+-- TODO: Replace `cond_eq_zero`
+@[simp] lemma cond_eq_zero' : μ[|s] = 0 ↔ μ s = ∞ ∨ μ s = 0 := by simp [cond]
+
+end ProbabilityTheory
diff --git a/LeanAPAP/Mathlib/Probability/UniformOn.lean b/LeanAPAP/Mathlib/Probability/UniformOn.lean
new file mode 100644
index 0000000000..620cb5e935
--- /dev/null
+++ b/LeanAPAP/Mathlib/Probability/UniformOn.lean
@@ -0,0 +1,11 @@
+import Mathlib.Probability.UniformOn
+import LeanAPAP.Mathlib.Probability.ConditionalProbability
+
+namespace ProbabilityTheory
+variable {Ω : Type*} [MeasurableSpace Ω] [MeasurableSingletonClass Ω] {s : Set Ω}
+
+@[simp] lemma uniformOn_eq_zero : uniformOn s = 0 ↔ s.Infinite ∨ s = ∅ := by simp [uniformOn]
+@[simp] lemma uniformOn_eq_zero' (hs : s.Finite) : uniformOn s = 0 ↔ s = ∅ := by
+  simp [uniformOn, hs]
+
+end ProbabilityTheory
diff --git a/LeanAPAP/Physics/AlmostPeriodicity.lean b/LeanAPAP/Physics/AlmostPeriodicity.lean
index f79d543bad..8aac4a5e15 100644
--- a/LeanAPAP/Physics/AlmostPeriodicity.lean
+++ b/LeanAPAP/Physics/AlmostPeriodicity.lean
@@ -91,7 +91,7 @@ variable {G : Type*} [Fintype G] {A S : Finset G} {f : G → ℂ} {x ε K : ℝ}
 local notation "𝓛" x => 1 + log (min 1 x)⁻¹
 
 private lemma curlog_pos (hx₀ : 0 < x) : 0 < 𝓛 x := by
-  have : 0 ≤ log (min 1 x)⁻¹ := log_nonneg $ one_le_inv (by positivity) inf_le_left
+  have : 0 ≤ log (min 1 x)⁻¹ := log_nonneg $ (one_le_inv₀ (by positivity)).2 inf_le_left
   positivity
 
 section
@@ -433,7 +433,7 @@ theorem linfty_almost_periodicity (ε : ℝ) (hε₀ : 0 < ε) (hε₁ : ε ≤
   have hm₀ : 0 < m := curlog_pos (by positivity)
   have hm₁ : 1 ≤ ⌈m⌉₊ := Nat.one_le_iff_ne_zero.2 $ by positivity
   obtain ⟨T, hKT, hT⟩ := almost_periodicity (ε / exp 1) (by positivity)
-    (div_le_one_of_le (hε₁.trans $ one_le_exp zero_le_one) $ by positivity) ⌈m⌉₊ (𝟭 B) hK₂ hK
+    (div_le_one_of_le₀ (hε₁.trans $ one_le_exp zero_le_one) $ by positivity) ⌈m⌉₊ (𝟭 B) hK₂ hK
   norm_cast at hT
   set M : ℕ := 2 * ⌈m⌉₊
   have hM₀ : (M : ℝ≥0) ≠ 0 := by positivity
@@ -481,13 +481,13 @@ theorem linfty_almost_periodicity (ε : ℝ) (hε₀ : 0 < ε) (hε₁ : ε ≤
       ≤ r ^ (-(M : ℝ)⁻¹) :=
         rpow_le_rpow_of_nonpos (by positivity) inf_le_right $ neg_nonpos.2 $ by positivity
     _ ≤ r ^ (-(1 + log r⁻¹)⁻¹) :=
-        rpow_le_rpow_of_exponent_ge (by positivity) inf_le_left $ neg_le_neg $ inv_le_inv_of_le
+        rpow_le_rpow_of_exponent_ge (by positivity) inf_le_left $ neg_le_neg $ inv_anti₀
           (by positivity) $ (Nat.le_ceil _).trans $
             mod_cast Nat.le_mul_of_pos_left _ (by positivity)
     _ ≤ r ^ (-(0 + log r⁻¹)⁻¹) := by
       obtain hr | hr : r = 1 ∨ r < 1 := inf_le_left.eq_or_lt
       · simp [hr]
-      have : 0 < log r⁻¹ := log_pos <| one_lt_inv (by positivity) hr
+      have : 0 < log r⁻¹ := log_pos <| (one_lt_inv₀ (by positivity)).2 hr
       exact rpow_le_rpow_of_exponent_ge (by positivity) inf_le_left (by gcongr; exact zero_le_one)
     _ = r ^ (log r)⁻¹ := by simp [inv_neg]
     _ ≤ exp 1 := rpow_inv_log_le_exp_one
@@ -499,7 +499,7 @@ theorem linfty_almost_periodicity_boosted (ε : ℝ) (hε₀ : 0 < ε) (hε₁ :
       K ^ (-4096 * ⌈𝓛 (C.card / B.card)⌉ * k ^ 2/ ε ^ 2) * S.card ≤ T.card ∧
       ‖μ T ∗^ k ∗ (μ_[ℂ] A ∗ 𝟭 B ∗ μ C) - μ A ∗ 𝟭 B ∗ μ C‖_[∞] ≤ ε := by
   obtain ⟨T, hKT, hT⟩ := linfty_almost_periodicity (ε / k) (by positivity)
-    (div_le_one_of_le (hε₁.trans $ mod_cast Nat.one_le_iff_ne_zero.2 hk) $ by positivity) hK₂ hK
+    (div_le_one_of_le₀ (hε₁.trans $ mod_cast Nat.one_le_iff_ne_zero.2 hk) $ by positivity) hK₂ hK
     _ _ hB hC
   refine ⟨T, by simpa only [div_pow, div_div_eq_mul_div] using hKT, ?_⟩
   set F := μ_[ℂ] A ∗ 𝟭 B ∗ μ C
diff --git a/LeanAPAP/Physics/DRC.lean b/LeanAPAP/Physics/DRC.lean
index 4887087d8a..b03234478a 100644
--- a/LeanAPAP/Physics/DRC.lean
+++ b/LeanAPAP/Physics/DRC.lean
@@ -126,9 +126,9 @@ lemma drc (hp₂ : 2 ≤ p) (f : G → ℝ≥0) (hf : ∃ x, x ∈ B₁ - B₂ 
         mul_div_right_comm] using h
       positivity
     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 ?_ ?_⟩
+      ?_ $ 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, star_trivial, mul_assoc]
+        wInner_smul_left, smul_eq_mul, star_trivial, mul_assoc]
     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,
@@ -223,7 +223,7 @@ lemma sifting (B₁ B₂ : Finset G) (hε : 0 < ε) (hε₁ : ε ≤ 1) (hδ : 0
         := ?_
     _ ≤ _ :=
       mul_le_of_le_one_left (mul_nonneg (hp.pow_nonneg _) $ hp.pow_nonneg _) $
-        mul_le_one dL1Norm_mu_le_one (NNReal.coe_nonneg _) dL1Norm_mu_le_one
+        mul_le_one₀ dL1Norm_mu_le_one (NNReal.coe_nonneg _) dL1Norm_mu_le_one
     _ ≤ _ := mul_le_mul_of_nonneg_right ?_ $ hp.pow_nonneg _
   · have : 0 ≤ μ_[ℝ] B₁ ○ μ B₂ := dconv_nonneg mu_nonneg mu_nonneg
     simp_rw [← NNReal.coe_mul, ← dL1Norm_dconv mu_nonneg mu_nonneg, dL1Norm_eq_sum_nnnorm,
diff --git a/LeanAPAP/Physics/Unbalancing.lean b/LeanAPAP/Physics/Unbalancing.lean
index adf5dda556..c3709d3f59 100644
--- a/LeanAPAP/Physics/Unbalancing.lean
+++ b/LeanAPAP/Physics/Unbalancing.lean
@@ -1,8 +1,8 @@
 import Mathlib.Algebra.Order.Group.PosPart
+import Mathlib.Analysis.RCLike.Inner
 import Mathlib.Data.Complex.ExponentialBounds
 import LeanAPAP.Prereqs.Convolution.Discrete.Defs
 import LeanAPAP.Prereqs.Function.Indicator.Complex
-import LeanAPAP.Prereqs.Inner.Weighted
 import LeanAPAP.Prereqs.LpNorm.Weighted
 
 /-!
@@ -219,13 +219,13 @@ lemma unbalancing' (p : ℕ) (hp : p ≠ 0) (ε : ℝ) (hε₀ : 0 < ε) (hε₁
           (2⁻¹ : ℝ) ≤ 120 * 1 * 1 * 1 := by norm_num
           _ ≤ 120 * ε⁻¹ * log (3 * ε⁻¹) * p := by
             gcongr
-            · exact one_le_inv hε₀ hε₁
+            · exact (one_le_inv₀ hε₀).2 hε₁
             · rw [← log_exp 1]
               gcongr
               calc
                 exp 1 ≤ 2.7182818286 := exp_one_lt_d9.le
                 _ ≤ 3 * 1 := by norm_num
-                _ ≤ 3 * ε⁻¹ := by gcongr; exact one_le_inv hε₀ hε₁
+                _ ≤ 3 * ε⁻¹ := by gcongr; exact (one_le_inv₀ hε₀).2 hε₁
             · exact mod_cast hp
       _ ≤ 2 * (120 * ε⁻¹ * (3 * ε⁻¹) * p) := by gcongr; exact Real.log_le_self (by positivity)
       _ ≤ 2 * (2 ^ 7 * ε⁻¹ * (2 ^ 2 * ε⁻¹) * p) := by gcongr <;> norm_num
diff --git a/LeanAPAP/Prereqs/AddChar/Basic.lean b/LeanAPAP/Prereqs/AddChar/Basic.lean
index 37d7ec69aa..1d4ae361a9 100644
--- a/LeanAPAP/Prereqs/AddChar/Basic.lean
+++ b/LeanAPAP/Prereqs/AddChar/Basic.lean
@@ -1,6 +1,6 @@
 import Mathlib.Algebra.BigOperators.Expect
 import Mathlib.Algebra.Group.AddChar
-import LeanAPAP.Prereqs.Inner.Weighted
+import Mathlib.Analysis.RCLike.Inner
 
 open Finset hiding card
 open Fintype (card)
@@ -34,8 +34,8 @@ end Semifield
 section RCLike
 variable [RCLike R] [Fintype G]
 
-lemma wInner_compact_self (ψ : AddChar G R) : ⟪(ψ : G → R), ψ⟫ₙ_[R] = 1 := by
-  simp [wInner_compact_eq_expect, ψ.norm_apply, RCLike.conj_mul]
+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
@@ -46,32 +46,32 @@ variable [AddCommGroup G]
 section RCLike
 variable [RCLike R] {ψ₁ ψ₂ : AddChar G R}
 
-lemma wInner_compact_eq_boole [Fintype G] (ψ₁ ψ₂ : 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_compact_self]
+  · rw [h, wInner_cWeight_self]
   have : ψ₁⁻¹ * ψ₂ ≠ 1 := by rwa [Ne, inv_mul_eq_one]
-  simp_rw [wInner_compact_eq_expect, RCLike.inner_apply, ← inv_apply_eq_conj]
+  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_compact_eq_zero_iff_ne [Fintype G] : ⟪(ψ₁ : G → R), ψ₂⟫ₙ_[R] = 0 ↔ ψ₁ ≠ ψ₂ := by
-  rw [wInner_compact_eq_boole, one_ne_zero.ite_eq_right_iff]
+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_compact_eq_one_iff_eq [Fintype G] : ⟪(ψ₁ : G → R), ψ₂⟫ₙ_[R] = 1 ↔ ψ₁ = ψ₂ := by
-  rw [wInner_compact_eq_boole, one_ne_zero.ite_eq_left_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_compact_eq_zero AddChar.coe_ne_zero fun ψ₁ ψ₂ ↦
-    wInner_compact_eq_zero_iff_ne.2
+  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 [FiniteDimensional.finrank_fintype_fun_eq_card] using
+  simpa only [Module.finrank_fintype_fun_eq_card] using
     (AddChar.linearIndependent G R).fintype_card_le_finrank
 
 end RCLike
diff --git a/LeanAPAP/Prereqs/AddChar/MeasurableSpace.lean b/LeanAPAP/Prereqs/AddChar/MeasurableSpace.lean
deleted file mode 100644
index 8153db1443..0000000000
--- a/LeanAPAP/Prereqs/AddChar/MeasurableSpace.lean
+++ /dev/null
@@ -1,10 +0,0 @@
-import Mathlib.Algebra.Group.AddChar
-import Mathlib.MeasureTheory.MeasurableSpace.Defs
-
-namespace AddChar
-variable {A M : Type*} [AddMonoid A] [Monoid M]
-
-instance instMeasurableSpace : MeasurableSpace (AddChar A M) := ⊤
-instance instDiscreteMeasurableSpace : DiscreteMeasurableSpace (AddChar A M) := ⟨fun _ ↦ trivial⟩
-
-end AddChar
diff --git a/LeanAPAP/Prereqs/AddChar/PontryaginDuality.lean b/LeanAPAP/Prereqs/AddChar/PontryaginDuality.lean
index 4a7f2b6b28..e22240be06 100644
--- a/LeanAPAP/Prereqs/AddChar/PontryaginDuality.lean
+++ b/LeanAPAP/Prereqs/AddChar/PontryaginDuality.lean
@@ -142,7 +142,7 @@ 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, FiniteDimensional.finrank_fintype_fun_eq_card]
+    cases nonempty_fintype α; rw [card_eq, Module.finrank_fintype_fun_eq_card]
 
 @[simp, norm_cast]
 lemma coe_complexBasis : ⇑(complexBasis α) = ((⇑) : AddChar α ℂ → α → ℂ) := by
diff --git a/LeanAPAP/Prereqs/Balance/Complex.lean b/LeanAPAP/Prereqs/Balance/Complex.lean
deleted file mode 100644
index e811bde46c..0000000000
--- a/LeanAPAP/Prereqs/Balance/Complex.lean
+++ /dev/null
@@ -1,31 +0,0 @@
-import Mathlib.Algebra.BigOperators.Balance
-import Mathlib.Analysis.RCLike.Basic
-import Mathlib.Data.Complex.BigOperators
-
-open Fintype
-open scoped NNReal
-
-namespace Complex
-variable {ι : Type*}
-
-@[simp] lemma ofReal_comp_balance [Fintype ι] (f : ι → ℝ) :
-    ofReal ∘ balance f = balance (ofReal ∘ f) := by simp [balance]
-
-@[simp] lemma ofReal'_comp_balance [Fintype ι] (f : ι → ℝ) :
-    ofReal' ∘ balance f = balance (ofReal' ∘ f) := ofReal_comp_balance _
-
-end Complex
-
-namespace RCLike
-variable {ι 𝕜 : Type*} [RCLike 𝕜] [Fintype ι] (f : ι → ℝ) (a : ι)
-
-@[simp, norm_cast]
-lemma coe_balance : (↑(balance f a) : 𝕜) = balance ((↑) ∘ f) a := map_balance (algebraMap ..) ..
-
-@[simp] lemma coe_comp_balance : ((↑) : ℝ → 𝕜) ∘ balance f = balance ((↑) ∘ f) :=
-  funext $ coe_balance _
-
-@[simp] lemma ofReal_comp_balance : ofReal ∘ balance f = balance (ofReal ∘ f : ι → 𝕜) := by
-  simp [balance]
-
-end RCLike
diff --git a/LeanAPAP/Prereqs/Chang.lean b/LeanAPAP/Prereqs/Chang.lean
index 744df2bd23..31f47c7b37 100644
--- a/LeanAPAP/Prereqs/Chang.lean
+++ b/LeanAPAP/Prereqs/Chang.lean
@@ -1,6 +1,5 @@
 import Mathlib.Algebra.Order.Chebyshev
 import Mathlib.Analysis.MeanInequalities
-import LeanAPAP.Mathlib.Data.ENNReal.Basic
 import LeanAPAP.Prereqs.Energy
 import LeanAPAP.Prereqs.LargeSpec
 import LeanAPAP.Prereqs.Rudin
@@ -20,7 +19,7 @@ local notation "𝓛" x:arg => 1 + log x⁻¹
 private lemma curlog_pos (hx₀ : 0 ≤ x) (hx₁ : x ≤ 1) : 0 < 𝓛 x := by
   obtain rfl | hx₀ := hx₀.eq_or_lt
   · simp
-  have : 0 ≤ log x⁻¹ := log_nonneg $ one_le_inv (by positivity) hx₁
+  have : 0 ≤ log x⁻¹ := log_nonneg $ (one_le_inv₀ (by positivity)).2 hx₁
   positivity
 
 private lemma rpow_inv_neg_curlog_le (hx₀ : 0 ≤ x) (hx₁ : x ≤ 1) : x⁻¹ ^ (𝓛 x)⁻¹ ≤ exp 1 := by
@@ -28,7 +27,7 @@ private lemma rpow_inv_neg_curlog_le (hx₀ : 0 ≤ x) (hx₁ : x ≤ 1) : x⁻
   · simp; positivity
   obtain rfl | hx₁ := hx₁.eq_or_lt
   · simp
-  have hx := one_lt_inv hx₀ hx₁
+  have hx := (one_lt_inv₀ hx₀).2 hx₁
   calc
     x⁻¹ ^ (𝓛 x)⁻¹ ≤ x⁻¹ ^ (log x⁻¹)⁻¹ := by
       gcongr
@@ -80,7 +79,7 @@ local notation:70 s:70 " ^^ " n:71 => Fintype.piFinset fun _ : Fin n ↦ s
 variable [MeasurableSpace G] [DiscreteMeasurableSpace G]
 
 private lemma α_le_one (f : G → ℂ) : ‖f‖_[1] ^ 2 / ‖f‖_[2] ^ 2 / card G ≤ 1 := by
-  refine div_le_one_of_le (div_le_of_nonneg_of_le_mul ?_ ?_ ?_) ?_
+  refine div_le_one_of_le₀ (div_le_of_le_mul₀ ?_ ?_ ?_) ?_
   any_goals positivity
   rw [dL1Norm_eq_sum_nnnorm, dL2Norm_sq_eq_sum_nnnorm, ← NNReal.coe_le_coe]
   push_cast
@@ -190,7 +189,7 @@ lemma chang (hf : f ≠ 0) (hη : 0 < η) :
       rw [div_self hη.ne', one_pow, one_mul]
     _ = _ := by ring
   refine le_mul_of_one_le_right (by positivity) ?_
-  rw [← inv_pos_le_iff_one_le_mul']
+  rw [← inv_le_iff_one_le_mul₀']
   calc
     α⁻¹ = exp (0 + log α⁻¹) := by rw [zero_add, exp_log]; norm_cast; positivity
     _ ≤ exp ⌈0 + log α⁻¹⌉₊ := by gcongr; exact Nat.le_ceil _
diff --git a/LeanAPAP/Prereqs/Convolution/Discrete/Defs.lean b/LeanAPAP/Prereqs/Convolution/Discrete/Defs.lean
index ed79912197..863ebfd9e8 100644
--- a/LeanAPAP/Prereqs/Convolution/Discrete/Defs.lean
+++ b/LeanAPAP/Prereqs/Convolution/Discrete/Defs.lean
@@ -468,7 +468,7 @@ end CommSemiring
 namespace NNReal
 
 @[simp, norm_cast]
-lemma coe_iterConv (f : G → ℝ≥0) (n : ℕ) (a : G) : (↑((f ∗^ n) a) : ℝ) = ((↑) ∘ f ∗^ n) a :=
+lemma ofReal_iterConv (f : G → ℝ≥0) (n : ℕ) (a : G) : (↑((f ∗^ n) a) : ℝ) = ((↑) ∘ f ∗^ n) a :=
   map_iterConv NNReal.toRealHom _ _ _
 
 end NNReal
@@ -476,7 +476,7 @@ end NNReal
 namespace Complex
 
 @[simp, norm_cast]
-lemma coe_iterConv (f : G → ℝ) (n : ℕ) (a : G) : (↑((f ∗^ n) a) : ℂ) = ((↑) ∘ f ∗^ n) a :=
-  map_iterConv ofReal _ _ _
+lemma ofReal_iterConv (f : G → ℝ) (n : ℕ) (a : G) : (↑((f ∗^ n) a) : ℂ) = ((↑) ∘ f ∗^ n) a :=
+  map_iterConv ofRealHom _ _ _
 
 end Complex
diff --git a/LeanAPAP/Prereqs/Convolution/Norm.lean b/LeanAPAP/Prereqs/Convolution/Norm.lean
index 34945ab8c5..fb96931636 100644
--- a/LeanAPAP/Prereqs/Convolution/Norm.lean
+++ b/LeanAPAP/Prereqs/Convolution/Norm.lean
@@ -1,7 +1,7 @@
 import Mathlib.Algebra.Order.Star.Conjneg
+import Mathlib.Analysis.RCLike.Inner
 import Mathlib.Data.Real.StarOrdered
 import LeanAPAP.Prereqs.Convolution.Discrete.Defs
-import LeanAPAP.Prereqs.Inner.Weighted
 import LeanAPAP.Prereqs.LpNorm.Discrete.Basic
 
 /-!
diff --git a/LeanAPAP/Prereqs/Convolution/ThreeAP.lean b/LeanAPAP/Prereqs/Convolution/ThreeAP.lean
index f81f091e68..fcf911c061 100644
--- a/LeanAPAP/Prereqs/Convolution/ThreeAP.lean
+++ b/LeanAPAP/Prereqs/Convolution/ThreeAP.lean
@@ -1,8 +1,8 @@
+import Mathlib.Analysis.RCLike.Inner
 import Mathlib.Combinatorics.Additive.AP.Three.Defs
 import Mathlib.Data.Real.StarOrdered
 import LeanAPAP.Prereqs.Convolution.Discrete.Defs
 import LeanAPAP.Prereqs.Function.Indicator.Defs
-import LeanAPAP.Prereqs.Inner.Weighted
 
 /-!
 # The convolution characterisation of 3AP-free sets
diff --git a/LeanAPAP/Prereqs/Energy.lean b/LeanAPAP/Prereqs/Energy.lean
index 38ed01cada..8a48e2ebdc 100644
--- a/LeanAPAP/Prereqs/Energy.lean
+++ b/LeanAPAP/Prereqs/Energy.lean
@@ -52,15 +52,15 @@ lemma cLpNorm_dft_indicate_pow (n : ℕ) (s : Finset G) :
   refine Complex.ofReal_injective ?_
   calc
     _ = ⟪dft (𝟭 s ∗^ n), dft (𝟭 s ∗^ n)⟫ₙ_[ℂ] := ?_
-    _ = ⟪𝟭 s ∗^ n, 𝟭 s ∗^ n⟫_[ℂ] := wInner_compact_dft _ _
+    _ = ⟪𝟭 s ∗^ n, 𝟭 s ∗^ n⟫_[ℂ] := wInner_cWeight_dft _ _
     _ = _ := ?_
   · rw [cLpNorm_pow_eq_expect_norm]
     simp_rw [pow_mul', ← norm_pow _ n, Complex.ofReal_expect, Complex.ofReal_pow,
-      ← Complex.conj_mul', wInner_compact_eq_expect, inner_apply, dft_iterConv_apply]
+      ← Complex.conj_mul', wInner_cWeight_eq_expect, inner_apply, dft_iterConv_apply]
     positivity
   · simp only [wInner_one_eq_sum, inner_apply, boringEnergy_eq, Complex.ofReal_mul,
       Complex.ofReal_natCast, Complex.ofReal_sum, Complex.ofReal_pow, mul_eq_mul_left_iff,
-      Nat.cast_eq_zero, Fintype.card_ne_zero, or_false, sq, Complex.coe_iterConv,
+      Nat.cast_eq_zero, Fintype.card_ne_zero, or_false, sq, Complex.ofReal_iterConv,
       (((indicate_isSelfAdjoint _).iterConv _).apply _).conj_eq, Complex.ofReal_comp_indicate]
 
 lemma cL2Norm_dft_indicate (s : Finset G) : ‖dft (𝟭 s)‖ₙ_[2] = sqrt s.card := by
diff --git a/LeanAPAP/Prereqs/FourierTransform/Compact.lean b/LeanAPAP/Prereqs/FourierTransform/Compact.lean
index 1c371f2bdd..e5ffd3fc1e 100644
--- a/LeanAPAP/Prereqs/FourierTransform/Compact.lean
+++ b/LeanAPAP/Prereqs/FourierTransform/Compact.lean
@@ -32,17 +32,18 @@ lemma cft_apply (f : α → ℂ) (ψ : AddChar α ℂ) : cft f ψ = ⟪ψ, f⟫
   ext; simp [wInner_sub_right, cft_apply]
 
 @[simp] lemma cft_const (a : ℂ) (hψ : ψ ≠ 0) : cft (const α a) ψ = 0 := by
-  simp only [cft_apply, wInner_compact_eq_expect, inner_apply, const_apply, ← expect_mul,
+  simp only [cft_apply, wInner_cWeight_eq_expect, inner_apply, const_apply, ← expect_mul,
     ← map_expect, expect_eq_zero_iff_ne_zero.2 hψ, map_zero, zero_mul]
 
-@[simp] lemma cft_smul {𝕝 : Type*} [CommSemiring 𝕝] [Algebra 𝕝 ℂ] [IsScalarTower 𝕝 ℂ ℂ] (c : 𝕝)
-    (f : α → ℂ) : cft (c • f) = c • cft f := by ext; simp [wInner_smul_right, cft_apply]
+@[simp] lemma cft_smul {𝕝 : Type*} [CommSemiring 𝕝] [StarRing 𝕝] [Algebra 𝕝 ℂ] [StarModule 𝕝 ℂ]
+    [IsScalarTower 𝕝 ℂ ℂ] (c : 𝕝) (f : α → ℂ) :  cft (c • f) = c • cft f := by
+  ext; simp [wInner_smul_right, cft_apply]
 
 /-- **Parseval-Plancherel identity** for the discrete Fourier transform. -/
 @[simp] lemma wInner_one_cft (f g : α → ℂ) : ⟪cft f, cft g⟫_[ℂ] = ⟪f, g⟫ₙ_[ℂ] := by
   classical
   unfold cft
-  simp_rw [wInner_one_eq_sum, wInner_compact_eq_expect, inner_apply, map_expect, map_mul,
+  simp_rw [wInner_one_eq_sum, wInner_cWeight_eq_expect, inner_apply, map_expect, map_mul,
     starRingEnd_self_apply, expect_mul, mul_expect, ← expect_sum_comm,
     mul_mul_mul_comm _ (conj $ f _), ← sum_mul, ← AddChar.inv_apply_eq_conj, ← map_neg_eq_inv,
     ← map_add_eq_mul, AddChar.sum_apply_eq_ite]
@@ -52,11 +53,11 @@ lemma cft_apply (f : α → ℂ) (ψ : AddChar α ℂ) : cft f ψ = ⟪ψ, f⟫
 @[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
-    push_cast; simpa only [RCLike.wInner_compact_self, wInner_one_self] using wInner_one_cft f f
+    push_cast; simpa only [RCLike.wInner_cWeight_self, wInner_one_self] using wInner_one_cft f f
 
 /-- **Fourier inversion** for the discrete Fourier transform. -/
 lemma cft_inversion (f : α → ℂ) (a : α) : ∑ ψ, cft f ψ * ψ a = f a := by
-  classical simp_rw [cft, wInner_compact_eq_expect, inner_apply, expect_mul, ← expect_sum_comm,
+  classical simp_rw [cft, wInner_cWeight_eq_expect, inner_apply, expect_mul, ← expect_sum_comm,
     mul_right_comm _ (f _), ← sum_mul, ← AddChar.inv_apply_eq_conj, inv_mul_eq_div,
     ← map_sub_eq_div, AddChar.sum_apply_eq_ite, sub_eq_zero, ite_mul, zero_mul,
     Fintype.expect_ite_eq]
@@ -70,7 +71,7 @@ lemma dft_cft_doubleDualEmb (f : α → ℂ) (a : α) : dft (cft f) (doubleDualE
     map_neg_eq_inv, AddChar.inv_apply_eq_conj, doubleDualEmb_apply]
 
 lemma cft_dft_doubleDualEmb (f : α → ℂ) (a : α) : cft (dft f) (doubleDualEmb a) = f (-a) := by
-  simp only [← dft_inversion f (-a), mul_comm (conj _), cft_apply, wInner_compact_eq_expect,
+  simp only [← dft_inversion f (-a), mul_comm (conj _), cft_apply, wInner_cWeight_eq_expect,
     inner_apply, map_neg_eq_inv, AddChar.inv_apply_eq_conj, doubleDualEmb_apply]
 
 lemma dft_cft (f : α → ℂ) : dft (cft f) = f ∘ doubleDualEquiv.symm ∘ Neg.neg :=
@@ -85,16 +86,16 @@ lemma cft_injective : Injective (cft : (α → ℂ) → AddChar α ℂ → ℂ)
   funext fun a ↦ (cft_inversion _ _).symm.trans $ by rw [h, cft_inversion]
 
 lemma cft_inv (ψ : AddChar α ℂ) (hf : IsSelfAdjoint f) : cft f ψ⁻¹ = conj (cft f ψ) := by
-  simp_rw [cft_apply, wInner_compact_eq_expect, inner_apply, map_expect, AddChar.inv_apply',
+  simp_rw [cft_apply, wInner_cWeight_eq_expect, inner_apply, map_expect, AddChar.inv_apply',
     map_mul, AddChar.inv_apply_eq_conj, Complex.conj_conj, (hf.apply _).conj_eq]
 
 @[simp]
 lemma cft_conj (f : α → ℂ) (ψ : AddChar α ℂ) : cft (conj f) ψ = conj (cft f ψ⁻¹) := by
-  simp only [cft_apply, wInner_compact_eq_expect, inner_apply, map_expect, map_mul, ← inv_apply',
+  simp only [cft_apply, wInner_cWeight_eq_expect, inner_apply, map_expect, map_mul, ← inv_apply',
     ← inv_apply_eq_conj, inv_inv, Pi.conj_apply]
 
 lemma cft_conjneg_apply (f : α → ℂ) (ψ : AddChar α ℂ) : cft (conjneg f) ψ = conj (cft f ψ) := by
-  simp only [cft_apply, wInner_compact_eq_expect, inner_apply, conjneg_apply, map_expect, map_mul,
+  simp only [cft_apply, wInner_cWeight_eq_expect, inner_apply, conjneg_apply, map_expect, map_mul,
     RCLike.conj_conj]
   refine Fintype.expect_equiv (Equiv.neg _) _ _ fun i ↦ ?_
   simp only [Equiv.neg_apply, ← inv_apply_eq_conj, ← inv_apply', inv_apply]
@@ -107,14 +108,14 @@ lemma cft_conjneg (f : α → ℂ) : cft (conjneg f) = conj (cft f) := funext $
 
 lemma cft_dilate (f : α → ℂ) (ψ : AddChar α ℂ) (hn : (card α).Coprime n) :
     cft (dilate f n) ψ = cft f (ψ ^ n) := by
-  simp_rw [cft_apply, wInner_compact_eq_expect, dilate]
+  simp_rw [cft_apply, wInner_cWeight_eq_expect, dilate]
   rw [← Nat.card_eq_fintype_card] at hn
   refine (Fintype.expect_bijective _ hn.nsmul_right_bijective _ _  ?_).symm
   simp only [pow_apply, ← map_nsmul_eq_pow, zmod_val_inv_nsmul_nsmul hn, forall_const]
 
 @[simp] lemma cft_trivNChar [DecidableEq α] : cft (trivNChar : α → ℂ) = 1 := by
   ext
-  simp [trivChar_apply, cft_apply, wInner_compact_eq_expect, ← map_expect, card_univ, NNRat.smul_def]
+  simp [trivChar_apply, cft_apply, wInner_cWeight_eq_expect, ← map_expect, card_univ, NNRat.smul_def]
 
 @[simp] lemma cft_one : cft (1 : α → ℂ) = trivChar :=
   dft_injective $ by classical rw [dft_trivChar, dft_cft, Pi.one_comp]
@@ -122,11 +123,11 @@ lemma cft_dilate (f : α → ℂ) (ψ : AddChar α ℂ) (hn : (card α).Coprime
 variable [DecidableEq α]
 
 @[simp] lemma cft_indicate_zero (s : Finset α) : cft (𝟭 s) 0 = s.dens := by
-  simp [cft_apply, wInner_compact_eq_expect, inner_apply, expect_indicate, AddChar.zero_apply,
+  simp [cft_apply, wInner_cWeight_eq_expect, inner_apply, expect_indicate, AddChar.zero_apply,
     map_one, one_mul, dens, NNRat.smul_def (K := ℂ), div_eq_inv_mul]
 
 lemma cft_cconv_apply (f g : α → ℂ) (ψ : AddChar α ℂ) : cft (f ∗ₙ g) ψ = cft f ψ * cft g ψ := by
-  simp_rw [cft, wInner_compact_eq_expect, inner_apply, cconv_eq_expect_sub', mul_expect, expect_mul,
+  simp_rw [cft, wInner_cWeight_eq_expect, inner_apply, cconv_eq_expect_sub', mul_expect, expect_mul,
     ← expect_product', univ_product_univ]
   refine Fintype.expect_equiv ((Equiv.prodComm _ _).trans $
     ((Equiv.refl _).prodShear Equiv.subRight).trans $ Equiv.prodComm _ _)  _ _ fun (a, b) ↦ ?_
diff --git a/LeanAPAP/Prereqs/FourierTransform/Convolution.lean b/LeanAPAP/Prereqs/FourierTransform/Convolution.lean
index ca536580bc..91929abcea 100644
--- a/LeanAPAP/Prereqs/FourierTransform/Convolution.lean
+++ b/LeanAPAP/Prereqs/FourierTransform/Convolution.lean
@@ -1,4 +1,3 @@
-import LeanAPAP.Prereqs.AddChar.MeasurableSpace
 import LeanAPAP.Prereqs.AddChar.PontryaginDuality
 import LeanAPAP.Prereqs.Convolution.Compact
 import LeanAPAP.Prereqs.Function.Indicator.Defs
diff --git a/LeanAPAP/Prereqs/FourierTransform/Discrete.lean b/LeanAPAP/Prereqs/FourierTransform/Discrete.lean
index f530b64f15..0c21e5a123 100644
--- a/LeanAPAP/Prereqs/FourierTransform/Discrete.lean
+++ b/LeanAPAP/Prereqs/FourierTransform/Discrete.lean
@@ -1,5 +1,5 @@
 import Mathlib.Algebra.BigOperators.Balance
-import LeanAPAP.Prereqs.AddChar.MeasurableSpace
+import Mathlib.MeasureTheory.Constructions.AddChar
 import LeanAPAP.Prereqs.AddChar.PontryaginDuality
 import LeanAPAP.Prereqs.Convolution.Discrete.Defs
 import LeanAPAP.Prereqs.Function.Indicator.Defs
@@ -36,14 +36,16 @@ lemma dft_apply (f : α → ℂ) (ψ : AddChar α ℂ) : dft f ψ = ⟪ψ, f⟫_
   simp only [dft_apply, wInner_one_eq_sum, inner_apply, const_apply, ← sum_mul, ← map_sum,
     sum_eq_zero_iff_ne_zero.2 hψ, map_zero, zero_mul]
 
-@[simp] lemma dft_smul {𝕝 : Type*} [CommSemiring 𝕝] [Algebra 𝕝 ℂ] [IsScalarTower 𝕝 ℂ ℂ] (c : 𝕝)
-    (f : α → ℂ) : dft (c • f) = c • dft f := by ext; simp [wInner_smul_right, dft_apply]
+@[simp]
+lemma dft_smul {𝕝 : Type*} [CommSemiring 𝕝] [StarRing 𝕝] [Algebra 𝕝 ℂ] [StarModule 𝕝 ℂ]
+    [IsScalarTower 𝕝 ℂ ℂ] (c : 𝕝) (f : α → ℂ) : dft (c • f) = c • dft f := by
+  ext; simp [wInner_smul_right, dft_apply]
 
 /-- **Parseval-Plancherel identity** for the discrete Fourier transform. -/
-@[simp] lemma wInner_compact_dft (f g : α → ℂ) : ⟪dft f, dft g⟫ₙ_[ℂ] = ⟪f, g⟫_[ℂ] := by
+@[simp] lemma wInner_cWeight_dft (f g : α → ℂ) : ⟪dft f, dft g⟫ₙ_[ℂ] = ⟪f, g⟫_[ℂ] := by
   classical
   unfold dft
-  simp_rw [wInner_one_eq_sum, wInner_compact_eq_expect, inner_apply, map_sum, map_mul,
+  simp_rw [wInner_one_eq_sum, wInner_cWeight_eq_expect, inner_apply, map_sum, map_mul,
     starRingEnd_self_apply, sum_mul, mul_sum, expect_sum_comm, mul_mul_mul_comm _ (conj $ f _),
     ← expect_mul, ← AddChar.inv_apply_eq_conj, ← map_neg_eq_inv, ← map_add_eq_mul,
     AddChar.expect_apply_eq_ite, add_neg_eq_zero, boole_mul, Fintype.sum_ite_eq]
@@ -52,7 +54,7 @@ lemma dft_apply (f : α → ℂ) (ψ : AddChar α ℂ) : dft f ψ = ⟪ψ, f⟫_
 @[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
-    push_cast; simpa only [RCLike.wInner_compact_self, wInner_one_self] using wInner_compact_dft f f
+    push_cast; simpa only [RCLike.wInner_cWeight_self, wInner_one_self] using wInner_cWeight_dft f f
 
 /-- **Fourier inversion** for the discrete Fourier transform. -/
 lemma dft_inversion (f : α → ℂ) (a : α) : 𝔼 ψ, dft f ψ * ψ a = f a := by
diff --git a/LeanAPAP/Prereqs/Function/Indicator/Complex.lean b/LeanAPAP/Prereqs/Function/Indicator/Complex.lean
index 137672b9e3..ec3a718a75 100644
--- a/LeanAPAP/Prereqs/Function/Indicator/Complex.lean
+++ b/LeanAPAP/Prereqs/Function/Indicator/Complex.lean
@@ -37,7 +37,7 @@ end NNReal
 namespace Complex
 
 @[simp, norm_cast] lemma ofReal_indicate (s : Finset α) (x : α) : ↑(𝟭_[ℝ] s x) = 𝟭_[ℂ] s x :=
-  map_indicate ofReal _ _
+  map_indicate ofRealHom _ _
 
 @[simp] lemma ofReal_comp_indicate (s : Finset α) : (↑) ∘ 𝟭_[ℝ] s = 𝟭_[ℂ] s := by
   ext; exact ofReal_indicate _ _
diff --git a/LeanAPAP/Prereqs/Inner/Function.lean b/LeanAPAP/Prereqs/Inner/Function.lean
index 31615d33de..57c371ead3 100644
--- a/LeanAPAP/Prereqs/Inner/Function.lean
+++ b/LeanAPAP/Prereqs/Inner/Function.lean
@@ -1,6 +1,6 @@
 import Mathlib.Algebra.BigOperators.Expect
+import Mathlib.Analysis.RCLike.Inner
 import LeanAPAP.Prereqs.Function.Indicator.Defs
-import LeanAPAP.Prereqs.Inner.Weighted
 
 open Finset RCLike
 open scoped BigOperators ComplexConjugate
diff --git a/LeanAPAP/Prereqs/Inner/Hoelder/Compact.lean b/LeanAPAP/Prereqs/Inner/Hoelder/Compact.lean
index 8704990d88..16f63c0167 100644
--- a/LeanAPAP/Prereqs/Inner/Hoelder/Compact.lean
+++ b/LeanAPAP/Prereqs/Inner/Hoelder/Compact.lean
@@ -13,17 +13,17 @@ variable {ι κ 𝕜 : Type*} [Fintype ι]
 namespace RCLike
 variable [RCLike 𝕜] {mι : MeasurableSpace ι} [DiscreteMeasurableSpace ι] {f : ι → 𝕜}
 
-@[simp] lemma wInner_compact_self (f : ι → 𝕜) :
+@[simp] lemma wInner_cWeight_self (f : ι → 𝕜) :
     ⟪f, f⟫ₙ_[𝕜] = ((‖f‖ₙ_[2] : ℝ) : 𝕜) ^ 2 := by
   simp_rw [← algebraMap.coe_pow, ← NNReal.coe_pow]
-  simp [cL2Norm_sq_eq_expect_nnnorm, wInner_compact_eq_expect, RCLike.conj_mul]
+  simp [cL2Norm_sq_eq_expect_nnnorm, wInner_cWeight_eq_expect, RCLike.conj_mul]
 
 lemma cL1Norm_mul (f g : ι → 𝕜) : ‖f * g‖ₙ_[1] = ⟪fun i ↦ ‖f i‖, fun i ↦ ‖g i‖⟫ₙ_[ℝ] := by
-  simp [wInner_compact_eq_expect, cL1Norm_eq_expect_nnnorm]
+  simp [wInner_cWeight_eq_expect, cL1Norm_eq_expect_nnnorm]
 
 /-- **Cauchy-Schwarz inequality** -/
-lemma wInner_compact_le_cL2Norm_mul_cL2Norm (f g : ι → ℝ) : ⟪f, g⟫ₙ_[ℝ] ≤ ‖f‖ₙ_[2] * ‖g‖ₙ_[2] := by
-  simp only [wInner_compact_eq_smul_wInner_one, cL2Norm_eq_expect_nnnorm, ← NNReal.coe_mul, expect,
+lemma wInner_cWeight_le_cL2Norm_mul_cL2Norm (f g : ι → ℝ) : ⟪f, g⟫ₙ_[ℝ] ≤ ‖f‖ₙ_[2] * ‖g‖ₙ_[2] := by
+  simp only [wInner_cWeight_eq_smul_wInner_one, cL2Norm_eq_expect_nnnorm, ← NNReal.coe_mul, expect,
     NNReal.coe_nnqsmul, ← NNRat.cast_smul_eq_nnqsmul ℝ≥0, smul_eq_mul, ← NNReal.mul_rpow,
     mul_mul_mul_comm, ← sq]
   simp only [NNReal.mul_rpow, ← dL2Norm_eq_sum_nnnorm, card_univ]
@@ -45,12 +45,12 @@ lemma cL1Norm_mul_of_nonneg (hf : 0 ≤ f) (hg : 0 ≤ g) : ‖f * g‖ₙ_[1] =
   convert cL1Norm_mul f g using 2 <;> ext a <;> refine (norm_of_nonneg ?_).symm; exacts [hf _, hg _]
 
 /-- **Hölder's inequality**, binary case. -/
-lemma wInner_compact_le_cLpNorm_mul_cLpNorm (hpq : p.IsConjExponent q) (f g : α → ℝ) :
+lemma wInner_cWeight_le_cLpNorm_mul_cLpNorm (hpq : p.IsConjExponent q) (f g : α → ℝ) :
     ⟪f, g⟫ₙ_[ℝ] ≤ ‖f‖ₙ_[p] * ‖g‖ₙ_[q] := by
   have hp := hpq.ne_zero
   have hq := hpq.symm.ne_zero
   norm_cast at hp hq
-  rw [wInner_compact_eq_expect, expect_eq_sum_div_card, cLpNorm_eq_expect_nnnorm hp,
+  rw [wInner_cWeight_eq_expect, expect_eq_sum_div_card, cLpNorm_eq_expect_nnnorm hp,
     cLpNorm_eq_expect_nnnorm hq, expect_eq_sum_div_card, expect_eq_sum_div_card,
     NNReal.div_rpow, NNReal.div_rpow, ← NNReal.coe_mul, div_mul_div_comm, ← NNReal.rpow_add',
     hpq.coe.inv_add_inv_conj, NNReal.rpow_one]
@@ -61,10 +61,10 @@ lemma wInner_compact_le_cLpNorm_mul_cLpNorm (hpq : p.IsConjExponent q) (f g : α
   · simp [hpq.coe.inv_add_inv_conj]
 
 /-- **Hölder's inequality**, binary case. -/
-lemma abs_wInner_compact_le_dLpNorm_mul_dLpNorm (hpq : p.IsConjExponent q) (f g : α → ℝ) :
+lemma abs_wInner_cWeight_le_dLpNorm_mul_dLpNorm (hpq : p.IsConjExponent q) (f g : α → ℝ) :
     |⟪f, g⟫ₙ_[ℝ]| ≤ ‖f‖ₙ_[p] * ‖g‖ₙ_[q] :=
-  (abs_wInner_le_wInner_abs fun _ ↦ by dsimp; positivity).trans $
-    (wInner_compact_le_cLpNorm_mul_cLpNorm hpq _ _).trans_eq $ by simp_rw [cLpNorm_abs]
+  (abs_wInner_le fun _ ↦ by dsimp; positivity).trans $
+    (wInner_cWeight_le_cLpNorm_mul_cLpNorm hpq _ _).trans_eq $ by simp_rw [cLpNorm_abs]
 
 end Real
 
@@ -72,17 +72,17 @@ section Hoelder
 variable {α : Type*} {mα : MeasurableSpace α} [DiscreteMeasurableSpace α] [Fintype α] [RCLike 𝕜]
   {p q : ℝ≥0} {f g : α → 𝕜}
 
-lemma norm_wInner_compact_le (f g : α → 𝕜) :
+lemma norm_wInner_cWeight_le (f g : α → 𝕜) :
     ‖⟪f, g⟫ₙ_[𝕜]‖₊ ≤ ⟪fun a ↦ ‖f a‖, fun a ↦ ‖g a‖⟫ₙ_[ℝ] := by
-  simpa [wInner_compact_eq_expect, norm_mul]
+  simpa [wInner_cWeight_eq_expect, norm_mul]
     using norm_expect_le (K := ℝ) (f := fun i ↦ conj (f i) * g i)
 
 /-- **Hölder's inequality**, binary case. -/
-lemma nnnorm_wInner_compact_le_dLpNorm_mul_dLpNorm (hpq : p.IsConjExponent q) (f g : α → 𝕜) :
+lemma nnnorm_wInner_cWeight_le_dLpNorm_mul_dLpNorm (hpq : p.IsConjExponent q) (f g : α → 𝕜) :
     ‖⟪f, g⟫ₙ_[𝕜]‖₊ ≤ ‖f‖ₙ_[p] * ‖g‖ₙ_[q] :=
   calc
-    _ ≤ ⟪fun a ↦ ‖f a‖, fun a ↦ ‖g a‖⟫ₙ_[ℝ] := norm_wInner_compact_le _ _
-    _ ≤ ‖fun a ↦ ‖f a‖‖ₙ_[p] * ‖fun a ↦ ‖g a‖‖ₙ_[q] := wInner_compact_le_cLpNorm_mul_cLpNorm hpq _ _
+    _ ≤ ⟪fun a ↦ ‖f a‖, fun a ↦ ‖g a‖⟫ₙ_[ℝ] := norm_wInner_cWeight_le _ _
+    _ ≤ ‖fun a ↦ ‖f a‖‖ₙ_[p] * ‖fun a ↦ ‖g a‖‖ₙ_[q] := wInner_cWeight_le_cLpNorm_mul_cLpNorm hpq _ _
     _ = ‖f‖ₙ_[p] * ‖g‖ₙ_[q] := by simp_rw [cLpNorm_norm]
 
 /-- **Hölder's inequality**, binary case. -/
@@ -97,7 +97,7 @@ lemma cLpNorm_mul_le (hp : p ≠ 0) (hq : q ≠ 0) (r : ℝ≥0) (hpqr : p⁻¹
   push_cast
   rw [cL1Norm_mul_of_nonneg, mul_rpow, ← NNReal.coe_rpow, ← NNReal.coe_rpow, cLpNorm_rpow',
     cLpNorm_rpow', ← ENNReal.coe_div, ← ENNReal.coe_div]
-  refine wInner_compact_le_cLpNorm_mul_cLpNorm ⟨?_, ?_⟩ _ _
+  refine wInner_cWeight_le_cLpNorm_mul_cLpNorm ⟨?_, ?_⟩ _ _
   · norm_cast
     rw [div_eq_mul_inv, ← hpqr, mul_add, mul_inv_cancel₀ hp]
     exact lt_add_of_pos_right _ (by positivity)
diff --git a/LeanAPAP/Prereqs/Inner/Hoelder/Discrete.lean b/LeanAPAP/Prereqs/Inner/Hoelder/Discrete.lean
index 97c06ca62c..6f62abb706 100644
--- a/LeanAPAP/Prereqs/Inner/Hoelder/Discrete.lean
+++ b/LeanAPAP/Prereqs/Inner/Hoelder/Discrete.lean
@@ -1,4 +1,4 @@
-import LeanAPAP.Prereqs.Inner.Weighted
+import Mathlib.Analysis.RCLike.Inner
 import LeanAPAP.Prereqs.LpNorm.Discrete.Defs
 
 /-! # Inner product -/
@@ -48,7 +48,7 @@ lemma wInner_one_le_dLpNorm_mul_dLpNorm (hpq : p.IsConjExponent q) (f g : α →
 /-- **Hölder's inequality**, binary case. -/
 lemma abs_wInner_one_le_dLpNorm_mul_dLpNorm (hpq : p.IsConjExponent q) (f g : α → ℝ) :
     |⟪f, g⟫_[ℝ]| ≤ ‖f‖_[p] * ‖g‖_[q] :=
-  (abs_wInner_le_wInner_abs zero_le_one).trans $
+  (abs_wInner_le zero_le_one).trans $
     (wInner_one_le_dLpNorm_mul_dLpNorm hpq _ _).trans_eq $ by simp_rw [dLpNorm_abs]
 
 end Real
diff --git a/LeanAPAP/Prereqs/Inner/Weighted.lean b/LeanAPAP/Prereqs/Inner/Weighted.lean
deleted file mode 100644
index 213d0387ed..0000000000
--- a/LeanAPAP/Prereqs/Inner/Weighted.lean
+++ /dev/null
@@ -1,134 +0,0 @@
-import Mathlib.Analysis.InnerProductSpace.PiL2
-
-/-! # Inner product -/
-
-open Finset Function Real
-open scoped BigOperators ComplexConjugate ENNReal NNReal NNRat
-
-variable {ι κ 𝕜 : Type*} {E : ι → Type*} [Fintype ι]
-
-namespace RCLike
-variable [RCLike 𝕜]
-
-section Pi
-variable [∀ i, SeminormedAddCommGroup (E i)] [∀ i, InnerProductSpace 𝕜 (E i)] {w : ι → ℝ}
-
-/-- Inner product giving rise to the L2 norm. -/
-def wInner (w : ι → ℝ) (f g : ∀ i, E i) : 𝕜 := ∑ i, w i • inner (f i) (g i)
-
-noncomputable abbrev compact : ι → ℝ := Function.const _ (Fintype.card ι)⁻¹
-
-notation "⟪" f ", " g "⟫_[" 𝕝 ", " w "]" => wInner (𝕜 := 𝕝) w f g
-notation "⟪" f ", " g "⟫_[" 𝕝 "]" => ⟪f, g⟫_[𝕝, 1]
-notation "⟪" f ", " g "⟫ₙ_[" 𝕝 "]" => ⟪f, g⟫_[𝕝, compact]
-
-lemma wInner_compact_eq_smul_wInner_one (f g : ∀ i, E i) :
-    ⟪f, g⟫ₙ_[𝕜] = (Fintype.card ι : ℚ≥0)⁻¹ • ⟪f, g⟫_[𝕜] := by
-  simp [wInner, smul_sum, ← NNRat.cast_smul_eq_nnqsmul ℝ]
-
-@[simp] lemma conj_wInner_symm (w : ι → ℝ) (f g : ∀ i, E i) :
-    conj ⟪f, g⟫_[𝕜, w] = ⟪g, f⟫_[𝕜, w] := by
-  simp [wInner, map_sum, inner_conj_symm, rclike_simps]
-
-@[simp] lemma wInner_zero_left (w : ι → ℝ) (g : ∀ i, E i) : ⟪0, g⟫_[𝕜, w] = 0 := by simp [wInner]
-@[simp] lemma wInner_zero_right (w : ι → ℝ) (f : ∀ i, E i) : ⟪f, 0⟫_[𝕜, w] = 0 := by simp [wInner]
-
-lemma wInner_add_left (w : ι → ℝ) (f₁ f₂ g : ∀ i, E i) :
-    ⟪f₁ + f₂, g⟫_[𝕜, w] = ⟪f₁, g⟫_[𝕜, w] + ⟪f₂, g⟫_[𝕜, w] := by
-  simp [wInner, inner_add_left, smul_add, sum_add_distrib]
-
-lemma wInner_add_right (w : ι → ℝ) (f g₁ g₂ : ∀ i, E i) :
-    ⟪f, g₁ + g₂⟫_[𝕜, w] = ⟪f, g₁⟫_[𝕜, w] + ⟪f, g₂⟫_[𝕜, w] := by
-  simp [wInner, inner_add_right, smul_add, sum_add_distrib]
-
-@[simp] lemma wInner_neg_left (w : ι → ℝ) (f g : ∀ i, E i) : ⟪-f, g⟫_[𝕜, w] = -⟪f, g⟫_[𝕜, w] := by
-  simp [wInner]
-
-@[simp] lemma wInner_neg_right (w : ι → ℝ) (f g : ∀ i, E i) : ⟪f, -g⟫_[𝕜, w] = -⟪f, g⟫_[𝕜, w] := by
-  simp [wInner]
-
-lemma wInner_sub_left (w : ι → ℝ) (f₁ f₂ g : ∀ i, E i) :
-    ⟪f₁ - f₂, g⟫_[𝕜, w] = ⟪f₁, g⟫_[𝕜, w] - ⟪f₂, g⟫_[𝕜, w] := by
-  simp_rw [sub_eq_add_neg, wInner_add_left, wInner_neg_left]
-
-lemma wInner_sub_right (w : ι → ℝ) (f g₁ g₂ : ∀ i, E i) :
-    ⟪f, g₁ - g₂⟫_[𝕜, w] = ⟪f, g₁⟫_[𝕜, w] - ⟪f, g₂⟫_[𝕜, w] := by
-  simp_rw [sub_eq_add_neg, wInner_add_right, wInner_neg_right]
-
-@[simp] lemma wInner_of_isEmpty [IsEmpty ι] (w : ι → ℝ) (f g : ∀ i, E i) : ⟪f, g⟫_[𝕜, w] = 0 := by
-  simp [Subsingleton.elim f 0]
-
-lemma wInner_smul_left (c : 𝕜) (w : ι → ℝ) (f g : ∀ i, E i) :
-    ⟪c • f, g⟫_[𝕜, w] = star c * ⟪f, g⟫_[𝕜, w] := by simp [wInner, mul_sum, inner_smul_left]
-
-lemma wInner_smul_right {𝕝 : Type*} [CommSemiring 𝕝] [Algebra 𝕝 𝕜] [∀ i, Module 𝕝 (E i)]
-    [∀ i, IsScalarTower 𝕝 𝕜 (E i)] (c : 𝕝) (w : ι → ℝ) (f g : ∀ i, E i) :
-    ⟪f, c • g⟫_[𝕜, w] = c • ⟪f, g⟫_[𝕜, w] := by
-  simp_rw [wInner, Pi.smul_apply, ← algebraMap_smul 𝕜 c, inner_smul_right, smul_sum,
-    ← mul_smul_comm, smul_eq_mul]
-
-lemma mul_wInner_left (c : 𝕜) (w : ι → ℝ) (f g : ∀ i, E i) :
-    c * ⟪f, g⟫_[𝕜, w] = ⟪star c • f, g⟫_[𝕜, w] := by rw [wInner_smul_left, star_star]
-
-lemma wInner_one_eq_sum (f g : ∀ i, E i) : ⟪f, g⟫_[𝕜] = ∑ i, inner (f i) (g i) := by simp [wInner]
-lemma wInner_compact_eq_expect (f g : ∀ i, E i) : ⟪f, g⟫ₙ_[𝕜] = 𝔼 i, inner (f i) (g i) := by
-  simp [wInner, expect, smul_sum, ← NNRat.cast_smul_eq_nnqsmul ℝ]
-
-end Pi
-
-section Function
-variable {w : ι → ℝ} {f g : ι → 𝕜}
-
-lemma wInner_const_left (a : 𝕜) (f : ι → 𝕜) :
-    ⟪const _ a, f⟫_[𝕜, w] = conj a * ∑ i, w i • f i := by simp [wInner, const_apply, mul_sum]
-
-lemma wInner_const_right (f : ι → 𝕜) (a : 𝕜) :
-  ⟪f, const _ a⟫_[𝕜, w] = (∑ i, w i • conj (f i)) * a := by simp [wInner, const_apply, sum_mul]
-
-@[simp] lemma wInner_one_const_left (a : 𝕜) (f : ι → 𝕜) :
-    ⟪const _ a, f⟫_[𝕜] = conj a * ∑ i, f i := by simp [wInner_one_eq_sum, mul_sum]
-
-@[simp] lemma wInner_one_const_right (f : ι → 𝕜) (a : 𝕜) :
-    ⟪f, const _ a⟫_[𝕜] = (∑ i, conj (f i)) * a := by simp [wInner_one_eq_sum, sum_mul]
-
-@[simp] lemma wInner_compact_const_left (a : 𝕜) (f : ι → 𝕜) :
-    ⟪const _ a, f⟫ₙ_[𝕜] = conj a * 𝔼 i, f i := by simp [wInner_compact_eq_expect, mul_expect]
-
-@[simp] lemma wInner_compact_const_right (f : ι → 𝕜) (a : 𝕜) :
-    ⟪f, const _ a⟫ₙ_[𝕜] = (𝔼 i, conj (f i)) * a := by simp [wInner_compact_eq_expect, expect_mul]
-
-lemma wInner_one_eq_inner (f g : ι → 𝕜) :
-    ⟪f, g⟫_[𝕜, 1] = inner ((WithLp.equiv 2 _).symm f) ((WithLp.equiv 2 _).symm g) := by
-  simp [wInner]
-
-lemma inner_eq_wInner_one (f g : PiLp 2 fun _i : ι ↦ 𝕜) :
-    inner f g = ⟪WithLp.equiv 2 _ f, WithLp.equiv 2 _ g⟫_[𝕜, 1] := by simp [wInner]
-
-lemma linearIndependent_of_ne_zero_of_wInner_one_eq_zero {f : κ → ι → 𝕜} (hf : ∀ k, f k ≠ 0)
-    (hinner : Pairwise fun k₁ k₂ ↦ ⟪f k₁, f k₂⟫_[𝕜] = 0) : LinearIndependent 𝕜 f := by
-  simp_rw [wInner_one_eq_inner] at hinner
-  have := linearIndependent_of_ne_zero_of_inner_eq_zero ?_ hinner
-  exacts [this, hf]
-
-lemma linearIndependent_of_ne_zero_of_wInner_compact_eq_zero {f : κ → ι → 𝕜} (hf : ∀ k, f k ≠ 0)
-    (hinner : Pairwise fun k₁ k₂ ↦ ⟪f k₁, f k₂⟫_[𝕜, compact] = 0) : LinearIndependent 𝕜 f := by
-  cases isEmpty_or_nonempty ι
-  · have : IsEmpty κ := ⟨fun k ↦ hf k <| Subsingleton.elim ..⟩
-    exact linearIndependent_empty_type
-  · exact linearIndependent_of_ne_zero_of_wInner_one_eq_zero hf <| by
-      simpa [wInner_compact_eq_smul_wInner_one, ← NNRat.cast_smul_eq_nnqsmul 𝕜] using hinner
-
-end Function
-
-section Real
-variable {w f g : ι → ℝ}
-
-lemma wInner_nonneg (hw : 0 ≤ w) (hf : 0 ≤ f) (hg : 0 ≤ g) : 0 ≤ ⟪f, g⟫_[ℝ, w] :=
-  sum_nonneg fun _ _ ↦ mul_nonneg (hw _) <| mul_nonneg (hf _) (hg _)
-
-lemma abs_wInner_le_wInner_abs (hw : 0 ≤ w) : |⟪f, g⟫_[ℝ, w]| ≤ ⟪|f|, |g|⟫_[ℝ, w] :=
-  (abs_sum_le_sum_abs ..).trans_eq <|sum_congr rfl fun i _ ↦ by
-    simp [abs_mul, abs_of_nonneg (hw i)]
-
-end Real
-end RCLike
diff --git a/LeanAPAP/Prereqs/LpNorm/Compact.lean b/LeanAPAP/Prereqs/LpNorm/Compact.lean
index 42a2190810..23ff2b6f59 100644
--- a/LeanAPAP/Prereqs/LpNorm/Compact.lean
+++ b/LeanAPAP/Prereqs/LpNorm/Compact.lean
@@ -1,11 +1,7 @@
-import Mathlib.Algebra.Order.BigOperators.Expect
 import Mathlib.Algebra.Star.Conjneg
-import Mathlib.Data.Finset.Density
 import Mathlib.Data.Fintype.Order
-import Mathlib.Probability.ConditionalProbability
-import LeanAPAP.Mathlib.MeasureTheory.Function.EssSup
-import LeanAPAP.Prereqs.Function.Translate
 import LeanAPAP.Prereqs.Function.Indicator.Defs
+import LeanAPAP.Prereqs.Function.Translate
 import LeanAPAP.Prereqs.NNLpNorm
 
 /-!
@@ -28,7 +24,7 @@ section NormedAddCommGroup
 variable [NormedAddCommGroup E] {p q : ℝ≥0∞} {f g h : α → E}
 
 /-- The Lp norm of a function with the compact normalisation. -/
-noncomputable def cLpNorm (p : ℝ≥0∞) (f : α → E) : ℝ≥0 := nnLpNorm f p .count[|Set.univ]
+noncomputable def cLpNorm (p : ℝ≥0∞) (f : α → E) : ℝ≥0 := nnLpNorm f p (uniformOn .univ)
 
 notation "‖" f "‖ₙ_[" p "]" => cLpNorm p f
 
@@ -126,13 +122,13 @@ end DiscreteMeasurableSpace
 variable [Fintype α]
 
 @[simp] lemma cLpNorm_const [Nonempty α] {p : ℝ≥0∞} (hp : p ≠ 0) (a : E) :
-    ‖fun _i : α ↦ a‖ₙ_[p] = ‖a‖₊ := by simp [cLpNorm, *]
+    ‖fun _i : α ↦ a‖ₙ_[p] = ‖a‖₊ := by simp [cLpNorm, uniformOn, *]
 
 section NormedField
 variable [NormedField 𝕜] {p : ℝ≥0∞} {f g : α → 𝕜}
 
-@[simp] lemma cLpNorm_one [Nonempty α] (hp : p ≠ 0) :
-    ‖(1 : α → 𝕜)‖ₙ_[p] = 1 := by simp [cLpNorm, *]
+@[simp] lemma cLpNorm_one [Nonempty α] (hp : p ≠ 0) : ‖(1 : α → 𝕜)‖ₙ_[p] = 1 := by
+  simp [cLpNorm, uniformOn, *]
 
 end NormedField
 
@@ -140,16 +136,16 @@ variable [DiscreteMeasurableSpace α]
 
 lemma cLpNorm_eq_expect_norm' (hp₀ : p ≠ 0) (hp : p ≠ ∞) (f : α → E) :
     ‖f‖ₙ_[p] = (𝔼 i, ‖f i‖ ^ p.toReal) ^ p.toReal⁻¹ := by
-  simp [cLpNorm, coe_nnLpNorm_eq_integral_norm_rpow_toReal hp₀ hp .of_discrete, one_div, ← mul_sum,
+  simp [cLpNorm, uniformOn, coe_nnLpNorm_eq_integral_norm_rpow_toReal hp₀ hp .of_discrete,
     integral_fintype, tsum_eq_sum' (s := univ) (by simp), ENNReal.coe_rpow_of_nonneg, cond_apply,
-    expect_eq_sum_div_card, div_eq_inv_mul]
+    expect_eq_sum_div_card, div_eq_inv_mul, ← mul_sum]
 
 lemma cLpNorm_eq_expect_nnnorm' (hp₀ : p ≠ 0) (hp : p ≠ ∞) (f : α → E) :
     ‖f‖ₙ_[p] = (𝔼 i, ‖f i‖₊ ^ p.toReal) ^ p.toReal⁻¹ := by
   ext
-  simp [cLpNorm, coe_nnLpNorm_eq_integral_norm_rpow_toReal hp₀ hp .of_discrete, one_div, ← mul_sum,
+  simp [cLpNorm, uniformOn, coe_nnLpNorm_eq_integral_norm_rpow_toReal hp₀ hp .of_discrete,
     integral_fintype, tsum_eq_sum' (s := univ) (by simp), ENNReal.coe_rpow_of_nonneg, cond_apply,
-    expect_eq_sum_div_card, div_eq_inv_mul]
+    expect_eq_sum_div_card, div_eq_inv_mul, ← mul_sum]
 
 lemma cLpNorm_toNNReal_eq_expect_norm {p : ℝ} (hp : 0 < p) (f : α → E) :
     ‖f‖ₙ_[p.toNNReal] = (𝔼 i, ‖f i‖ ^ p) ^ p⁻¹ := by
@@ -212,7 +208,7 @@ lemma cLinftyNorm_eq_iSup_norm (f : α → E) : ‖f‖ₙ_[∞] = ⨆ i, ‖f i
   · simp [cLpNorm, nnLinftyNorm_eq_essSup]
 
 @[simp] lemma cLpNorm_eq_zero (hp : p ≠ 0) : ‖f‖ₙ_[p] = 0 ↔ f = 0 := by
-  simp [cLpNorm, nnLpNorm_eq_zero .of_discrete hp, ae_eq_top.2, cond_apply, Set.finite_univ]
+  simp [cLpNorm, uniformOn, nnLpNorm_eq_zero .of_discrete hp, ae_eq_top.2, cond_apply]
 
 @[simp] lemma cLpNorm_pos (hp : p ≠ 0) : 0 < ‖f‖ₙ_[p] ↔ f ≠ 0 :=
   pos_iff_ne_zero.trans (cLpNorm_eq_zero hp).not
diff --git a/LeanAPAP/Prereqs/LpNorm/Discrete/Defs.lean b/LeanAPAP/Prereqs/LpNorm/Discrete/Defs.lean
index ebfae0c3ab..a494d87caa 100644
--- a/LeanAPAP/Prereqs/LpNorm/Discrete/Defs.lean
+++ b/LeanAPAP/Prereqs/LpNorm/Discrete/Defs.lean
@@ -1,5 +1,4 @@
 import Mathlib.Data.Fintype.Order
-import LeanAPAP.Mathlib.MeasureTheory.Function.EssSup
 import LeanAPAP.Prereqs.NNLpNorm
 
 /-!
diff --git a/LeanAPAP/Prereqs/Rudin.lean b/LeanAPAP/Prereqs/Rudin.lean
index f21a8e6a60..405c8fc81e 100644
--- a/LeanAPAP/Prereqs/Rudin.lean
+++ b/LeanAPAP/Prereqs/Rudin.lean
@@ -1,6 +1,5 @@
 import Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
 import Mathlib.Analysis.SpecialFunctions.Trigonometric.Series
-import LeanAPAP.Mathlib.Data.ENNReal.Basic
 import LeanAPAP.Prereqs.FourierTransform.Compact
 import LeanAPAP.Prereqs.Randomisation
 
@@ -83,7 +82,7 @@ private lemma rudin_ineq_aux (hp : 2 ≤ p) (f : α → ℂ) (hf : AddDissociate
       _ ≤ 𝔼 a, |(f a).re| ^ p / p ! := by gcongr; norm_cast; exact p.factorial_le_pow
       _ ≤ 𝔼 a, exp |(f a).re| := by gcongr; exact pow_div_factorial_le_exp _ (abs_nonneg _) _
       _ ≤ _ := rudin_exp_abs_ineq f hf
-      _ ≤ 2 ^ p * exp (‖f‖ₙ_[2] ^ 2 / 2) := by gcongr; exact le_self_pow one_le_two hp₀
+      _ ≤ 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) ?_
diff --git a/lake-manifest.json b/lake-manifest.json
index d5319ed35d..2cc5b6d395 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "f274aed7ae8d1addd3e70adaf3183ccc6e1ed43d",
+   "rev": "daf1ed91789811cf6bbb7bf2f4dad6b3bad8fbf4",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -15,7 +15,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "2c8ae451ce9ffc83554322b14437159c1a9703f9",
+   "rev": "fa3d73a2cf077f4b14c7840352ac7b08aeb6eb41",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -25,7 +25,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "ff420521a0c098891f4f44ecda9dd7ff57b50bad",
+   "rev": "b20a88676fd00affb90cbc9f1ff004ae588103b3",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -35,16 +35,16 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "eb08eee94098fe530ccd6d8751a86fe405473d4c",
+   "rev": "cd20dae87c48495f0220663014dff11671597fcf",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.42",
+   "inputRev": "v0.0.43-pre",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover/lean4-cli",
    "type": "git",
    "subDir": null,
-   "scope": "",
+   "scope": "leanprover",
    "rev": "2cf1030dc2ae6b3632c84a09350b675ef3e347d0",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
@@ -55,7 +55,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "e285a7ade149c551c17a4b24f127e1ef782e4bb1",
+   "rev": "9b4088ccf0f44ddd7b1132bb1348aef8cf481e12",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -65,7 +65,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "781beceb959c68b36d3d96205b3531e341879d2c",
+   "rev": "4b61d4abc1659f15ffda5ec24fdebc229d51d066",
    "name": "LeanSearchClient",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -75,7 +75,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "d369bba55fcefeb0d7600e9c2e4856ac9bbece72",
+   "rev": "cfdf6e790c2f52c3f68bdd0e162e0e69427f4e0d",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,
diff --git a/lean-toolchain b/lean-toolchain
index 89985206ac..eff86fd63d 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.12.0
+leanprover/lean4:v4.13.0-rc3