Source indexedlemma · leanprover/lean4:v4.32.0

DerivUpperBnd_aux7_tendsto

PrimeNumberTheoremAnd.ZetaBounds · PrimeNumberTheoremAnd/ZetaBounds.lean:1911 to 1926

Mathematical statement

Exact Lean statement

lemma DerivUpperBnd_aux7_tendsto {σ : ℝ} (σpos : 0 < σ) :
    Tendsto (fun t ↦ -(1 / σ ^ 2 * t ^ (-σ) + 1 / σ * t ^ (-σ) * Real.log t)) atTop (nhds 0)

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma DerivUpperBnd_aux7_tendsto {σ : ℝ} (σpos : 0 < σ) :    Tendsto (fun t ↦ -(1 / σ ^ 2 * t ^ (-σ) + 1 / σ * t ^ (-σ) * Real.log t)) atTop (nhds 0) := by  have h1 := tendsto_rpow_neg_atTop σpos  have h2 := h1.const_mul (1 / σ^2)  have h3 : Tendsto (fun t : ℝ ↦ t ^ (-σ) * Real.log t) atTop (nhds 0) := by    have := Real.tendsto_pow_log_div_pow_atTop σ 1 σpos    simp only [Real.rpow_one] at this    apply Tendsto.congr' _ this    filter_upwards [eventually_ge_atTop 0] with x hx    rw [mul_comm]    apply div_rpow_eq_rpow_neg _ _ _ hx  have h4 := h3.const_mul (1 / σ)  have h5 := (h2.add h4).neg  convert h5 using 1  · ext; ring  simp