auto_cheby_fourier_summable

lemma auto_cheby_fourier_summable (hpos : 0 ≤ f) (hf : ∀ σ', 1 < σ' → Summable (nterm f σ'))    (hG : ContinuousOn G {s | 1 ≤ s.re})    (hG' : Set.EqOn G (fun s ↦ LSeries f s - A / (s - 1)) {s | 1 < s.re})    (ψ : ℝ → ℂ) (hψSmooth : ContDiff ℝ ∞ ψ) (hψCompact : HasCompactSupport ψ)    (hψpos : ∀ y, 0 ≤ (𝓕 ψ y).re ∧ (𝓕 ψ y).im = 0) (x : ℝ) (hx : 1 ≤ x) :    Summable fun n ↦ (f n : ℂ) / n * 𝓕 ψ (1 / (2 * π) * Real.log (n / x)) := by  let ψCS : CS 2 ℂ := ⟨ψ, hψSmooth.of_le (by norm_cast), hψCompact⟩  let S : ℝ → ℂ := fun σ' ↦ ∑' n, term (f · : ℕ → ℂ) σ' n * 𝓕 ψCS.toFun (1 / (2 * π) * Real.log (n / x))  let Pole : ℝ → ℂ := fun σ' ↦ (A : ℂ) * (x ^ (1 - σ') : ℝ) *    ∫ u in Set.Ici (-Real.log x), (rexp (-u * (σ' - 1)) : ℂ) * 𝓕 (W21.ofCS2 ψCS).toFun (u / (2 * π))  let RHS : ℝ → ℂ := fun σ' ↦ ∫ t : ℝ, G (σ' + t * I) * ψCS.toFun t * (x : ℂ) ^ (t * I)  have l2 := limiting_fourier_lim2 (A := A) (x := x) ψCS hx  have l3 := limiting_fourier_lim3 (G := G) hG ψCS hx  have haux : (fun σ' ↦ S σ' - Pole σ') =ᶠ[𝓝[>] 1] RHS := eventually_nhdsWithin_of_forall fun σ' hσ' ↦ by    simpa [S, Pole, RHS] using! limiting_fourier_aux hG' hf ψCS hx σ' hσ'  have hS_tendsto : Tendsto S (𝓝[>] 1) (𝓝 (RHS 1 + A * ∫ u in Set.Ici (-Real.log x),      𝓕 (W21.ofCS2 ψCS).toFun (u / (2 * π)))) := by    convert! (l3.congr' haux.symm).add l2 using 1; ext σ'; simp [S, Pole]  have hbounded : BoundedAtFilter (𝓝[>] 1) (fun σ' ↦ ‖S σ'‖) := by    simp only [BoundedAtFilter]    let L := ‖RHS 1 + A * ∫ u in Set.Ici (-Real.log x), 𝓕 (W21.ofCS2 ψCS).toFun (u / (2 * π))‖    have : ∀ᶠ σ' in 𝓝[>] 1, ‖S σ'‖ < L + 1 :=      hS_tendsto.norm.eventually_lt tendsto_const_nhds (lt_add_one L)    exact Asymptotics.IsBigO.of_bound (L + 1) (by filter_upwards [this] with σ h; simpa using h.le)  let y : ℕ → ℝ := fun n ↦ (1 / (2 * π)) * Real.log (n / x)  let w : ℕ → ℝ := fun n ↦ (𝓕 ψCS.toFun (y n)).re  have hw : ∀ n, 0 ≤ w n := fun n ↦ (hψpos (y n)).1  let rt : ℝ → ℕ → ℝ := fun σ n ↦ if n = 0 then 0 else f n / (n : ℝ) ^ σ * w n  have rt_nn σ n : 0 ≤ rt σ n := by    simp only [rt]; split_ifs with hn    · rfl    · exact mul_nonneg (div_nonneg (hpos n) (Real.rpow_pos_of_pos (Nat.cast_pos.mpr        (Nat.pos_of_ne_zero hn)) σ).le) (hw n)  have hS_eq σ' (hσ' : 1 < σ') : S σ' = ↑(∑' n, rt σ' n) := by    rw [Complex.ofReal_tsum]; apply tsum_congr; intro n    simp only [rt, term, LSeries.term, y, w, one_div, mul_inv_rev]    split_ifs with hn <;> simp only [hn, CharP.cast_eq_zero, Complex.ofReal_zero, zero_mul,      Complex.ofReal_mul, Complex.ofReal_div]    rw [Complex.ofReal_cpow (Nat.cast_nonneg n)]; congr 1    exact Complex.ext rfl (hψpos _).2  have hMono n : AntitoneOn (fun σ ↦ rt σ n) (Set.Ioi 1) := fun σ₁ _ σ₂ _ h ↦ by    simp only [rt]; split_ifs with hn; · rfl    apply mul_le_mul_of_nonneg_right _ (hw n)    apply div_le_div_of_nonneg_left (hpos n) (Real.rpow_pos_of_pos (Nat.cast_pos.mpr      (Nat.pos_of_ne_zero hn)) σ₁)    exact Real.rpow_le_rpow_of_exponent_le (Nat.one_le_cast.mpr (Nat.pos_of_ne_zero hn)) h  have hT_bdd : BoundedAtFilter (𝓝[>] 1) fun σ ↦ ∑' n, rt σ n := by    rw [BoundedAtFilter, Asymptotics.isBigO_iff] at hbounded ⊢    obtain ⟨C, hC⟩ := hbounded    refine ⟨C, ?_⟩    filter_upwards [hC, self_mem_nhdsWithin] with σ hnorm hσ    rw [hS_eq σ hσ] at hnorm; simpa using hnorm  have hSumm σ (hσ : 1 < σ) : Summable (rt σ ·) := by    simpa [rt, w, y] using limiting_fourier_variant_lim1_aux ψCS hpos hf hψpos σ hσ  have hSumm_1 : Summable (rt 1 ·) := by    let σ_seq : ℕ → ℝ := fun k ↦ 1 + 1 / ((k : ℝ) + 1)    have hσ_gt k : 1 < σ_seq k := by simp only [σ_seq, lt_add_iff_pos_right, one_div]; positivity    have h_tendsto : Tendsto σ_seq atTop (𝓝[>] 1) := by      rw [tendsto_nhdsWithin_iff]      refine ⟨?_, by filter_upwards with k; exact hσ_gt k⟩      have : Tendsto (fun k : ℕ ↦ 1 / ((k : ℝ) + 1)) atTop (𝓝 0) := by        simp only [one_div]; exact (tendsto_natCast_atTop_atTop.atTop_add tendsto_const_nhds).inv_tendsto_atTop      simpa [σ_seq] using tendsto_const_nhds.add this    have h_ptwise n : Tendsto (fun k ↦ rt (σ_seq k) n) atTop (𝓝 (rt 1 n)) := by      simp only [rt]; split_ifs with hn; · exact tendsto_const_nhds      refine ((tendsto_const_nhds.rpow (tendsto_nhdsWithin_iff.mp h_tendsto).1 (Or.inl ?_)).inv₀        (by simp [hn])).const_mul (f n) |>.mul_const (w n)      exact (Nat.cast_pos.mpr (Nat.pos_of_ne_zero hn)).ne'    obtain ⟨C, hC⟩ := Asymptotics.isBigO_iff.mp (hT_bdd.comp_tendsto h_tendsto)    refine summable_of_sum_range_le (c := C) (rt_nn 1) fun m ↦ le_of_tendsto (tendsto_finsetSum _        fun i _ ↦ h_ptwise i) ?_    filter_upwards [h_tendsto.eventually self_mem_nhdsWithin, hC] with k hk hCk    calc ∑ i ∈ Finset.range m, rt (σ_seq k) i        ≤ ∑' n, rt (σ_seq k) n := (hSumm _ hk).sum_le_tsum _ fun n _ ↦ rt_nn _ n      _ ≤ |∑' n, rt (σ_seq k) n| := le_abs_self _      _ ≤ C := by simpa using hCk  rw [show (fun n ↦ (f n : ℂ) / n * 𝓕 ψ (1 / (2 * π) * Real.log (n / x))) =      Complex.ofRealCLM ∘ (rt 1 ·) from ?_]  · exact hSumm_1.map Complex.ofRealCLM Complex.ofRealCLM.continuous  ext n; simp only [rt, Real.rpow_one, one_div, w, y, Function.comp_apply]  split_ifs with hn; · simp [hn]  have him0 : (𝓕 ψCS.toFun ((2 * π)⁻¹ * Real.log (n / x))).im = 0 := (hψpos _).2  have hre_eq : 𝓕 ψCS.toFun ((2 * π)⁻¹ * Real.log (n / x)) =      Complex.ofReal ((𝓕 ψCS.toFun ((2 * π)⁻¹ * Real.log (n / x))).re) := by    rw [← Complex.re_add_im (𝓕 ψCS.toFun _), him0]; simp  conv_lhs => rw [show ψ = ψCS.toFun from rfl, hre_eq]  simp only [Complex.ofRealCLM_apply, Complex.ofReal_div, Complex.ofReal_mul, Complex.ofReal_natCast]