From 07231ce3d5fbf791e132bd2fe82ff5478a8c5a81 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= <yael.dillies@gmail.com>
Date: Wed, 2 Oct 2024 09:50:06 +0000
Subject: [PATCH] Bump mathlib

---
 LeanAPAP.lean                                 |  5 --
 LeanAPAP/Mathlib/Algebra/Star/Rat.lean        | 16 ----
 LeanAPAP/Mathlib/Data/Complex/Basic.lean      |  8 --
 LeanAPAP/Mathlib/Data/ENNReal/Operations.lean | 15 ----
 LeanAPAP/Mathlib/Data/Real/ConjExponents.lean | 82 +++++++++++++------
 LeanAPAP/Physics/AlmostPeriodicity.lean       |  1 -
 LeanAPAP/Physics/DRC.lean                     |  2 +-
 LeanAPAP/Prereqs/Balance/Complex.lean         | 10 +--
 LeanAPAP/Prereqs/Balance/Defs.lean            | 46 -----------
 LeanAPAP/Prereqs/Bohr/Basic.lean              |  6 +-
 LeanAPAP/Prereqs/Convolution/Compact.lean     | 11 ++-
 .../Prereqs/Convolution/Discrete/Basic.lean   |  2 +-
 LeanAPAP/Prereqs/Energy.lean                  |  1 -
 LeanAPAP/Prereqs/Expect/Complex.lean          | 43 ----------
 .../Prereqs/FourierTransform/Compact.lean     |  3 +-
 .../Prereqs/FourierTransform/Discrete.lean    |  7 +-
 LeanAPAP/Prereqs/LpNorm/Compact.lean          |  1 -
 LeanAPAP/Prereqs/LpNorm/Discrete/Defs.lean    |  4 +-
 LeanAPAP/Prereqs/LpNorm/Weighted.lean         |  8 +-
 LeanAPAP/Prereqs/MarcinkiewiczZygmund.lean    |  5 +-
 LeanAPAP/Prereqs/Randomisation.lean           |  1 -
 LeanAPAP/Prereqs/Rudin.lean                   |  4 +-
 lake-manifest.json                            | 16 ++--
 lean-toolchain                                |  2 +-
 24 files changed, 92 insertions(+), 207 deletions(-)
 delete mode 100644 LeanAPAP/Mathlib/Algebra/Star/Rat.lean
 delete mode 100644 LeanAPAP/Mathlib/Data/Complex/Basic.lean
 delete mode 100644 LeanAPAP/Mathlib/Data/ENNReal/Operations.lean
 delete mode 100644 LeanAPAP/Prereqs/Balance/Defs.lean
 delete mode 100644 LeanAPAP/Prereqs/Expect/Complex.lean

diff --git a/LeanAPAP.lean b/LeanAPAP.lean
index aeda2b9413..cdcf10c558 100644
--- a/LeanAPAP.lean
+++ b/LeanAPAP.lean
@@ -4,11 +4,8 @@ import LeanAPAP.Integer
 import LeanAPAP.Mathlib.Algebra.Order.Group.Unbundled.Basic
 import LeanAPAP.Mathlib.Algebra.Order.GroupWithZero.Unbundled
 import LeanAPAP.Mathlib.Algebra.Order.Ring.Basic
-import LeanAPAP.Mathlib.Algebra.Star.Rat
 import LeanAPAP.Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar
-import LeanAPAP.Mathlib.Data.Complex.Basic
 import LeanAPAP.Mathlib.Data.ENNReal.Basic
-import LeanAPAP.Mathlib.Data.ENNReal.Operations
 import LeanAPAP.Mathlib.Data.ENNReal.Real
 import LeanAPAP.Mathlib.Data.Real.ConjExponents
 import LeanAPAP.Mathlib.MeasureTheory.Function.EssSup
@@ -22,7 +19,6 @@ import LeanAPAP.Prereqs.AddChar.Basic
 import LeanAPAP.Prereqs.AddChar.MeasurableSpace
 import LeanAPAP.Prereqs.AddChar.PontryaginDuality
 import LeanAPAP.Prereqs.Balance.Complex
-import LeanAPAP.Prereqs.Balance.Defs
 import LeanAPAP.Prereqs.Bohr.Arc
 import LeanAPAP.Prereqs.Bohr.Basic
 import LeanAPAP.Prereqs.Bohr.Regular
@@ -35,7 +31,6 @@ import LeanAPAP.Prereqs.Convolution.Order
 import LeanAPAP.Prereqs.Convolution.ThreeAP
 import LeanAPAP.Prereqs.Convolution.WithConv
 import LeanAPAP.Prereqs.Energy
-import LeanAPAP.Prereqs.Expect.Complex
 import LeanAPAP.Prereqs.FourierTransform.Compact
 import LeanAPAP.Prereqs.FourierTransform.Convolution
 import LeanAPAP.Prereqs.FourierTransform.Discrete
