ZetaBnd_aux2

@[blueprint  (title := "ZetaBnd-aux2")  (statement := /--  Given $n ≤ t$ and $\sigma$ with $1-A/\log t \le \sigma$, we have  that  $$  |n^{-s}| \le n^{-1} e^A.  $$  -/)  (proof := /--  Use $|n^{-s}| = n^{-\sigma}  = e^{-\sigma \log n}  \le  \exp(-\left(1-\frac{A}{\log t}\right)\log n)  \le  n^{-1} e^A$,  since $n\le t$.  -/)  (latexEnv := "lemma")]lemma ZetaBnd_aux2 {n : ℕ} {t A σ : ℝ} (Apos : 0 < A) (σpos : 0 < σ) (n_le_t : n ≤ |t|)    (σ_ge : (1 : ℝ) - A / Real.log |t| ≤ σ) :    ‖(n : ℂ) ^ (-(σ + t * I))‖ ≤ (n : ℝ)⁻¹ * Real.exp A := by  set s := σ + t * I  by_cases n0 : n = 0  · simp_rw [n0, CharP.cast_eq_zero, inv_zero, zero_mul]    rw [Complex.zero_cpow ?_]    · simp    · exact fun h ↦ σpos.ne' <| zero_eq_neg.mp <| zero_re ▸ h ▸ (by simp [s])  have n_gt_0 : 0 < n := Nat.pos_of_ne_zero n0  have n_gt_0' : (0 : ℝ) < (n : ℝ) := Nat.cast_pos.mpr n_gt_0  have n_ge_1 : 1 ≤ (n : ℝ) := Nat.one_le_cast.mpr <| Nat.succ_le_of_lt n_gt_0  calc    _ = |((n : ℝ) ^ (-σ))| := ?_    _ ≤ Real.exp (Real.log n * -σ) := Real.abs_rpow_le_exp_log_mul (n : ℝ) (-σ)    _ ≤ Real.exp (Real.log n *  -(1 - A / Real.log t)) := ?_    _ ≤ Real.exp (- Real.log n + A) := Real.exp_le_exp_of_le ?_    _ ≤ _ := by rw [Real.exp_add, Real.exp_neg, Real.exp_log n_gt_0']  · have : ‖(n : ℂ) ^ (-s)‖ = n ^ (-s.re) := norm_cpow_eq_rpow_re_of_pos n_gt_0' (-s)    rw [this, abs_eq_self.mpr <| Real.rpow_nonneg n_gt_0'.le _]; simp [s]  · apply Real.exp_le_exp_of_le <| mul_le_mul_of_nonneg_left _ <| Real.log_nonneg n_ge_1    rw [neg_sub, neg_le_sub_iff_le_add, add_comm, ← Real.log_abs]; linarith  · simp only [neg_sub, le_neg_add_iff_add_le]    ring_nf    conv => rw [mul_comm, ← mul_assoc, ← Real.log_abs]; rhs; rw [← one_mul A]    gcongr    by_cases ht1 : |t| = 1    · simp [ht1]    apply (inv_mul_le_iff₀ ?_).mpr    · convert! Real.log_le_log n_gt_0' n_le_t using 1; rw [mul_one]    · exact Real.log_pos <| lt_of_le_of_ne (le_trans n_ge_1 n_le_t) <| fun t ↦ ht1 (t.symm)