Kadiri.kadiri_thm_3_1_q1_eq_14_of_uniform_laplace_trunc_cpow_bound

lemma kadiri_thm_3_1_q1_eq_14_of_uniform_laplace_trunc_cpow_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 →      ‖laplaceIntegralCpowTrunc φ a ((n : ℝ)⁻¹) T‖ ≤ C * ((n : ℝ)⁻¹) ^ a) :    Filter.Tendsto (fun T : ℝ ↦ kadiri_thm_3_1_q1_I_2 φ a T)      Filter.atTop      (nhds (-∑' n : ℕ, ((Λ n : ℂ) / (n : ℂ)) * φ (-Real.log n))) := by  let bound : ℕ → ℝ :=    fun n => C * ‖(Λ n : ℂ) / (n : ℂ) ^ (((1 + a : ℝ) : ℂ))‖  have hbound_sum : Summable bound := by    have hs : 1 < (((1 + a : ℝ) : ℂ)).re := by      simp      linarith    exact (summable_norm_vonMangoldt_cpow hs).mul_left C  have hweighted : ∀ᶠ T in Filter.atTop, ∀ n : ℕ,      ‖((Λ n : ℂ) / (n : ℂ)) *        laplaceIntegralCpowTrunc φ a ((n : ℝ)⁻¹) T‖ ≤ bound n := by    filter_upwards [hbound] with T hT n    by_cases hn : n = 0    · subst n      simp [bound]    by_cases h1 : n = 1    · subst n      simp [bound]    · rw [norm_mul]      calc        ‖(Λ n : ℂ) / (n : ℂ)‖ *            ‖laplaceIntegralCpowTrunc φ a ((n : ℝ)⁻¹) T‖            ≤ ‖(Λ n : ℂ) / (n : ℂ)‖ * (C * ((n : ℝ)⁻¹) ^ a) :=              mul_le_mul_of_nonneg_left (hT n hn h1) (norm_nonneg _)        _ = C * (‖(Λ n : ℂ) / (n : ℂ)‖ * ((n : ℝ)⁻¹) ^ a) := by ring        _ = C * (‖(Λ n : ℂ) / (((n : ℝ) : ℂ))‖ * ((n : ℝ)⁻¹) ^ a) := by          norm_num        _ = bound n := by          rw [kadiri_norm_vonMangoldt_nat_inv_cpow_coeff_eq ha n]  exact kadiri_thm_3_1_q1_eq_14_of_weighted_laplace_trunc_dominated_bound    hφ hb hφ_decay ha hab ha1 bound hbound_sum hweighted