Source indexedtheorem · leanprover/lean4:v4.32.0

neg_id_mul_decay

PrimeNumberTheoremAnd.IEANTN.KadiriEq12Helpers · PrimeNumberTheoremAnd/IEANTN/KadiriEq12Helpers.lean:164 to 173

Source documentation

The decay hypothesis transfers from φ to -(·)·φ with a slightly smaller rate.

Exact Lean statement

theorem neg_id_mul_decay {φ : ℝ → ℂ} {b b' : ℝ} (hbb : b' < b)
    (hφ_decay : (fun x : ℝ ↦ φ x * Complex.exp ((x:ℂ)/2)) =O[cocompact ℝ]
      fun x ↦ Real.exp (-(1/2+b)*|x|)) :
    (fun x : ℝ ↦ (-(x:ℂ) * φ x) * Complex.exp ((x:ℂ)/2)) =O[cocompact ℝ]
      fun x ↦ Real.exp (-(1/2+b')*|x|)

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem neg_id_mul_decay {φ : ℝ → ℂ} {b b' : ℝ} (hbb : b' < b)    (hφ_decay : (fun x : ℝ ↦ φ x * Complex.exp ((x:ℂ)/2)) =O[cocompact ℝ]      fun x ↦ Real.exp (-(1/2+b)*|x|)) :    (fun x : ℝ ↦ (-(x:ℂ) * φ x) * Complex.exp ((x:ℂ)/2)) =O[cocompact ℝ]      fun x ↦ Real.exp (-(1/2+b')*|x|) := by  have hx : (fun x : ℝ ↦ (x:ℂ)) =O[cocompact ℝ] (fun x : ℝ ↦ |x|) := by    rw [isBigO_iff]; exact ⟨1, Filter.Eventually.of_forall (fun x ↦ by simp [Complex.norm_real])⟩  rw [show (fun x : ℝ ↦ (-(x:ℂ) * φ x) * Complex.exp ((x:ℂ)/2))      = (fun x : ℝ ↦ -((x:ℂ) * (φ x * Complex.exp ((x:ℂ)/2)))) from by funext x; ring]  exact ((hx.mul hφ_decay).neg_left).trans (abs_mul_exp_isBigO hbb)