hardy_sigma_delayed_bound

theorem hardy_sigma_delayed_bound (u : ℕ → ℝ) (n k : ℕ) (A : ℝ) (hk : k ≠ 0)    (h_u_bound : ∀ m, n < m → m ≤ n + k → |u m| ≤ A / m) :    |hardy_sigma_delayed u n k - hardy_s u n| ≤ (k : ℝ) / (n + 1) * A := by  -- Applying the bound $|u_{n+j}| \leq A / (n+j)$ to each term in the sum.  have h_sum_bound : ∑ j ∈ Finset.Icc 1 k, (k - j + 1 : ℝ) * |u (n + j)| ≤ ∑ j ∈ Finset.Icc 1 k, (k - j + 1 : ℝ) * (A / (n + j : ℝ)) := by    exact Finset.sum_le_sum fun x hx => mul_le_mul_of_nonneg_left ( mod_cast h_u_bound _ ( by linarith [ Finset.mem_Icc.mp hx ] ) ( by linarith [ Finset.mem_Icc.mp hx ] ) ) ( by linarith [ show ( x : ℝ ) ≤ k by norm_cast; linarith [ Finset.mem_Icc.mp hx ] ] );  -- Applying the bound $|(k - j + 1) u_{n+j}| \leq k |u_{n+j}|$ to each term in the sum.  have h_sum_bound' : ∑ j ∈ Finset.Icc 1 k, (k - j + 1 : ℝ) * |u (n + j)| ≤ ∑ j ∈ Finset.Icc 1 k, k * (A / (n + 1 : ℝ)) := by    refine le_trans h_sum_bound <| Finset.sum_le_sum fun x hx => mul_le_mul ?_ ?_ ?_ ?_;    · linarith [ show ( x : ℝ ) ≥ 1 by norm_cast; linarith [ Finset.mem_Icc.mp hx ] ];    · field_simp;      rw [ div_le_iff₀ ] <;> nlinarith only [ show ( x : ℝ ) ≥ 1 by norm_cast; linarith [ Finset.mem_Icc.mp hx ], show ( n : ℝ ) ≥ 0 by positivity, show ( A : ℝ ) ≥ 0 by exact le_of_not_gt fun h => by have := h_u_bound ( n + 1 ) ( by linarith [ Finset.mem_Icc.mp hx ] ) ( by linarith [ Finset.mem_Icc.mp hx ] ) ; rw [ le_div_iff₀ ] at this <;> norm_num at * <;> nlinarith [ abs_nonneg ( u ( n + 1 ) ) ] ];    · exact le_trans ( abs_nonneg _ ) ( h_u_bound ( n + x ) ( by linarith [ Finset.mem_Icc.mp hx ] ) ( by linarith [ Finset.mem_Icc.mp hx ] ) ) |> le_trans <| by norm_num;    · positivity;  -- Applying the bound $|(k - j + 1) u_{n+j}| \leq k |u_{n+j}|$ to each term in the sum and using the triangle inequality.  have h_triangle : |hardy_sigma_delayed u n k - hardy_s u n| ≤ (1 / k : ℝ) * ∑ j ∈ Finset.Icc 1 k, (k - j + 1 : ℝ) * |u (n + j)| := by    rw [ hardy_sigma_delayed_sub_s_eq u n k hk ];    rw [ abs_mul, abs_of_nonneg ( by positivity ) ];    exact mul_le_mul_of_nonneg_left ( le_trans ( Finset.abs_sum_le_sum_abs _ _ ) ( Finset.sum_le_sum fun _ _ => by rw [ abs_mul, abs_of_nonneg ] ; linarith [ show ( ↑‹ℕ› : ℝ ) ≤ k by norm_cast; linarith [ Finset.mem_Icc.mp ‹_› ] ] ) ) ( by positivity );  convert h_triangle.trans ( mul_le_mul_of_nonneg_left h_sum_bound' <| by positivity ) using 1 ; norm_num ; ring;  simp +decide [ sq, mul_right_comm, hk ]