Kadiri.kadiri_laplace_positive_line_pv

lemma kadiri_laplace_positive_line_pv {φ : ℝ → ℂ}    (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|))    {a x : ℝ} (ha : 0 < a) (hab : a < b) (hx : 0 < x) :    Filter.Tendsto (fun T : ℝ => laplaceIntegralCpowTrunc φ a x T)      Filter.atTop (nhds (φ (Real.log x))) := by  have h_weighted :      Integrable (fun y : ℝ => exp (-((a : ℂ) * (y : ℂ))) * φ y) :=    kadiri_laplace_positive_line_weight_integrable hφ hφ_decay ha hab  have hq :      IntervalIntegrable        (fun u : ℝ =>          if u = 0 then 0 else            (1 / (Real.pi * u) : ℂ) •              (exp (-((a : ℂ) * ((Real.log x - u : ℝ) : ℂ))) *                  φ (Real.log x - u) -                exp (-((a : ℂ) * (Real.log x : ℂ))) *                  φ (Real.log x)))        volume (-1) 1 := by    simpa using kadiri_laplace_line_local_quotient_integrable      (φ := φ) hφ a (Real.log x) (by norm_num : (0 : ℝ) < 1)  exact kadiri_laplaceIntegralCpowTrunc_tendsto_of_integrable_local_quotient    (sigma := a) (f := φ) (x := x) (R := 1) hx    (by norm_num : (0 : ℝ) < 1) h_weighted hq