diff --git a/LeanAPAP.lean b/LeanAPAP.lean
index 30bdae363b..093a197c4a 100644
--- a/LeanAPAP.lean
+++ b/LeanAPAP.lean
@@ -1,25 +1,23 @@
 import LeanAPAP.Extras.BSG
 import LeanAPAP.FiniteField.Basic
+import LeanAPAP.Mathlib.Algebra.Group.Action.Defs
 import LeanAPAP.Mathlib.Algebra.Group.AddChar
 import LeanAPAP.Mathlib.Algebra.Order.Group.Unbundled.Basic
+import LeanAPAP.Mathlib.Algebra.Order.Module.Defs
+import LeanAPAP.Mathlib.Algebra.Star.Basic
+import LeanAPAP.Mathlib.Algebra.Star.Rat
 import LeanAPAP.Mathlib.Analysis.RCLike.Basic
 import LeanAPAP.Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar
-import LeanAPAP.Mathlib.Analysis.SpecialFunctions.Log.Basic
 import LeanAPAP.Mathlib.Analysis.SpecialFunctions.Pow.NNReal
-import LeanAPAP.Mathlib.Analysis.SpecialFunctions.Pow.Real
-import LeanAPAP.Mathlib.Data.ENNReal.Basic
-import LeanAPAP.Mathlib.Data.ENNReal.Operations
-import LeanAPAP.Mathlib.Data.ENNReal.Real
 import LeanAPAP.Mathlib.Data.Fintype.Order
 import LeanAPAP.Mathlib.Data.NNReal.Basic
-import LeanAPAP.Mathlib.Data.Rat.Cast.Order
 import LeanAPAP.Mathlib.MeasureTheory.Function.EssSup
 import LeanAPAP.Mathlib.MeasureTheory.Function.LpSeminorm.Basic
 import LeanAPAP.Mathlib.MeasureTheory.MeasurableSpace.Defs
 import LeanAPAP.Mathlib.MeasureTheory.Measure.MeasureSpaceDef
-import LeanAPAP.Mathlib.MeasureTheory.Measure.Typeclasses
 import LeanAPAP.Mathlib.Order.Filter.Basic
 import LeanAPAP.Mathlib.Order.LiminfLimsup
+import LeanAPAP.Mathlib.Probability.ConditionalProbability
 import LeanAPAP.Mathlib.Tactic.Positivity
 import LeanAPAP.Physics.AlmostPeriodicity
 import LeanAPAP.Physics.DRC
diff --git a/LeanAPAP/Extras/BSG.lean b/LeanAPAP/Extras/BSG.lean
index a4959905df..7ede410bd5 100644
--- a/LeanAPAP/Extras/BSG.lean
+++ b/LeanAPAP/Extras/BSG.lean
@@ -1,5 +1,6 @@
 import Mathlib.Combinatorics.Additive.Energy
 import Mathlib.Data.Real.StarOrdered
+import LeanAPAP.Prereqs.Convolution.Discrete.Basic
 import LeanAPAP.Prereqs.Convolution.Order
 
 open BigOperators Finset
diff --git a/LeanAPAP/FiniteField/Basic.lean b/LeanAPAP/FiniteField/Basic.lean
index 64980c0219..3aae2650f0 100644
--- a/LeanAPAP/FiniteField/Basic.lean
+++ b/LeanAPAP/FiniteField/Basic.lean
@@ -1,7 +1,5 @@
-import LeanAPAP.Mathlib.Analysis.SpecialFunctions.Log.Basic
-import LeanAPAP.Mathlib.Data.Rat.Cast.Order
+import Mathlib.FieldTheory.Finite.Basic
 import LeanAPAP.Prereqs.Convolution.ThreeAP
-import LeanAPAP.Prereqs.FourierTransform.Compact
 import LeanAPAP.Prereqs.LargeSpec
 import LeanAPAP.Physics.AlmostPeriodicity
 import LeanAPAP.Physics.Unbalancing
@@ -229,9 +227,8 @@ theorem ff (hq₃ : 3 ≤ q) (hq : q.Prime) {A : Finset G} (hA₀ : A.Nonempty)
           gcongr
           rw [inv_le ‹_› (by positivity)]
           calc