diff --git a/LeanAPAP/Mathlib/Algebra/Star/Rat.lean b/LeanAPAP/Mathlib/Algebra/Star/Rat.lean
deleted file mode 100644
index cb9e712090..0000000000
--- a/LeanAPAP/Mathlib/Algebra/Star/Rat.lean
+++ /dev/null
@@ -1,16 +0,0 @@
-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/Data/Complex/Basic.lean b/LeanAPAP/Mathlib/Data/Complex/Basic.lean
deleted file mode 100644
index 62b10cd0ff..0000000000
--- a/LeanAPAP/Mathlib/Data/Complex/Basic.lean
+++ /dev/null
@@ -1,8 +0,0 @@
-import Mathlib.Data.Complex.Basic
-
-namespace Complex
-
-@[simp] lemma coe_comp_sub {α : Type*} (f g : α → ℝ) :
-    ofReal' ∘ (f - g) = ofReal' ∘ f - ofReal' ∘ g := map_comp_sub ofReal _ _
-
-end Complex
diff --git a/LeanAPAP/Mathlib/Data/ENNReal/Operations.lean b/LeanAPAP/Mathlib/Data/ENNReal/Operations.lean
deleted file mode 100644
index 3f2942ae9b..0000000000
--- a/LeanAPAP/Mathlib/Data/ENNReal/Operations.lean
+++ /dev/null
@@ -1,15 +0,0 @@
-import Mathlib.Data.ENNReal.Operations
-
-namespace ENNReal
-variable {a b c : ℝ≥0∞}
-
-protected lemma sub_eq_of_eq_add' (ha : a ≠ ∞) (h : a = c + b) : a - b = c :=
-  ENNReal.sub_eq_of_eq_add (mt (by rintro rfl; simpa using h) ha) h
-
-protected lemma eq_sub_of_add_eq' (hb : b ≠ ∞) (h : a + c = b) : a = b - c :=
-  ENNReal.eq_sub_of_add_eq (mt (by rintro rfl; simpa [eq_comm] using h) hb) h
-
-protected lemma sub_eq_of_eq_add_rev' (ha : a ≠ ∞) (h : a = b + c) : a - b = c :=
-  ENNReal.sub_eq_of_eq_add_rev (mt (by rintro rfl; simpa using h) ha) h
-
-end ENNReal
diff --git a/LeanAPAP/Mathlib/Data/Real/ConjExponents.lean b/LeanAPAP/Mathlib/Data/Real/ConjExponents.lean
index c34b1cba25..cd6181b6ad 100644
--- a/LeanAPAP/Mathlib/Data/Real/ConjExponents.lean
+++ b/LeanAPAP/Mathlib/Data/Real/ConjExponents.lean
@@ -1,6 +1,5 @@
 import Mathlib.Data.ENNReal.Inv
 import Mathlib.Data.Real.ConjExponents
-import LeanAPAP.Mathlib.Data.ENNReal.Operations
 
 open scoped NNReal
 
@@ -20,21 +19,45 @@ variable {a b p q : ℝ≥0∞} (h : p.IsConjExponent q)
 
 @[simp, norm_cast] lemma isConjExponent_coe {p q : ℝ≥0} :
     IsConjExponent p q ↔ p.IsConjExponent q := by
