diff --git a/LeanAPAP.lean b/LeanAPAP.lean
index 355f3d9678..798bd1b685 100644
--- a/LeanAPAP.lean
+++ b/LeanAPAP.lean
@@ -5,7 +5,6 @@ import LeanAPAP.Mathlib.Algebra.Group.Basic
 import LeanAPAP.Mathlib.Algebra.Order.Field.Defs
 import LeanAPAP.Mathlib.Algebra.Order.Group.Unbundled.Basic
 import LeanAPAP.Mathlib.Algebra.Star.Rat
-import LeanAPAP.Mathlib.Analysis.Complex.Basic
 import LeanAPAP.Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar
 import LeanAPAP.Mathlib.Analysis.SpecialFunctions.Pow.NNReal
 import LeanAPAP.Mathlib.Analysis.SpecialFunctions.Pow.Real
@@ -14,7 +13,6 @@ import LeanAPAP.Mathlib.Data.Finset.Pointwise.Basic
 import LeanAPAP.Mathlib.Data.Finset.Preimage
 import LeanAPAP.Mathlib.MeasureTheory.Function.EssSup
 import LeanAPAP.Mathlib.MeasureTheory.Function.LpSeminorm.Basic
-import LeanAPAP.Mathlib.Order.ConditionallyCompleteLattice.Basic
 import LeanAPAP.Mathlib.Order.Filter.Basic
 import LeanAPAP.Mathlib.Order.LiminfLimsup
 import LeanAPAP.Mathlib.Tactic.Positivity
@@ -39,18 +37,20 @@ import LeanAPAP.Prereqs.Curlog
 import LeanAPAP.Prereqs.Energy
 import LeanAPAP.Prereqs.Expect.Basic
 import LeanAPAP.Prereqs.Expect.Complex
+import LeanAPAP.Prereqs.Expect.Order
 import LeanAPAP.Prereqs.FourierTransform.Compact
 import LeanAPAP.Prereqs.FourierTransform.Discrete
 import LeanAPAP.Prereqs.Function.Indicator.Basic
 import LeanAPAP.Prereqs.Function.Indicator.Complex
 import LeanAPAP.Prereqs.Function.Indicator.Defs
 import LeanAPAP.Prereqs.Function.Translate
+import LeanAPAP.Prereqs.Inner.Compact.Basic
+import LeanAPAP.Prereqs.Inner.Discrete.Basic
+import LeanAPAP.Prereqs.Inner.Discrete.Defs
 import LeanAPAP.Prereqs.LargeSpec
 import LeanAPAP.Prereqs.LpNorm.Compact.Defs
-import LeanAPAP.Prereqs.LpNorm.Compact.Inner
 import LeanAPAP.Prereqs.LpNorm.Discrete.Basic
 import LeanAPAP.Prereqs.LpNorm.Discrete.Defs
-import LeanAPAP.Prereqs.LpNorm.Discrete.Inner
 import LeanAPAP.Prereqs.LpNorm.Weighted
 import LeanAPAP.Prereqs.MarcinkiewiczZygmund
 import LeanAPAP.Prereqs.NNLpNorm
diff --git a/LeanAPAP/FiniteField/Basic.lean b/LeanAPAP/FiniteField/Basic.lean
index 06a625e3c6..ab1d9c7fcc 100644
--- a/LeanAPAP/FiniteField/Basic.lean
+++ b/LeanAPAP/FiniteField/Basic.lean
@@ -1,12 +1,11 @@
 import Mathlib.FieldTheory.Finite.Basic
 import LeanAPAP.Mathlib.Combinatorics.Additive.FreimanHom
-import LeanAPAP.Mathlib.Data.Finset.Pointwise.Basic
 import LeanAPAP.Mathlib.Data.Finset.Preimage
 import LeanAPAP.Prereqs.Convolution.ThreeAP
 import LeanAPAP.Prereqs.LargeSpec
 import LeanAPAP.Physics.AlmostPeriodicity
-import LeanAPAP.Physics.DRC
 import LeanAPAP.Physics.Unbalancing
+import LeanAPAP.Prereqs.Function.Indicator.Complex
 
 /-!
 # Finite field case
diff --git a/LeanAPAP/Mathlib/Algebra/Group/AddChar.lean b/LeanAPAP/Mathlib/Algebra/Group/AddChar.lean
index d2063678ee..4bc3c8ede1 100644
--- a/LeanAPAP/Mathlib/Algebra/Group/AddChar.lean
+++ b/LeanAPAP/Mathlib/Algebra/Group/AddChar.lean
@@ -1,17 +1,9 @@
 import Mathlib.Algebra.Group.AddChar
 
-open Finset hiding card
-open Fintype (card)
-open Function
-open scoped NNRat
-
-variable {G H R : Type*}
+variable {G R : Type*}
 
 namespace AddChar
-section AddMonoid
-variable [AddMonoid G] [AddMonoid H] [CommMonoid R] {ψ : AddChar G R}
-
-instance instAddCommMonoid : AddCommMonoid (AddChar G R) := Additive.addCommMonoid
+variable [AddMonoid G] [CommMonoid R] {ψ : AddChar G R}
 
 @[simp] lemma toMonoidHomEquiv_zero : toMonoidHomEquiv (0 : AddChar G R) = 1 := rfl
 @[simp] lemma toMonoidHomEquiv_symm_one :
@@ -22,98 +14,8 @@ instance instAddCommMonoid : AddCommMonoid (AddChar G R) := Additive.addCommMono
 @[simp] lemma toMonoidHomEquiv_symm_mul (ψ φ : Multiplicative G →* R) :
   toMonoidHomEquiv.symm (ψ * φ) = toMonoidHomEquiv.symm ψ + toMonoidHomEquiv.symm φ := rfl
 
