tendsto_S_S_zero

lemma tendsto_S_S_zero {f : ℕ → ℝ} (hpos : 0 ≤ f) (hcheby : cheby f) :    TendstoUniformlyOnFilter (S f) (S f 0) (𝓝[>] 0) atTop := by  rw [Metric.tendstoUniformlyOnFilter_iff] ; intro δ hδ  obtain ⟨C, hC⟩ := hcheby  have l1 : ∀ᶠ (p : ℝ × ℕ) in 𝓝[>] 0 ×ˢ atTop, C * ⌈p.1 * p.2⌉₊ / p.2 < δ := by    have r1 := tendsto_mul_ceil_div.const_mul C    simp only [mul_div_assoc', mul_zero] at r1 ; exact r1 (Iio_mem_nhds hδ)  have : Ioc 0 1 ∈ 𝓝[>] (0 : ℝ) := inter_mem_nhdsWithin _ (Iic_mem_nhds zero_lt_one)  filter_upwards [l1, Eventually.prod_inl this _] with (ε, N) h1 h2  have l2 : ‖cumsum f ⌈ε * ↑N⌉₊ / ↑N‖ ≤ C * ⌈ε * N⌉₊ / N := by    have r1 := hC ⌈ε * N⌉₊    have r2 : 0 ≤ cumsum f ⌈ε * N⌉₊ := by apply cumsum_nonneg hpos    simp only [norm_real, norm_of_nonneg (hpos _), norm_div,      norm_of_nonneg r2, Real.norm_natCast] at r1 ⊢    apply div_le_div_of_nonneg_right r1 (by positivity)  simpa [← S_sub_S h2.2] using! l2.trans_lt h1