Kadiri.kadiri_thm_3_1_q1_eq_14_of_uniform_fourier_inv_trunc_bound

lemma kadiri_thm_3_1_q1_eq_14_of_uniform_fourier_inv_trunc_bound    {φ : ℝ → ℂ} (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 : ℝ} (ha : 0 < a) (hab : a < b) (ha1 : a < 1)    (C : ℝ)    (hbound : ∀ᶠ T in Filter.atTop, ∀ n : ℕ, n ≠ 0 → n ≠ 1 →      ‖fourierInvTrunc          (𝓕 (fun y : ℝ => exp (-((a : ℂ) * (y : ℂ))) • φ y))          (-Real.log n) T‖ ≤ C) :    Filter.Tendsto (fun T : ℝ ↦ kadiri_thm_3_1_q1_I_2 φ a T)      Filter.atTop      (nhds (-∑' n : ℕ, ((Λ n : ℂ) / (n : ℂ)) * φ (-Real.log n))) := by  refine kadiri_thm_3_1_q1_eq_14_of_uniform_laplace_trunc_cpow_bound    hφ hb hφ_decay ha hab ha1 C ?_  filter_upwards [hbound] with T hT n hn h1  have hnpos : 0 < (n : ℝ) := Nat.cast_pos.mpr (Nat.pos_of_ne_zero hn)  have hxpos : 0 < ((n : ℝ)⁻¹) := inv_pos.mpr hnpos  rw [laplaceIntegralCpowTrunc_eq_laplaceInvLineTrunc    (sigma := a) (f := φ) (x := ((n : ℝ)⁻¹)) hxpos T]  rw [laplaceInvLineTrunc_laplaceTransformBilateral_eq_fourierInvTrunc]  rw [norm_smul]  have hlog : Real.log ((n : ℝ)⁻¹) = -Real.log n := by    simp [Real.log_inv]  have hscale :      ‖exp ((a : ℂ) * (Real.log ((n : ℝ)⁻¹) : ℂ))‖ = ((n : ℝ)⁻¹) ^ a := by    rw [Complex.exp_mul_log_of_pos_eq_cpow hxpos (a : ℂ)]    rw [Complex.norm_cpow_eq_rpow_re_of_pos hxpos]    simp  rw [hscale]  calc    ((n : ℝ)⁻¹) ^ a *        ‖fourierInvTrunc          (𝓕 (fun y : ℝ => exp (-((a : ℂ) * (y : ℂ))) • φ y))          (Real.log ((n : ℝ)⁻¹)) T‖        = ((n : ℝ)⁻¹) ^ a *            ‖fourierInvTrunc              (𝓕 (fun y : ℝ => exp (-((a : ℂ) * (y : ℂ))) • φ y))              (-Real.log n) T‖ := by rw [hlog]    _ ≤ ((n : ℝ)⁻¹) ^ a * C :=      mul_le_mul_of_nonneg_left (hT n hn h1)        (Real.rpow_nonneg (inv_nonneg.mpr hnpos.le) a)    _ ≤ C * ((n : ℝ)⁻¹) ^ a := by rw [mul_comm]