UpperBnd_aux3

lemma UpperBnd_aux3 {A C σ t : ℝ} (hA : A ∈ Ioc 0 (1 / 2))    (σ_ge : 1 - A / Real.log |t| ≤ σ) (t_gt : 3 < |t|) (hC : 2 ≤ C) : let N := ⌊|t|⌋₊;    ‖∑ n ∈ Finset.range (N + 1), (n : ℂ) ^ (-(σ + t * I))‖ ≤      Real.exp A * C * Real.log |t| := by  intro N  obtain ⟨Npos, N_le_t, _, _, σPos, _⟩ := UpperBnd_aux hA t_gt σ_ge  have logt_gt := logt_gt_one t_gt.le  have (n : ℕ) (hn : n ∈ Finset.range (N + 1)) := ZetaBnd_aux2 (n := n) hA.1 σPos ?_ σ_ge  · replace := norm_sum_le_of_le (Finset.range (N + 1)) this    rw [← Finset.sum_mul, mul_comm _ (Real.exp A)] at this    rw [mul_assoc]    apply le_trans this <| (mul_le_mul_iff_right₀ A.exp_pos).mpr ?_    have : 1 + Real.log (N : ℝ) ≤ C * Real.log |t| := by      by_cases hN : N = 1      · simp only [hN, Nat.cast_one, Real.log_one, add_zero]        have : 2 * 1 ≤ C * Real.log |t| := mul_le_mul hC logt_gt.le (by linarith) (by linarith)        linarith      · rw [(by ring : C * Real.log |t| = Real.log |t| + (C - 1) * Real.log |t|),          ← one_mul <| Real.log (N: ℝ)]        apply add_le_add logt_gt.le        refine mul_le_mul (by linarith) ?_ (by positivity) (by linarith)        exact Real.log_le_log (by positivity) N_le_t    refine le_trans ?_ this    convert! harmonic_eq_sum_Icc ▸ harmonic_le_one_add_log N    · simp only [Rat.cast_sum, Rat.cast_inv, Rat.cast_natCast, Finset.range_eq_Ico]      rw [riemannZeta0_zero_aux (N + 1) (by linarith)]; congr! 1  · simp only [Finset.mem_range] at hn    linarith [(by exact_mod_cast (by omega : n ≤ N) : (n : ℝ) ≤ N)]