hardy_tauberian

theorem hardy_tauberian (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      convert tendsto_of_approx_aux _ _;      exact |A| + 1;      · positivity;      · intro ε hε        use fun n => hardy_sigma_delayed u n (hardy_k ε n);        constructor;        · convert hardy_sigma_delayed_tendsto u S ( fun n => hardy_k ε n ) h_conv _ _ using 1;          · convert hardy_k_ratio_bounded ε hε using 1;          · exact fun n => Nat.pos_of_ne_zero ( by unfold hardy_k; aesop );        · have := hardy_diff_bound u A ε hε h_bound;          filter_upwards [ this ] with n hn using by rw [ abs_sub_comm ] ; exact le_trans hn ( mul_le_mul_of_nonneg_left ( by cases abs_cases A <;> linarith ) hε.le ) ;