-            65⁻¹ = (1 + 64)⁻¹ := by norm_num
-            _ ≤ log (1 + 64⁻¹) := le_log_one_add_inv (by norm_num)
-            _ = log (65 / 64) := by norm_num
+            65⁻¹ = 1 - (65 / 64)⁻¹ := by norm_num
+            _ ≤ log (65 / 64) := one_sub_inv_le_log_of_pos (by positivity)
     _ = ↑(card V) := by simp [card_eq_pow_finrank (K := ZMod q) (V := V)]
     _ ≤ 2 * β⁻¹ ^ 2 := by
       rw [← natCast_card_mul_nnratCast_dens, mul_pow, mul_inv, ← mul_assoc,
diff --git a/LeanAPAP/Mathlib/Algebra/Group/Action/Defs.lean b/LeanAPAP/Mathlib/Algebra/Group/Action/Defs.lean
new file mode 100644
index 0000000000..b99bb308a8
--- /dev/null
+++ b/LeanAPAP/Mathlib/Algebra/Group/Action/Defs.lean
@@ -0,0 +1,6 @@
+import Mathlib.Algebra.Group.Action.Defs
+
+@[to_additive]
+lemma smul_mul_smul_comm {α β : Type*} [Mul α] [Mul β] [SMul α β] [IsScalarTower α β β]
+    [IsScalarTower α α β] [SMulCommClass β α β] (a : α) (b : β) (c : α) (d : β) :
+    (a • b) * c • d = (a * c) • (b * d) := smul_smul_smul_comm a b c d
diff --git a/LeanAPAP/Mathlib/Algebra/Order/Module/Defs.lean b/LeanAPAP/Mathlib/Algebra/Order/Module/Defs.lean
new file mode 100644
index 0000000000..8534515b29
--- /dev/null
+++ b/LeanAPAP/Mathlib/Algebra/Order/Module/Defs.lean
@@ -0,0 +1,4 @@
+import Mathlib.Algebra.Order.Module.Defs
+
+attribute [gcongr] smul_le_smul_of_nonneg_left smul_le_smul_of_nonneg_right
+  smul_lt_smul_of_pos_left smul_lt_smul_of_pos_right
diff --git a/LeanAPAP/Mathlib/Algebra/Star/Basic.lean b/LeanAPAP/Mathlib/Algebra/Star/Basic.lean
new file mode 100644
index 0000000000..2c54b306b2
--- /dev/null
+++ b/LeanAPAP/Mathlib/Algebra/Star/Basic.lean
@@ -0,0 +1,12 @@
+import Mathlib.Algebra.Star.Basic
+
+/-!
+# TODO
+
+Swap arguments to `star_nsmul`/`star_zsmul`
+-/
+
+variable {α : Type*}
+
+instance StarAddMonoid.toStarModuleInt [AddCommGroup α] [StarAddMonoid α] : StarModule ℤ α where
+  star_smul _ _ := star_zsmul _ _
diff --git a/LeanAPAP/Mathlib/Algebra/Star/Rat.lean b/LeanAPAP/Mathlib/Algebra/Star/Rat.lean
new file mode 100644
index 0000000000..cb9e712090
--- /dev/null
+++ b/LeanAPAP/Mathlib/Algebra/Star/Rat.lean
@@ -0,0 +1,16 @@
+import Mathlib.Algebra.Module.Defs
+import Mathlib.Algebra.Star.Rat
+
+variable {α : Type*}
+
+@[simp] lemma star_nnqsmul [AddCommMonoid α] [Module ℚ≥0 α] [StarAddMonoid α] (q : ℚ≥0) (a : α) :
+    star (q • a) = q • star a := sorry
+
+@[simp] lemma star_qsmul [AddCommGroup α] [Module ℚ α] [StarAddMonoid α] (q : ℚ) (a : α) :
+    star (q • a) = q • star a := sorry
+
+instance StarAddMonoid.toStarModuleNNRat [AddCommMonoid α] [Module ℚ≥0 α] [StarAddMonoid α] :
+    StarModule ℚ≥0 α where star_smul := star_nnqsmul
+
+instance StarAddMonoid.toStarModuleRat [AddCommGroup α] [Module ℚ α] [StarAddMonoid α] :
+    StarModule ℚ α where star_smul := star_qsmul
diff --git a/LeanAPAP/Mathlib/Analysis/SpecialFunctions/Complex/CircleAddChar.lean b/LeanAPAP/Mathlib/Analysis/SpecialFunctions/Complex/CircleAddChar.lean
index 911405ccab..c7d8182a2c 100644
--- a/LeanAPAP/Mathlib/Analysis/SpecialFunctions/Complex/CircleAddChar.lean
+++ b/LeanAPAP/Mathlib/Analysis/SpecialFunctions/Complex/CircleAddChar.lean
@@ -1,4 +1,6 @@
-import Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar
+import Mathlib.Algebra.EuclideanDomain.Basic
+import Mathlib.Algebra.EuclideanDomain.Field
+import Mathlib.Analysis.SpecialFunctions.Complex.Circle
 
 open AddChar Multiplicative Real
 open scoped ComplexConjugate Real
diff --git a/LeanAPAP/Mathlib/Analysis/SpecialFunctions/Log/Basic.lean b/LeanAPAP/Mathlib/Analysis/SpecialFunctions/Log/Basic.lean
deleted file mode 100644
index f28c08842b..0000000000
--- a/LeanAPAP/Mathlib/Analysis/SpecialFunctions/Log/Basic.lean
+++ /dev/null
@@ -1,192 +0,0 @@
-import Mathlib.Analysis.SpecialFunctions.Log.Basic
-
-namespace Real
-variable {x : ℝ}
-
-lemma le_log_one_add_inv (hx : 0 < x) : (1 + x)⁻¹ ≤ log (1 + x⁻¹) := by
-  have' := log_le_sub_one_of_pos (x := (1 + x⁻¹)⁻¹) (by positivity)
-  rw [log_inv, neg_le] at this
-  exact this.trans' (by field_simp [add_comm])
-
-end Real
-
-namespace Mathlib.Meta.Positivity
-open Lean Meta Qq Function Real NormNum Nat Sum3
-
-section
-variable {R : Type*} {e : R} {n : ℕ}
-
-private lemma le_one_of_isNat [StrictOrderedSemiring R] (h : IsNat e n) (w : ble 1 n = true) :
-    1 ≤ (e : R) := by simpa [h.to_eq rfl] using w
-
-private lemma lt_one_of_isNat [StrictOrderedSemiring R] (h : IsNat e n) (w : ble 2 n = true) :
-    1 < (e : R) := by simpa [h.to_eq rfl] using w
-
-private lemma ne_one_of_isNegNat [StrictOrderedRing R] (h : IsInt e (.negOfNat n)) :
-    (e : R) ≠ 1 := by
-  rw [h.neg_to_eq rfl]; exact ((neg_nonpos.2 n.cast_nonneg).trans_lt zero_lt_one).ne
-
-private lemma lt_one_of_isRat {n : ℤ} {d : ℕ} [LinearOrderedRing R] :
-    IsRat e n d → decide (d < n) → 1 < e := by
-  rintro ⟨inv, rfl⟩ h
-  refine one_lt_of_lt_mul_right₀ d.cast_nonneg ?_
-  rw [mul_assoc, invOf_mul_self, mul_one]
-  exact mod_cast of_decide_eq_true h
-
-private lemma le_one_of_isRat {n : ℤ} {d : ℕ} [LinearOrderedRing R] :
-    IsRat e n d → decide (d ≤ n) → 1 ≤ e := by
-  rintro ⟨inv, rfl⟩ h
-  refine one_le_of_le_mul_right₀ (d.cast_nonneg.lt_of_ne' inv.ne_zero) ?_
-  rw [mul_assoc, invOf_mul_self, mul_one]
-  exact mod_cast of_decide_eq_true h
-
-private lemma ne_one_of_isRat {n : ℤ} {d : ℕ} [LinearOrderedRing R] :
-    IsRat e n d → decide (n ≠ d) → e ≠ 1 := by
-  rintro ⟨inv, rfl⟩ h
-  refine (mul_eq_right₀ inv.ne_zero).ne.1 ?_
-  rw [mul_assoc, invOf_mul_self, mul_one]
-  exact mod_cast of_decide_eq_true h
-
-end
-
-variable {u : Level} {α : Q(Type u)} (oα : Q(One $α)) (pα : Q(PartialOrder $α))
-
-/-- Attempts to prove a `Strictness` result when `e` evaluates to a literal number. -/
-def normNumOne (e : Q($α)) : MetaM (Option (Q(1 < $e) ⊕ Q(1 ≤ $e) ⊕ Q($e ≠ 1))) := do
-  match ← NormNum.derive e with
-  | .isBool .. => pure none
-  | .isNat _ lit p =>
-    if 0 < lit.natLit! then
-      let _a ← synthInstanceQ q(StrictOrderedSemiring $α)
-      assumeInstancesCommute
-      have p : Q(NormNum.IsNat $e $lit) := p
-      haveI' p' : Nat.ble 2 $lit =Q true := ⟨⟩
-      pure $ some $ in₀ q(lt_one_of_isNat $p $p')
-    else
-      let _a ← synthInstanceQ q(StrictOrderedSemiring $α)
-      assumeInstancesCommute
-      have p : Q(NormNum.IsNat $e $lit) := p
-      haveI' p' : Nat.ble 1 $lit =Q true := ⟨⟩
-      pure $ some $ in₁ q(le_one_of_isNat $p $p')
-  | .isNegNat _ lit p =>
-    let _a ← synthInstanceQ q(StrictOrderedRing $α)
-    assumeInstancesCommute
-    have p : Q(NormNum.IsInt $e (Int.negOfNat $lit)) := p
-    haveI' p' : Nat.ble 1 $lit =Q true := ⟨⟩
-    pure $ some $ in₂ q(ne_one_of_isNegNat $p)
-  | .isRat _i q n d p =>
-    let _a ← synthInstanceQ q(LinearOrderedRing $α)
-    assumeInstancesCommute
-    have p : Q(NormNum.IsRat $e $n $d) := p
-    if 0 < q then
-      haveI' w : decide ($d < $n) =Q true := ⟨⟩
-      pure $ some $ .inl q(lt_one_of_isRat $p $w)
-    else if q = 0 then -- should not be reachable, but just in case
-      haveI' w : decide ($d ≤ $n) =Q true := ⟨⟩
-      pure $ some $ in₁ q(le_one_of_isRat $p $w)
-    else
-      haveI' w : decide ($n ≠ $d) =Q true := ⟨⟩
-      pure $ some $ in₂ q(ne_one_of_isRat $p $w)
-
-/-- A variation on `assumption` which checks if the hypothesis `ldecl` is `a [</≤/=] e`
-where `a` is a numeral. -/
-def compareHypOne (e : Q($α)) (ldecl : LocalDecl) :
-    MetaM (Option (Q(1 < $e) ⊕ Q(1 ≤ $e) ⊕ Q($e ≠ 1))) := do
-  have e' : Q(Prop) := ldecl.type
-  let p : Q($e') := .fvar ldecl.fvarId
-  match e' with
-  | ~q(@LE.le.{u} $β $_le $lo $hi) =>
-    let .defEq (_ : $α =Q $β) ← isDefEqQ α β | return none
-    let .defEq _ ← isDefEqQ e hi | return none
-    assertInstancesCommute
-    match lo with
-    | ~q(1) => pure $ some $ .inr $ .inl q($p)
-    | _ =>
-      match ← normNumOne oα pα lo with
-      | some $ in₀ p₁ => pure $ some $ in₀ q(lt_of_lt_of_le $p₁ $p)
-      | some $ in₁ p₁ => pure $ some $ in₁ q(le_trans $p₁ $p)
-      | _ => return none
-  | ~q(@LT.lt.{u} $β $_lt $lo $hi) =>
-    let .defEq (_ : $α =Q $β) ← isDefEqQ α β | return none
-    let .defEq _ ← isDefEqQ e hi | return none
-    assertInstancesCommute
-    match lo with
-    | ~q(1) => pure $ some $ in₀ q($p)
-    | _ =>
-      match ← normNumOne oα pα lo with
-      | some $ in₀ p₁ => pure $ some $ in₀ q(lt_trans $p₁ $p)
-      | some $ in₁ p₁ => pure $ some $ in₀ q(lt_of_le_of_lt $p₁ $p)
-      | _ => return none
-  | ~q(@Eq.{u+1} $α' $lhs $rhs) =>
-    let .defEq (_ : $α =Q $α') ← isDefEqQ α α' | return none
-    match ← isDefEqQ e rhs with
-    | .defEq _ =>
-      match lhs with
-      | ~q(1) => pure $ some $ in₁ q(le_of_eq $p)
-      | _ =>
-        match ← normNumOne oα pα lhs with
-        | some $ in₀ p₁ => pure $ some $ in₀ q(lt_of_lt_of_eq $p₁ $p)
-        | some $ in₁ p₁ => pure $ some $ in₁ q(le_of_le_of_eq $p₁ $p)
-        | some $ in₂ p₁ => pure $ some $ in₂ q(ne_of_ne_of_eq' $p₁ $p)
-        | none => pure none
-    | .notDefEq =>
-      let .defEq _ ← isDefEqQ e lhs | return none
-      match rhs with
-      | ~q(1) => pure $ some $ in₁ q(ge_of_eq $p)
-      | _ =>
-        assertInstancesCommute
-        match ← normNumOne oα pα rhs with
-        | some $ in₀ p₁ => pure $ some $ in₀ q(lt_of_lt_of_eq $p₁ $ Eq.symm $p)
-        | some $ in₁ p₁ => pure $ some $ in₁ q(le_of_le_of_eq $p₁ $ Eq.symm $p)
-        | some $ in₂ p₁ => pure $ some $ in₂ q(ne_of_ne_of_eq' $p₁ $ Eq.symm $p)
-        | none => pure none
-  | ~q(@Ne.{u + 1} $α' $lhs $rhs) =>
-    let .defEq (_ : $α =Q $α') ← isDefEqQ α α' | return none
-    match lhs, rhs with
-    | ~q(1), _ =>
-      let .defEq _ ← isDefEqQ e rhs | return none
-      pure $ some $ in₂ q(Ne.symm $p)
-    | _, ~q(1) =>
-      let .defEq _ ← isDefEqQ e lhs | return none
-      pure $ some $ in₂ p
-    | _, _ => return none
-  | _ => return none
-
-variable {oα pα} in
-def orElseOne {e : Q($α)} (t₁ : Option (Q(1 < $e) ⊕ Q(1 ≤ $e) ⊕ Q($e ≠ 1)))
-    (t₂ : MetaM (Option (Q(1 < $e) ⊕ Q(1 ≤ $e) ⊕ Q($e ≠ 1)))) :
-    MetaM (Option (Q(1 < $e) ⊕ Q(1 ≤ $e) ⊕ Q($e ≠ 1))) := do
-  match t₁ with
-  | none => t₂
-  | p@(some $ in₀ _) => pure p
-  | some $ in₁ p₁ =>
-    match ← t₂ with
-    | p@(some $ in₀ _) => pure p
-    | some $ in₂ p₂ => pure $ some $ in₀ q(lt_of_le_of_ne' $p₁ $p₂)
-    | _ => pure $ some $ in₁ p₁
-  | some $ in₂ p₁ =>
-    match ← t₂ with
-    | p@(some $ in₀ _) => pure p
-    | some $ in₁ p₂ => pure $ some $ in₀ q(lt_of_le_of_ne' $p₂ $p₁)
-    | _ => pure $ some $ in₂ p₁
-
-/-- Extension for the `positivity` tactic: `Nat.cast` is always non-negative,
-and positive when its input is. -/
-@[positivity Real.log _] def evalRealLog : PositivityExt where eval {u α} _ _ e := do
-  match u, α, e with
-  | 0, ~q(ℝ), ~q(log $a) =>
-    let mut ra ← normNumOne q(inferInstance) q(inferInstance) a
-    for ldecl in ← getLCtx do
-      if !ldecl.isImplementationDetail then
-        ra ← orElseOne ra <| compareHypOne q(inferInstance) q(inferInstance) a ldecl
-    assertInstancesCommute
-    match ra with
-    | some $ in₀ pa => pure $ .positive q(Real.log_pos $pa)
-    | some $ in₁ pa => pure $ .nonnegative q(Real.log_nonneg $pa)
-    | _ => pure .none
-  | _, _, _ => throwError "not `Real.log`"
-
--- example {x : ℝ} (hx : 1 ≤ x) : 0 ≤ log x := by positivity
--- example {x : ℝ} (hx : 1 < x) : 0 < log x := by positivity
-
-end Mathlib.Meta.Positivity
diff --git a/LeanAPAP/Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean b/LeanAPAP/Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean
index 42d018691d..20004ebe35 100644
--- a/LeanAPAP/Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean
+++ b/LeanAPAP/Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean
@@ -1,5 +1,4 @@
 import Mathlib.Analysis.SpecialFunctions.Pow.NNReal
-import LeanAPAP.Mathlib.Analysis.SpecialFunctions.Pow.Real
 
 /-!
 # TODO
diff --git a/LeanAPAP/Mathlib/Analysis/SpecialFunctions/Pow/Real.lean b/LeanAPAP/Mathlib/Analysis/SpecialFunctions/Pow/Real.lean
deleted file mode 100644
index 901df46926..0000000000
--- a/LeanAPAP/Mathlib/Analysis/SpecialFunctions/Pow/Real.lean
+++ /dev/null
@@ -1,16 +0,0 @@
-import Mathlib.Analysis.SpecialFunctions.Pow.Real
-
-namespace Real
-variable {x y z : ℝ}
-
--- TODO: Replace in mathlib
-alias rpow_add_intCast := rpow_add_int
-alias rpow_add_natCast := rpow_add_nat
-alias rpow_sub_intCast := rpow_sub_int
-alias rpow_sub_natCast := rpow_sub_nat
-alias rpow_add_intCast' := rpow_add_int'
-alias rpow_add_natCast' := rpow_add_nat'
-alias rpow_sub_intCast' := rpow_sub_int'
-alias rpow_sub_natCast' := rpow_sub_nat'
-
-end Real
diff --git a/LeanAPAP/Mathlib/Data/ENNReal/Basic.lean b/LeanAPAP/Mathlib/Data/ENNReal/Basic.lean
deleted file mode 100644
index d9b9df3d9b..0000000000
--- a/LeanAPAP/Mathlib/Data/ENNReal/Basic.lean
+++ /dev/null
@@ -1,10 +0,0 @@
-import Mathlib.Data.ENNReal.Basic
-
-open scoped NNReal
-
-namespace ENNReal
-
--- TODO: Replace in mathlib
-lemma toNNReal_coe' (r : ℝ≥0) : ENNReal.toNNReal r = r := toNNReal_coe
-
-end ENNReal
diff --git a/LeanAPAP/Mathlib/Data/ENNReal/Operations.lean b/LeanAPAP/Mathlib/Data/ENNReal/Operations.lean
deleted file mode 100644
index ca6849d839..0000000000
--- a/LeanAPAP/Mathlib/Data/ENNReal/Operations.lean
+++ /dev/null
@@ -1,12 +0,0 @@
-import Mathlib.Data.ENNReal.Operations
-
-namespace ENNReal
-variable {α : Type*} {s : Finset α} {f : α → ℝ≥0∞}
-
--- TODO: Unify `sum_lt_top` and `sum_lt_top_iff`
-attribute [simp] sum_lt_top_iff
-
-@[simp] lemma sum_ne_top : ∑ a ∈ s, f a ≠ ∞ ↔ ∀ a ∈ s, f a ≠ ⊤ := by
-  simpa [lt_top_iff_ne_top] using sum_lt_top_iff
-
-end ENNReal
diff --git a/LeanAPAP/Mathlib/Data/ENNReal/Real.lean b/LeanAPAP/Mathlib/Data/ENNReal/Real.lean
deleted file mode 100644
index a32925aeb2..0000000000
--- a/LeanAPAP/Mathlib/Data/ENNReal/Real.lean
+++ /dev/null
@@ -1,3 +0,0 @@
-import Mathlib.Data.ENNReal.Real
-
-attribute [simp] ENNReal.toReal_inv
diff --git a/LeanAPAP/Mathlib/Data/NNReal/Basic.lean b/LeanAPAP/Mathlib/Data/NNReal/Basic.lean
index ba0c486ac2..30d49ef3a5 100644
--- a/LeanAPAP/Mathlib/Data/NNReal/Basic.lean
+++ b/LeanAPAP/Mathlib/Data/NNReal/Basic.lean
@@ -1,15 +1,7 @@
 import Mathlib.Data.NNReal.Basic
 
-open Set
-
 namespace NNReal
-variable {ι : Sort*} {f : ι → ℝ≥0}
-
-attribute [simp] coe_sum
 
-@[simp] lemma iSup_eq_zero (hf : BddAbove (range f)) : ⨆ i, f i = 0 ↔ ∀ i, f i = 0 := by
-  cases isEmpty_or_nonempty ι
-  · simp
-  · simp [← bot_eq_zero', ← le_bot_iff, ciSup_le_iff hf]
+@[simp, norm_cast] lemma coe_nnqsmul (q : ℚ≥0) (x : ℝ≥0) : ↑(q • x) = (q • x : ℝ) := rfl
 
 end NNReal
diff --git a/LeanAPAP/Mathlib/Data/Rat/Cast/Order.lean b/LeanAPAP/Mathlib/Data/Rat/Cast/Order.lean
deleted file mode 100644
index 40c86d0c7d..0000000000
--- a/LeanAPAP/Mathlib/Data/Rat/Cast/Order.lean
+++ /dev/null
@@ -1,11 +0,0 @@
-import Mathlib.Data.Rat.Cast.Order
-
-namespace NNRat
-variable {K : Type*} [LinearOrderedSemifield K] {p : ℚ≥0}
-
-@[simp, norm_cast] lemma cast_le_one : (p : K) ≤ 1 ↔ p ≤ 1 := by rw [← cast_le (K := K), cast_one]
-@[simp, norm_cast] lemma one_le_cast : 1 ≤ (p : K) ↔ 1 ≤ p := by rw [← cast_le (K := K), cast_one]
-@[simp, norm_cast] lemma cast_lt_one : (p : K) < 1 ↔ p < 1 := by rw [← cast_lt (K := K), cast_one]
-@[simp, norm_cast] lemma one_lt_cast : 1 < (p : K) ↔ 1 < p := by rw [← cast_lt (K := K), cast_one]
-
-end NNRat
diff --git a/LeanAPAP/Mathlib/MeasureTheory/Function/EssSup.lean b/LeanAPAP/Mathlib/MeasureTheory/Function/EssSup.lean
index e191ff525b..642a561780 100644
--- a/LeanAPAP/Mathlib/MeasureTheory/Function/EssSup.lean
+++ b/LeanAPAP/Mathlib/MeasureTheory/Function/EssSup.lean
@@ -1,5 +1,4 @@
 import Mathlib.MeasureTheory.Function.EssSup
-import Mathlib.MeasureTheory.Measure.MeasureSpace
 import LeanAPAP.Mathlib.Order.LiminfLimsup
 
 open Filter MeasureTheory
diff --git a/LeanAPAP/Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean b/LeanAPAP/Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean
index 93fa959365..44f27cc0b2 100644
--- a/LeanAPAP/Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean
+++ b/LeanAPAP/Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean
@@ -1,5 +1,4 @@
 import Mathlib.MeasureTheory.Function.LpSeminorm.Basic
-import LeanAPAP.Mathlib.Data.ENNReal.Real
 
 noncomputable section
 
diff --git a/LeanAPAP/Mathlib/MeasureTheory/Measure/Typeclasses.lean b/LeanAPAP/Mathlib/MeasureTheory/Measure/Typeclasses.lean
deleted file mode 100644
index 2448faebce..0000000000
--- a/LeanAPAP/Mathlib/MeasureTheory/Measure/Typeclasses.lean
+++ /dev/null
@@ -1,13 +0,0 @@
-import Mathlib.MeasureTheory.Measure.Typeclasses
-import LeanAPAP.Mathlib.Data.ENNReal.Operations
-
-namespace MeasureTheory
-variable {ι α : Type*} {mα : MeasurableSpace α} {s : Finset ι} {μ : ι → Measure α}
-  [∀ i, IsFiniteMeasure (μ i)]
-
-instance : IsFiniteMeasure (∑ i ∈ s, μ i) where measure_univ_lt_top := by simp [measure_lt_top]
-
-instance [Fintype ι] : IsFiniteMeasure (.sum μ) where
-  measure_univ_lt_top := by simp [measure_lt_top]
-
-end MeasureTheory
diff --git a/LeanAPAP/Mathlib/Probability/ConditionalProbability.lean b/LeanAPAP/Mathlib/Probability/ConditionalProbability.lean
new file mode 100644
index 0000000000..f2b432f493
--- /dev/null
+++ b/LeanAPAP/Mathlib/Probability/ConditionalProbability.lean
@@ -0,0 +1,13 @@
+import Mathlib.Probability.ConditionalProbability
+
+open ENNReal MeasureTheory MeasureTheory.Measure MeasurableSpace Set
+
+variable {Ω Ω' α : Type*} {m : MeasurableSpace Ω} {m' : MeasurableSpace Ω'} (μ : Measure Ω)
+  {s t : Set Ω}
+
+namespace ProbabilityTheory
+
+@[simp] lemma cond_apply_self (hs₀ : μ s ≠ 0) (hs : μ s ≠ ∞) : μ[|s] s = 1 := by
+  simpa [cond] using ENNReal.inv_mul_cancel hs₀ hs
+
+end ProbabilityTheory
diff --git a/LeanAPAP/Physics/AlmostPeriodicity.lean b/LeanAPAP/Physics/AlmostPeriodicity.lean
index e0a1f5e53b..ec36585ebb 100644
--- a/LeanAPAP/Physics/AlmostPeriodicity.lean
+++ b/LeanAPAP/Physics/AlmostPeriodicity.lean
@@ -1,7 +1,7 @@
 import Mathlib.Algebra.Order.Chebyshev
 import Mathlib.Combinatorics.Additive.DoublingConst
-import Mathlib.Combinatorics.Pigeonhole
 import Mathlib.Data.Complex.ExponentialBounds
+import LeanAPAP.Prereqs.Convolution.Discrete.Basic
 import LeanAPAP.Prereqs.Convolution.Norm
 import LeanAPAP.Prereqs.Curlog
 import LeanAPAP.Prereqs.MarcinkiewiczZygmund
diff --git a/LeanAPAP/Physics/DRC.lean b/LeanAPAP/Physics/DRC.lean
index 479c196a8f..4677ab14f3 100644
--- a/LeanAPAP/Physics/DRC.lean
+++ b/LeanAPAP/Physics/DRC.lean
@@ -1,4 +1,7 @@
+import LeanAPAP.Prereqs.Convolution.Discrete.Basic
 import LeanAPAP.Prereqs.Convolution.Norm
+import LeanAPAP.Prereqs.Convolution.Order
+import LeanAPAP.Prereqs.Function.Indicator.Basic
 import LeanAPAP.Prereqs.LpNorm.Weighted
 
 /-!
diff --git a/LeanAPAP/Physics/Unbalancing.lean b/LeanAPAP/Physics/Unbalancing.lean
index 2867d48e32..3936a82760 100644
--- a/LeanAPAP/Physics/Unbalancing.lean
+++ b/LeanAPAP/Physics/Unbalancing.lean
@@ -1,6 +1,6 @@
 import Mathlib.Algebra.Order.Group.PosPart
 import Mathlib.Data.Complex.ExponentialBounds
-import LeanAPAP.Prereqs.Convolution.Discrete.Basic
+import LeanAPAP.Prereqs.Convolution.Discrete.Defs
 import LeanAPAP.Prereqs.LpNorm.Weighted
 
 /-!
diff --git a/LeanAPAP/Prereqs/Convolution/Compact.lean b/LeanAPAP/Prereqs/Convolution/Compact.lean
index 7b39e694fe..85054e684e 100644
--- a/LeanAPAP/Prereqs/Convolution/Compact.lean
+++ b/LeanAPAP/Prereqs/Convolution/Compact.lean
@@ -1,5 +1,6 @@
-import LeanAPAP.Prereqs.Convolution.Discrete.Basic
+import LeanAPAP.Prereqs.Convolution.Discrete.Defs
 import LeanAPAP.Prereqs.Expect.Complex
+import LeanAPAP.Prereqs.Function.Indicator.Defs
 
 /-!
 # Convolution in the compact normalisation
diff --git a/LeanAPAP/Prereqs/Convolution/Discrete/Basic.lean b/LeanAPAP/Prereqs/Convolution/Discrete/Basic.lean
index fbddc92b87..25f6328584 100644
--- a/LeanAPAP/Prereqs/Convolution/Discrete/Basic.lean
+++ b/LeanAPAP/Prereqs/Convolution/Discrete/Basic.lean
@@ -149,7 +149,7 @@ lemma indicate_iterConv_apply (s : Finset G) (n : ℕ) (a : G) :
   simp_rw [iterConv_succ', conv_eq_sum_sub', ih, indicate_apply, boole_mul, sum_ite,
     filter_univ_mem, sum_const_zero, add_zero, ← Nat.cast_sum, ← Finset.card_sigma]
   congr 1
-  refine card_equiv ((Equiv.sigmaEquivProd ..).trans (Equiv.piFinSucc ..).symm) ?_
+  refine card_equiv ((Equiv.sigmaEquivProd ..).trans <| Fin.consEquiv fun _ ↦ G) ?_
   aesop (add simp [Fin.sum_cons, Fin.forall_fin_succ])
 
 lemma indicate_iterConv_conv (s : Finset G) (n : ℕ) (f : G → R) :
diff --git a/LeanAPAP/Prereqs/Convolution/Norm.lean b/LeanAPAP/Prereqs/Convolution/Norm.lean
index bedd81a968..cb1d8f979d 100644
--- a/LeanAPAP/Prereqs/Convolution/Norm.lean
+++ b/LeanAPAP/Prereqs/Convolution/Norm.lean
@@ -1,6 +1,6 @@
 import Mathlib.Data.Real.StarOrdered
-import LeanAPAP.Prereqs.Convolution.Order
-import LeanAPAP.Prereqs.LpNorm.Compact
+import LeanAPAP.Prereqs.Convolution.Discrete.Defs
+import LeanAPAP.Prereqs.LpNorm.Discrete.Basic
 
 /-!
 # Norm of a convolution
diff --git a/LeanAPAP/Prereqs/Convolution/Order.lean b/LeanAPAP/Prereqs/Convolution/Order.lean
index 68ff0fc2bb..8cf955aa8c 100644
--- a/LeanAPAP/Prereqs/Convolution/Order.lean
+++ b/LeanAPAP/Prereqs/Convolution/Order.lean
@@ -1,5 +1,5 @@
 import LeanAPAP.Mathlib.Tactic.Positivity
-import LeanAPAP.Prereqs.Convolution.Discrete.Basic
+import LeanAPAP.Prereqs.Convolution.Discrete.Defs
 
 open Finset Function Real
 open scoped ComplexConjugate NNReal Pointwise
diff --git a/LeanAPAP/Prereqs/Convolution/ThreeAP.lean b/LeanAPAP/Prereqs/Convolution/ThreeAP.lean
index d7d29814f8..a6badb143d 100644
--- a/LeanAPAP/Prereqs/Convolution/ThreeAP.lean
+++ b/LeanAPAP/Prereqs/Convolution/ThreeAP.lean
@@ -1,5 +1,8 @@
 import Mathlib.Combinatorics.Additive.AP.Three.Defs
-import LeanAPAP.Prereqs.Convolution.Norm
+import Mathlib.Data.Real.StarOrdered
+import LeanAPAP.Prereqs.Convolution.Discrete.Defs
+import LeanAPAP.Prereqs.Function.Indicator.Defs
+import LeanAPAP.Prereqs.LpNorm.Discrete.Defs
 
 /-!
 # The convolution characterisation of 3AP-free sets
diff --git a/LeanAPAP/Prereqs/Convolution/WithConv.lean b/LeanAPAP/Prereqs/Convolution/WithConv.lean
index aa25146320..54240e28e2 100644
--- a/LeanAPAP/Prereqs/Convolution/WithConv.lean
+++ b/LeanAPAP/Prereqs/Convolution/WithConv.lean
@@ -1,4 +1,4 @@
-import LeanAPAP.Prereqs.Convolution.Discrete.Basic
+import LeanAPAP.Prereqs.Convolution.Discrete.Defs
 
 /-!
 # The ring of functions under convolution
diff --git a/LeanAPAP/Prereqs/Energy.lean b/LeanAPAP/Prereqs/Energy.lean
index f8acf1446f..eab58479f7 100644
--- a/LeanAPAP/Prereqs/Energy.lean
+++ b/LeanAPAP/Prereqs/Energy.lean
@@ -1,6 +1,7 @@
 import LeanAPAP.Prereqs.AddChar.Basic
-import LeanAPAP.Prereqs.Convolution.Order
-import LeanAPAP.Prereqs.FourierTransform.Compact
+import LeanAPAP.Prereqs.Convolution.Discrete.Basic
+import LeanAPAP.Prereqs.Expect.Complex
+import LeanAPAP.Prereqs.FourierTransform.Discrete
 
 noncomputable section
 
diff --git a/LeanAPAP/Prereqs/FourierTransform/Compact.lean b/LeanAPAP/Prereqs/FourierTransform/Compact.lean
index b3caf848b1..1ba57ac97f 100644
--- a/LeanAPAP/Prereqs/FourierTransform/Compact.lean
+++ b/LeanAPAP/Prereqs/FourierTransform/Compact.lean
@@ -1,6 +1,7 @@
 import LeanAPAP.Prereqs.Convolution.Compact
-import LeanAPAP.Prereqs.FourierTransform.Discrete
 import LeanAPAP.Prereqs.Expect.Complex
+import LeanAPAP.Prereqs.FourierTransform.Discrete
+import LeanAPAP.Prereqs.Function.Indicator.Basic
 
 /-!
 # Discrete Fourier transform in the compact normalisation
diff --git a/LeanAPAP/Prereqs/FourierTransform/Discrete.lean b/LeanAPAP/Prereqs/FourierTransform/Discrete.lean
index b008d1c346..8cb380ab89 100644
--- a/LeanAPAP/Prereqs/FourierTransform/Discrete.lean
+++ b/LeanAPAP/Prereqs/FourierTransform/Discrete.lean
@@ -93,6 +93,9 @@ lemma dft_conjneg_apply (f : α → ℂ) (ψ : AddChar α ℂ) : dft (conjneg f)
 @[simp]
 lemma dft_conjneg (f : α → ℂ) : dft (conjneg f) = conj (dft f) := funext $ dft_conjneg_apply _
 
+lemma dft_comp_neg_apply (f : α → ℂ) (ψ : AddChar α ℂ) :
+    dft (fun x ↦ f (-x)) ψ = dft f (-ψ) := Fintype.sum_equiv (Equiv.neg _) _ _ (by simp)
+
 @[simp] lemma dft_balance (f : α → ℂ) (hψ : ψ ≠ 0) : dft (balance f) ψ = dft f ψ := by
   simp only [balance, Pi.sub_apply, dft_sub, dft_const _ hψ, sub_zero]
 
diff --git a/LeanAPAP/Prereqs/Function/Indicator/Basic.lean b/LeanAPAP/Prereqs/Function/Indicator/Basic.lean
index 71851d9862..d014eec156 100644
--- a/LeanAPAP/Prereqs/Function/Indicator/Basic.lean
+++ b/LeanAPAP/Prereqs/Function/Indicator/Basic.lean
@@ -1,6 +1,5 @@
 import Mathlib.Data.Complex.Basic
 import Mathlib.Data.Fintype.Lattice
-import Mathlib.Data.NNReal.Basic
 import LeanAPAP.Prereqs.Expect.Basic
 import LeanAPAP.Prereqs.Function.Translate
 import LeanAPAP.Prereqs.Function.Indicator.Defs
diff --git a/lake-manifest.json b/lake-manifest.json
index d7e63b603e..3cef812756 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "31fb27d6b89dc94cf7349df247fc44d2a1d130af",
+   "rev": "e6d3a32d66252a70fda1d56463e1da975b3b8f53",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -25,7 +25,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "c792cfd1efe6e01cb176e158ddb195bedfb7ad33",
+   "rev": "adaeb6b4d4bf02f60ba3ff6717486a7e895eba77",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -65,7 +65,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "b5f7e1c26c6cb2be97c2ad36bf7038c159e359b3",
+   "rev": "79ef7496100b18304654c1476691e872fa7c491a",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,
@@ -105,7 +105,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "b5c59823650e1e36145625411c896de0088947cb",
+   "rev": "83f718b9055972dce4f92f5b3917426b91a0d2fe",
    "name": "«doc-gen4»",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",