Source indexedtheorem · leanprover/lean4:v4.32.0

abs_mul_exp_isBigO

PrimeNumberTheoremAnd.IEANTN.KadiriEq12Helpers · PrimeNumberTheoremAnd/IEANTN/KadiriEq12Helpers.lean:148 to 161

Source documentation

Keystone: a linear weight is absorbed by an exponential with a slightly smaller rate.

Exact Lean statement

theorem abs_mul_exp_isBigO {b b' : ℝ} (hbb : b' < b) :
    (fun x : ℝ ↦ |x| * Real.exp (-(1/2+b)*|x|)) =O[cocompact ℝ]
      (fun x ↦ Real.exp (-(1/2+b')*|x|))

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem abs_mul_exp_isBigO {b b' : ℝ} (hbb : b' < b) :    (fun x : ℝ ↦ |x| * Real.exp (-(1/2+b)*|x|)) =O[cocompact ℝ]      (fun x ↦ Real.exp (-(1/2+b')*|x|)) := by  have hδ : 0 < b - b' := by linarith  have hg : Tendsto (fun t : ℝ ↦ t * Real.exp (-(b-b')*t)) atTop (nhds 0) := by    simpa [Real.rpow_one] using tendsto_rpow_mul_exp_neg_mul_atTop_nhds_zero 1 (b-b') hδ  have htend : Tendsto (fun x : ℝ ↦ |x| * Real.exp (-(b-b')*|x|)) (cocompact ℝ) (nhds 0) := by    simpa [Function.comp_def, Real.norm_eq_abs] using hg.comp (tendsto_norm_cocompact_atTop (E := ℝ))  have hbound : (fun x : ℝ ↦ |x| * Real.exp (-(b-b')*|x|)) =O[cocompact ℝ] (fun _ ↦ (1:ℝ)) :=    htend.isBigO_one ℝ  rw [show (fun x : ℝ ↦ |x| * Real.exp (-(1/2+b)*|x|)) =      (fun x ↦ (|x| * Real.exp (-(b-b')*|x|)) * Real.exp (-(1/2+b')*|x|)) from by    funext x; rw [mul_assoc, ← Real.exp_add]; congr 2; ring]  simpa using hbound.mul (isBigO_refl (fun x : ℝ ↦ Real.exp (-(1/2+b')*|x|)) (cocompact ℝ))