Kadiri.kadiri_thm_3_1_q1_eq_13_core

theorem kadiri_thm_3_1_q1_eq_13_core    {φ : ℝ → ℂ} (_hφ : ContDiff ℝ 1 φ)    {b : ℝ} (_hb : 0 < b)    (_hφ_decay : (fun x : ℝ ↦ φ x * exp ((x : ℂ) / 2))        =O[Filter.cocompact ℝ] fun x : ℝ ↦ Real.exp (-(1/2 + b) * |x|))    (_hφ'_decay : (fun x : ℝ ↦ deriv φ x * exp ((x : ℂ) / 2))        =O[Filter.cocompact ℝ] fun x : ℝ ↦ Real.exp (-(1/2 + b) * |x|))    {a : ℝ} (_ha : 0 < a) (_hab : a < b) (_ha1 : a < 1) :    Filter.Tendsto (fun T : ℝ ↦ kadiri_thm_3_1_q1_I_1 φ a T)      Filter.atTop (nhds (φ 0 * ((-Real.log Real.pi : ℝ) : ℂ))) := by  let c : ℂ := ((-Real.log Real.pi : ℝ) : ℂ)  have hraw := kadiri_laplace_positive_line_pv_one    (φ := φ) _hφ _hb _hφ_decay _ha _hab _ha1  have hmul : Filter.Tendsto      (fun T : ℝ => c * laplaceIntegralCpowTrunc φ a 1 T)      Filter.atTop (nhds (c * φ 0)) := hraw.const_mul c  have heq := kadiri_thm_3_1_q1_I_1_eventually_eq_const_mul_trunc φ a  refine hmul.congr' ?_ |>.trans_eq ?_  · exact heq.symm  · simp [c, mul_comm]