Bump mathlib

LeanAPAP.lean

@@ -1,8 +1,7 @@
 import LeanAPAP.Extras.BSG
 import LeanAPAP.FiniteField
 import LeanAPAP.Integer
-import LeanAPAP.Mathlib.MeasureTheory.Function.LpSpace
-import LeanAPAP.Mathlib.MeasureTheory.Integral.Bochner
+import LeanAPAP.Mathlib.Analysis.Normed.Group.Basic
 import LeanAPAP.Physics.AlmostPeriodicity
 import LeanAPAP.Physics.DRC
 import LeanAPAP.Physics.Unbalancing

LeanAPAP/FiniteField.lean

@@ -461,8 +461,8 @@ theorem ff (hq₃ : 3 ≤ q) (hq : q.Prime) (hA₀ : A.Nonempty) (hA : ThreeAPFr
       (B.dens < (65 / 64 : ℝ) ^ i * α →
         2⁻¹ ≤ card V * ⟪μ_[ℝ] B ∗ μ B, μ (B.image (2 • ·))⟫_[ℝ]) := by
     induction' i with i ih hi
-    · exact ⟨G, inferInstance, inferInstance, inferInstance, inferInstance, A, by simp, hA,
-        by simp, by simp [α, nnratCast_dens, Fintype.card_subtype, subset_iff]⟩
+    · exact ⟨G, inferInstance, inferInstance, inferInstance, inferInstance, A, by simp [n], hA,
+        by simp [α], by simp [α, nnratCast_dens, Fintype.card_subtype, subset_iff]⟩
     obtain ⟨V, _, _, _, _, B, hV, hB, hαβ, hBV⟩ := ih
     obtain hB' | hB' := le_or_lt 2⁻¹ (card V * ⟪μ_[ℝ] B ∗ μ B, μ (B.image (2 • ·))⟫_[ℝ])
     · exact ⟨V, inferInstance, inferInstance, inferInstance, inferInstance, B,
@@ -486,7 +486,7 @@ theorem ff (hq₃ : 3 ≤ q) (hq : q.Prime) (hA₀ : A.Nonempty) (hA : ThreeAPFr
         _ ≤ ‖(𝟭_[ℝ] B ∗ μ (V' : Set V).toFinset) x‖ := hx
         _ = B'.dens := ?_
       rw [mu, conv_smul, Pi.smul_apply, indicate_conv_indicate_eq_card_vadd_inter_neg,
-        norm_of_nonneg (by positivity), nnratCast_dens, card_preimage, smul_eq_mul, inv_mul_eq_div]
+        Real.norm_of_nonneg (by positivity), nnratCast_dens, card_preimage, smul_eq_mul, inv_mul_eq_div]
       congr 2
       · congr 1 with x
         simp

LeanAPAP/Mathlib/Analysis/Normed/Group/Basic.lean

@@ -0,0 +1,10 @@
+import Mathlib.Analysis.Normed.Group.Basic
+
+section
+variable {E : Type*} [NNNorm E]
+
+@[simp] lemma toNNReal_enorm (x : E) : ‖x‖ₑ.toNNReal = ‖x‖₊ := rfl
+
+end
+
+attribute [simp] toReal_enorm toReal_enorm'

LeanAPAP/Physics/AlmostPeriodicity.lean

@@ -138,7 +138,7 @@ lemma lemma28_part_one (hm : 1 ≤ m) (x : G) :
     simp only [boole_mul, indicate_apply]
     rw [← sum_filter, filter_mem_eq_inter, univ_inter, sub_self, smul_zero]
   congr with a : 1
-  simp only [sum_sub_distrib, Pi.smul_apply, sum_const, card_fin]
+  simp only [sum_sub_distrib, Pi.smul_apply, sum_const, card_fin, f']
 
 lemma big_shifts_step2 (L : Finset (Fin k → G)) (hk : k ≠ 0) :
     (∑ x ∈ L + S.piDiag (Fin k), ∑ l ∈ L, ∑ s ∈ S.piDiag (Fin k), ite (l + s = x) (1 : ℝ) 0) ^ 2

LeanAPAP/Physics/DRC.lean

@@ -128,7 +128,7 @@ lemma drc (hp₂ : 2 ≤ p) (f : G → ℝ≥0) (hf : ∃ x, x ∈ B₁ - B₂ 
     refine ⟨(lt_of_mul_lt_mul_left (hs.trans_eq' ?_) $ hg s).le, this.trans $ mul_le_of_le_one_right
       ?_ $ div_le_one_of_le₀ ?_ ?_, this.trans $ mul_le_of_le_one_left ?_ $ div_le_one_of_le₀ ?_ ?_⟩
     · simp_rw [A₁, A₂, g, ← card_smul_mu, smul_dconv, dconv_smul, ← Nat.cast_smul_eq_nsmul ℝ,
-        wInner_smul_left, smul_eq_mul, star_trivial, mul_assoc]
+        wInner_smul_left, smul_eq_mul, star_trivial, mul_assoc, A₁, A₂]
     any_goals positivity
     all_goals exact Nat.cast_le.2 $ card_mono inter_subset_left
   rw [← sum_mul, lemma_0, nsmul_eq_mul, Nat.cast_mul, ← sum_mul, mul_right_comm, ← hgB,
@@ -156,7 +156,7 @@ lemma drc (hp₂ : 2 ≤ p) (f : G → ℝ≥0) (hf : ∃ x, x ∈ B₁ - B₂ 
         := sum_lt_sum_of_nonempty ⟨s, mem_filter.2 ⟨mem_univ _, hs.symm⟩⟩ ?_
     _ ≤ ∑ s, M * sqrt (g s) := sum_le_univ_sum_of_nonneg fun s ↦ by positivity
     _ = M * (∑ s, sqrt #(A₁ s) * sqrt #(A₂ s))
-        := by simp_rw [mul_sum, sqrt_mul $ Nat.cast_nonneg _]
+        := by simp_rw [mul_sum, g, sqrt_mul $ Nat.cast_nonneg _]
     _ ≤ M * (sqrt (∑ s, #(A₁ s)) * sqrt (∑ s, #(A₂ s))) := by
       gcongr; exact sum_sqrt_mul_sqrt_le _ fun i ↦ by positivity fun i ↦ by positivity
     _ = _ := ?_
@@ -172,7 +172,7 @@ lemma drc (hp₂ : 2 ≤ p) (f : G → ℝ≥0) (hf : ∃ x, x ∈ B₁ - B₂ 
 lemma sifting (B₁ B₂ : Finset G) (hε : 0 < ε) (hε₁ : ε ≤ 1) (hδ : 0 < δ) (hp : Even p)
     (hp₂ : 2 ≤ p) (hpε : ε⁻¹ * log (2 / δ) ≤ p) (hB : (B₁ ∩ B₂).Nonempty) (hA : A.Nonempty)
     (hf : ∃ x, x ∈ B₁ - B₂ ∧ x ∈ A - A ∧ x ∉ s p ε B₁ B₂ A) :
-    ∃ A₁, A₁ ⊆ B₁ ∧ ∃ A₂, A₂ ⊆ B₂ ∧ 1 - δ ≤ ∑ x in s p ε B₁ B₂ A, (μ A₁ ○ μ A₂) x ∧
+    ∃ A₁, A₁ ⊆ B₁ ∧ ∃ A₂, A₂ ⊆ B₂ ∧ 1 - δ ≤ ∑ x ∈ s p ε B₁ B₂ A, (μ A₁ ○ μ A₂) x ∧
         (4 : ℝ)⁻¹ * ‖𝟭_[ℝ] A ○ 𝟭 A‖_[p, μ B₁ ○ μ B₂] ^ (2 * p) / #A ^ (2 * p) ≤
             #A₁ / #B₁ ∧
           (4 : ℝ)⁻¹ * ‖𝟭_[ℝ] A ○ 𝟭 A‖_[p, μ B₁ ○ μ B₂] ^ (2 * p) / #A ^ (2 * p) ≤
@@ -196,7 +196,7 @@ lemma sifting (B₁ B₂ : Finset G) (hε : 0 < ε) (hε₁ : ε ≤ 1) (hδ : 0
   clear hcard₁ hcard₂ aux
   rw [sub_le_comm]
   calc
-    _ = ∑ x in (s p ε B₁ B₂ A)ᶜ, (μ A₁ ○ μ A₂) x := ?_
+    _ = ∑ x ∈ (s p ε B₁ B₂ A)ᶜ, (μ A₁ ○ μ A₂) x := ?_
     _ = ⟪μ_[ℝ] A₁ ○ μ A₂, (↑) ∘ 𝟭_[ℝ≥0] ((s (↑p) ε B₁ B₂ A)ᶜ)⟫_[ℝ] := by
       simp [wInner_one_eq_sum, -mem_compl, -mem_s, apply_ite NNReal.toReal, indicate_apply]
     _ ≤ _ := (le_div_iff₀ $ dLpNorm_conv_pos hp₀.ne' hB hA).2 h
@@ -207,8 +207,8 @@ lemma sifting (B₁ B₂ : Finset G) (hε : 0 < ε) (hε₁ : ε ≤ 1) (hδ : 0
   simp only [apply_ite NNReal.toReal, indicate_apply, NNReal.coe_one, NNReal.coe_zero, mul_boole,
     Fintype.sum_ite_mem, mul_div_right_comm]
   calc
-    ∑ x in (s p ε B₁ B₂ A)ᶜ, (μ B₁ ○ μ B₂) x * (𝟭 A ○ 𝟭 A) x ^ p ≤
-        ∑ x in (s p ε B₁ B₂ A)ᶜ,
+    ∑ x ∈ (s p ε B₁ B₂ A)ᶜ, (μ B₁ ○ μ B₂) x * (𝟭 A ○ 𝟭 A) x ^ p ≤
+        ∑ x ∈ (s p ε B₁ B₂ A)ᶜ,
           (μ B₁ ○ μ B₂) x * ((1 - ε) * ‖𝟭_[ℝ] A ○ 𝟭 A‖_[p, μ B₁ ○ μ B₂]) ^ p := by
       gcongr with x hx
       · exact Pi.le_def.1 (dconv_nonneg (R := ℝ) mu_nonneg mu_nonneg) x
@@ -240,7 +240,7 @@ lemma sifting (B₁ B₂ : Finset G) (hε : 0 < ε) (hε₁ : ε ≤ 1) (hδ : 0
 /-- Special case of `sifting` when `B₁ = B₂ = univ`. -/
 lemma sifting_cor (hε : 0 < ε) (hε₁ : ε ≤ 1) (hδ : 0 < δ) (hp : Even p) (hp₂ : 2 ≤ p)
     (hpε : ε⁻¹ * log (2 / δ) ≤ p) (hA : A.Nonempty) :
-    ∃ A₁ A₂, 1 - δ ≤ ∑ x in s p ε univ univ A, (μ A₁ ○ μ A₂) x ∧
+    ∃ A₁ A₂, 1 - δ ≤ ∑ x ∈ s p ε univ univ A, (μ A₁ ○ μ A₂) x ∧
         (4 : ℝ)⁻¹ * A.dens ^ (2 * p) ≤ A₁.dens ∧
           (4 : ℝ)⁻¹ * A.dens ^ (2 * p) ≤ A₂.dens := by
   by_cases hf : ∃ x, x ∈ A - A ∧ (𝟭 A ○ 𝟭 A) x ≤ (1 - ε) * ‖𝟭_[ℝ] A ○ 𝟭 A‖_[p, μ univ]

LeanAPAP/Physics/Unbalancing.lean

@@ -103,7 +103,7 @@ private lemma unbalancing'' (p : ℕ) (hp : 5 ≤ p) (hp₁ : Odd p) (hε₀ : 0
   set P : Finset _ := {i | 0 ≤ f i}
   set T : Finset _ := {i | 3 / 4 * ε ≤ f i}
   have hTP : T ⊆ P := monotone_filter_right _ fun i ↦ le_trans $ by positivity
-  have : 2⁻¹ * ε ^ p ≤ ∑ i in P, ↑(ν i) * (f ^ p) i := by
+  have : 2⁻¹ * ε ^ p ≤ ∑ i ∈ P, ↑(ν i) * (f ^ p) i := by
     rw [inv_mul_le_iff₀ (zero_lt_two' ℝ), sum_filter]
     convert this using 3
     rw [Pi.posPart_apply, posPart_eq_ite]
@@ -112,10 +112,10 @@ private lemma unbalancing'' (p : ℕ) (hp : 5 ≤ p) (hp₁ : Odd p) (hε₀ : 0
     norm_cast
     rw [Nat.succ_le_iff]
     positivity
-  have : ∑ i in P \ T, ↑(ν i) * (f ^ p) i ≤ 4⁻¹ * ε ^ p := by
+  have : ∑ i ∈ P \ T, ↑(ν i) * (f ^ p) i ≤ 4⁻¹ * ε ^ p := by
     calc
-      _ ≤ ∑ i in P \ T, ↑(ν i) * (3 / 4 * ε) ^ p := sum_le_sum fun i hi ↦ ?_
-      _ = (3 / 4) ^ p * ε ^ p * ∑ i in P \ T, (ν i : ℝ) := by rw [← sum_mul, mul_comm, mul_pow]
+      _ ≤ ∑ i ∈ P \ T, ↑(ν i) * (3 / 4 * ε) ^ p := sum_le_sum fun i hi ↦ ?_
+      _ = (3 / 4) ^ p * ε ^ p * ∑ i ∈ P \ T, (ν i : ℝ) := by rw [← sum_mul, mul_comm, mul_pow]
       _ ≤ 4⁻¹ * ε ^ p * ∑ i, (ν i : ℝ) := ?_
       _ = 4⁻¹ * ε ^ p := by norm_cast; simp [hν₁]
     · simp only [mem_sdiff, mem_filter, mem_univ, true_and, not_le, P, T] at hi
@@ -137,19 +137,19 @@ private lemma unbalancing'' (p : ℕ) (hp : 5 ≤ p) (hp₁ : Odd p) (hε₀ : 0
         simp [wLpNorm_one, ENNReal.mul_ne_top, *]
       _ = 3 := by norm_num
   replace hp' := zero_lt_one.trans_le hp'
-  have : 4⁻¹ * ε ^ p ≤ sqrt (∑ i in T, ν i) * 3 ^ p := by
+  have : 4⁻¹ * ε ^ p ≤ sqrt (∑ i ∈ T, ν i) * 3 ^ p := by
     calc
       4⁻¹ * ε ^ p = 2⁻¹ * ε ^ p - 4⁻¹ * ε ^ p := by rw [← sub_mul]; norm_num
       _ ≤ _ := (sub_le_sub ‹_› ‹_›)
-      _ = ∑ i in T, ν i * (f ^ p) i := by rw [sum_sdiff_eq_sub hTP, sub_sub_cancel]
-      _ ≤ ∑ i in T, ν i * |(f ^ p) i| :=
+      _ = ∑ i ∈ T, ν i * (f ^ p) i := by rw [sum_sdiff_eq_sub hTP, sub_sub_cancel]
+      _ ≤ ∑ i ∈ T, ν i * |(f ^ p) i| :=
         (sum_le_sum fun i _ ↦ mul_le_mul_of_nonneg_left (le_abs_self _) ?_)
-      _ = ∑ i in T, sqrt (ν i) * sqrt (ν i * |(f ^ (2 * p)) i|) := by simp [← mul_assoc, pow_mul']
-      _ ≤ sqrt (∑ i in T, ν i) * sqrt (∑ i in T, ν i * |(f ^ (2 * p)) i|) :=
+      _ = ∑ i ∈ T, sqrt (ν i) * sqrt (ν i * |(f ^ (2 * p)) i|) := by simp [← mul_assoc, pow_mul']
+      _ ≤ sqrt (∑ i ∈ T, ν i) * sqrt (∑ i ∈ T, ν i * |(f ^ (2 * p)) i|) :=
         (sum_sqrt_mul_sqrt_le _ (fun i ↦ ?_) fun i ↦ ?_)
-      _ ≤ sqrt (∑ i in T, ν i) * sqrt (∑ i, ν i * |(f ^ (2 * p)) i|) := by
+      _ ≤ sqrt (∑ i ∈ T, ν i) * sqrt (∑ i, ν i * |(f ^ (2 * p)) i|) := by
         gcongr; exact T.subset_univ
-      _ = sqrt (∑ i in T, ν i) * ‖f‖_[2 * ↑p, ν] ^ p := ?_
+      _ = sqrt (∑ i ∈ T, ν i) * ‖f‖_[2 * ↑p, ν] ^ p := ?_
       _ ≤ _ := by gcongr; exact mod_cast hf₁
     any_goals positivity
     rw [wLpNorm_eq_sum_nnnorm (mod_cast hp'.ne') (by simp [ENNReal.mul_ne_top])]
@@ -159,7 +159,7 @@ private lemma unbalancing'' (p : ℕ) (hp : 5 ≤ p) (hp₁ : Odd p) (hε₀ : 0
     simp [mul_comm, this, Real.sqrt_eq_rpow]
   set p' := 24 / ε * log (3 / ε) * p
   have hp' : 0 < p' := p'_pos hp hε₀ hε₁
-  have : 1 - 8⁻¹ * ε ≤ (∑ i in T, ↑(ν i)) ^ p'⁻¹ := by
+  have : 1 - 8⁻¹ * ε ≤ (∑ i ∈ T, ↑(ν i)) ^ p'⁻¹ := by
     rw [← div_le_iff₀, mul_div_assoc, ← div_pow, le_sqrt, mul_pow, ← pow_mul'] at this
     calc
       _ ≤ exp (-(8⁻¹ * ε)) := one_sub_le_exp_neg _
@@ -184,10 +184,10 @@ private lemma unbalancing'' (p : ℕ) (hp : 5 ≤ p) (hp₁ : Odd p) (hε₀ : 0
     _ = 1 + 5 / 8 * ε - 3 / 32 * ε * 1 := by ring
     _ ≤ 1 + 5 / 8 * ε - 3 / 32 * ε * ε := (sub_le_sub_left (mul_le_mul_of_nonneg_left hε₁ ?_) _)
     _ = (1 - 8⁻¹ * ε) * (1 + 3 / 4 * ε) := by ring
-    _ ≤ (∑ i in T, ↑(ν i)) ^ p'⁻¹ * (1 + 3 / 4 * ε) := (mul_le_mul_of_nonneg_right ‹_› ?_)
-    _ = (∑ i in T, ↑(ν i) * |3 / 4 * ε + 1| ^ p') ^ p'⁻¹ := by
+    _ ≤ (∑ i ∈ T, ↑(ν i)) ^ p'⁻¹ * (1 + 3 / 4 * ε) := (mul_le_mul_of_nonneg_right ‹_› ?_)
+    _ = (∑ i ∈ T, ↑(ν i) * |3 / 4 * ε + 1| ^ p') ^ p'⁻¹ := by
       rw [← sum_mul, mul_rpow, rpow_rpow_inv, abs_of_nonneg, add_comm] <;> positivity
-    _ ≤ (∑ i in T, ↑(ν i) * |f i + 1| ^ p') ^ p'⁻¹ :=
+    _ ≤ (∑ i ∈ T, ↑(ν i) * |f i + 1| ^ p') ^ p'⁻¹ :=
         rpow_le_rpow ?_ (sum_le_sum fun i hi ↦ mul_le_mul_of_nonneg_left (rpow_le_rpow ?_
           (abs_le_abs_of_nonneg ?_ $ add_le_add_right (mem_filter.1 hi).2 _) ?_) ?_) ?_
     _ ≤ (∑ i, ↑(ν i) * |f i + 1| ^ p') ^ p'⁻¹ :=

LeanAPAP/Prereqs/Chang.lean

@@ -95,13 +95,13 @@ lemma general_hoelder (hη : 0 ≤ η) (ν : G → ℝ≥0) (hfν : ∀ x, f x 
   choose c norm_c hc using fun γ ↦ RCLike.exists_norm_eq_mul_self (dft f γ)
   have :=
     calc
-      η * ‖f‖_[1] * #Δ ≤ ∑ γ in Δ, ‖dft f γ‖ := ?_
-      _ ≤ ‖∑ x, f x * ∑ γ in Δ, c γ * conj (γ x)‖ := ?_
-      _ ≤ ∑ x, ‖f x * ∑ γ in Δ, c γ * conj (γ x)‖ := (norm_sum_le _ _)
-      _ = ∑ x, ‖f x‖ * ‖∑ γ in Δ, c γ * conj (γ x)‖ := by simp_rw [norm_mul]
+      η * ‖f‖_[1] * #Δ ≤ ∑ γ ∈ Δ, ‖dft f γ‖ := ?_
+      _ ≤ ‖∑ x, f x * ∑ γ ∈ Δ, c γ * conj (γ x)‖ := ?_
+      _ ≤ ∑ x, ‖f x * ∑ γ ∈ Δ, c γ * conj (γ x)‖ := (norm_sum_le _ _)
+      _ = ∑ x, ‖f x‖ * ‖∑ γ ∈ Δ, c γ * conj (γ x)‖ := by simp_rw [norm_mul]
       _ ≤ _ := inner_le_weight_mul_Lp_of_nonneg _ (p := m) ?_ _ _ (fun _ ↦ norm_nonneg _)
             fun _ ↦ norm_nonneg _
-      _ = ‖f‖_[1] ^ (1 - (m : ℝ)⁻¹) * (∑ x, ‖f x‖ * ‖∑ γ in Δ, c γ * conj (γ x)‖ ^ m) ^ (m⁻¹ : ℝ) :=
+      _ = ‖f‖_[1] ^ (1 - (m : ℝ)⁻¹) * (∑ x, ‖f x‖ * ‖∑ γ ∈ Δ, c γ * conj (γ x)‖ ^ m) ^ (m⁻¹ : ℝ) :=
         by simp_rw [dL1Norm_eq_sum_norm, rpow_natCast]
   rotate_left
   · rw [← nsmul_eq_mul']
@@ -127,22 +127,22 @@ lemma general_hoelder (hη : 0 ≤ η) (ν : G → ℝ≥0) (hfν : ∀ x, f x 
     calc
       (‖f‖_[1] * (η ^ m * #Δ ^ m)) ^ 2
         ≤ (∑ x, ‖f x‖ * ‖∑ γ ∈ Δ, c γ * conj (γ x)‖ ^ m) ^ 2 := by gcongr
-      _ ≤ (∑ x, ‖f x‖ * sqrt (ν x) * ‖∑ γ in Δ, c γ * conj (γ x)‖ ^ m) ^ 2 := by
+      _ ≤ (∑ x, ‖f x‖ * sqrt (ν x) * ‖∑ γ ∈ Δ, c γ * conj (γ x)‖ ^ m) ^ 2 := by
         gcongr with x; exact hfν _
-      _ = (∑ x, ‖f x‖ * (sqrt (ν x) * ‖∑ γ in Δ, c γ * conj (γ x)‖ ^ m)) ^ 2 := by
+      _ = (∑ x, ‖f x‖ * (sqrt (ν x) * ‖∑ γ ∈ Δ, c γ * conj (γ x)‖ ^ m)) ^ 2 := by
         simp_rw [mul_assoc]
-      _ ≤ (∑ x, ‖f x‖ ^ 2) * ∑ x, (sqrt (ν x) * ‖∑ γ in Δ, c γ * conj (γ x)‖ ^ m) ^ 2 :=
+      _ ≤ (∑ x, ‖f x‖ ^ 2) * ∑ x, (sqrt (ν x) * ‖∑ γ ∈ Δ, c γ * conj (γ x)‖ ^ m) ^ 2 :=
         sum_mul_sq_le_sq_mul_sq _ _ _
-      _ ≤ ‖f‖_[2] ^ 2 * ∑ x, ν x * (‖∑ γ in Δ, c γ * conj (γ x)‖ ^ 2) ^ m := by
+      _ ≤ ‖f‖_[2] ^ 2 * ∑ x, ν x * (‖∑ γ ∈ Δ, c γ * conj (γ x)‖ ^ 2) ^ m := by
         simp_rw [dL2Norm_sq_eq_sum_norm, mul_pow, sq_sqrt (NNReal.coe_nonneg _), pow_right_comm]; rfl
   rw [mul_rotate', mul_left_comm, mul_pow, mul_pow, ← pow_mul', ← pow_mul', ← div_le_iff₀',
     mul_div_assoc, mul_div_assoc] at this
   calc
     _ ≤ _ := this
     _ = ‖(_ : ℂ)‖ := Eq.symm $ RCLike.norm_of_nonneg $ sum_nonneg fun _ _ ↦ by positivity
-    _ = ‖∑ γ in Δ ^^ m, ∑ δ in Δ ^^ m,
+    _ = ‖∑ γ ∈ Δ ^^ m, ∑ δ ∈ Δ ^^ m,
           (∏ i, conj (c (γ i)) * c (δ i)) * conj (dft (fun a ↦ ν a) (∑ i, γ i - ∑ i, δ i))‖ := ?_
-    _ ≤ ∑ γ in Δ ^^ m, ∑ δ in Δ ^^ m,
+    _ ≤ ∑ γ ∈ Δ ^^ m, ∑ δ ∈ Δ ^^ m,
           ‖(∏ i, conj (c (γ i)) * c (δ i)) * conj (dft (fun a ↦ ν a) (∑ i, γ i - ∑ i, δ i))‖ :=
       (norm_sum_le _ _).trans $ sum_le_sum fun _ _ ↦ norm_sum_le _ _
     _ = _ := by simp [energy, norm_c, -Complex.norm_eq_abs, norm_prod]
@@ -170,7 +170,7 @@ lemma chang (hf : f ≠ 0) (hη : 0 < η) :
       #Δ ≤ ⌈changConst * exp 1 * ⌈𝓛 ↑(‖f‖_[1] ^ 2 / ‖f‖_[2] ^ 2 / card G)⌉₊ / η ^ 2⌉₊ ∧
       largeSpec f η ⊆ Δ.addSpan := by
   refine exists_subset_addSpan_card_le_of_forall_addDissociated fun Δ hΔη hΔ ↦ ?_
-  obtain hΔ' | hΔ' := @eq_zero_or_pos _ _ #Δ
+  obtain hΔ' | hΔ' := eq_zero_or_pos #Δ
   · simp [hΔ']
   let α := ‖f‖_[1] ^ 2 / ‖f‖_[2] ^ 2 / card G
   have : 0 < α := by positivity

LeanAPAP/Prereqs/Energy.lean

@@ -10,7 +10,7 @@ open scoped Nat
 variable {G : Type*} [AddCommGroup G] {s : Finset G}
 
 def energy (n : ℕ) (s : Finset G) (ν : G → ℂ) : ℝ :=
-  ∑ γ in piFinset fun _ : Fin n ↦ s, ∑ δ in piFinset fun _ : Fin n ↦ s, ‖ν (∑ i, γ i - ∑ i, δ i)‖
+  ∑ γ ∈ piFinset fun _ : Fin n ↦ s, ∑ δ ∈ piFinset fun _ : Fin n ↦ s, ‖ν (∑ i, γ i - ∑ i, δ i)‖
 
 @[simp]
 lemma energy_nonneg (n : ℕ) (s : Finset G) (ν : G → ℂ) : 0 ≤ energy n s ν := by

LeanAPAP/Prereqs/Function/Indicator/Defs.lean

@@ -105,10 +105,10 @@ section CommSemiring
 variable [CommSemiring β]
 
 lemma indicate_inf_apply [Fintype α] (s : Finset ι) (t : ι → Finset α) (x : α) :
-    𝟭_[β] (s.inf t) x = ∏ i in s, 𝟭 (t i) x := by simp [indicate_apply, mem_inf, prod_boole]
+    𝟭_[β] (s.inf t) x = ∏ i ∈ s, 𝟭 (t i) x := by simp [indicate_apply, mem_inf, prod_boole]
 
 lemma indicate_inf [Fintype α] (s : Finset ι) (t : ι → Finset α) :
-    𝟭_[β] (s.inf t) = ∏ i in s, 𝟭 (t i) :=
+    𝟭_[β] (s.inf t) = ∏ i ∈ s, 𝟭 (t i) :=
   funext fun x ↦ by rw [Finset.prod_apply, indicate_inf_apply]
 
 variable [StarRing β]

LeanAPAP/Prereqs/MarcinkiewiczZygmund.lean

@@ -27,7 +27,7 @@ private lemma step_one (hA : A.Nonempty) (f : ι → ℝ) (a : Fin n → ι)
   calc
     |∑ i, f (a i)| ^ (m + 1)
       = |∑ i, (f (a i) - (∑ b ∈ B, f (b i)) / #B)| ^ (m + 1) := by
-      simp only [hf, sub_zero, zero_div]
+      simp only [B, hf, sub_zero, zero_div]
     _ = |(∑ b ∈ B, ∑ i, (f (a i) - f (b i))) / #B| ^ (m + 1) := by
       simp only [sum_sub_distrib]
       rw [sum_const, sub_div, sum_comm, sum_div, nsmul_eq_mul, card_piFinset, prod_const,
@@ -72,18 +72,18 @@ private lemma step_two_aux (A : Finset ι) (f : ι → ℝ) (ε : Fin n → ℝ)
     intro xy
     exact (fun i ↦ if ε i = 1 then xy.1 i else xy.2 i, fun i ↦ if ε i = 1 then xy.2 i else xy.1 i)
   have h₁ : ∀ a ∈ (A ^^ n) ×ˢ (A ^^ n), swapper a ∈ (A ^^ n) ×ˢ (A ^^ n) := by
-    simp only [mem_product, and_imp, mem_piFinset, ← forall_and]
+    simp only [mem_product, and_imp, mem_piFinset, ← forall_and, swapper]
     intro a h i
     split_ifs
     · exact h i
     · exact (h i).symm
   have h₂ : ∀ a ∈ (A ^^ n) ×ˢ (A ^^ n), swapper (swapper a) = a := fun a _ ↦ by
-    ext <;> simp only <;> split_ifs <;> rfl
+    ext <;> simp only [swapper] <;> split_ifs <;> rfl
   refine sum_nbij' swapper swapper h₁ h₁ h₂ h₂ ?_
   · rintro ⟨a, b⟩ _
     congr with i : 1
-    simp only [Pi.mul_apply, Pi.sub_apply, Function.comp_apply]
     simp only [mem_piFinset, mem_insert, mem_singleton] at hε
+    simp only [Pi.mul_apply, Pi.sub_apply, Function.comp_apply, swapper]
     split_ifs with h
     · simp [h]
     rw [(hε i).resolve_right h]
@@ -171,6 +171,7 @@ private lemma end_step {f : ι → ℝ} (hm : 1 ≤ m) (hA : A.Nonempty) :
         add_assoc, Nat.sub_add_cancel hm, pow_add, ← mul_pow, ← mul_pow, card_piFinset, prod_const,
         Finset.card_univ, Fintype.card_fin, Nat.cast_pow, mul_div_cancel_left₀]
       norm_num
+      dsimp [B]
       positivity
 
 namespace Real