ZetaBnd_aux1p fix

AlexKontorovich · Jan 28, 2025 · bafaa8b · bafaa8b
1 parent f6c75bc
commit bafaa8b
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/PrimeNumberTheoremAnd/ZetaBounds.lean b/PrimeNumberTheoremAnd/ZetaBounds.lean
@@ -754,7 +754,7 @@ $$
 $$
 \end{lemma}
 %%-/
-lemma ZetaBnd_aux1p (N : ℕ) (Npos : 1 ≤ N) {σ t : ℝ} (hσ : σ ∈ Ioc 0 2) (ht : 2 ≤ |t|) :
+lemma ZetaBnd_aux1p (N : ℕ) (Npos : 1 ≤ N) {σ : ℝ} (hσ : σ ∈ Ioc 0 2) :
     (fun (t : ℝ) ↦ ‖(σ + t * I) * ∫ x in Ioi (N : ℝ), (⌊x⌋ + 1 / 2 - x) / (x : ℂ) ^ ((σ + t * I) + 1)‖)
     =O[Filter.principal {t | 2 ≤ |t|}] fun t ↦ |t| * N ^ (-σ) / σ := by
   rw [Asymptotics.IsBigO_def]