riemannZetaLogDerivResidue

@[blueprint  (title := "riemannZetaLogDerivResidue")  (statement := /--  The log derivative of the Riemann zeta function $\zeta(s)$ has a simple pole at $s=1$ with  residue $-1$: $-\frac{\zeta'(s)}{\zeta(s)} - \frac{1}{s-1} = O(1)$.  -/)  (proof := /--  This follows from Theorem \ref{logDerivResidue} and Theorem \ref{riemannZetaResidue}.  -/)]theorem riemannZetaLogDerivResidue :    ∃ U ∈ 𝓝 1, BddAbove (norm ∘ (-(ζ' / ζ) - (fun s ↦ (s - 1)⁻¹)) '' (U \ {1})) := by  obtain ⟨U,U_in_nhds, hU⟩ := riemannZetaResidue  have hU' : BddAbove (norm ∘ (ζ - fun s ↦ 1 * (s - 1)⁻¹) '' (U \ {1})) := by    simp only [Function.comp_apply, Pi.sub_apply, one_mul] at hU ⊢    exact hU  obtain ⟨V,V_in_nhds, V_is_open, hV⟩ := nonZeroOfBddAbove U_in_nhds one_ne_zero hU'  let W := V ∩ interior U  have hW : ∀ s ∈ W \ {1}, ζ s ≠ 0 := by    intro s hs    have s_in_V_diff : s ∈ V \ {1} := ⟨hs.1.1, hs.2⟩    exact hV s s_in_V_diff  have ζ_holc: HolomorphicOn ζ (W \ {1}) := by    intro y hy    simp only [Set.mem_sdiff, mem_singleton_iff] at hy    refine DifferentiableAt.differentiableWithinAt ?_    apply differentiableAt_riemannZeta hy.2  have W_in_nhds : W ∈ 𝓝 1 := by    refine inter_mem V_in_nhds ?_    exact interior_mem_nhds.mpr U_in_nhds  have := logDerivResidue'' hW ζ_holc W_in_nhds one_ne_zero  have HW : BddAbove (norm ∘ (ζ - fun s ↦ (s - 1)⁻¹) '' (W \ {1})) := by    obtain ⟨c, hc⟩ := bddAbove_def.mp hU    apply bddAbove_def.mpr    use c    rintro y ⟨x, x_in_W, fxy⟩    apply hc    exact ⟨x, ⟨interior_subset x_in_W.1.2, x_in_W.2⟩, fxy⟩  simp only [one_mul] at this  have aux: ∀ a, ‖-(deriv ζ a / ζ a) - (a - 1)⁻¹‖ = ‖(deriv ζ a / ζ a) + (a - 1)⁻¹‖ := by    intro a    calc ‖-(deriv ζ a / ζ a) - (a - 1)⁻¹‖         = ‖-((deriv ζ a / ζ a) + (a - 1)⁻¹)‖ := by ring_nf       _ = ‖(deriv ζ a / ζ a) + (a - 1)⁻¹‖ := by rw [norm_neg]  simp only [Function.comp_apply, Pi.sub_apply] at hU  simp only [Function.comp_apply, Pi.sub_apply, Pi.neg_apply, Pi.div_apply, aux]  apply this HW