Kadiri.summable_one_div_add_one_div_at_zeros

theorem summable_one_div_add_one_div_at_zeros (s : ℂ) :    Summable (fun ρ : riemannZeta.zeroes_rect (.Ioo 0 1) (.univ : Set ℝ) ↦      (1 / (ρ.val : ℂ) + 1 / (s - ρ.val))) := by  have htail0 : Summable (fun ρ : NontrivialZeros ↦ |(ρ : ℂ).im|⁻¹ ^ (2 : ℕ)) := by    have h := zeroImagSquareTailSummable_of_crude_majorant    unfold zeroImagSquareTailSummable zeroImagSquareTail at h    exact h  have htails : Summable (fun ρ : NontrivialZeros ↦      ‖s‖ / 2 * (|(ρ : ℂ).im|⁻¹ ^ (2 : ℕ) + |(s - (ρ : ℂ)).im|⁻¹ ^ (2 : ℕ))) :=    (htail0.add (summable_zeroImagSquareTail_shifted_unconditional s)).mul_left _  refine Summable.of_norm_bounded_eventually htails ?_  rw [Filter.eventually_cofinite]  apply Set.Finite.subset    (nontrivialZeros_abs_im_lt_one_finite.union      (nontrivialZeros_shifted_abs_im_lt_one_finite s))  intro ρ hbad  rw [Set.mem_setOf_eq] at hbad  rw [Set.mem_union, Set.mem_setOf_eq, Set.mem_setOf_eq]  by_contra hsmall  rw [not_or] at hsmall  obtain ⟨h1, h2⟩ := hsmall  have him1 : 1 ≤ |(ρ : ℂ).im| := not_lt.mp h1  have him2 : 1 ≤ |(s - (ρ : ℂ)).im| := not_lt.mp h2  apply hbad  have hρ0 : ((ρ : ℂ)) ≠ 0 := nontrivialZero_ne_zero ρ  have him2ne : (s - (ρ : ℂ)).im ≠ 0 := by    intro h    rw [h] at him2    norm_num at him2  have hsρ : s - (ρ : ℂ) ≠ 0 := by    intro h    apply him2ne    rw [h]    rfl  have hnρ : (0 : ℝ) < ‖(ρ : ℂ)‖ := norm_pos_iff.mpr hρ0  have hnsρ : (0 : ℝ) < ‖s - (ρ : ℂ)‖ := norm_pos_iff.mpr hsρ  have him1pos : (0 : ℝ) < |(ρ : ℂ).im| := lt_of_lt_of_le one_pos him1  have him2pos : (0 : ℝ) < |(s - (ρ : ℂ)).im| := lt_of_lt_of_le one_pos him2  have hpacket : 1 / ((ρ : ℂ)) + 1 / (s - (ρ : ℂ)) =      s / (((ρ : ℂ)) * (s - (ρ : ℂ))) := by    field_simp    ring  rw [hpacket, norm_div, norm_mul]  have hstep1 : ‖s‖ / (‖(ρ : ℂ)‖ * ‖s - (ρ : ℂ)‖) ≤      ‖s‖ * (|(ρ : ℂ).im|⁻¹ * |(s - (ρ : ℂ)).im|⁻¹) := by    rw [div_eq_mul_inv, mul_inv]    have ha : ‖(ρ : ℂ)‖⁻¹ ≤ |(ρ : ℂ).im|⁻¹ :=      inv_anti₀ him1pos (Complex.abs_im_le_norm _)    have hb : ‖s - (ρ : ℂ)‖⁻¹ ≤ |(s - (ρ : ℂ)).im|⁻¹ :=      inv_anti₀ him2pos (Complex.abs_im_le_norm _)    have hb0 : (0 : ℝ) ≤ ‖s - (ρ : ℂ)‖⁻¹ := by positivity    have ha0 : (0 : ℝ) ≤ |(ρ : ℂ).im|⁻¹ := by positivity    refine mul_le_mul_of_nonneg_left ?_ (norm_nonneg s)    exact mul_le_mul ha hb hb0 ha0  have hstep2 : |(ρ : ℂ).im|⁻¹ * |(s - (ρ : ℂ)).im|⁻¹ ≤      (|(ρ : ℂ).im|⁻¹ ^ (2 : ℕ) + |(s - (ρ : ℂ)).im|⁻¹ ^ (2 : ℕ)) / 2 := by    nlinarith [two_mul_le_add_sq (|(ρ : ℂ).im|⁻¹) (|(s - (ρ : ℂ)).im|⁻¹)]  calc ‖s‖ / (‖(ρ : ℂ)‖ * ‖s - (ρ : ℂ)‖)      ≤ ‖s‖ * (|(ρ : ℂ).im|⁻¹ * |(s - (ρ : ℂ)).im|⁻¹) := hstep1    _ ≤ ‖s‖ * ((|(ρ : ℂ).im|⁻¹ ^ (2 : ℕ) + |(s - (ρ : ℂ)).im|⁻¹ ^ (2 : ℕ)) / 2) :=        mul_le_mul_of_nonneg_left hstep2 (norm_nonneg s)    _ = ‖s‖ / 2 * (|(ρ : ℂ).im|⁻¹ ^ (2 : ℕ) + |(s - (ρ : ℂ)).im|⁻¹ ^ (2 : ℕ)) := by        ring