hardy_tauberian_theorem

theorem hardy_tauberian_theorem (u : ℕ → ℝ) (A : ℝ) (S : ℝ)    (h_conv : Filter.Tendsto (hardy_sigma u) Filter.atTop (nhds S))    (h_bound : ∀ n ≥ 1, |u n| ≤ A / n) :    Filter.Tendsto (hardy_s u) Filter.atTop (nhds S) := by  have hA : 0 ≤ A := by    have := h_bound 1 le_rfl    norm_num at this    exact le_trans (abs_nonneg _) this  apply tendsto_of_approx_aux hA  intro ε hε  let k := hardy_k ε  have hk_pos : ∀ n, 0 < k n := fun n => lt_of_lt_of_le zero_lt_one (le_max_left _ _)  use fun n => hardy_sigma_delayed u n (k n)  constructor  · apply hardy_sigma_delayed_tendsto u S k h_conv (hardy_k_ratio_bounded ε hε) hk_pos  · have := hardy_diff_bound u A ε hε h_bound    filter_upwards [this] with n hn    rw [abs_sub_comm]    exact hn