I1NewIntegrandBound

lemma I1NewIntegrandBound {SmoothingF : ℝ → ℝ}    (suppSmoothingF : Function.support SmoothingF ⊆ Set.Icc (1 / 2) 2)    (ContDiffSmoothingF : ContDiff ℝ 1 SmoothingF) :    ∃ C > 0, ∀ {ε X T : ℝ} (_εinIoo : ε ∈ Set.Ioo 0 1) (_Xgt3 : 3 < X) (_Tgt3 : 3 < T)    (t : ℝ) (_ht : t ≤ -T),    ‖SmoothedChebyshevIntegrand SmoothingF ε X (1 + (Real.log X)⁻¹ + t * I)‖ ≤    C * (X / ε) * (Real.log (-t))^2 / (-t)^2 := by  obtain ⟨C₁, hC₁₀, hC₁⟩ := @LogDerivZetaBoundForI1  obtain ⟨C₂, hC₂₀, hC₂⟩ := @MellinOfSmooth1b SmoothingF ContDiffSmoothingF suppSmoothingF  refine ⟨C₁ * C₂ * Real.exp 1, by positivity, fun {ε X T} hε hX hT t ht ↦ ?_⟩  specialize hC₁ hX hT t ht  specialize hC₂ 1 zero_lt_one (1 + (Real.log X)⁻¹ + t * Complex.I) ?_ ?_ ε hε.1 hε.2 <;> norm_num at *  · exact Real.log_nonneg (by linarith)  · linarith [inv_le_one_of_one_le₀ (show 1 ≤ Real.log X from by      rw [Real.le_log_iff_exp_le (by linarith)]      exact Real.exp_one_lt_d9.le.trans (by grind))]  · refine (mul_le_mul_of_nonneg_right        (mul_le_mul hC₁ hC₂ (by positivity) (by positivity)) (by positivity)).trans ?_    rw [Complex.norm_cpow_of_ne_zero (by norm_cast; linarith)]    norm_num [Complex.normSq, Complex.sq_norm]    ring_nf    norm_num    rw [abs_of_pos (by positivity)]    norm_num [Complex.arg]    ring_nf    norm_num    rw [if_pos (by positivity)]    norm_num [Real.rpow_add (by positivity : 0 < X), Real.rpow_one]    ring_nf    norm_num    rw [show X ^ (Real.log X)⁻¹ = Real.exp 1 by      rw [Real.rpow_def_of_pos (by positivity)]      norm_num [Real.exp_ne_zero, ne_of_gt (Real.log_pos (by linarith : 1 < X))]]    ring_nf    norm_num    field_simp    gcongr    · exact mul_pos (sq_pos_of_neg (by linarith)) hε.1    · linarith    · exact le_add_of_nonneg_left <| add_nonneg (add_nonneg zero_le_one          (div_nonneg zero_le_two (Real.log_nonneg (by linarith))))          (div_nonneg zero_le_one (sq_nonneg _))