Perron.formulaGtOne

@[blueprint  "formulaGtOne"  (title := "formulaGtOne")  (statement := /--  For $x>1$ and $\sigma>0$, we have  $$  \frac1{2\pi i}  \int_{(\sigma)}\frac{x^s}{s(s+1)}ds =1-1/x.  $$  -/)  (latexEnv := "lemma")]lemma formulaGtOne (x_gt_one : 1 < x) (σ_pos : 0 < σ) :    VerticalIntegral' (fun s ↦ x^s / (s * (s + 1))) σ = 1 - 1 / x := by  /-- Let $f(s) = x^s/(s(s+1))$. Then $f$ is holomorphic on $\C \setminus {0,-1}$. -/  set f : ℂ → ℂ := (fun s ↦ x^s / (s * (s + 1)))  /-- First pull the contour from $(\sigma)$ to $(-1/2)$, picking up a residue $1$ at $s=0$. -/  rw [residuePull1 x_gt_one σ_pos]  /-- Next pull the contour from $(-1/2)$ to $(-3/2)$, picking up a residue $-1/x$ at  $s=-1$. -/  rw [residuePull2 x_gt_one]  /-- Then pull the contour all the way to $(\sigma')$ with $\sigma'<-3/2$. -/  have contourPull₃ (σ' σ'' : ℝ) (hσ' : σ' ≤ -3/2) (hσ'' : σ'' ≤ -3/2) :      VerticalIntegral' f σ' = VerticalIntegral' f σ'' :=    contourPull3 x_gt_one hσ' hσ''  /-- For $\sigma' < -3/2$, the integral is bounded by  $x^{\sigma'}\int_\R\frac{1}{|(1+t ^ 2)(2+t ^ 2)|^{1/2}}dt$. -/  have VertIntBound : ∃ C, ∀ σ' < -3/2, ‖VerticalIntegral' f σ'‖ ≤ C * x ^ σ' :=    vertIntBoundLeft (by linarith : 0 < x)  /-- Therefore $\int_{(\sigma')}\to 0$ as $\sigma'\to\infty$. -/  have AbsVertIntTendsto :      Tendsto ((‖·‖ : ℂ → ℝ) ∘ (VerticalIntegral' f)) atBot (𝓝 0) := by    obtain ⟨C, hC⟩ := VertIntBound    have := tendsto_rpow_atTop_nhds_zero_of_norm_gt_one x_gt_one C    apply tendsto_of_tendsto_of_tendsto_of_le_of_le' tendsto_const_nhds this    · filter_upwards using fun _ ↦ norm_nonneg _    · filter_upwards [eventually_lt_atBot (-3/2)]      (conv at hC => intro σ hσ; rw [mul_comm]); exact fun _ ↦ hC _  /-- So pulling contours gives $\int_{(-3/2)}=0$. -/  rw [limitOfConstantLeft (σ := -3/2) (Eq.le rfl) contourPull₃ ?_]  · ring  · exact tendsto_zero_iff_norm_tendsto_zero.mpr AbsVertIntTendsto