Kadiri.weighted_zeroImagSquareTail_shifted_summable

theorem weighted_zeroImagSquareTail_shifted_summable (s : ℂ) :    Summable (fun ρ : NontrivialZeros ↦      ((riemannZeta.order (ρ : ℂ) : ℤ) : ℝ) * (|(s - (ρ : ℂ)).im|⁻¹ ^ (2 : ℕ))) := by  refine Summable.of_norm_bounded_eventually    (weighted_zeroImagSquareTail_summable.mul_left 4) ?_  rw [Filter.eventually_cofinite]  apply Set.Finite.subset (nontrivialZeros_abs_im_lt_finite (2 * |s.im| + 2))  intro ρ hbad  rw [Set.mem_setOf_eq] at hbad ⊢  by_contra hsmall  have hlarge : 2 * |s.im| + 2 ≤ |(ρ : ℂ).im| := le_of_not_gt hsmall  apply hbad  have hle := zeroImagSquareTail_shifted_le_four (s := s) (rho := ρ) hlarge  have hord : (0 : ℝ) ≤ ((riemannZeta.order (ρ : ℂ) : ℤ) : ℝ) := by    exact_mod_cast riemannZeta_order_nonneg (nontrivialZero_ne_one ρ)  have hshift_nn : (0 : ℝ) ≤ |(s - (ρ : ℂ)).im|⁻¹ ^ (2 : ℕ) := by positivity  rw [Real.norm_eq_abs, abs_of_nonneg (mul_nonneg hord hshift_nn)]  calc ((riemannZeta.order (ρ : ℂ) : ℤ) : ℝ) * (|(s - (ρ : ℂ)).im|⁻¹ ^ (2 : ℕ))      ≤ ((riemannZeta.order (ρ : ℂ) : ℤ) : ℝ) * (4 * zeroImagSquareTail ρ) :=        mul_le_mul_of_nonneg_left hle hord    _ = 4 * (((riemannZeta.order (ρ : ℂ) : ℤ) : ℝ) * zeroImagSquareTail ρ) := by        ring