Shifting tsum index

Stream: Is there code for X?

[Gareth Ma]

Does the following not exist? ft. my somewhat hilarious proof:

example {f : ℤ → ℂ} {k : ℤ} : ∑' n, f n = ∑' n, f (n + k) := by
  let e : ℤ ≃ ℤ := {
    toFun := fun x ↦ x + k
    invFun := fun x ↦ x - k
    left_inv := by intro; simp
    right_inv := by intro; simp
  }
  change ∑' n, f n = ∑' n, f (e n)
  rw [e.tsum_eq]

Seems like it would belong in Topology/Algebra/InfiniteSum/NatInt.lean if it exists, but I can't find it

[Yaël Dillies]

Your Equiv is just Equiv.addRight k

[Gareth Ma]

Ah so it's

theorem tsum_of_ {f : ℤ → ℂ} {k : ℤ} : ∑' n, f n = ∑' n, f (n + k) :=
  ((Equiv.addRight k).tsum_eq f).symm

[Gareth Ma]

Great thanks :D

[Yaël Dillies]

theorem tsum_of_ {f : ℤ → ℂ} {k : ℤ} : ∑' n, f n = ∑' n, f (n + k) :=
  (Equiv.subRight k).tsum_eq f

even

[Gareth Ma]

Doesn't seem to work for me

[Gareth Ma]

It proves ∑' n, f (n - k) = ∑' n, f n only

[Yaël Dillies]

Ah yeah whoops