-lemma eq_zero_iff : ψ = 0 ↔ ∀ x, ψ x = 1 := DFunLike.ext_iff
-lemma ne_zero_iff : ψ ≠ 0 ↔ ∃ x, ψ x ≠ 1 := DFunLike.ne_iff
-
-@[simp, norm_cast] lemma coe_zero : ⇑(0 : AddChar G R) = 1 := rfl
-
-lemma zero_apply (a : G) : (0 : AddChar G R) a = 1 := rfl
-
-@[simp, norm_cast] lemma coe_eq_zero : ⇑ψ = 1 ↔ ψ = 0 := by rw [← coe_zero, DFunLike.coe_fn_eq]
-@[simp, norm_cast] lemma coe_add (ψ χ : AddChar G R) : ⇑(ψ + χ) = ψ * χ := rfl
-
-lemma add_apply (ψ χ : AddChar G R) (a : G) : (ψ + χ) a = ψ a * χ a := rfl
-
-@[simp, norm_cast] lemma coe_nsmul (n : ℕ) (ψ : AddChar G R) : ⇑(n • ψ) = ψ ^ n := rfl
-
-lemma nsmul_apply (n : ℕ) (ψ : AddChar G R) (a : G) : (ψ ^ n) a = ψ a ^ n := rfl
-
-variable {ι : Type*}
-
-@[simp, norm_cast]
-lemma coe_sum (s : Finset ι) (ψ : ι → AddChar G R) : ∑ i in s, ψ i = ∏ i in s, ⇑(ψ i) := by
-  induction s using Finset.cons_induction <;> simp [*]
-
-lemma sum_apply (s : Finset ι) (ψ : ι → AddChar G R) (a : G) :
-    (∑ i in s, ψ i) a = ∏ i in s, ψ i a := by rw [coe_sum, Finset.prod_apply]
+@[simp, norm_cast] lemma coe_eq_one : ⇑ψ = 1 ↔ ψ = 0 := by rw [← coe_zero, DFunLike.coe_fn_eq]
 
 noncomputable instance : DecidableEq (AddChar G R) := Classical.decEq _
 
