riemannZeta_isBigO_near_one_horizontal

lemma riemannZeta_isBigO_near_one_horizontal :    (fun x : ℝ ↦ ζ (1 + x)) =O[𝓝[>] 0] (fun x ↦ (1 : ℂ) / x) := by  have : (fun w : ℂ ↦ ζ (1 + w)) =O[𝓝[≠] 0] (1 / ·) := by    have H : Tendsto (fun w ↦ w * ζ (1 + w)) (𝓝[≠] 0) (𝓝 1) := by      convert Tendsto.comp (f := fun w ↦ 1 + w) riemannZeta_residue_one ?_ using 1      · ext w        simp only [Function.comp_apply, add_sub_cancel_left]      · refine tendsto_iff_comap.mpr <| map_le_iff_le_comap.mp <| Eq.le ?_        convert Homeomorph.map_punctured_nhds_eq (Homeomorph.addLeft (1 : ℂ)) 0 using 2 <;> simp    exact ((Asymptotics.isBigO_mul_iff_isBigO_div eventually_mem_nhdsWithin).mp <|      Tendsto.isBigO_one ℂ H).trans <| Asymptotics.isBigO_refl ..  exact (isBigO_comp_ofReal_nhds_ne this).mono <| nhdsGT_le_nhdsNE 0