hardy_diff_bound

lemma hardy_diff_bound (u : ℕ → ℝ) (A : ℝ) (ε : ℝ) (hε : 0 < ε)    (h_bound : ∀ n ≥ 1, |u n| ≤ A / n) :    ∀ᶠ n in Filter.atTop, |hardy_sigma_delayed u n (hardy_k ε n) - hardy_s u n| ≤ ε * A := by  -- Apply `hardy_sigma_delayed_bound` with `k = hardy_k ε n`.  have h_bound : ∀ᶠ n in Filter.atTop, |hardy_sigma_delayed u n (hardy_k ε n) - hardy_s u n| ≤ (hardy_k ε n : ℝ) / (n + 1) * A := by    field_simp;    -- By the bound on the difference between the delayed arithmetic mean and the partial sum, we have:    have h_diff_bound : ∀ n ≥ 1, |hardy_sigma_delayed u n (hardy_k ε n) - hardy_s u n| ≤ (hardy_k ε n : ℝ) / (n + 1) * A := by      intros n hn      apply hardy_sigma_delayed_bound u n (hardy_k ε n) A (by      exact ne_of_gt ( lt_max_of_lt_left zero_lt_one )) (by      exact fun m hm₁ hm₂ => h_bound m ( by linarith ));    filter_upwards [ Filter.eventually_ge_atTop 1 ] with n hn using by have := h_diff_bound n hn; rw [ div_mul_eq_mul_div, le_div_iff₀ ] at this <;> linarith;;  -- Since `hardy_k ε n` is eventually equal to `Nat.floor (ε * n)`, we can simplify the expression.  have h_floor : ∀ᶠ n in Filter.atTop, (hardy_k ε n : ℝ) ≤ ε * n := by    simp [hardy_k];    exact ⟨ ⌈ε⁻¹⌉₊ + 1, fun n hn => ⟨ by nlinarith [ Nat.le_ceil ( ε⁻¹ ), mul_inv_cancel₀ ( ne_of_gt hε ), ( by norm_cast : ( ⌈ε⁻¹⌉₊ : ℝ ) + 1 ≤ n ) ], Nat.floor_le ( by positivity ) ⟩ ⟩;  filter_upwards [ h_bound, h_floor ] with n hn hn' using le_trans hn ( by rw [ div_mul_eq_mul_div, div_le_iff₀ ] <;> nlinarith [ show ( 0 :ℝ ) ≤ ε * A by exact mul_nonneg hε.le ( show 0 ≤ A by have := ‹∀ n ≥ 1, |u n| ≤ A / ( n :ℝ ) › 1 le_rfl; norm_num at this; linarith [ abs_le.mp this ] ) ] )