CH2.prop_2_4_plus

@[blueprint  "ch2-prop-2-4-plus"  (title := "CH2 Proposition 2.4, upper bound")  (statement := /--  Let $a_n$ be a non-negative sequence with $\sum_{n>1} \frac{|a_n|}{n \log^\beta n} < \infty$ for some $\beta > 1$.  Assume that $\sum_n a_n n^{-s} - \frac{1}{s-1}$ extends continuously to a function $G$ defined on $1 + i[-T,T]$.  Let $\varphi_+$ be absolutely integrable, supported on $[-1,1]$, and has Fourier decay $\hat \varphi_+(y) = O(1/|y|^\beta)$.  Let $\sigma \neq 1$ and write $\lambda = 2\pi(\sigma-1)/T$.  Assume $I_\lambda(y) \leq \hat \varphi_+(y)$ for all $y$. Then for any $x\geq 1$,  $$ S_\sigma(x) \leq \frac{2\pi x^{1-\sigma}}{T} \varphi_+(0) + \frac{x^{-\sigma}}{T} \int_{-T}^T \varphi_+(t/T) G(1+it) x^{1+it}\ dt - \frac{1_{(-\infty,1)}(\sigma)}{1-\sigma}.$$  -/)  (proof := /-- By the nonnegativity of $a_n$ we have  $$ S_\sigma(x) \leq x^{-\sigma} \sum_n a_n \frac{x}{n} \hat \varphi_+(\frac{T}{2\pi} \log \frac{n}{x} ).$$  By Proposition \ref{ch2-prop-2-3} we can express the right-hand side as  $$ \frac{1}{2\pi i T} \int_{1-iT}^{1+iT} \varphi_+(\frac{s-1}{iT}) G(s) x^{s}\ ds + (\varphi_+(0) - \int_{-\infty}^{-T \log x/2\pi} \hat \varphi_+(y)\ dy) \frac{x}{T}.$$  If $\lambda > 0$, then $I_\lambda(y)=0$ for negative $y$, so  $$ -\int_{-\infty}^{-T \log x/2π} \hat \varphi_+(y)\ dy \leq 0.$$  If $\lambda < 0$, then $I_\lambda(y)=e^{-\lambda y}$ for $y$ negative, so$$ -\int_{-\infty}^{-T \log x/2π} I_\lambda(y)\ dy \leq e^{\lambda T \log x/2π}/(-\lambda) = x^{\sigma-1}/(-\lambda).$$hence$$ -\int_{-\infty}^{-T \log x/2π} \hat \varphi_+(y)\ dy \leq - x^{\sigma-1}/(-\lambda).$$Since $x^{-\sigma} * (2\pi x / T) * x^{\sigma-1}/(-\lambda) = 1/(1-\sigma)$, the result follows.  -/)  (latexEnv := "proposition")  (discussion := 882)]theorem prop_2_4_plus {a : ℕ → ℝ} (ha_pos : ∀ n, a n ≥ 0) {T β σ : ℝ} (hT : 0 < T) (hβ : 1 < β) (hσ : σ ≠ 1)    (ha : Summable (fun n : ℕ ↦ ‖(a n : ℂ)‖ / (n * log n ^ β)))    {G : ℂ → ℂ} (hG : ContinuousOn G { z | z.re ≥ 1 ∧ z.im ∈ Set.Icc (-T) T })    (hG' : Set.EqOn G (fun s ↦ ∑' n, a n / (n ^ s : ℂ) - 1 / (s - 1)) { z | z.re > 1 })    {φ_plus : ℝ → ℂ} (hφ_mes : Measurable φ_plus) (hφ_int : Integrable φ_plus)    (hφ_cont : ContinuousAt φ_plus 0)    (hφ_supp : ∀ x, x ∉ Set.Icc (-1) 1 → φ_plus x = 0)    (hφ_Fourier : ∃ C : ℝ, ∀ y : ℝ, y ≠ 0 → ‖𝓕 φ_plus y‖ ≤ C / |y| ^ β)    (hI_le_Fourier : ∀ y : ℝ,      let lambda := (2 * π * (σ - 1)) / T      I' lambda y ≤ (𝓕 φ_plus y).re)    (x : ℝ) (hx : 1 ≤ x) :    S a σ x ≤      ((2 * π * (x ^ (1 - σ) : ℝ) / T) * φ_plus 0).re +      (x ^ (-σ) : ℝ) / T *        (∫ t in Set.Icc (-T) T, φ_plus (t/T) * G (1 + t * I) * (x ^ (1 + t * I))).re -      if σ < 1 then 1 / (1 - σ) else 0 := by  have h_summable : Summable (fun n : ℕ+ ↦ (a n : ℂ) * (x / n) * 𝓕 φ_plus ((T / (2 * π)) * log (n / x))) :=    summable_dirichlet_fourier_complex hT hβ ha hφ_Fourier x (zero_lt_one.trans_le hx)  have h_sum_RHS : Summable (fun n : ℕ+ ↦ a n * (x / n) * (𝓕 φ_plus ((T / (2 * π)) * log (n / x))).re) := by    convert h_summable.map Complex.reCLM Complex.reCLM.continuous using 1    ext n    norm_cast    simp only [Function.comp_apply, Complex.reCLM_apply, Complex.mul_re, Complex.ofReal_re,      Complex.ofReal_im, zero_mul, sub_zero]  have h_pointwise : ∀ (n : ℕ+), a n * (x / n) * I' ((2 * π * (σ - 1)) / T) ((T / (2 * π)) * log (n / x)) ≤      a n * (x / n) * (𝓕 φ_plus ((T / (2 * π)) * log (n / x))).re := by    intro n    apply mul_le_mul_of_nonneg_left    · exact hI_le_Fourier ((T / (2 * π)) * log (n / x))    · exact mul_nonneg (ha_pos _) (by positivity)  have h_sum_LHS : Summable (fun (n : ℕ+) ↦ a n * (x / n) * I' ((2 * π * (σ - 1)) / T) ((T / (2 * π)) * log (n / x))) := by    apply Summable.of_nonneg_of_le    · intro n      apply mul_nonneg (mul_nonneg (ha_pos _) (div_nonneg (zero_le_one.trans hx) (by positivity)))      unfold I'; split_ifs <;> positivity    · exact h_pointwise    · exact h_sum_RHS  have h_sum_total : ∑' (n : ℕ+), (a n : ℂ) * (x / n) * 𝓕 φ_plus ((T / (2 * π)) * log (n / x)) =      2 * π * ((1 / (2 * π * T)) * (∫ t in Set.Icc (-T) T, φ_plus (t / T) * G (1 + t * I) * x ^ (1 + t * I)) +      (φ_plus 0 - ∫ y in Set.Iic (-T * log x / (2 * π)), 𝓕 φ_plus y) * (x / T)) := by    have h_sum_eq := prop_2_3 hT hβ ha hG hG' hφ_mes hφ_int hφ_cont hφ_supp hφ_Fourier x (by positivity)    rw [← h_sum_eq]    field_simp [Real.pi_pos.ne']    congr 1    ext x; ring_nf  calc S a σ x    _ ≤ (x ^ (-σ) : ℝ) * ∑' (n : ℕ+), a n * (x / n) * (𝓕 φ_plus ((T / (2 * π)) * log (n / x))).re := by      rw [S_eq_I a σ x T hσ hT (by linarith [hx])]      apply mul_le_mul_of_nonneg_left      · exact Summable.tsum_le_tsum h_pointwise h_sum_LHS h_sum_RHS      · positivity    _ = (x ^ (-σ) : ℝ) * (∑' (n : ℕ+), (a n : ℂ) * (x / n) * 𝓕 φ_plus ((T / (2 * π)) * log (n / x))).re := by      rw [Complex.re_tsum h_summable]      congr with n      ring_nf; simp    _ = (x ^ (-σ) : ℝ) * (2 * π * ((1 / (2 * π * T)) * (∫ t in Set.Icc (-T) T, φ_plus (t / T) * G (1 + t * I) * x ^ (1 + t * I)) +        (φ_plus 0 - ∫ y in Set.Iic (-T * log x / (2 * π)), 𝓕 φ_plus y) * (x / T))).re := by rw [h_sum_total]    _ = (((x ^ (-σ) : ℝ) : ℂ) * (2 * π * ((1 / (2 * π * T)) * (∫ t in Set.Icc (-T) T, φ_plus (t / T) * G (1 + t * I) * x ^ (1 + t * I)) +        (φ_plus 0 - ∫ y in Set.Iic (-T * log x / (2 * π)), 𝓕 φ_plus y) * (x / T)))).re := by rw [← Complex.re_ofReal_mul]    _ = (((2 * π * (x ^ (1 - σ) : ℝ) / T) : ℂ) * φ_plus 0).re +        (((x ^ (-σ) / T : ℝ) : ℂ) * (∫ t in Set.Icc (-T) T, φ_plus (t / T) * G (1 + t * I) * x ^ (1 + t * I))).re -        (((2 * π * (x ^ (1 - σ) : ℝ) / T) : ℂ) * (∫ y in Set.Iic (-T * log x / (2 * π)), 𝓕 φ_plus y)).re := by      rw [complex_residual_algebraic_identity (zero_lt_one.trans_le hx) hT.ne']      simp only [Complex.add_re, Complex.sub_re]    _ ≤ (((2 * π * (x ^ (1 - σ) : ℝ) / T) : ℂ) * φ_plus 0).re +        (((x ^ (-σ) / T : ℝ) : ℂ) * (∫ t in Set.Icc (-T) T, φ_plus (t / T) * G (1 + t * I) * x ^ (1 + t * I))).re -        (if σ < 1 then 1 / (1 - σ) else 0) := by      gcongr      exact prop_2_4_plus_fourier_bound hT hβ hσ hφ_int hφ_Fourier hI_le_Fourier x hx    _ ≤ _ := by      gcongr; norm_cast      rw [Complex.re_ofReal_mul]