CH2.prop_2_4_minus

@[blueprint  "ch2-prop-2-4-minus"  (title := "CH2 Proposition 2.4, lower 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 $\hat \varphi_-(y) \leq I_\lambda(y)$ for all $y$. Then for any $x\geq 1$ and $\sigma \neq 1$,  $$ S_\sigma(x) \geq \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 := /-- Similar to the proof of Proposition \ref{ch2-prop-2-4-plus}; see \cite[Proposition 2.4]{CH2} for details.  -/)  (latexEnv := "proposition")  (discussion := 883)]theorem prop_2_4_minus {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 })    {φ_minus : ℝ → ℂ} (hφ_mes : Measurable φ_minus) (hφ_int : Integrable φ_minus)    (hφ_cont : ContinuousAt φ_minus 0)    (hφ_supp : ∀ x, x ∉ Set.Icc (-1) 1 → φ_minus x = 0)    (hφ_Fourier : ∃ C : ℝ, ∀ y : ℝ, y ≠ 0 → ‖𝓕 φ_minus y‖ ≤ C / |y| ^ β)    (hFourier_le_I : ∀ y : ℝ,      let lambda := (2 * π * (σ - 1)) / T      (𝓕 φ_minus y).re ≤ I' lambda y)    {x : ℝ} (hx : 1 ≤ x) :    S a σ x ≥      ((2 * π * (x ^ (1 - σ) : ℝ) / T) * φ_minus 0).re +      (x ^ (-σ) : ℝ) / T *        (∫ t in Set.Icc (-T) T, φ_minus (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) * 𝓕 φ_minus ((T / (2 * π)) * log (n / x))) :=    summable_dirichlet_fourier_complex hT hβ ha hφ_Fourier x (zero_lt_one.trans_le hx)  have h_sum_eq : (1 / (2 * π) : ℂ) * ∑' (n : ℕ+), a n * (x / n) * 𝓕 φ_minus ((T / (2 * π)) * log (n / x)) =      (1 / (2 * π * T)) * (∫ t in Set.Icc (-T) T, φ_minus (t / T) * G (1 + t * I) * x ^ (1 + t * I)) +      (φ_minus 0 - ∫ y in Set.Iic (-T * log x / (2 * π)), 𝓕 φ_minus y) * (x / T) :=    prop_2_3 hT hβ ha hG hG' hφ_mes hφ_int hφ_cont hφ_supp hφ_Fourier x (zero_lt_one.trans_le hx)  have h_sum_total : ∑' (n : ℕ+), (a n : ℂ) * (x / n) * 𝓕 φ_minus ((T / (2 * π)) * log (n / x)) =      2 * π * ((1 / (2 * π * T)) * (∫ t in Set.Icc (-T) T, φ_minus (t / T) * G (1 + t * I) * x ^ (1 + t * I)) +      (φ_minus 0 - ∫ y in Set.Iic (-T * log x / (2 * π)), 𝓕 φ_minus y) * (x / T)) := by    rw [← h_sum_eq]    field_simp [Real.pi_pos.ne']    congr 1; ext x; ring_nf  have h_sum_LHS : Summable (fun n : ℕ+ ↦ a n * (x / n) * (𝓕 φ_minus ((T / (2 * π)) * log (n / x))).re) := by    convert h_summable.map Complex.reCLM Complex.reCLM.continuous using 1    ext n; simp  have h_sum_RHS : Summable (fun (n : ℕ+) ↦ a n * (x / n) * I' ((2 * π * (σ - 1)) / T) ((T / (2 * π)) * log (n / x))) :=    summable_I'_residual ha_pos hT hσ ha hx  have h_pointwise : ∀ (n : ℕ+), a n * (x / n) * (𝓕 φ_minus ((T / (2 * π)) * log (n / x))).re ≤      a n * (x / n) * I' ((2 * π * (σ - 1)) / T) ((T / (2 * π)) * log (n / x)) :=    fun n ↦ mul_le_mul_of_nonneg_left (hFourier_le_I ((T / (2 * π)) * log (n / x)))      (mul_nonneg (ha_pos n) (div_nonneg (zero_lt_one.trans_le hx).le (by positivity)))  calc S a σ x    _ = (x ^ (-σ) : ℝ) * ∑' (n : ℕ+), a n * (x / n) * I' ((2 * π * (σ - 1)) / T) ((T / (2 * π)) * log (n / x)) := S_eq_I a σ x T hσ hT (zero_lt_one.trans_le hx)    _ ≥ (x ^ (-σ) : ℝ) * ∑' (n : ℕ+), a n * (x / n) * (𝓕 φ_minus ((T / (2 * π)) * log (n / x))).re :=      ge_iff_le.mpr (mul_le_mul_of_nonneg_left (Summable.tsum_le_tsum h_pointwise h_sum_LHS h_sum_RHS) (by positivity))    _ = (x ^ (-σ) : ℝ) * (∑' (n : ℕ+), (a n : ℂ) * (x / n) * 𝓕 φ_minus ((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, φ_minus (t / T) * G (1 + t * I) * x ^ (1 + t * I)) +        (φ_minus 0 - ∫ y in Set.Iic (-T * log x / (2 * π)), 𝓕 φ_minus y) * (x / T))).re := by rw [h_sum_total]    _ = (((x ^ (-σ) : ℝ) : ℂ) * (2 * π * ((1 / (2 * π * T)) * (∫ t in Set.Icc (-T) T, φ_minus (t / T) * G (1 + t * I) * x ^ (1 + t * I)) +        (φ_minus 0 - ∫ y in Set.Iic (-T * log x / (2 * π)), 𝓕 φ_minus y) * (x / T)))).re := by rw [← Complex.re_ofReal_mul]    _ = (((2 * π * (x ^ (1 - σ) : ℝ) / T) : ℂ) * φ_minus 0).re +        (((x ^ (-σ) / T : ℝ) : ℂ) * (∫ t in Set.Icc (-T) T, φ_minus (t / T) * G (1 + t * I) * x ^ (1 + t * I))).re -        (((2 * π * (x ^ (1 - σ) : ℝ) / T) : ℂ) * (∫ y in Set.Iic (-T * log x / (2 * π)), 𝓕 φ_minus 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) : ℂ) * φ_minus 0).re +        (((x ^ (-σ) / T : ℝ) : ℂ) * (∫ t in Set.Icc (-T) T, φ_minus (t / T) * G (1 + t * I) * x ^ (1 + t * I))).re -        (if σ < 1 then 1 / (1 - σ) else 0) := by      gcongr      exact prop_2_4_minus_fourier_bound hT hβ hσ hφ_int hφ_Fourier (fun y ↦ hFourier_le_I y) x hx    _ ≥ _ := by      gcongr; norm_cast      rw [Complex.re_ofReal_mul]