limiting_fourier_lim1

theorem limiting_fourier_lim1 (hcheby : cheby f) (ψ : W21) (hx : 0 < x) :    Tendsto (fun σ' : ℝ ↦        ∑' n, term f σ' n * 𝓕 (ψ : ℝ → ℂ) (1 / (2 * π) * Real.log (n / x))) (𝓝[>] 1)      (𝓝 (∑' n, f n / n * 𝓕 (ψ : ℝ → ℂ) (1 / (2 * π) * Real.log (n / x)))) := by   obtain ⟨C, hC⟩ := decay_bounds_cor ψ  have : 0 ≤ C := by simpa using (norm_nonneg _).trans (hC 0)  refine tendsto_tsum_of_dominated_convergence    (limiting_fourier_lim1_aux hcheby hx C this) (fun n => ?_) ?_  · apply Tendsto.mul_const    by_cases h : n = 0 <;> simp only [term, h, ↓reduceIte, CharP.cast_eq_zero, div_zero,      tendsto_const_nhds_iff]    refine tendsto_const_nhds.div ?_ (by simp [h])    simpa using ((continuous_ofReal.tendsto 1).mono_left nhdsWithin_le_nhds).const_cpow  · rw [eventually_nhdsWithin_iff]    apply Eventually.of_forall    intro σ' (hσ' : 1 < σ') n    rw [norm_mul, ← nterm_eq_norm_term]    refine mul_le_mul ?_ (hC _) (norm_nonneg _) (div_nonneg (norm_nonneg _) (Nat.cast_nonneg _))    by_cases h : n = 0 <;> simp only [nterm, h, ↓reduceIte, CharP.cast_eq_zero, div_zero, le_refl]    have : 1 ≤ (n : ℝ) := by simpa using! Nat.pos_iff_ne_zero.mpr h    refine div_le_div₀ (norm_nonneg _) le_rfl (by simpa [Nat.pos_iff_ne_zero]) ?_    simpa using Real.rpow_le_rpow_of_exponent_le this hσ'.le