Source indexedlemma · leanprover/lean4:v4.32.0

Perron.tendsto_zero_Upper

PrimeNumberTheoremAnd.PerronFormula · PrimeNumberTheoremAnd/PerronFormula.lean:700 to 715

Mathematical statement

Exact Lean statement

@[blueprint
  (title := "tendsto-zero-Upper")
  (statement := /--
  Let $x>0$ and $\sigma',\sigma''\in\R$. Then
  $$\int_{\sigma'}^{\sigma''}\frac{x^{\sigma+it}}{(\sigma+it)(1+\sigma + it)}d\sigma$$
  goes to $0$ as $t\to\infty$.
  -/)
  (proof := /-- The numerator is bounded and the denominator tends to infinity. -/)
  (latexEnv := "lemma")]
lemma tendsto_zero_Upper (xpos : 0 < x) (σ' σ'' : ℝ) :
    Tendsto (fun (t : ℝ) ↦ ∫ (σ : ℝ) in σ'..σ'', f x (σ + t * I)) atTop (𝓝 0)

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

@[blueprint  (title := "tendsto-zero-Upper")  (statement := /--  Let $x>0$ and $\sigma',\sigma''\in\R$. Then  $$\int_{\sigma'}^{\sigma''}\frac{x^{\sigma+it}}{(\sigma+it)(1+\sigma + it)}d\sigma$$  goes to $0$ as $t\to\infty$.  -/)  (proof := /-- The numerator is bounded and the denominator tends to infinity. -/)  (latexEnv := "lemma")]lemma tendsto_zero_Upper (xpos : 0 < x) (σ' σ'' : ℝ) :    Tendsto (fun (t : ℝ) ↦ ∫ (σ : ℝ) in σ'..σ'', f x (σ + t * I)) atTop (𝓝 0) := by   have hcast : (fun (y : ℝ) ↦ 1 / y ^ 2) =ᶠ[atTop] fun y ↦ y ^ (-2 : ℝ) := by    filter_upwards [Ici_mem_atTop 0] with y hy using by rw [rpow_neg hy, inv_eq_one_div, rpow_two]  refine isBigO_sup.mp (horizontal_integral_isBigO xpos σ' σ'' volume)    |>.2.trans_eventuallyEq hcast |>.trans_tendsto <| tendsto_rpow_neg_atTop (by norm_num)