Perron.diffBddAtNegOne

@[blueprint  "diffBddAtNegOne"  (title := "diffBddAtNegOne")  (statement := /--  Let $x>0$. Then for $0 < c < 1 /2$, we have that the function  $$  s ↦ \frac{x^s}{s(s+1)} - \frac{-x^{-1}}{s+1}  $$  is bounded above on the rectangle with corners at $-1-c-i*c$ and $-1+c+i*c$ (except at $s=-1$).  -/)  (proof := /--  Applying Lemma \ref{keyIdentity}, the   function $s ↦ x^s/s(s+1) - x^{-1}/(s+1) = x^s/s - x^s/(s+1) - (-x^{-1})/(s+1)$. The first term   is bounded for $s$   away from $0$. The last two terms are the difference quotient of the function $s ↦ x^s$ at   $-1$; since it's differentiable, the difference remains bounded as $s\to -1$.  -/)  (latexEnv := "lemma")]lemma diffBddAtNegOne {x : ℝ} (xpos : 0 < x) :    ∀ᶠ (c : ℝ) in 𝓝[>] 0,      BddAbove ((norm ∘ (fun (s : ℂ) ↦ (x : ℂ) ^ s / (s * (s + 1)) -          (-x⁻¹) / (s + 1))) '' (Square (-1) c \ {-1})) := by   apply bddAbove_square_of_tendsto  suffices      Tendsto (norm ∘ (fun (s : ℂ) ↦ ↑x ^ s / s - (↑x ^ s / (s + 1) - x⁻¹ / (s + 1))))        (𝓝[≠] (-1))        (𝓝 (‖x ^ (-1 : ℂ) / -1 - (deriv (fun (s : ℂ) ↦ (x : ℂ) ^ s) (-1))‖))    by    apply this.congr'    filter_upwards      [sdiff_mem_nhdsWithin_compl (isOpen_compl_singleton.mem_nhds        (Set.mem_compl_singleton_iff.mpr (by norm_num : (-1 : ℂ) ≠ 0))) {-1}]    with s hs    rw [Function.comp_apply, Function.comp_apply, keyIdentity _ hs.1 hs.2]    ring_nf  have hx0 : (x : ℂ) ≠ 0 := slitPlane_ne_zero (.inl xpos)  refine (Tendsto.sub (tendsto_nhdsWithin_of_tendsto_nhds ?_) ?_).norm  · exact ((continuous_id.const_cpow (.inl hx0)).tendsto _).div tendsto_id (by norm_num)  · convert hasDerivAt_iff_tendsto_slope.mp      (differentiableAt_fun_id.const_cpow (.inl hx0)).hasDerivAt using 2    rw [slope_def_field, cpow_neg_one, ofReal_inv]; ring