Perron.formulaLtOne

@[blueprint  "formulaLtOne"  (title := "formulaLtOne")  (statement := /--  For $x>0$, $\sigma>0$, and $x<1$, we have  $$  \frac1{2\pi i}  \int_{(\sigma)}\frac{x^s}{s(s+1)}ds =0.  $$  -/)  (latexEnv := "lemma")]lemma formulaLtOne (xpos : 0 < x) (x_lt_one : x < 1) (σ_pos : 0 < σ)    : VerticalIntegral (f x) σ = 0 := by  /--  Let $f(s) = x^s/(s(s+1))$. Then $f$ is holomorphic on the half-plane  $\{s\in\mathbb{C}:\Re(s)>0\}$. The rectangle integral of $f$ with corners $\sigma-iT$ and  $\sigma+iT$ is zero. The limit of this rectangle integral as $T\to\infty$ is  $\int_{(\sigma')}-\int_{(\sigma)}$. Therefore, $\int_{(\sigma')}=\int_{(\sigma)}$.  -/  have h_contourPull (σ' σ'' : ℝ) (σ'pos : 0 < σ') (σ''pos : 0 < σ'') :      VerticalIntegral (f x) σ' = VerticalIntegral (f x) σ'' :=    contourPull xpos (notMem_uIcc_of_lt σ'pos σ''pos)      (notMem_uIcc_of_lt (by linarith) (by linarith))  /--  But we also have the bound $\int_{(\sigma')} \leq x^{\sigma'} * C$, where  $C=\int_\R\frac{1}{|(1+t)(1+t+1)|}dt$.  -/  have VertIntBound : ∃ C > 0, ∀ σ' > 1, ‖VerticalIntegral (f x) σ'‖ ≤ x^σ' * C := by    let C := ∫ (t : ℝ), 1 / ((1 + t ^ 2).sqrt * (2 + t ^ 2).sqrt)    exact ⟨C, integralPosAux, fun _ ↦ vertIntBound xpos⟩  /-- Therefore $\int_{(\sigma')}\to 0$ as $\sigma'\to\infty$. -/  have AbsVertIntTendsto :      Tendsto ((‖·‖ : ℂ → ℝ) ∘ (VerticalIntegral (f x))) atTop (𝓝 0) := by    obtain ⟨C, _, hC⟩ := VertIntBound    have := tendsto_rpow_atTop_nhds_zero_of_norm_lt_one xpos x_lt_one C    apply tendsto_of_tendsto_of_tendsto_of_le_of_le' tendsto_const_nhds this    · filter_upwards; exact fun _ ↦ norm_nonneg _    · filter_upwards [eventually_gt_atTop 1]; exact hC  have VertIntTendsto : Tendsto (VerticalIntegral (f x)) atTop (𝓝 0) :=    tendsto_zero_iff_norm_tendsto_zero.mpr AbsVertIntTendsto  /-- So pulling contours gives $\int_{(\sigma)}=0$. -/  exact limitOfConstant σ_pos h_contourPull VertIntTendsto