lint

PrimeNumberTheoremAnd/Mathlib/NumberTheory/Sieve/Basic.lean

@@ -62,7 +62,7 @@ def selbergTerms : ArithmeticFunction ℝ :=
 
 local notation3 "g" => Sieve.selbergTerms s
 
-def selbergTerms_apply (d : ℕ) :
+lemma selbergTerms_apply (d : ℕ) :
     g d = ν d * ∏ p in d.primeFactors, 1/(1 - ν p) := by
   unfold selbergTerms
   by_cases h : d=0

PrimeNumberTheoremAnd/Mathlib/NumberTheory/Sieve/Selberg.lean

@@ -95,11 +95,9 @@ theorem selbergWeights_eq_zero (d : ℕ) (hd : ¬d ^ 2 ≤ y) :
 
 @[aesop safe]
 theorem selbergWeights_mul_mu_nonneg (d : ℕ) (hdP : d ∣ P) :
-    0 ≤ γ d * μ d :=
-  by
-  have := s.selbergBoundingSum_nonneg
+    0 ≤ γ d * μ d := by
   dsimp only [selbergWeights]
-  rw [if_pos hdP]; rw [mul_assoc]
+  rw [if_pos hdP, mul_assoc]
   trans ((μ d :ℝ)^2 * (ν d)⁻¹ * g d * S⁻¹ * ∑ m in divisors P,
           if (d * m) ^ 2 ≤ y ∧ Coprime m d then g m else 0)
   swap; apply le_of_eq; ring

PrimeNumberTheoremAnd/MellinCalculus.lean

@@ -128,8 +128,7 @@ lemma IntervalIntegral.integral_eq_integral_of_support_subset_Icc {a b : ℝ} {
       have : ∫ (x : ℝ), f x ∂μ = ∫ (x : ℝ) in {a}, f x ∂μ := by
         rw [ ← integral_indicator (by simp), indicator_eq_self.2 h]
       rw [this, integral_singleton]; simp
-    · have : ¬a ≤ b := by exact fun x ↦ hab2 <| le_antisymm hab x
-      rw [Icc_eq_empty_iff.mpr <| by exact fun x ↦ hab2 <| le_antisymm hab x, subset_empty_iff,
+    · rw [Icc_eq_empty_iff.mpr <| by exact fun x ↦ hab2 <| le_antisymm hab x, subset_empty_iff,
           Function.support_eq_empty_iff] at h; simp [h]
 
 lemma SetIntegral.integral_eq_integral_inter_of_support_subset {μ : Measure ℝ}

PrimeNumberTheoremAnd/PerronFormula.lean

@@ -956,7 +956,6 @@ tendsto_rpow_atTop_nhds_zero_of_norm_gt_one, limitOfConstantLeft}
   Let $f(s) = x^s/(s(s+1))$. Then $f$ is holomorphic on $\C \setminus {0,1}$.
 %%-/
   set f : ℂ → ℂ := (fun s ↦ x^s / (s * (s + 1)))
-  have : HolomorphicOn f {0, -1}ᶜ := isHolomorphicOn (by linarith : 0 < x)
 --%% First pull the contour from $(\sigma)$ to $(-1/2)$, picking up a residue $1$ at $s=0$.
   rw [residuePull1 x_gt_one σ_pos]
 --%% Next pull the contour from $(-1/2)$ to $(-3/2)$, picking up a residue $-1/x$ at $s=-1$.

PrimeNumberTheoremAnd/Wiener.lean

@@ -1125,8 +1125,8 @@ lemma hh_continuous (a : ℝ) : ContinuousOn (hh a) (Ioi 0) :=
 
 lemma hh'_nonpos {a x : ℝ} (ha : a ∈ Ioo (-1) 1) : hh' a x ≤ 0 := by
   have := pp_pos ha (log x)
-  have := hh_nonneg a (sq_nonneg x)
-  simp [hh'] ; positivity
+  simp only [hh', neg_mul, Left.neg_nonpos_iff, ge_iff_le]
+  positivity
 
 lemma hh_antitone {a : ℝ} (ha : a ∈ Ioo (-1) 1) : AntitoneOn (hh a) (Ioi 0) := by
   have l1 x (hx : x ∈ interior (Ioi 0)) : HasDerivWithinAt (hh a) (hh' a x) (interior (Ioi 0)) x := by
@@ -2128,7 +2128,6 @@ theorem vonMangoldt_cheby : cheby Λ := by
     have := hC 2
     norm_cast at this
     have hpos : 0 < 2 / Real.log 2 := by positivity
-    have : (0 : ℝ) ≤ ↑(Finset.filter IsPrimePow (Finset.range 2)).card := by norm_cast
     rw [← mul_le_mul_right hpos]
     linarith
   use C

PrimeNumberTheoremAnd/ZetaBounds.lean

@@ -10,8 +10,7 @@ import Mathlib.MeasureTheory.Function.Floor
 import Mathlib.Analysis.Complex.CauchyIntegral
 import Mathlib.NumberTheory.Harmonic.Bounds
 
--- set_option quotPrecheck false
-open BigOperators Complex Topology Filter Interval Set
+open Complex Topology Filter Interval Set
 
 lemma div_cpow_eq_cpow_neg (a x s : ℂ) : a / x ^ s = a * x ^ (-s) := by
   rw [div_eq_mul_inv, cpow_neg]
@@ -1597,9 +1596,7 @@ lemma ZetaInvBound1 {σ t : ℝ} (σ_gt : 1 < σ) :
   · refine mul_nonneg (mul_nonneg ?_ ?_) ?_ <;> simp [Real.rpow_nonneg]
   · have s_ne_one : σ + t * I ≠ 1 := by
       contrapose! σ_gt; apply le_of_eq; apply And.left; simpa [Complex.ext_iff] using σ_gt
-    have zeta_ne_zero:= riemannZeta_ne_zero_of_one_le_re s_ne_one (by simp [σ_gt.le])
-    suffices 0 ≤ ‖ζ (↑σ + ↑t * I)‖ by simp [le_iff_lt_or_eq.mp this, zeta_ne_zero]
-    apply norm_nonneg
+    simpa using riemannZeta_ne_zero_of_one_le_re s_ne_one (by simp [σ_gt.le])
 /-%%
 \begin{proof}\leanok
 The identity