Convergence of Series of Tail Sequence

Stream: Is there code for X?

[Yongxi Lin (Aaron)]

Do we have

theorem HasSumLocallyUniformlyOn_iff_tailsumHasSumLocallyUniformlyOn
    (f : ℕ → ℝ → ℝ) (s : Set ℝ) (k : ℕ) :
    HasSumLocallyUniformlyOn f (fun b => ∑' (i : ℕ), f i b) s ↔
    HasSumLocallyUniformlyOn (fun n ↦ f (n + k)) (fun b => ∑' (i : ℕ), f (i + k) b) s := by
  sorry

or a version for HasSumUniformlyOn? This results should also hold for more type of convergence.

[Kenny Lau]

@Yongxi Lin (Aaron) given HasSumUniformlyOn only has 19 declarations you probably just use hasSum_nat_add_iff' to prove it (HasSumUniformlyOn is defined in terms of HasSum)