CH2.prop_2_3_1

@[blueprint  "ch2-prop-2-3-1"  (title := "CH2 Proposition 2.3, substep 1")  (statement := /--  Let $a_n$ be a sequence with $\sum_{n>1} \frac{|a_n|}{n \log^\beta n} < \infty$ for some $\beta > 1$.  Write $G(s)= \sum_n a_n n^{-s} - \frac{1}{s-1}$ for $\mathrm{Re} s > 1$.  Let $\varphi$ be absolutely integrable, supported on $[-1,1]$, and has Fourier decay $\hat \psi(y) = O(1/|y|^\beta)$.  Then for any $x>0$ and $\sigma > 1$  $$ \frac{1}{2\pi} \sum a_n \frac{x}{n^\sigma} \hat \psi(\frac{T}{2\pi} \log \frac{n}{x} ) = \frac{1}{2\pi T} \int_{-T}^{T} \varphi(\frac{t}{T}) G(\sigma+it) x^{it}\ dt + \int_{-T \log x/2\pi}^\infty e^{-y(\sigma-1)} \hat \varphi(y)\ dy) \frac{x^{2-\sigma}}{T}.$$  -/)  (proof := /-- Use Lemma \ref{first-fourier} and Lemma \ref{second-fourier}, similar to the proof of `limiting\_fourier\_aux`.  -/)  (latexEnv := "sublemma")  (discussion := 879)]theorem prop_2_3_1 {a : ℕ → ℂ} {T β : ℝ} (hT : 0 < T) (_hβ : 1 < β)    (ha : Summable (fun n ↦ ‖a n‖ / (n * log n ^ β)))    {G : ℂ → ℂ}    (hG' : Set.EqOn G (fun s ↦ LSeries a s - 1 / (s - 1)) { z | z.re > 1 })    {φ : ℝ → ℂ} (hφ_mes : Measurable φ) (hφ_int : Integrable φ)    (hφ_supp : ∀ x, x ∉ Set.Icc (-1) 1 → φ x = 0) -- this hypothesis may be unnecessary    (_hφ_Fourier : ∃ C : ℝ, ∀ y : ℝ, y ≠ 0 → ‖𝓕 φ y‖ ≤ C / |y| ^ β)    (x sig : ℝ) (hx : 0 < x) (hsig : 1 < sig) :    (1 / (2 * π)) * ∑' (n : ℕ), (x : ℂ) * LSeries.term a sig n *      𝓕 φ ((T / (2 * π)) * log (n / x)) =      (1 / (2 * π * T)) *        (∫ t in Set.Icc (-T) T, φ (t / T) * G (sig + t * I) * x ^ (1 + t * I)) +      (x ^ (2 - sig) / (2 * π * T) : ℝ) *        (∫ u in Set.Ici (-log x), Real.exp (-u * (sig - 1)) *          𝓕 (fun t : ℝ ↦ φ (t / T)) (u / (2 * π))) := by  let phiScaled : ℝ → ℂ := fun t => φ (t / T)  have hphiScaled_meas : Measurable phiScaled := by simp only [phiScaled]; fun_prop  have hphiScaled_int : Integrable phiScaled :=    (MeasureTheory.integrable_comp_mul_right_iff (g := φ) (inv_ne_zero hT.ne')).2 hφ_int |>.congr      (by simp [phiScaled, div_eq_mul_inv])  have hsummable : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm a σ') :=    fun σ' hσ' => summable_nterm_of_log_weight hσ' ha  have hfirst := @first_fourier x sig phiScaled a hsummable hphiScaled_int hx hsig  have hsecond := @second_fourier phiScaled hphiScaled_meas hphiScaled_int x sig hx hsig  have hxpow (t : ℝ) : ‖(x : ℂ) ^ (t * I)‖ = 1 := by    rw [Complex.norm_cpow_eq_rpow_re_of_pos hx]; simp  let C0 : ℝ := ∑' n : ℕ, nterm a sig n  have hC0_nonneg : 0 ≤ C0 := tsum_nonneg fun n => by    by_cases hn : n = 0 <;> simp [nterm, hn, div_nonneg, Real.rpow_nonneg]  have hLS_bound (t : ℝ) : ‖LSeries a (sig + t * I)‖ ≤ C0 := by    have hs_term : Summable (fun n : ℕ => ‖LSeries.term a (sig + t * I) n‖) := by      convert hsummable sig hsig with n; simp [norm_term_eq_nterm_re]    exact (norm_tsum_le_tsum_norm hs_term).trans (by simp [C0, norm_term_eq_nterm_re])  have hLS_aesm : AEStronglyMeasurable (fun t : ℝ ↦ LSeries a (sig + t * I) * phiScaled t * x ^ (t * I)) :=    (((continuous_LSeries_aux (hsummable sig hsig)).measurable.mul hphiScaled_meas).mul      (continuous_const.cpow (continuous_ofReal.mul continuous_const) (by simp [hx])).measurable).aestronglyMeasurable  have hLS_int : Integrable (fun t : ℝ ↦ LSeries a (sig + t * I) * phiScaled t * x ^ (t * I)) :=    .mono' (hphiScaled_int.norm.const_mul C0) hLS_aesm (.of_forall fun t => by      simp only [norm_mul, mul_assoc, hxpow, mul_one]      exact mul_le_mul_of_nonneg_right (hLS_bound t) (norm_nonneg _))  have hPole_denom_ne (t : ℝ) : sig + t * I - 1 ≠ 0 := by    intro h; have := congrArg Complex.re h; simp at this; linarith  have hPole_bound (t : ℝ) : ‖1 / (sig + t * I - 1)‖ ≤ (sig - 1)⁻¹ := by    have hσpos : 0 < sig - 1 := sub_pos.mpr hsig    simpa [norm_div, one_div] using one_div_le_one_div_of_le hσpos      (by simpa [abs_of_pos hσpos] using Complex.abs_re_le_norm (sig + t * I - 1))  have hcontX : Continuous (fun t : ℝ => (x : ℂ) ^ (t * I)) :=    continuous_const.cpow (continuous_ofReal.mul continuous_const) (by simp [hx])  have hPole_aesm :      AEStronglyMeasurable (fun t : ℝ ↦ (1 / (sig + t * I - 1)) * phiScaled t * x ^ (t * I)) :=    (((by simpa [one_div, Pi.inv_def] using Continuous.inv₀ (by fun_prop) (hPole_denom_ne) :      Continuous (fun t : ℝ => (1 / (sig + t * I - 1) : ℂ))).measurable.mul hphiScaled_meas).mul        hcontX.measurable).aestronglyMeasurable  have hPole_int : Integrable (fun t : ℝ ↦ (1 / (sig + t * I - 1)) * phiScaled t * x ^ (t * I)) :=    .mono' (hphiScaled_int.norm.const_mul (sig - 1)⁻¹) hPole_aesm (.of_forall fun t => by      simp only [norm_mul, mul_assoc, hxpow, mul_one]      exact mul_le_mul_of_nonneg_right (hPole_bound t) (norm_nonneg _))  have hG_rewrite :      ∫ t : ℝ, phiScaled t * G (sig + t * I) * x ^ (t * I) =        (∫ t : ℝ, LSeries a (sig + t * I) * phiScaled t * x ^ (t * I)) -          ∫ t : ℝ, (1 / (sig + t * I - 1)) * phiScaled t * x ^ (t * I) := by    rw [← integral_sub hLS_int hPole_int]; congr 1; ext t    rw [hG' (by simp [hsig] : (sig + t * I).re > 1)]; ring  have hIcc_to_univ :      ∫ t in Set.Icc (-T) T, φ (t / T) * G (sig + t * I) * x ^ (1 + t * I) =        ∫ t : ℝ, φ (t / T) * G (sig + t * I) * x ^ (1 + t * I) := by    rw [← integral_indicator measurableSet_Icc]    refine integral_congr_ae (.of_forall fun t => ?_)    by_cases ht : t ∈ Set.Icc (-T) T    · simp [ht]    · simp [ht, hφ_supp _ (show t / T ∉ Set.Icc (-1) 1 from by        intro ⟨h1, h2⟩; exact ht ⟨by linarith [(le_div_iff₀ hT).mp h1],          by linarith [(div_le_iff₀ hT).mp h2]⟩)]  have hG_with_x :      (1 / (2 * π * T)) *          ∫ t : ℝ, φ (t / T) * G (sig + t * I) * x ^ (1 + t * I) =        (x / (2 * π * T) : ℂ) *          ((∫ t : ℝ, LSeries a (sig + t * I) * phiScaled t * x ^ (t * I)) -            ∫ t : ℝ, (1 / (sig + t * I - 1)) * phiScaled t * x ^ (t * I)) := by    have hcpow (t : ℝ) : (x : ℂ) ^ (1 + ↑t * I) = x * x ^ (↑t * I) := by      rw [Complex.cpow_add (x := (x : ℂ)) (y := (1 : ℂ)) (z := t * I)        (by exact_mod_cast hx.ne')]; simp    simp_rw [show ∀ t : ℝ, φ (t / T) * G (sig + t * I) * x ^ (1 + ↑t * I) =        (x : ℂ) * (phiScaled t * G (sig + t * I) * x ^ (↑t * I)) from      fun t => by rw [hcpow]; simp only [phiScaled]; ring]    rw [show (∫ (t : ℝ), (x : ℂ) * (phiScaled t * G (sig + t * I) * x ^ (↑t * I))) =        (x : ℂ) * ∫ (t : ℝ), phiScaled t * G (sig + t * I) * x ^ (↑t * I) from      MeasureTheory.integral_const_mul _ _]    simp_rw [hG_rewrite]; ring  have hPole_from_second :      (x ^ (2 - sig) / (2 * π * T) : ℝ) * ∫ u in Set.Ici (-log x),          Real.exp (-u * (sig - 1)) * 𝓕 phiScaled (u / (2 * π)) =        (x / (2 * π * T) : ℂ) *          ∫ t : ℝ, (1 / (sig + t * I - 1)) * phiScaled t * x ^ (t * I) := by    have hpowx : (x ^ (2 - sig) * x ^ (sig - 1) : ℝ) = x := by      rw [← Real.rpow_add hx]; norm_num    calc (x ^ (2 - sig) / (2 * π * T) : ℝ) * ∫ u in Set.Ici (-log x),            Real.exp (-u * (sig - 1)) * 𝓕 phiScaled (u / (2 * π))        _ = ((x ^ (2 - sig) / (2 * π * T) * x ^ (sig - 1) : ℝ) : ℂ) *              ∫ t : ℝ, (1 / (sig + t * I - 1)) * phiScaled t * x ^ (t * I) := by            rw [hsecond]; push_cast; ring        _ = _ := by rw [show (x ^ (2 - sig) / (2 * π * T) * x ^ (sig - 1) : ℝ) = x / (2 * π * T)              from by rw [div_mul_eq_mul_div, hpowx]]; simp  have hleft_scale :      (1 / (2 * π)) * ∑' n : ℕ, (x : ℂ) * LSeries.term a sig n * 𝓕 φ ((T / (2 * π)) * log (n / x)) =        (x / (2 * π * T) : ℂ) *          ∑' n : ℕ, LSeries.term a sig n * 𝓕 phiScaled ((1 / (2 * π)) * log (n / x)) := by    have hS : ∑' n : ℕ, LSeries.term a sig n * 𝓕 phiScaled ((1 / (2 * π)) * log (n / x)) =        (T : ℂ) * ∑' n : ℕ, LSeries.term a sig n * 𝓕 φ (T * ((1 / (2 * π)) * log (n / x))) := by      rw [← tsum_mul_left]; congr with n      simpa [phiScaled, mul_assoc, mul_left_comm, mul_comm] using        congrArg (fun z : ℂ => LSeries.term a sig n * z)          (fourier_scale_div_noscalar φ T ((1 / (2 * π)) * log (↑n / x)) hT)    simp_rw [hS, ← tsum_mul_left]; field_simp [hT.ne']  rw [hleft_scale, hfirst]  rw [show (x / (2 * π * T) : ℂ) * ∫ t : ℝ, LSeries a (sig + t * I) * phiScaled t * x ^ (t * I) =      (x / (2 * π * T) : ℂ) * ((∫ t : ℝ, LSeries a (sig + t * I) * phiScaled t * x ^ (t * I)) -        ∫ t : ℝ, (1 / (sig + t * I - 1)) * phiScaled t * x ^ (t * I)) +      (x / (2 * π * T) : ℂ) * ∫ t : ℝ, (1 / (sig + t * I - 1)) * phiScaled t * x ^ (t * I) from    by rw [mul_sub, sub_add_cancel]]  rw [← hG_with_x, ← hIcc_to_univ, ← hPole_from_second]