DerivUpperBnd_aux4

theorem DerivUpperBnd_aux4 {A σ t : ℝ} (t_gt : 3 < |t|) (hσ : σ ∈ Icc (1 - A / |t|.log) 2) :    let N := ⌊|t|⌋₊;    let s := ↑σ + ↑t * I;    0 < N → ↑N ≤ |t| → s ≠ 1 → 1 / 2 < σ →    ‖↑(N : ℝ).log * (N : ℂ) ^ (-s) / 2‖ ≤ A.exp * |t|.log := by  intro N s Npos N_le_t neOne σ_gt  rw [norm_div, norm_mul, mul_div_assoc, mul_comm, RCLike.norm_ofNat]  apply mul_le_mul ?_ ?_ (by positivity) (by positivity)  · have h := UpperBnd_aux6 t_gt ⟨σ_gt, hσ.2⟩ neOne Npos N_le_t |>.2.1    convert le_trans h (UpperBnd_aux2 t_gt hσ.1) using 1    simp [s, norm_natCast_cpow_of_pos Npos _, N]  · rw [natCast_log, norm_complex_log_ofNat]    exact Real.log_le_log (by positivity) N_le_t