-/-- The double dual embedding. -/
-def doubleDualEmb : G →+ AddChar (AddChar G R) R where
-  toFun a := { toFun := fun ψ ↦ ψ a
-               map_zero_eq_one' := by simp
-               map_add_eq_mul' := by simp }
-  map_zero' := by ext; simp
-  map_add' _ _ := by ext; simp [map_add_eq_mul]
-
-@[simp] lemma doubleDualEmb_apply (a : G) (ψ : AddChar G R) : doubleDualEmb a ψ = ψ a := rfl
-
-end AddMonoid
-
-section AddGroup
-variable [AddGroup G]
-
-section CommSemiring
-variable [Fintype G] [CommSemiring R] [IsDomain R] {ψ : AddChar G R}
-
-lemma sum_eq_ite (ψ : AddChar G R) : ∑ a, ψ a = if ψ = 0 then ↑(card G) else 0 := by
-  split_ifs with h
-  · simp [h, card_univ]
-  obtain ⟨x, hx⟩ := ne_one_iff.1 h
-  refine eq_zero_of_mul_eq_self_left hx ?_
-  rw [Finset.mul_sum]
-  exact Fintype.sum_equiv (Equiv.addLeft x) _ _ fun y ↦ (map_add_eq_mul ..).symm
-
-variable [CharZero R]
-
-lemma sum_eq_zero_iff_ne_zero : ∑ x, ψ x = 0 ↔ ψ ≠ 0 := by
-  rw [sum_eq_ite, Ne.ite_eq_right_iff]
-  exact Nat.cast_ne_zero.2 Fintype.card_ne_zero
-
-lemma sum_ne_zero_iff_eq_zero : ∑ x, ψ x ≠ 0 ↔ ψ = 0 :=
-  sum_eq_zero_iff_ne_zero.not_left
-
-end CommSemiring
-end AddGroup
-
-section AddCommGroup
-variable [AddCommGroup G]
-
-section CommMonoid
-variable [CommMonoid R]
-
-/-- The additive characters on a commutative additive group form a commutative group. -/
-instance : AddCommGroup (AddChar G R) :=
-  @Additive.addCommGroup (AddChar G R) _
-
-@[simp]
-lemma neg_apply (ψ : AddChar G R) (a : G) : (-ψ) a = ψ (-a) := rfl
-
-@[simp]
-lemma sub_apply (ψ χ : AddChar G R) (a : G) : (ψ - χ) a = ψ a * χ (-a) := rfl
-
-end CommMonoid
-
-section DivisionCommMonoid
-variable [DivisionCommMonoid R]
-
-lemma neg_apply' (ψ : AddChar G R) (x : G) : (-ψ) x = (ψ x)⁻¹ :=
-  map_neg_eq_inv _ _
-
-lemma sub_apply' (ψ χ : AddChar G R) (a : G) : (ψ - χ) a = ψ a / χ a := by
-  rw [sub_apply, map_neg_eq_inv, div_eq_mul_inv]
-
-end DivisionCommMonoid
-end AddCommGroup
 end AddChar
diff --git a/LeanAPAP/Mathlib/Analysis/Complex/Basic.lean b/LeanAPAP/Mathlib/Analysis/Complex/Basic.lean
deleted file mode 100644
index 4ca235d98b..0000000000
--- a/LeanAPAP/Mathlib/Analysis/Complex/Basic.lean
+++ /dev/null
@@ -1,7 +0,0 @@
-import Mathlib.Analysis.Complex.Basic
-
-namespace Complex
-
-@[simp] lemma nnnorm_I : ‖I‖₊ = 1 := by simp [nnnorm]
-
-end Complex
diff --git a/LeanAPAP/Mathlib/Order/ConditionallyCompleteLattice/Basic.lean b/LeanAPAP/Mathlib/Order/ConditionallyCompleteLattice/Basic.lean
deleted file mode 100644
index 058bca5a74..0000000000
--- a/LeanAPAP/Mathlib/Order/ConditionallyCompleteLattice/Basic.lean
+++ /dev/null
@@ -1,5 +0,0 @@
-import Mathlib.Order.ConditionallyCompleteLattice.Basic
-
-variable {α β : Type*} [CompleteLattice β] {S : Set α} {f : α → β}
-
-lemma iInf_lt_top : ⨅ i ∈ S, f i < ⊤ ↔ ∃ i ∈ S, f i < ⊤ := by simp [lt_top_iff_ne_top]
diff --git a/LeanAPAP/Physics/AlmostPeriodicity.lean b/LeanAPAP/Physics/AlmostPeriodicity.lean
index 366dad4bab..1ad1e63488 100644
--- a/LeanAPAP/Physics/AlmostPeriodicity.lean
+++ b/LeanAPAP/Physics/AlmostPeriodicity.lean
@@ -523,4 +523,3 @@ theorem linfty_almost_periodicity_boosted (ε : ℝ) (hε₀ : 0 < ε) (hε₁ :
     _ = ε := by simp only [sum_const, card_fin, nsmul_eq_mul]; rw [mul_div_cancel₀]; positivity
 
 end AlmostPeriodicity
-#min_imports
diff --git a/LeanAPAP/Physics/Unbalancing.lean b/LeanAPAP/Physics/Unbalancing.lean
index 532fb9adbb..4b54a21b37 100644
--- a/LeanAPAP/Physics/Unbalancing.lean
+++ b/LeanAPAP/Physics/Unbalancing.lean
@@ -1,7 +1,7 @@
 import Mathlib.Algebra.Order.Group.PosPart
 import Mathlib.Data.Complex.ExponentialBounds
 import LeanAPAP.Prereqs.Convolution.Discrete.Defs
-import LeanAPAP.Prereqs.LpNorm.Discrete.Inner
+import LeanAPAP.Prereqs.Inner.Discrete.Basic
 import LeanAPAP.Prereqs.LpNorm.Weighted
 
 /-!
diff --git a/LeanAPAP/Prereqs/AddChar/Basic.lean b/LeanAPAP/Prereqs/AddChar/Basic.lean
index b55a3f0d00..837b5c587b 100644
--- a/LeanAPAP/Prereqs/AddChar/Basic.lean
+++ b/LeanAPAP/Prereqs/AddChar/Basic.lean
@@ -1,6 +1,6 @@
 import LeanAPAP.Mathlib.Algebra.Group.AddChar
 import LeanAPAP.Prereqs.Expect.Basic
-import LeanAPAP.Prereqs.LpNorm.Discrete.Inner
+import LeanAPAP.Prereqs.Inner.Discrete.Basic
 
 open Finset hiding card
 open Fintype (card)
diff --git a/LeanAPAP/Prereqs/Bohr/Arc.lean b/LeanAPAP/Prereqs/Bohr/Arc.lean
index d99909ffd5..411f70f308 100644
--- a/LeanAPAP/Prereqs/Bohr/Arc.lean
+++ b/LeanAPAP/Prereqs/Bohr/Arc.lean
@@ -1,6 +1,5 @@
 import Mathlib.Analysis.Complex.Angle
 import LeanAPAP.Prereqs.AddChar.PontryaginDuality
-import LeanAPAP.Prereqs.Function.Translate
 import LeanAPAP.Prereqs.Bohr.Basic
 
 /- ### Arc Bohr sets -/
diff --git a/LeanAPAP/Prereqs/Convolution/Norm.lean b/LeanAPAP/Prereqs/Convolution/Norm.lean
index 14f1d1e33a..f172a1594d 100644
--- a/LeanAPAP/Prereqs/Convolution/Norm.lean
+++ b/LeanAPAP/Prereqs/Convolution/Norm.lean
@@ -1,7 +1,7 @@
 import Mathlib.Data.Real.StarOrdered
 import LeanAPAP.Prereqs.Convolution.Discrete.Defs
 import LeanAPAP.Prereqs.LpNorm.Discrete.Basic
-import LeanAPAP.Prereqs.LpNorm.Discrete.Inner
+import LeanAPAP.Prereqs.Inner.Discrete.Basic
 
 /-!
 # Norm of a convolution
diff --git a/LeanAPAP/Prereqs/Convolution/ThreeAP.lean b/LeanAPAP/Prereqs/Convolution/ThreeAP.lean
index b0b69a2599..802c00506f 100644
--- a/LeanAPAP/Prereqs/Convolution/ThreeAP.lean
+++ b/LeanAPAP/Prereqs/Convolution/ThreeAP.lean
@@ -2,7 +2,7 @@ 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.LpNorm.Discrete.Inner
+import LeanAPAP.Prereqs.Inner.Discrete.Basic
 
 /-!
 # The convolution characterisation of 3AP-free sets
diff --git a/LeanAPAP/Prereqs/Expect/Basic.lean b/LeanAPAP/Prereqs/Expect/Basic.lean
index ac9ea8bcf8..ac1ad296d6 100644
--- a/LeanAPAP/Prereqs/Expect/Basic.lean
+++ b/LeanAPAP/Prereqs/Expect/Basic.lean
@@ -1,11 +1,12 @@
+import Mathlib.Algebra.Algebra.Rat
+import Mathlib.Algebra.BigOperators.GroupWithZero.Action
 import Mathlib.Algebra.BigOperators.Ring
+import Mathlib.Algebra.CharP.Defs
+import Mathlib.Algebra.Module.Rat
 import Mathlib.Algebra.Order.Module.Rat
-import Mathlib.Algebra.Algebra.Field
-import Mathlib.Algebra.Star.Order
-import Mathlib.Analysis.CStarAlgebra.Basic
-import Mathlib.Analysis.Normed.Operator.ContinuousLinearMap
-import Mathlib.Data.Real.Sqrt
-import Mathlib.Tactic.Positivity.Finset
+import Mathlib.Data.Finset.Density
+import Mathlib.Data.Finset.Pointwise.Basic
+import Mathlib.Data.Fintype.BigOperators
 
 /-!
 # Average over a finset
@@ -25,7 +26,7 @@ This file defines `Finset.expect`, the average (aka expectation) of a function o
 
 open Function
 open Fintype (card)
-open scoped Pointwise NNRat NNReal
+open scoped Pointwise NNRat
 
 variable {ι κ α β : Type*}
 
@@ -218,13 +219,14 @@ lemma card_smul_expect (s : Finset ι) (f : ι → α) : s.card • 𝔼 i ∈ s
   obtain rfl | hs := s.eq_empty_or_nonempty
   · simp
   · rw [expect, ← Nat.cast_smul_eq_nsmul ℚ≥0, smul_inv_smul₀]
-    positivity
+    exact mod_cast hs.card_ne_zero
 
 @[simp] nonrec lemma _root_.Fintype.card_smul_expect [Fintype ι] (f : ι → α) :
     Fintype.card ι • 𝔼 i, f i = ∑ i, f i := card_smul_expect _ _
 
 @[simp] lemma expect_const (hs : s.Nonempty) (a : α) : 𝔼 _i ∈ s, a = a := by
-  rw [expect, sum_const, ← Nat.cast_smul_eq_nsmul ℚ≥0, inv_smul_smul₀]; positivity
+  rw [expect, sum_const, ← Nat.cast_smul_eq_nsmul ℚ≥0, inv_smul_smul₀]
+  exact mod_cast hs.card_ne_zero
 
 lemma smul_expect {G : Type*} [DistribSMul G α] [SMulCommClass G ℚ≥0 α] (a : G)
     (s : Finset ι) (f : ι → α) : a • 𝔼 i ∈ s, f i = 𝔼 i ∈ s, a • f i := by
@@ -360,11 +362,11 @@ lemma _root_.GCongr.expect_le_expect (h : ∀ i ∈ s, f i ≤ g i) : s.expect f
   Finset.expect_le_expect h
 
 lemma expect_le (hs : s.Nonempty) (f : ι → α) (a : α) (h : ∀ x ∈ s, f x ≤ a) : 𝔼 i ∈ s, f i ≤ a :=
-  (inv_smul_le_iff_of_pos $ by positivity).2 $ by
+  (inv_smul_le_iff_of_pos $ mod_cast hs.card_pos).2 $ by
     rw [Nat.cast_smul_eq_nsmul]; exact sum_le_card_nsmul _ _ _ h
 
 lemma le_expect (hs : s.Nonempty) (f : ι → α) (a : α) (h : ∀ x ∈ s, a ≤ f x) : a ≤ 𝔼 i ∈ s, f i :=
-  (le_inv_smul_iff_of_pos $ by positivity).2 $ by
+  (le_inv_smul_iff_of_pos $ mod_cast hs.card_pos).2 $ by
     rw [Nat.cast_smul_eq_nsmul]; exact card_nsmul_le_sum _ _ _ h
 
 lemma expect_nonneg (hf : ∀ i ∈ s, 0 ≤ f i) : 0 ≤ 𝔼 i ∈ s, f i :=
@@ -394,7 +396,7 @@ section PosSMulStrictMono
 variable [PosSMulStrictMono ℚ≥0 α]
 
 lemma expect_pos (hf : ∀ i ∈ s, 0 < f i) (hs : s.Nonempty) : 0 < 𝔼 i ∈ s, f i :=
-  smul_pos (by positivity) $ sum_pos hf hs
+  smul_pos (inv_pos.2 $ mod_cast hs.card_pos) $ sum_pos hf hs
 
 end PosSMulStrictMono
 end OrderedCancelAddCommMonoid
@@ -493,49 +495,3 @@ instance LinearOrderedSemifield.toPosSMulStrictMono [LinearOrderedSemifield α]
     PosSMulStrictMono ℚ≥0 α where
   elim a ha b₁ b₂ hb := by
     simp_rw [NNRat.smul_def]; exact mul_lt_mul_of_pos_left hb (NNRat.cast_pos.2 ha)
-
-namespace Mathlib.Meta.Positivity
-open Qq Lean Meta
-
-@[positivity Finset.expect _ _]
-def evalFinsetExpect : PositivityExt where eval {u α} zα pα e := do
-  match e with
-  | ~q(@Finset.expect $ι _ $instα $instmod $s $f) =>
-    let (lhs, _, (rhs : Q($α))) ← lambdaMetaTelescope f
-    let so : Option Q(Finset.Nonempty $s) ← do -- TODO: It doesn't complain if we make a typo?
-      try
-        let _fi ← synthInstanceQ q(Fintype $ι)
-        let _no ← synthInstanceQ q(Nonempty $ι)
-        match s with
-        | ~q(@univ _ $fi) => pure (some q(Finset.univ_nonempty (α := $ι)))
-        | _ => pure none
-      catch _ => do
-        let .some fv ← findLocalDeclWithType? q(Finset.Nonempty $s) | pure none
-        pure (some (.fvar fv))
-    match ← core zα pα rhs, so with
-    | .nonnegative pb, _ => do
-      let instαordmon ← synthInstanceQ q(OrderedAddCommMonoid $α)
-      let instαordsmul ← synthInstanceQ q(PosSMulMono ℚ≥0 $α)
-      assumeInstancesCommute
-      let pr : Q(∀ i, 0 ≤ $f i) ← mkLambdaFVars lhs pb
-      return .nonnegative q(@expect_nonneg $ι $α $instαordmon $instmod $s $f $instαordsmul
-        fun i _ ↦ $pr i)
-    | .positive pb, .some (fi : Q(Finset.Nonempty $s)) => do
-      let instαordmon ← synthInstanceQ q(OrderedCancelAddCommMonoid $α)
-      let instαordsmul ← synthInstanceQ q(PosSMulStrictMono ℚ≥0 $α)
-      assumeInstancesCommute
-      let pr : Q(∀ i, 0 < $f i) ← mkLambdaFVars lhs pb
-      return .positive q(@expect_pos $ι $α $instαordmon $instmod $s $f $instαordsmul
-        (fun i _ ↦ $pr i) $fi)
-    | _, _ => pure .none
-  | _ => throwError "not Finset.expect"
-
-example (n : ℕ) (a : ℕ → ℝ) : 0 ≤ 𝔼 j ∈ range n, a j^2 := by positivity
-example (a : ULift.{2} ℕ → ℝ) (s : Finset (ULift.{2} ℕ)) : 0 ≤ 𝔼 j ∈ s, a j^2 := by positivity
-example (n : ℕ) (a : ℕ → ℝ) : 0 ≤ 𝔼 j : Fin 8, 𝔼 i ∈ range n, (a j^2 + i ^ 2) := by positivity
-example (n : ℕ) (a : ℕ → ℝ) : 0 < 𝔼 j : Fin (n + 1), (a j^2 + 1) := by positivity
-example (a : ℕ → ℝ) : 0 < 𝔼 j ∈ ({1} : Finset ℕ), (a j^2 + 1) := by
-  have : Finset.Nonempty {1} := singleton_nonempty 1
-  positivity
-
-end Mathlib.Meta.Positivity
diff --git a/LeanAPAP/Prereqs/Expect/Order.lean b/LeanAPAP/Prereqs/Expect/Order.lean
new file mode 100644
index 0000000000..85a64c5e22
--- /dev/null
+++ b/LeanAPAP/Prereqs/Expect/Order.lean
@@ -0,0 +1,49 @@
+import Mathlib.Data.Real.Basic
+import LeanAPAP.Prereqs.Expect.Basic
+
+namespace Mathlib.Meta.Positivity
+open Qq Lean Meta Finset
+open scoped BigOperators
+
+@[positivity Finset.expect _ _]
+def evalFinsetExpect : PositivityExt where eval {u α} zα pα e := do
+  match e with
+  | ~q(@Finset.expect $ι _ $instα $instmod $s $f) =>
+    let (lhs, _, (rhs : Q($α))) ← lambdaMetaTelescope f
+    let so : Option Q(Finset.Nonempty $s) ← do -- TODO: It doesn't complain if we make a typo?
+      try
+        let _fi ← synthInstanceQ q(Fintype $ι)
+        let _no ← synthInstanceQ q(Nonempty $ι)
+        match s with
+        | ~q(@univ _ $fi) => pure (some q(Finset.univ_nonempty (α := $ι)))
+        | _ => pure none
+      catch _ => do
+        let .some fv ← findLocalDeclWithType? q(Finset.Nonempty $s) | pure none
+        pure (some (.fvar fv))
+    match ← core zα pα rhs, so with
+    | .nonnegative pb, _ => do
+      let instαordmon ← synthInstanceQ q(OrderedAddCommMonoid $α)
+      let instαordsmul ← synthInstanceQ q(PosSMulMono ℚ≥0 $α)
+      assumeInstancesCommute
+      let pr : Q(∀ i, 0 ≤ $f i) ← mkLambdaFVars lhs pb
+      return .nonnegative q(@expect_nonneg $ι $α $instαordmon $instmod $s $f $instαordsmul
+        fun i _ ↦ $pr i)
+    | .positive pb, .some (fi : Q(Finset.Nonempty $s)) => do
+      let instαordmon ← synthInstanceQ q(OrderedCancelAddCommMonoid $α)
+      let instαordsmul ← synthInstanceQ q(PosSMulStrictMono ℚ≥0 $α)
+      assumeInstancesCommute
+      let pr : Q(∀ i, 0 < $f i) ← mkLambdaFVars lhs pb
+      return .positive q(@expect_pos $ι $α $instαordmon $instmod $s $f $instαordsmul
+        (fun i _ ↦ $pr i) $fi)
+    | _, _ => pure .none
+  | _ => throwError "not Finset.expect"
+
+example (n : ℕ) (a : ℕ → ℝ) : 0 ≤ 𝔼 j ∈ range n, a j^2 := by positivity
+example (a : ULift.{2} ℕ → ℝ) (s : Finset (ULift.{2} ℕ)) : 0 ≤ 𝔼 j ∈ s, a j^2 := by positivity
+example (n : ℕ) (a : ℕ → ℝ) : 0 ≤ 𝔼 j : Fin 8, 𝔼 i ∈ range n, (a j^2 + i ^ 2) := by positivity
+example (n : ℕ) (a : ℕ → ℝ) : 0 < 𝔼 j : Fin (n + 1), (a j^2 + 1) := by positivity
+example (a : ℕ → ℝ) : 0 < 𝔼 j ∈ ({1} : Finset ℕ), (a j^2 + 1) := by
+  have : Finset.Nonempty {1} := singleton_nonempty 1
+  positivity
+
+end Mathlib.Meta.Positivity
diff --git a/LeanAPAP/Prereqs/FourierTransform/Discrete.lean b/LeanAPAP/Prereqs/FourierTransform/Discrete.lean
index a2f98fefaf..695e771010 100644
--- a/LeanAPAP/Prereqs/FourierTransform/Discrete.lean
+++ b/LeanAPAP/Prereqs/FourierTransform/Discrete.lean
@@ -2,8 +2,8 @@ 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.Inner.Compact.Basic
+import LeanAPAP.Prereqs.Inner.Discrete.Basic
 
 /-!
 # Discrete Fourier transform
diff --git a/LeanAPAP/Prereqs/Function/Indicator/Basic.lean b/LeanAPAP/Prereqs/Function/Indicator/Basic.lean
index d014eec156..6a3b22840d 100644
--- a/LeanAPAP/Prereqs/Function/Indicator/Basic.lean
+++ b/LeanAPAP/Prereqs/Function/Indicator/Basic.lean
@@ -1,8 +1,8 @@
-import Mathlib.Data.Complex.Basic
 import Mathlib.Data.Fintype.Lattice
 import LeanAPAP.Prereqs.Expect.Basic
 import LeanAPAP.Prereqs.Function.Translate
 import LeanAPAP.Prereqs.Function.Indicator.Defs
+import Mathlib.Algebra.AddTorsor
 
 open Finset Function
 open Fintype (card)
diff --git a/LeanAPAP/Prereqs/LpNorm/Compact/Inner.lean b/LeanAPAP/Prereqs/Inner/Compact/Basic.lean
similarity index 99%
rename from LeanAPAP/Prereqs/LpNorm/Compact/Inner.lean
rename to LeanAPAP/Prereqs/Inner/Compact/Basic.lean
index 492b40c819..81557ec5a9 100644
--- a/LeanAPAP/Prereqs/LpNorm/Compact/Inner.lean
+++ b/LeanAPAP/Prereqs/Inner/Compact/Basic.lean
@@ -2,7 +2,7 @@ import Mathlib.Analysis.InnerProductSpace.PiL2
 import LeanAPAP.Mathlib.Algebra.Star.Rat
 import LeanAPAP.Prereqs.Expect.Complex
 import LeanAPAP.Prereqs.LpNorm.Compact.Defs
-import LeanAPAP.Prereqs.LpNorm.Discrete.Inner
+import LeanAPAP.Prereqs.Inner.Discrete.Basic
 
 /-! # Inner product -/
 
diff --git a/LeanAPAP/Prereqs/Inner/Discrete/Basic.lean b/LeanAPAP/Prereqs/Inner/Discrete/Basic.lean
new file mode 100644
index 0000000000..d173c5f1e1
--- /dev/null
+++ b/LeanAPAP/Prereqs/Inner/Discrete/Basic.lean
@@ -0,0 +1,122 @@
+import Mathlib.Analysis.InnerProductSpace.PiL2
+import LeanAPAP.Prereqs.LpNorm.Discrete.Defs
+import LeanAPAP.Prereqs.Inner.Discrete.Defs
+
+/-! # Inner product -/
+
+open Finset Function Real
+open scoped ComplexConjugate ENNReal NNReal NNRat
+
+variable {ι R S : Type*} [Fintype ι]
+
+namespace MeasureTheory
+
+section RCLike
+variable {κ : Type*} [RCLike R] {f : ι → R}
+
+@[simp] lemma dL2Inner_self {_ : MeasurableSpace ι} [DiscreteMeasurableSpace ι] (f : ι → R) :
+    ⟪f, f⟫_[R] = ((‖f‖_[2] : ℝ) : R) ^ 2 := by
+  simp_rw [← algebraMap.coe_pow, ← NNReal.coe_pow]
+  simp [dL2Norm_sq_eq_sum_nnnorm, dL2Inner_eq_sum, RCLike.conj_mul]
+
+variable {mι : MeasurableSpace ι} [DiscreteMeasurableSpace ι]
+
+lemma dL1Norm_mul (f g : ι → R) : ‖f * g‖_[1] = ⟪fun i ↦ ‖f i‖, fun i ↦ ‖g i‖⟫_[ℝ] := by
+  simp [dL2Inner_eq_sum, dL1Norm_eq_sum_nnnorm]
+
+end RCLike
+
+variable {mι : MeasurableSpace ι} [DiscreteMeasurableSpace ι]
+
+/-- **Cauchy-Schwarz inequality** -/
+lemma dL2Inner_le_dL2Norm_mul_dL2Norm (f g : ι → ℝ) : ⟪f, g⟫_[ℝ] ≤ ‖f‖_[2] * ‖g‖_[2] := by
+  simpa [dL2Norm_eq_sum_nnnorm, PiLp.norm_eq_of_L2, sqrt_eq_rpow]
+    using real_inner_le_norm ((WithLp.equiv 2 _).symm f) _
+
+end MeasureTheory
+
+/-! ### Hölder inequality -/
+
+namespace MeasureTheory
+section Real
+variable {α : Type*} {mα : MeasurableSpace α} [DiscreteMeasurableSpace α] [Fintype α] {p q : ℝ≥0}
+  {f g : α → ℝ}
+
+lemma dL1Norm_mul_of_nonneg (hf : 0 ≤ f) (hg : 0 ≤ g) : ‖f * g‖_[1] = ⟪f, g⟫_[ℝ] := by
+  convert dL1Norm_mul f g using 2 <;> ext a <;> refine (norm_of_nonneg ?_).symm; exacts [hf _, hg _]
+
+/-- **Hölder's inequality**, binary case. -/
+lemma dL2Inner_le_dLpNorm_mul_dLpNorm (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
+  simpa [dL2Inner_eq_sum, dLpNorm_eq_sum_nnnorm, *] using inner_le_Lp_mul_Lq _ f g hpq.coe
+
+/-- **Hölder's inequality**, binary case. -/
+lemma abs_dL2Inner_le_dLpNorm_mul_dLpNorm (hpq : p.IsConjExponent q) (f g : α → ℝ) :
+    |⟪f, g⟫_[ℝ]| ≤ ‖f‖_[p] * ‖g‖_[q] :=
+  abs_dL2Inner_le_dL2Inner_abs.trans $
+    (dL2Inner_le_dLpNorm_mul_dLpNorm hpq _ _).trans_eq $ by simp_rw [dLpNorm_abs]
+
+end Real
+
+section Hoelder
+variable {α : Type*} {mα : MeasurableSpace α} [DiscreteMeasurableSpace α] [Fintype α] [RCLike R]
+  {p q : ℝ≥0} {f g : α → R}
+
+lemma norm_dL2Inner_le (f g : α → R) : ‖⟪f, g⟫_[R]‖₊ ≤ ⟪fun a ↦ ‖f a‖, fun a ↦ ‖g a‖⟫_[ℝ] :=
+  (norm_sum_le _ _).trans $ by simp [dL2Inner]
+
+/-- **Hölder's inequality**, binary case. -/
+lemma nnnorm_dL2Inner_le_dLpNorm_mul_dLpNorm (hpq : p.IsConjExponent q) (f g : α → R) :
+    ‖⟪f, g⟫_[R]‖₊ ≤ ‖f‖_[p] * ‖g‖_[q] :=
+  calc
+    _ ≤ ⟪fun a ↦ ‖f a‖, fun a ↦ ‖g a‖⟫_[ℝ] := norm_dL2Inner_le _ _
+    _ ≤ ‖fun a ↦ ‖f a‖‖_[p] * ‖fun a ↦ ‖g a‖‖_[q] := dL2Inner_le_dLpNorm_mul_dLpNorm hpq _ _
+    _ = ‖f‖_[p] * ‖g‖_[q] := by simp_rw [dLpNorm_norm]
+
+/-- **Hölder's inequality**, binary case. -/
+lemma dLpNorm_mul_le (hp : p ≠ 0) (hq : q ≠ 0) (r : ℝ≥0) (hpqr : p⁻¹ + q⁻¹ = r⁻¹) (f g : α → R) :
+    ‖f * g‖_[r] ≤ ‖f‖_[p] * ‖g‖_[q] := by
+  have hr : r ≠ 0 := by
+    rintro rfl
+    simp [hp] at hpqr
+  have : (‖(f * g) ·‖ ^ (r : ℝ)) = (‖f ·‖ ^ (r : ℝ)) * (‖g ·‖ ^ (r : ℝ)) := by
+    ext; simp [mul_rpow, abs_mul]
+  rw [dLpNorm_eq_dL1Norm_rpow, NNReal.rpow_inv_le_iff_of_pos, this, ← NNReal.coe_le_coe]
+  push_cast
+  rw [dL1Norm_mul_of_nonneg, mul_rpow, ← NNReal.coe_rpow, ← NNReal.coe_rpow, dLpNorm_rpow',
+    dLpNorm_rpow', ← ENNReal.coe_div, ← ENNReal.coe_div]
+  refine dL2Inner_le_dLpNorm_mul_dLpNorm ⟨?_, ?_⟩ _ _
+  · norm_cast
+    rw [div_eq_mul_inv, ← hpqr, mul_add, mul_inv_cancel₀ hp]
+    exact lt_add_of_pos_right _ (by positivity)
+  · norm_cast
+    simp [div_eq_mul_inv, hpqr, ← mul_add, hr]
+  any_goals intro a; dsimp
+  all_goals positivity
+
+/-- **Hölder's inequality**, binary case. -/
+lemma dL1Norm_mul_le (hpq : p.IsConjExponent q) (f g : α → R) :
+    ‖f * g‖_[1] ≤ ‖f‖_[p] * ‖g‖_[q] :=
+  dLpNorm_mul_le (mod_cast hpq.ne_zero) (mod_cast hpq.symm.ne_zero) _
+    (by simpa using hpq.inv_add_inv_conj) _ _
+
+/-- **Hölder's inequality**, finitary case. -/
+lemma dLpNorm_prod_le {ι : Type*} {s : Finset ι} (hs : s.Nonempty) {p : ι → ℝ≥0} (hp : ∀ i, p i ≠ 0)
+    (q : ℝ≥0) (hpq : ∑ i ∈ s, (p i)⁻¹ = q⁻¹) (f : ι → α → R) :
+    ‖∏ i ∈ s, f i‖_[q] ≤ ∏ i ∈ s, ‖f i‖_[p i] := by
+  induction' s using Finset.cons_induction with i s hi ih generalizing q
+  · cases not_nonempty_empty hs
+  obtain rfl | hs := s.eq_empty_or_nonempty
+  · simp only [sum_cons, sum_empty, add_zero, inv_inj] at hpq
+    simp [← hpq]
+  simp_rw [prod_cons]
+  rw [sum_cons, ← inv_inv (∑ _ ∈ _, _ : ℝ≥0)] at hpq
+  refine (dLpNorm_mul_le (hp _) (inv_ne_zero (sum_pos (fun _ _ ↦ ?_) hs).ne') _ hpq _ _).trans
+    (mul_le_mul_left' (ih hs _ (inv_inv _).symm) _)
+  exact pos_iff_ne_zero.2 (inv_ne_zero $ hp _)
+
+end Hoelder
+end MeasureTheory
diff --git a/LeanAPAP/Prereqs/LpNorm/Discrete/Inner.lean b/LeanAPAP/Prereqs/Inner/Discrete/Defs.lean
similarity index 57%
rename from LeanAPAP/Prereqs/LpNorm/Discrete/Inner.lean
rename to LeanAPAP/Prereqs/Inner/Discrete/Defs.lean
index 808a30f4c4..d27b7aa069 100644
--- a/LeanAPAP/Prereqs/LpNorm/Discrete/Inner.lean
+++ b/LeanAPAP/Prereqs/Inner/Discrete/Defs.lean
@@ -1,5 +1,4 @@
 import Mathlib.Analysis.InnerProductSpace.PiL2
-import LeanAPAP.Prereqs.LpNorm.Discrete.Defs
 
 /-! # Inner product -/
 
@@ -101,13 +100,8 @@ lemma dL2Inner_eq_inner (f g : ι → R) :
 lemma inner_eq_dL2Inner (f g : PiLp 2 fun _i : ι ↦ R) :
     inner f g = ⟪WithLp.equiv 2 _ f, WithLp.equiv 2 _ g⟫_[R] := rfl
 
-@[simp] lemma dL2Inner_self {_ : MeasurableSpace ι} [DiscreteMeasurableSpace ι] (f : ι → R) :
-    ⟪f, f⟫_[R] = ((‖f‖_[2] : ℝ) : R) ^ 2 := by
-  simp_rw [← algebraMap.coe_pow, ← NNReal.coe_pow]
-  simp [dL2Norm_sq_eq_sum_nnnorm, dL2Inner_eq_sum, RCLike.conj_mul]
-
 lemma dL2Inner_self_of_norm_eq_one (hf : ∀ x, ‖f x‖ = 1) : ⟪f, f⟫_[R] = Fintype.card ι := by
-  simp [-dL2Inner_self, dL2Inner_eq_sum, RCLike.conj_mul, hf, card_univ]
+  simp [dL2Inner_eq_sum, RCLike.conj_mul, hf, card_univ]
 
 lemma linearIndependent_of_ne_zero_of_dL2Inner_eq_zero {v : κ → ι → R} (hz : ∀ k, v k ≠ 0)
     (ho : Pairwise fun k l ↦ ⟪v k, v l⟫_[R] = 0) : LinearIndependent R v := by
@@ -115,20 +109,8 @@ lemma linearIndependent_of_ne_zero_of_dL2Inner_eq_zero {v : κ → ι → R} (hz
   have := linearIndependent_of_ne_zero_of_inner_eq_zero ?_ ho
   exacts [this, hz]
 
-variable {mι : MeasurableSpace ι} [DiscreteMeasurableSpace ι]
-
-lemma dL1Norm_mul (f g : ι → R) : ‖f * g‖_[1] = ⟪fun i ↦ ‖f i‖, fun i ↦ ‖g i‖⟫_[ℝ] := by
-  simp [dL2Inner_eq_sum, dL1Norm_eq_sum_nnnorm]
-
 end RCLike
 
-variable {mι : MeasurableSpace ι} [DiscreteMeasurableSpace ι]
-
-/-- **Cauchy-Schwarz inequality** -/
-lemma dL2Inner_le_dL2Norm_mul_dL2Norm (f g : ι → ℝ) : ⟪f, g⟫_[ℝ] ≤ ‖f‖_[2] * ‖g‖_[2] := by
-  simpa [dL2Norm_eq_sum_nnnorm, PiLp.norm_eq_of_L2, sqrt_eq_rpow]
-    using real_inner_le_norm ((WithLp.equiv 2 _).symm f) _
-
 end MeasureTheory
 
 namespace Mathlib.Meta.Positivity
@@ -176,89 +158,3 @@ example (hf : 0 ≤ f) (hg : 0 ≤ g) : 0 ≤ ⟪f, g⟫_[R] := by positivity
 
 end OrderedCommSemiring
 end Mathlib.Meta.Positivity
-
-/-! ### Hölder inequality -/
-
-namespace MeasureTheory
-section Real
-variable {α : Type*} {mα : MeasurableSpace α} [DiscreteMeasurableSpace α] [Fintype α] {p q : ℝ≥0}
-  {f g : α → ℝ}
-
-lemma dL1Norm_mul_of_nonneg (hf : 0 ≤ f) (hg : 0 ≤ g) : ‖f * g‖_[1] = ⟪f, g⟫_[ℝ] := by
-  convert dL1Norm_mul f g using 2 <;> ext a <;> refine (norm_of_nonneg ?_).symm; exacts [hf _, hg _]
-
-/-- **Hölder's inequality**, binary case. -/
-lemma dL2Inner_le_dLpNorm_mul_dLpNorm (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
-  simpa [dL2Inner_eq_sum, dLpNorm_eq_sum_nnnorm, *] using inner_le_Lp_mul_Lq _ f g hpq.coe
-
-/-- **Hölder's inequality**, binary case. -/
-lemma abs_dL2Inner_le_dLpNorm_mul_dLpNorm (hpq : p.IsConjExponent q) (f g : α → ℝ) :
-    |⟪f, g⟫_[ℝ]| ≤ ‖f‖_[p] * ‖g‖_[q] :=
-  abs_dL2Inner_le_dL2Inner_abs.trans $
-    (dL2Inner_le_dLpNorm_mul_dLpNorm hpq _ _).trans_eq $ by simp_rw [dLpNorm_abs]
-
-end Real
-
-section Hoelder
-variable {α : Type*} {mα : MeasurableSpace α} [DiscreteMeasurableSpace α] [Fintype α] [RCLike R]
-  {p q : ℝ≥0} {f g : α → R}
-
-lemma norm_dL2Inner_le (f g : α → R) : ‖⟪f, g⟫_[R]‖₊ ≤ ⟪fun a ↦ ‖f a‖, fun a ↦ ‖g a‖⟫_[ℝ] :=
-  (norm_sum_le _ _).trans $ by simp [dL2Inner]
-
-/-- **Hölder's inequality**, binary case. -/
-lemma nnnorm_dL2Inner_le_dLpNorm_mul_dLpNorm (hpq : p.IsConjExponent q) (f g : α → R) :
-    ‖⟪f, g⟫_[R]‖₊ ≤ ‖f‖_[p] * ‖g‖_[q] :=
-  calc
-    _ ≤ ⟪fun a ↦ ‖f a‖, fun a ↦ ‖g a‖⟫_[ℝ] := norm_dL2Inner_le _ _
-    _ ≤ ‖fun a ↦ ‖f a‖‖_[p] * ‖fun a ↦ ‖g a‖‖_[q] := dL2Inner_le_dLpNorm_mul_dLpNorm hpq _ _
-    _ = ‖f‖_[p] * ‖g‖_[q] := by simp_rw [dLpNorm_norm]
-
-/-- **Hölder's inequality**, binary case. -/
-lemma dLpNorm_mul_le (hp : p ≠ 0) (hq : q ≠ 0) (r : ℝ≥0) (hpqr : p⁻¹ + q⁻¹ = r⁻¹) (f g : α → R) :
-    ‖f * g‖_[r] ≤ ‖f‖_[p] * ‖g‖_[q] := by
-  have hr : r ≠ 0 := by
-    rintro rfl
-    simp [hp] at hpqr
-  have : (‖(f * g) ·‖ ^ (r : ℝ)) = (‖f ·‖ ^ (r : ℝ)) * (‖g ·‖ ^ (r : ℝ)) := by
-    ext; simp [mul_rpow, abs_mul]
-  rw [dLpNorm_eq_dL1Norm_rpow, NNReal.rpow_inv_le_iff_of_pos, this, ← NNReal.coe_le_coe]
-  push_cast
-  rw [dL1Norm_mul_of_nonneg, mul_rpow, ← NNReal.coe_rpow, ← NNReal.coe_rpow, dLpNorm_rpow',
-    dLpNorm_rpow', ← ENNReal.coe_div, ← ENNReal.coe_div]
-  refine dL2Inner_le_dLpNorm_mul_dLpNorm ⟨?_, ?_⟩ _ _
-  · norm_cast
-    rw [div_eq_mul_inv, ← hpqr, mul_add, mul_inv_cancel₀ hp]
-    exact lt_add_of_pos_right _ (by positivity)
-  · norm_cast
-    simp [div_eq_mul_inv, hpqr, ← mul_add, hr]
-  any_goals intro a; dsimp
-  all_goals positivity
-
-/-- **Hölder's inequality**, binary case. -/
-lemma dL1Norm_mul_le (hpq : p.IsConjExponent q) (f g : α → R) :
-    ‖f * g‖_[1] ≤ ‖f‖_[p] * ‖g‖_[q] :=
-  dLpNorm_mul_le (mod_cast hpq.ne_zero) (mod_cast hpq.symm.ne_zero) _
-    (by simpa using hpq.inv_add_inv_conj) _ _
-
-/-- **Hölder's inequality**, finitary case. -/
-lemma dLpNorm_prod_le {ι : Type*} {s : Finset ι} (hs : s.Nonempty) {p : ι → ℝ≥0} (hp : ∀ i, p i ≠ 0)
-    (q : ℝ≥0) (hpq : ∑ i ∈ s, (p i)⁻¹ = q⁻¹) (f : ι → α → R) :
-    ‖∏ i ∈ s, f i‖_[q] ≤ ∏ i ∈ s, ‖f i‖_[p i] := by
-  induction' s using Finset.cons_induction with i s hi ih generalizing q
-  · cases not_nonempty_empty hs
-  obtain rfl | hs := s.eq_empty_or_nonempty
-  · simp only [sum_cons, sum_empty, add_zero, inv_inj] at hpq
-    simp [← hpq]
-  simp_rw [prod_cons]
-  rw [sum_cons, ← inv_inv (∑ _ ∈ _, _ : ℝ≥0)] at hpq
-  refine (dLpNorm_mul_le (hp _) (inv_ne_zero (sum_pos (fun _ _ ↦ ?_) hs).ne') _ hpq _ _).trans
-    (mul_le_mul_left' (ih hs _ (inv_inv _).symm) _)
-  exact pos_iff_ne_zero.2 (inv_ne_zero $ hp _)
-
-end Hoelder
-end MeasureTheory
diff --git a/LeanAPAP/Prereqs/NNLpNorm.lean b/LeanAPAP/Prereqs/NNLpNorm.lean
index c4b588ed1b..903777a1fb 100644
--- a/LeanAPAP/Prereqs/NNLpNorm.lean
+++ b/LeanAPAP/Prereqs/NNLpNorm.lean
@@ -1,8 +1,9 @@
 import Mathlib.Analysis.Normed.Group.Constructions
 import Mathlib.MeasureTheory.Integral.Bochner
+import Mathlib.Tactic.Positivity.Finset
 import LeanAPAP.Mathlib.Analysis.SpecialFunctions.Pow.NNReal
 import LeanAPAP.Mathlib.MeasureTheory.Function.LpSeminorm.Basic
-import LeanAPAP.Prereqs.Expect.Basic
+import LeanAPAP.Prereqs.Expect.Order
 
 open Filter
 open scoped BigOperators ComplexConjugate ENNReal NNReal
diff --git a/LeanAPAP/Prereqs/Rudin.lean b/LeanAPAP/Prereqs/Rudin.lean
index 741539d354..8eea7ca725 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.Analysis.Complex.Basic
 import LeanAPAP.Prereqs.FourierTransform.Compact
 import LeanAPAP.Prereqs.Randomisation
 
diff --git a/lake-manifest.json b/lake-manifest.json
index 10f41a1d42..7c5396d82d 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "9c6c2d647e57b2b7a0b42dd8080c698bd33a1b6f",
+   "rev": "fa571ea02a804b52a59e58012b1e21fe4f0514f2",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -15,7 +15,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "9d0bdd07bdfe53383567509348b1fe917fc08de4",
+   "rev": "2c8ae451ce9ffc83554322b14437159c1a9703f9",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -25,7 +25,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "deb279eb7be16848d0bc8387f80d6e41bcdbe738",
+   "rev": "ad85095b6112bb3a7ad6c068fd0844d1e35706f2",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -35,10 +35,10 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "a96aee5245720f588876021b6a0aa73efee49c76",
+   "rev": "6f9a1b99e76899a578a6ca0fd1d435f00428014b",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.41",
+   "inputRev": "v0.0.42-pre2",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover/lean4-cli",
@@ -55,7 +55,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "1ef0b288623337cb37edd1222b9c26b4b77c6620",
+   "rev": "3e96ea03edd48b932566ca9b201285ae2d57130d",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -65,7 +65,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "00df099f8ed42c12b35cdedcfbf1fde6c7413662",
+   "rev": "b191738f9875e429b3680fecf251652a03f77cee",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,
diff --git a/lean-toolchain b/lean-toolchain
index 5a9c76dc98..98556ba065 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.11.0
+leanprover/lean4:v4.12.0-rc1