index shift in tsum

Stream: mathlib4

[Matthias Liesenfeld]

Hi there,
is there a lemma about shifting the index in a tsum? Something like
(n : ℕ) (f : ℕ → ℝ) : ∑' k, {k | k ≥ n}.indicator f k = ∑' k, f (k+n)
I wasnt able to find it using apply? and multiple ai tools.

Or is there even a more idomatic different way to express the shifted sum?

[Ruben Van de Velde]

Maybe with Set.Ici?

[Jireh Loreaux]

It's not quite immediate, but you should be able to get it from docs#Summable.sum_add_tsum_nat_add (start by rewriting backwards with that lemma). Then the finite sum of the indicator will be zero, and the remaining infinite sum of the indicator will simplify to f.

[Jireh Loreaux]

like so:

import Mathlib

example {f : ℕ → ℝ} (n : ℕ) (h : Summable f) :
    ∑' k, {k | k ≥ n}.indicator f k = ∑' k, f (k+n) := by
  rw [← (h.indicator {k | k ≥ n}).sum_add_tsum_nat_add n,
    Finset.sum_eq_zero (by simp_all), zero_add]
  congr! 2 with k
  simp

[Matthias Liesenfeld]

Thank you! :)
I tried to prove it for {f : ℕ → ℝ≥0∞} but keep running in a timeout (in the proof of h2):

lemma aux2 {f : ℕ → ℝ≥0∞} (n : ℕ) (h : Summable f) :
    ∑' k, {k | k ≥ n}.indicator f k = ∑' k, f (k+n) := by
  let g : ℕ → ℝ≥0∞ := fun i => {i | i ≥ n}.indicator f i
  have h1 : ∑' (k : ℕ), {k | k ≥ n}.indicator f k = ∑' (k : ℕ), g k := by rfl
  rw [h1]
  have hg : Summable g := ENNReal.summable
  have h2 : ∑' (k : ℕ), g k = ∑ k ∈ Finset.range n, g k + ∑' (k : ℕ), g (k + n) := (hg.sum_add_tsum_nat_add n).symm
  rw [Finset.sum_eq_zero (by simp_all), zero_add]
  congr! 2 with k
  simp

Do you have any ideas?

[Etienne Marion]

That's because sum_add_tsum_nat_add wants a function whose codomain is a group, which ENNReal is not.

[Etienne Marion]

You should use Summable.sum_add_tsum_nat_add' instead.

[Matthias Liesenfeld]

Now its working :)

lemma aux3 {f : ℕ → ℝ≥0∞} (n : ℕ) :
    ∑' k, {k | k ≥ n}.indicator f k = ∑' k, f (k+n) := by
  have h : Summable (fun k ↦ {m | m ≥ n}.indicator f (k + n)) := by simp
  rw [← h.sum_add_tsum_nat_add', Finset.sum_eq_zero (by simp_all), zero_add]
  congr! 2 with k
  simp