DerivUpperBnd_aux7

@[blueprint  (title := "DerivUpperBnd-aux7")  (statement := /--  For any $s = \sigma + tI \in \C$, $1/2 \le \sigma\le 2, 3 < |t|$, and any $0 < A < 1$  sufficiently small, and $1-A/\log |t| \le \sigma$, we have  $$  \left\|s \cdot \int_{N}^{\infty}    \left(\left\lfloor x \right\rfloor + \frac{1}{2} - x\right) \cdot x^{-s-1} \cdot (-\log x)  \right\|  \le 2 \cdot |t| \cdot N^{-\sigma} / \sigma \cdot \log |t|.  $$  -/)  (proof := /--  Estimate $|s|= |\sigma + tI|$ by $|s|\le 2 +|t| \le 2|t|$ (since $|t|>3$).  Estimating $|\left\lfloor x \right\rfloor+1/2-x|$ by $1$,  and using $|x^{-s-1}| = x^{-\sigma-1}$, we have  $$  \left\| s \cdot \int_{N}^{\infty}    \left(\left\lfloor x \right\rfloor + \frac{1}{2} - x\right) \cdot x^{-s-1} \cdot (-\log x)  \right\|  \le 2 \cdot |t|  \int_{N}^{\infty} x^{-\sigma} \cdot (\log x).  $$  For the last integral, integrate by parts, getting:  $$  \int_{N}^{\infty} x^{-\sigma-1} \cdot (\log x) =  \frac{1}{\sigma}N^{-\sigma} \cdot \log N + \frac1{\sigma^2} \cdot N^{-\sigma}.  $$  Now use $\log N \le \log |t|$ to get the result.  -/)  (latexEnv := "lemma")]theorem DerivUpperBnd_aux7 {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 < σ →    ‖s * ∫ (x : ℝ) in Ioi (N : ℝ), (↑⌊x⌋ + 1 / 2 - ↑x) * (x : ℂ) ^ (-s - 1) * -↑x.log‖ ≤      6 * |t| * ↑N ^ (-σ) / σ * |t|.log := by  intro N s Npos N_le_t neOne σ_gt  have σpos : 0 < σ := lt_trans (by norm_num) σ_gt  rw [norm_mul, (by ring : 6 * |t| * ↑N ^ (-σ) / σ * Real.log |t| = (2 * |t|) * (3 * ↑N ^ (-σ) / σ * Real.log |t|))]  apply mul_le_mul _ _ (by positivity) (by positivity)  · apply le_trans (by apply norm_add_le)    simp [abs_of_pos σpos]    linarith [hσ.2]  apply le_trans (by apply norm_integral_le_integral_norm)  calc ∫ (x : ℝ) in Ioi (N : ℝ), ‖(↑⌊x⌋ + 1 / 2 - ↑x) * (x : ℂ) ^ (-s - 1) * -↑x.log‖    _ = ∫ (x : ℝ) in Ioi (N : ℝ), |(↑⌊x⌋ + 1 / 2 - x)| * x ^ (-σ - 1) * x.log := by      apply setIntegral_congr_fun (by measurability)      intro x hx      simp only [mem_Ioi] at hx      exact DerivUpperBnd_aux7_1 (lt_of_le_of_lt (mod_cast Npos) hx).le    _ ≤ ∫ (x : ℝ) in Ioi (N : ℝ), x ^ (-σ - 1) * x.log := by      apply setIntegral_mono_on _ _ (by measurability)      · intro x hx        exact DerivUpperBnd_aux7_2 (lt_of_le_of_lt (mod_cast Npos) hx).le      · apply DerivUpperBnd_aux7_5 σpos (mod_cast Npos)      apply DerivUpperBnd_aux7_4 σpos (mod_cast Npos)    _ = 1 / σ^2 * N ^ (-σ) + 1 / σ * N ^ (-σ) * Real.log N :=      DerivUpperBnd_aux7_integral_eq (mod_cast Npos) σpos    _ ≤ 3 * ↑N ^ (-σ) / σ * |t|.log := by      have h2 : 1 / σ * ↑N ^ (-σ) * Real.log ↑N ≤ ↑N ^ (-σ) / σ * Real.log |t| := calc        _ = ↑N ^ (-σ) / σ * Real.log N := by ring        _ ≤ _ := by          apply mul_le_mul_of_nonneg_left _ (by positivity)          exact Real.log_le_log (mod_cast Npos) N_le_t      have : 2 ≤ 2 * Real.log |t| := by        nth_rewrite 1  [← mul_one 2]        apply mul_le_mul_of_nonneg_left _ (by norm_num)        exact logt_gt_one t_gt.le |>.le      have h1 : 1 / σ^2 * ↑N ^ (-σ) ≤ 2 * ↑N ^ (-σ) / σ * Real.log |t| := calc        1 / σ^2 * ↑N ^ (-σ) = (↑N ^ (-σ) / σ) * (1 / σ) := by ring        _ ≤ ↑N ^ (-σ) / σ * (2 * Real.log |t|):= by          apply mul_le_mul_of_nonneg_left _ (by positivity)          apply le_trans _ this          exact (one_div_le σpos (by norm_num)).mpr σ_gt.le        _ = _ := by ring      convert! add_le_add h1 h2 using 1      ring