-  simp [NNReal.isConjExponent_iff, isConjExponent_iff]; sorry
+  simp only [isConjExponent_iff, NNReal.isConjExponent_iff]
+  refine ⟨fun h ↦ ⟨?_, ?_⟩, ?_⟩
+  · simpa using (ENNReal.lt_add_right (fun hp ↦ by simp [hp] at h) <| by simp).trans_eq h
+  · rw [← coe_inv, ← coe_inv] at h
+    norm_cast at h
+    all_goals rintro rfl; simp at h
+  · rintro ⟨hp, h⟩
+    rw [← coe_inv (zero_lt_one.trans hp).ne', ← coe_inv, ← coe_add, h, coe_one]
+    rintro rfl
+    simp [hp.ne'] at h
 
 alias ⟨_, _root_.NNReal.IsConjExponent.coe_ennreal⟩ := isConjExponent_coe
 
 namespace IsConjExponent
 
-/- Register several non-vanishing results following from the fact that `p` has a conjugate exponent
-`q`: many computations using these exponents require clearing out denominators, which can be done
-with `field_simp` given a proof that these denominators are non-zero, so we record the most usual
-ones. -/
+protected lemma conjExponent (hp : 1 ≤ p) : p.IsConjExponent (conjExponent p) := by
+  have : p ≠ 0 := (zero_lt_one.trans_le hp).ne'
+  rw [isConjExponent_iff, conjExponent, add_comm]
+  refine (AddLECancellable.eq_tsub_iff_add_eq_of_le (α := ℝ≥0∞) (sorry) (by simpa)).1 ?_
+  rw [inv_eq_iff_eq_inv]
+  obtain rfl | hp₁ := hp.eq_or_lt
+  · simp
+  obtain rfl | hp := eq_or_ne p ∞
+  · sorry
+  calc
+    1 + (p - 1)⁻¹ = (p - 1 + 1) / (p - 1) := by
+      rw [ENNReal.add_div, ENNReal.div_self ((tsub_pos_of_lt hp₁).ne') (sub_ne_top hp), one_div]
+    _ = (1 - p⁻¹)⁻¹ := by
+      rw [tsub_add_cancel_of_le, ← inv_eq_iff_eq_inv, div_eq_mul_inv, ENNReal.mul_inv, inv_inv,
+        ENNReal.mul_sub, ENNReal.inv_mul_cancel, mul_one] <;> simp [*]
 
 section
 include h
 
-lemma one_le : 1 ≤ p := ENNReal.inv_le_one.1 $ by
+@[symm]
+protected lemma symm : q.IsConjExponent p where
+  inv_add_inv_conj := by simpa [add_comm] using h.inv_add_inv_conj
+
+lemma one_le : 1 ≤ p := ENNReal.inv_le_one.1 <| by
   rw [← add_zero p⁻¹, ← h.inv_add_inv_conj]; gcongr; positivity
 
 lemma pos : 0 < p := zero_lt_one.trans_le h.one_le
@@ -43,17 +66,29 @@ lemma ne_zero : p ≠ 0 := h.pos.ne'
 lemma one_sub_inv : 1 - p⁻¹ = q⁻¹ :=
   ENNReal.sub_eq_of_eq_add_rev' one_ne_top h.inv_add_inv_conj.symm
 
-lemma conj_eq : q = 1 + (p - 1)⁻¹ := sorry
-
-lemma conjExponent_eq : conjExponent p = q := h.conj_eq.symm
-
-lemma mul_eq_add : p * q = p + q := sorry
-
-@[symm]
-protected lemma symm : q.IsConjExponent p where
-  inv_add_inv_conj := by simpa [add_comm] using h.inv_add_inv_conj
-
-lemma div_conj_eq_sub_one : p / q = p - 1 := sorry
+lemma conjExponent_eq : conjExponent p = q := by
+  have hp : 1 ≤ p := h.one_le
+  have : p⁻¹ ≠ ∞ := by simpa using h.ne_zero
+  simpa [ENNReal.add_right_inj, *] using
+    (IsConjExponent.conjExponent hp).inv_add_inv_conj.trans h.inv_add_inv_conj.symm
+
+lemma conj_eq : q = 1 + (p - 1)⁻¹ := h.conjExponent_eq.symm
+
+lemma mul_eq_add : p * q = p + q := by
+  obtain rfl | hp := eq_or_ne p ∞
+  · simp [h.symm.ne_zero]
+  obtain rfl | hq := eq_or_ne q ∞
+  · simp [h.ne_zero]
+  rw [← mul_one (_ * _), ← h.inv_add_inv_conj, mul_add, mul_right_comm,
+    ENNReal.mul_inv_cancel h.ne_zero hp, one_mul, mul_assoc,
+    ENNReal.mul_inv_cancel h.symm.ne_zero hq, mul_one, add_comm]
+
+lemma div_conj_eq_sub_one : p / q = p - 1 := by
+  obtain rfl | hq := eq_or_ne q ∞
+  · sorry
+  refine ENNReal.eq_sub_of_add_eq one_ne_top ?_
+  rw [← ENNReal.div_self h.symm.ne_zero hq, ← ENNReal.add_div, ← h.mul_eq_add, mul_div_assoc,
+    ENNReal.div_self h.symm.ne_zero hq, mul_one]
 
 end
 
@@ -65,15 +100,12 @@ lemma inv_one_sub_inv (ha : a ≤ 1) : a⁻¹.IsConjExponent (1 - a)⁻¹ :=
 
 lemma one_sub_inv_inv (ha : a ≤ 1) : (1 - a)⁻¹.IsConjExponent a⁻¹ := (inv_one_sub_inv ha).symm
 
-lemma top_one : IsConjExponent ∞ 1 := sorry
-lemma one_top : IsConjExponent 1 ∞ := sorry
+lemma top_one : IsConjExponent ∞ 1 := ⟨by simp⟩
+lemma one_top : IsConjExponent 1 ∞ := ⟨by simp⟩
 
 end IsConjExponent
 
-lemma isConjExponent_iff_eq_conjExponent (h : 1 < p) : p.IsConjExponent q ↔ q = 1 + (p - 1)⁻¹ :=
-  sorry
-
-protected lemma IsConjExponent.conjExponent (h : 1 < p) : p.IsConjExponent (conjExponent p) :=
-  (isConjExponent_iff_eq_conjExponent h).2 rfl
+lemma isConjExponent_iff_eq_conjExponent (hp : 1 ≤ p) : p.IsConjExponent q ↔ q = 1 + (p - 1)⁻¹ :=
+  ⟨fun h ↦ h.conj_eq, by rintro rfl; exact .conjExponent hp⟩
 
 end ENNReal
diff --git a/LeanAPAP/Physics/AlmostPeriodicity.lean b/LeanAPAP/Physics/AlmostPeriodicity.lean
index 2e37f02717..2e0e59fa84 100644
--- a/LeanAPAP/Physics/AlmostPeriodicity.lean
+++ b/LeanAPAP/Physics/AlmostPeriodicity.lean
@@ -3,7 +3,6 @@ import Mathlib.Combinatorics.Additive.DoublingConst
 import Mathlib.Data.Complex.ExponentialBounds
 import LeanAPAP.Prereqs.Convolution.Discrete.Basic
 import LeanAPAP.Prereqs.Convolution.Norm
-import LeanAPAP.Prereqs.Expect.Complex
 import LeanAPAP.Prereqs.Inner.Hoelder.Discrete
 import LeanAPAP.Prereqs.MarcinkiewiczZygmund
 
diff --git a/LeanAPAP/Physics/DRC.lean b/LeanAPAP/Physics/DRC.lean
index 8abc6a92d3..cd7cd22dd9 100644
--- a/LeanAPAP/Physics/DRC.lean
+++ b/LeanAPAP/Physics/DRC.lean
@@ -87,7 +87,7 @@ lemma drc (hp₂ : 2 ≤ p) (f : G → ℝ≥0) (hf : ∃ x, x ∈ B₁ - B₂ 
   set M : ℝ :=
     2 ⁻¹ * ‖𝟭_[ℝ] A ○ 𝟭 A‖_[p, μ B₁ ○ μ B₂] ^ p * (sqrt B₁.card * sqrt B₂.card) / A.card ^ p
       with hM_def
-  have hM : 0 < M := by rw [hM_def]; sorry -- positivity
+  have hM : 0 < M := by rw [hM_def]; positivity
   replace hf : 0 < ∑ x, (μ_[ℝ] B₁ ○ μ B₂) x * (𝟭 A ○ 𝟭 A) x ^ p * f x := by
     have : 0 ≤ μ_[ℝ] B₁ ○ μ B₂ * (𝟭 A ○ 𝟭 A) ^ p * (↑) ∘ f :=
       mul_nonneg (mul_nonneg (dconv_nonneg mu_nonneg mu_nonneg) $ pow_nonneg
diff --git a/LeanAPAP/Prereqs/Balance/Complex.lean b/LeanAPAP/Prereqs/Balance/Complex.lean
index 18bab88079..e811bde46c 100644
--- a/LeanAPAP/Prereqs/Balance/Complex.lean
+++ b/LeanAPAP/Prereqs/Balance/Complex.lean
@@ -1,8 +1,9 @@
-import LeanAPAP.Prereqs.Balance.Defs
-import LeanAPAP.Prereqs.Expect.Complex
+import Mathlib.Algebra.BigOperators.Balance
+import Mathlib.Analysis.RCLike.Basic
+import Mathlib.Data.Complex.BigOperators
 
-open Finset
-open scoped BigOperators NNReal
+open Fintype
+open scoped NNReal
 
 namespace Complex
 variable {ι : Type*}
@@ -28,4 +29,3 @@ lemma coe_balance : (↑(balance f a) : 𝕜) = balance ((↑) ∘ f) a := map_b
   simp [balance]
 
 end RCLike
-
diff --git a/LeanAPAP/Prereqs/Balance/Defs.lean b/LeanAPAP/Prereqs/Balance/Defs.lean
deleted file mode 100644
index e08cb14e38..0000000000
--- a/LeanAPAP/Prereqs/Balance/Defs.lean
+++ /dev/null
@@ -1,46 +0,0 @@
-import Mathlib.Algebra.BigOperators.Expect
-
-/-!
-# Balancing a function
--/
-
-open Function
-open Fintype (card)
-open scoped BigOperators Pointwise NNRat
-
-variable {ι α β : Type*}
-
-namespace Finset
-
-section AddCommGroup
-variable [AddCommGroup α] [Module ℚ≥0 α] [Field β] [Module ℚ≥0 β] {s : Finset ι}
-
-variable [Fintype ι]
-
-def balance (f : ι → α) : ι → α := f - Function.const _ (𝔼 y, f y)
-
-lemma balance_apply (f : ι → α) (x : ι) : balance f x = f x - 𝔼 y, f y := rfl
-
-@[simp] lemma balance_zero : balance (0 : ι → α) = 0 := by simp [balance]
-
-@[simp] lemma balance_add (f g : ι → α) : balance (f + g) = balance f + balance g := by
-  simp only [balance, expect_add_distrib, ← const_add, add_sub_add_comm, Pi.add_apply]
-
-@[simp] lemma balance_sub (f g : ι → α) : balance (f - g) = balance f - balance g := by
-  simp only [balance, expect_sub_distrib, const_sub, sub_sub_sub_comm, Pi.sub_apply]
-
-@[simp] lemma balance_neg (f : ι → α) : balance (-f) = -balance f := by
-  simp only [balance, expect_neg_distrib, const_neg, neg_sub', Pi.neg_apply]
-
-@[simp] lemma sum_balance (f : ι → α) : ∑ x, balance f x = 0 := by
-  cases isEmpty_or_nonempty ι <;> simp [balance_apply]
-
-@[simp] lemma expect_balance (f : ι → α) : 𝔼 x, balance f x = 0 := by simp [expect]
-
-@[simp] lemma balance_idem (f : ι → α) : balance (balance f) = balance f := by
-  cases isEmpty_or_nonempty ι <;> ext x <;> simp [balance, expect_sub_distrib]
-
-@[simp] lemma map_balance {F : Type*} [FunLike F α β] [LinearMapClass F ℚ≥0 α β] (g : F) (f : ι → α)
-    (a : ι) : g (balance f a) = balance (g ∘ f) a := by simp [balance, map_expect]
-
-end AddCommGroup
diff --git a/LeanAPAP/Prereqs/Bohr/Basic.lean b/LeanAPAP/Prereqs/Bohr/Basic.lean
index 08b05818d0..5844c931d8 100644
--- a/LeanAPAP/Prereqs/Bohr/Basic.lean
+++ b/LeanAPAP/Prereqs/Bohr/Basic.lean
@@ -116,9 +116,11 @@ lemma mem_chordSet_iff_norm_width : x ∈ B.chordSet ↔ ∀ ⦃ψ⦄, ψ ∈ B.
 @[simp, norm_cast] lemma coeSort_coe (B : BohrSet G) : ↥(B : Set G) = B := rfl
 
 @[simp] lemma zero_mem : 0 ∈ B.chordSet := by simp [mem_chordSet_iff_nnnorm_width]
+
+-- TODO: This lemma needs `Finite G` because we are using `AddChar G ℂ` rather than `AddChar G ℂˣ`
+-- as the dual group.
 @[simp] lemma neg_mem [Finite G] : -x ∈ B.chordSet ↔ x ∈ B.chordSet :=
-  forall₂_congr fun ψ hψ ↦ by sorry
-    -- rw [Iff.comm, ← RCLike.nnnorm_conj, map_sub, map_one, map_neg_eq_conj]
+  forall₂_congr fun ψ hψ ↦ by rw [Iff.comm, ← RCLike.nnnorm_conj, map_sub, map_one, map_neg_eq_conj]
 
 /-! ### Lattice structure -/
 
diff --git a/LeanAPAP/Prereqs/Convolution/Compact.lean b/LeanAPAP/Prereqs/Convolution/Compact.lean
index a2f6bcd7f0..f1bc5b3273 100644
--- a/LeanAPAP/Prereqs/Convolution/Compact.lean
+++ b/LeanAPAP/Prereqs/Convolution/Compact.lean
@@ -1,6 +1,5 @@
-import LeanAPAP.Prereqs.Balance.Defs
+import Mathlib.Algebra.BigOperators.Balance
 import LeanAPAP.Prereqs.Convolution.Discrete.Defs
-import LeanAPAP.Prereqs.Expect.Complex
 import LeanAPAP.Prereqs.Function.Indicator.Defs
 
 /-!
@@ -393,11 +392,11 @@ end Field
 namespace RCLike
 variable {𝕜 : Type} [RCLike 𝕜] (f g : G → ℝ) (a : G)
 
-@[simp, norm_cast]
-lemma coe_cconv : (f ∗ₙ g) a = ((↑) ∘ f ∗ₙ (↑) ∘ g : G → 𝕜) a := map_cconv (algebraMap ℝ 𝕜) _ _ _
+@[simp, norm_cast] lemma coe_cconv : (f ∗ₙ g) a = ((↑) ∘ f ∗ₙ (↑) ∘ g : G → 𝕜) a :=
+  map_cconv (algebraMap ℝ 𝕜) ..
 
-@[simp, norm_cast]
-lemma coe_cdconv : (f ○ₙ g) a = ((↑) ∘ f ○ₙ (↑) ∘ g : G → 𝕜) a := by simp [cdconv_apply, coe_expect]
+@[simp, norm_cast] lemma coe_cdconv : (f ○ₙ g) a = ((↑) ∘ f ○ₙ (↑) ∘ g : G → 𝕜) a := by
+  simp [cdconv_apply, ofReal_expect]
 
 @[simp]
 lemma coe_comp_cconv : ofReal ∘ (f ∗ₙ g) = ((↑) ∘ f ∗ₙ (↑) ∘ g : G → 𝕜) := funext $ coe_cconv _ _
diff --git a/LeanAPAP/Prereqs/Convolution/Discrete/Basic.lean b/LeanAPAP/Prereqs/Convolution/Discrete/Basic.lean
index f568f958a2..22245f4799 100644
--- a/LeanAPAP/Prereqs/Convolution/Discrete/Basic.lean
+++ b/LeanAPAP/Prereqs/Convolution/Discrete/Basic.lean
@@ -1,6 +1,6 @@
+import Mathlib.Algebra.BigOperators.Balance
 import Mathlib.Algebra.Module.Pi
 import Mathlib.Analysis.Complex.Basic
-import LeanAPAP.Prereqs.Balance.Defs
 import LeanAPAP.Prereqs.Convolution.Discrete.Defs
 import LeanAPAP.Prereqs.Function.Indicator.Basic
 
diff --git a/LeanAPAP/Prereqs/Energy.lean b/LeanAPAP/Prereqs/Energy.lean
index 7c87e5c29e..38ed01cada 100644
--- a/LeanAPAP/Prereqs/Energy.lean
+++ b/LeanAPAP/Prereqs/Energy.lean
@@ -1,6 +1,5 @@
 import LeanAPAP.Prereqs.AddChar.Basic
 import LeanAPAP.Prereqs.Convolution.Discrete.Basic
-import LeanAPAP.Prereqs.Expect.Complex
 import LeanAPAP.Prereqs.FourierTransform.Discrete
 import LeanAPAP.Prereqs.Function.Indicator.Complex
 
diff --git a/LeanAPAP/Prereqs/Expect/Complex.lean b/LeanAPAP/Prereqs/Expect/Complex.lean
deleted file mode 100644
index 94805cf3cd..0000000000
--- a/LeanAPAP/Prereqs/Expect/Complex.lean
+++ /dev/null
@@ -1,43 +0,0 @@
-import Mathlib.Algebra.Order.BigOperators.Expect
-import Mathlib.Analysis.RCLike.Basic
-import Mathlib.Data.Complex.Basic
-
-open Finset
-open scoped BigOperators NNReal
-
-section
-variable {ι K E : Type*} [RCLike K] [NormedField E] [CharZero E] [NormedSpace K E]
-
-include K in
-@[bound]
-lemma norm_expect_le {s : Finset ι} {f : ι → E} : ‖𝔼 i ∈ s, f i‖ ≤ 𝔼 i ∈ s, ‖f i‖ :=
-  le_expect_of_subadditive norm_zero norm_add_le (fun _ _ ↦ by rw [RCLike.norm_nnqsmul K])
-
-end
-
-namespace NNReal
-variable {ι : Type*}
-
-@[simp, norm_cast]
-lemma coe_expect (s : Finset ι) (f : ι → ℝ≥0) : 𝔼 i ∈ s, f i = 𝔼 i ∈ s, (f i : ℝ) :=
-  map_expect toRealHom ..
-
-end NNReal
-
-namespace Complex
-variable {ι : Type*}
-
-@[simp, norm_cast]
-lemma ofReal_expect (s : Finset ι) (f : ι → ℝ) : 𝔼 i ∈ s, f i = 𝔼 i ∈ s, (f i : ℂ) :=
-  map_expect ofReal ..
-
-end Complex
-
-namespace RCLike
-variable {ι 𝕜 : Type*} [RCLike 𝕜]
-
-@[simp, norm_cast]
-lemma coe_expect (s : Finset ι) (f : ι → ℝ) : 𝔼 i ∈ s, f i = 𝔼 i ∈ s, (f i : 𝕜) :=
-  map_expect (algebraMap ..) ..
-
-end RCLike
diff --git a/LeanAPAP/Prereqs/FourierTransform/Compact.lean b/LeanAPAP/Prereqs/FourierTransform/Compact.lean
index f306e59cfd..1c371f2bdd 100644
--- a/LeanAPAP/Prereqs/FourierTransform/Compact.lean
+++ b/LeanAPAP/Prereqs/FourierTransform/Compact.lean
@@ -11,8 +11,7 @@ Parseval-Plancherel identity and Fourier inversion formula for it.
 
 noncomputable section
 
-open AddChar Finset Function MeasureTheory RCLike
-open Fintype (card)
+open AddChar Finset Fintype Function MeasureTheory RCLike
 open scoped ComplexConjugate ComplexOrder
 
 variable {α γ : Type*} [AddCommGroup α] [Fintype α] {f : α → ℂ} {ψ : AddChar α ℂ} {n : ℕ}
diff --git a/LeanAPAP/Prereqs/FourierTransform/Discrete.lean b/LeanAPAP/Prereqs/FourierTransform/Discrete.lean
index 1a7984d5ec..f530b64f15 100644
--- a/LeanAPAP/Prereqs/FourierTransform/Discrete.lean
+++ b/LeanAPAP/Prereqs/FourierTransform/Discrete.lean
@@ -1,6 +1,6 @@
+import Mathlib.Algebra.BigOperators.Balance
 import LeanAPAP.Prereqs.AddChar.MeasurableSpace
 import LeanAPAP.Prereqs.AddChar.PontryaginDuality
-import LeanAPAP.Prereqs.Balance.Defs
 import LeanAPAP.Prereqs.Convolution.Discrete.Defs
 import LeanAPAP.Prereqs.Function.Indicator.Defs
 import LeanAPAP.Prereqs.Inner.Hoelder.Compact
@@ -12,12 +12,9 @@ This file defines the discrete Fourier transform and shows the Parseval-Plancher
 Fourier inversion formula for it.
 -/
 
-open Fintype (card)
-open AddChar Finset Function MeasureTheory RCLike
+open AddChar Finset Fintype Function MeasureTheory RCLike
 open scoped BigOperators ComplexConjugate ComplexOrder
 
-local notation a " /ℚ " q => (q : ℚ≥0)⁻¹ • a
-
 variable {α γ : Type*} [AddCommGroup α] [Fintype α] {f : α → ℂ} {ψ : AddChar α ℂ} {n : ℕ}
 
 /-- The discrete Fourier transform. -/
diff --git a/LeanAPAP/Prereqs/LpNorm/Compact.lean b/LeanAPAP/Prereqs/LpNorm/Compact.lean
index 684664b845..42a2190810 100644
--- a/LeanAPAP/Prereqs/LpNorm/Compact.lean
+++ b/LeanAPAP/Prereqs/LpNorm/Compact.lean
@@ -4,7 +4,6 @@ import Mathlib.Data.Finset.Density
 import Mathlib.Data.Fintype.Order
 import Mathlib.Probability.ConditionalProbability
 import LeanAPAP.Mathlib.MeasureTheory.Function.EssSup
-import LeanAPAP.Prereqs.Expect.Complex
 import LeanAPAP.Prereqs.Function.Translate
 import LeanAPAP.Prereqs.Function.Indicator.Defs
 import LeanAPAP.Prereqs.NNLpNorm
diff --git a/LeanAPAP/Prereqs/LpNorm/Discrete/Defs.lean b/LeanAPAP/Prereqs/LpNorm/Discrete/Defs.lean
index 15bba63610..ebfae0c3ab 100644
--- a/LeanAPAP/Prereqs/LpNorm/Discrete/Defs.lean
+++ b/LeanAPAP/Prereqs/LpNorm/Discrete/Defs.lean
@@ -271,9 +271,7 @@ example {p : ℝ≥0∞} (hp : p ≠ 0) {f : α → ℝ} (hf : 0 < f) : 0 < ‖f
 end NormedAddCommGroup
 
 section Complex
-variable [Fintype α] [DiscreteMeasurableSpace α] {w : α → ℝ≥0} {f : α → ℂ}
-
-open scoped ComplexOrder
+variable [Fintype α] [DiscreteMeasurableSpace α] {f : α → ℂ}
 
 example {p : ℝ≥0∞} (hp : p ≠ 0) (hf : f ≠ 0) : 0 < ‖f‖_[p] := by positivity
 example {p : ℝ≥0∞} (hp : p ≠ 0) {f : α → ℝ} (hf : 0 < f) : 0 < ‖f‖_[p] := by positivity
diff --git a/LeanAPAP/Prereqs/LpNorm/Weighted.lean b/LeanAPAP/Prereqs/LpNorm/Weighted.lean
index cf87533a4f..ab6de63804 100644
--- a/LeanAPAP/Prereqs/LpNorm/Weighted.lean
+++ b/LeanAPAP/Prereqs/LpNorm/Weighted.lean
@@ -49,12 +49,6 @@ variable {K : Type*} [RCLike K]
 
 @[simp] lemma wLpNorm_conj (f : α → K) : ‖conj f‖_[p, w] = ‖f‖_[p, w] := by simp [← wLpNorm_norm]
 
-variable [AddGroup α]
-
-@[simp] lemma wLpNorm_conjneg (f : α → K) : ‖conjneg f‖_[p, w] = ‖f‖_[p, w] := by
-  simp [← wLpNorm_norm]
-  sorry
-
 end RCLike
 
 variable [Fintype α]
@@ -108,7 +102,7 @@ lemma wL1Norm_eq_sum_nnnorm (w : α → ℝ≥0) (f : α → E) : ‖f‖_[1, w]
 lemma wL1Norm_eq_sum_norm (w : α → ℝ≥0) (f : α → E) : ‖f‖_[1, w] = ∑ i, w i • ‖f i‖ := by
   simp [wLpNorm_eq_sum_norm]
 
-@[gcongr] 
+@[gcongr]
 lemma wLpNorm_mono_right (hpq : p ≤ q) (w : α → ℝ≥0) (f : α → E) : ‖f‖_[p, w] ≤ ‖f‖_[q, w] :=
   sorry
 
diff --git a/LeanAPAP/Prereqs/MarcinkiewiczZygmund.lean b/LeanAPAP/Prereqs/MarcinkiewiczZygmund.lean
index 8f80578f18..96d1c94d22 100644
--- a/LeanAPAP/Prereqs/MarcinkiewiczZygmund.lean
+++ b/LeanAPAP/Prereqs/MarcinkiewiczZygmund.lean
@@ -3,6 +3,7 @@ Copyright (c) 2023 Yaël Dillies, Bhavik Mehta. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yaël Dillies, Bhavik Mehta
 -/
+import Mathlib.Algebra.Order.Chebyshev
 import Mathlib.Analysis.MeanInequalitiesPow
 import Mathlib.Data.Nat.Choose.Multinomial
 import Mathlib.Tactic.Positivity.Finset
@@ -39,7 +40,7 @@ private lemma step_one (hA : A.Nonempty) (f : ι → ℝ) (a : Fin n → ι)
     _ = (∑ b in B, |∑ i, (f (a i) - f (b i))|) ^ (m + 1) / B.card ^ m / B.card := by
       rw [div_div, ← _root_.pow_succ]
     _ ≤ (∑ b in B, |∑ i, (f (a i) - f (b i))| ^ (m + 1)) / B.card := by
-      gcongr; exact pow_sum_div_card_le_sum_pow _ _ fun _ _ ↦ abs_nonneg _
+      gcongr; exact pow_sum_div_card_le_sum_pow (fun _ _ ↦ abs_nonneg _) _
     _ = _ := by simp [B]
 
 private lemma step_one' (hA : A.Nonempty) (f : ι → ℝ) (hf : ∀ i, ∑ a in A ^^ n, f (a i) = 0) (m : ℕ)
@@ -227,7 +228,7 @@ theorem marcinkiewicz_zygmund (hm : m ≠ 0) (f : ι → ℝ) (hf : ∀ i, ∑ a
       simp_rw [mul_assoc, mul_sum]; rfl
   gcongr with a
   rw [← div_le_iff₀']
-  have := Real.pow_sum_div_card_le_sum_pow (f := fun i ↦ f (a i) ^ 2) univ m fun i _ ↦ ?_
+  have := pow_sum_div_card_le_sum_pow (f := fun i ↦ f (a i) ^ 2) (s := univ) (fun i _ ↦ ?_) m
   simpa only [Finset.card_fin, pow_mul] using this
   all_goals { positivity }
 
diff --git a/LeanAPAP/Prereqs/Randomisation.lean b/LeanAPAP/Prereqs/Randomisation.lean
index ead086fdb0..a5a24e469d 100644
--- a/LeanAPAP/Prereqs/Randomisation.lean
+++ b/LeanAPAP/Prereqs/Randomisation.lean
@@ -1,6 +1,5 @@
 import Mathlib.Combinatorics.Additive.Dissociation
 import LeanAPAP.Prereqs.AddChar.Basic
-import LeanAPAP.Prereqs.Expect.Complex
 
 /-!
 # Randomisation
diff --git a/LeanAPAP/Prereqs/Rudin.lean b/LeanAPAP/Prereqs/Rudin.lean
index 8eea7ca725..f21a8e6a60 100644
--- a/LeanAPAP/Prereqs/Rudin.lean
+++ b/LeanAPAP/Prereqs/Rudin.lean
@@ -1,5 +1,6 @@
 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
 
@@ -68,8 +69,7 @@ private lemma rudin_ineq_aux (hp : 2 ≤ p) (f : α → ℂ) (hf : AddDissociate
     · simp
     specialize H hp ((sqrt p / ‖f‖ₙ_[2]) • f) ?_
     · rwa [cft_smul, support_const_smul_of_ne_zero]
-      sorry
-      -- positivity
+      positivity
     have : 0 < ‖f‖ₙ_[2] := (cLpNorm_pos two_ne_zero).2 hf
     have : 0 < |√ p| := by positivity
     simp_rw [Function.comp_def, Pi.smul_apply, Complex.smul_re, ← Pi.smul_def] at H
diff --git a/lake-manifest.json b/lake-manifest.json
index fb1d2a96d1..ff7312a621 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "bf12ff6041cbab6eba6b54d9467baed807bb2bfd",
+   "rev": "4756e0fc48acce0cc808df0ad149de5973240df6",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -25,7 +25,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "50aaaf78b7db5bd635c19c660d59ed31b9bc9b5a",
+   "rev": "ff420521a0c098891f4f44ecda9dd7ff57b50bad",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -55,7 +55,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "fb7841a6f4fb389ec0e47dd4677844d49906af3c",
+   "rev": "e285a7ade149c551c17a4b24f127e1ef782e4bb1",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -65,7 +65,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "2ba60fa2c384a94735454db11a2d523612eaabff",
+   "rev": "781beceb959c68b36d3d96205b3531e341879d2c",
    "name": "LeanSearchClient",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -75,7 +75,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "eed3300c27c9f168d53e13bb198a92a147b671d0",
+   "rev": "e4a8f5b0444a8dcd89f1ac4b7602f894bb177516",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,
@@ -95,7 +95,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "7afce91e4fcee25c1ed06dca8d71b82bed396776",
+   "rev": "6d2e06515f1ed1f74208d5a1da3a9cc26c60a7a0",
    "name": "UnicodeBasic",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -105,7 +105,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "0a294fe9bf23b396c5cc955054c50b9b652ec5ad",
+   "rev": "85e1e7143dd4cfa2b551826c27867bada60858e8",
    "name": "BibtexQuery",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -115,7 +115,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "1b0072fea2aa6a0ef8ef8b506ec5223b184cb4d0",
+   "rev": "5119580cd7510a440d54f67834c9024cc03a3e32",
    "name": "«doc-gen4»",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
diff --git a/lean-toolchain b/lean-toolchain
index 98556ba065..89985206ac 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.12.0-rc1
+leanprover/lean4:v4.12.0