Source indexedlemma · leanprover/lean4:v4.32.0

tendsto_const_mul_log_add_two_div_add_two_atTop

PrimeNumberTheoremAnd.Fourier · PrimeNumberTheoremAnd/Fourier.lean:85 to 94

Source documentation

The decay K * (log (T + 2) / (T + 2)) → 0 as T → ∞, for any constant K.

Exact Lean statement

lemma tendsto_const_mul_log_add_two_div_add_two_atTop (K : ℝ) :
    Filter.Tendsto (fun T : ℝ => K * (Real.log (T + 2) / (T + 2)))
      Filter.atTop (nhds 0)

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma tendsto_const_mul_log_add_two_div_add_two_atTop (K : ℝ) :    Filter.Tendsto (fun T : ℝ => K * (Real.log (T + 2) / (T + 2)))      Filter.atTop (nhds 0) := by  have h0 : Filter.Tendsto (fun x : ℝ => Real.log x / x) Filter.atTop (nhds 0) := by    simpa using (Real.tendsto_pow_log_div_mul_add_atTop 1 0 1 (by norm_num : (1 : ℝ) ≠ 0))  have hshift : Filter.Tendsto (fun T : ℝ => Real.log (T + 2) / (T + 2))      Filter.atTop (nhds 0) := by    have := h0.comp (tendsto_atTop_add_const_right Filter.atTop 2 tendsto_id)    simpa [Function.comp_def] using this  simpa using hshift.const_mul K