I6Bound

lemma I6Bound {SmoothingF : ℝ → ℝ}    (suppSmoothingF : Function.support SmoothingF ⊆ Icc (1 / 2) 2)    (ContDiffSmoothingF : ContDiff ℝ 1 SmoothingF)    {σ₂ : ℝ} (h_logDeriv_holo : LogDerivZetaIsHoloSmall σ₂) (hσ₂ : σ₂ ∈ Ioo 0 1)    {A : ℝ} (hA : A ∈ Ioc 0 (1 / 2)) :    ∃ (C : ℝ) (_ : 0 ≤ C) (Tlb : ℝ) (_ : 3 < Tlb),    ∀ (X : ℝ) (_ : 3 < X)    {ε : ℝ} (_ : 0 < ε) (_ : ε < 1)    {T : ℝ} (_ : Tlb < T),    let σ₁ : ℝ := 1 - A / (Real.log T) ^ 9    ‖I₆ SmoothingF ε X σ₁ σ₂‖ ≤ C * X * X ^ (- A / (Real.log T ^ 9)) / ε := by  obtain ⟨C, Cpos, Tlb, Tlb_gt, bound⟩ := I4Bound suppSmoothingF ContDiffSmoothingF h_logDeriv_holo hσ₂ hA  refine ⟨C, Cpos, Tlb, Tlb_gt, fun X X_gt ε εpos ε_lt_one T T_gt ↦ ?_⟩  specialize bound X X_gt εpos ε_lt_one T_gt  intro σ₁  rwa [I6I4 (by linarith), norm_neg, norm_conj]