X : Type u_1
Y : Type u_2
Z : Type ?u.1698588
inst✝¹⁵ : TopologicalSpace X
inst✝¹⁴ : TopologicalSpace Y
inst✝¹³ : TopologicalSpace Z
𝕜 : Type ?u.1698600
inst✝¹² : CommSemiring 𝕜
A : Type ?u.1698606
inst✝¹¹ : TopologicalSpace A
inst✝¹⁰ : Semiring A
inst✝⁹ : TopologicalSemiring A
inst✝⁸ : StarRing A
inst✝⁷ : ContinuousStar A
inst✝⁶ : Algebra 𝕜 A
inst✝⁵ : LocallyCompactSpace X
inst✝⁴ : AddCommGroup X
inst✝³ : TopologicalAddGroup X
inst✝² : AddCommMonoid Y
inst✝¹ : ContinuousAdd Y
inst✝ : T2Space Y
f : C(X, Y)
p x : X
⊢ ↑(∑' (n : ℤ), comp f (ContinuousMap.addRight (n • p))) (x + p) =
    ↑(∑' (n : ℤ), comp f (ContinuousMap.addRight (n • p))) x
X : Type u_1
Y : Type u_2
Z : Type ?u.1698588
inst✝¹⁵ : TopologicalSpace X
inst✝¹⁴ : TopologicalSpace Y
inst✝¹³ : TopologicalSpace Z
𝕜 : Type ?u.1698600
inst✝¹² : CommSemiring 𝕜
A : Type ?u.1698606
inst✝¹¹ : TopologicalSpace A
inst✝¹⁰ : Semiring A
inst✝⁹ : TopologicalSemiring A
inst✝⁸ : StarRing A
inst✝⁷ : ContinuousStar A
inst✝⁶ : Algebra 𝕜 A
inst✝⁵ : LocallyCompactSpace X
inst✝⁴ : AddCommGroup X
inst✝³ : TopologicalAddGroup X
inst✝² : AddCommMonoid Y
inst✝¹ : ContinuousAdd Y
inst✝ : T2Space Y
f : C(X, Y)
p : X
⊢ Function.Periodic (↑(∑' (n : ℤ), comp f (ContinuousMap.addRight (n • p)))) p
intro x
case pos
X : Type u_1
Y : Type u_2
Z : Type ?u.1698588
inst✝¹⁵ : TopologicalSpace X
inst✝¹⁴ : TopologicalSpace Y
inst✝¹³ : TopologicalSpace Z
𝕜 : Type ?u.1698600
inst✝¹² : CommSemiring 𝕜
A : Type ?u.1698606
inst✝¹¹ : TopologicalSpace A
inst✝¹⁰ : Semiring A
inst✝⁹ : TopologicalSemiring A
inst✝⁸ : StarRing A
inst✝⁷ : ContinuousStar A
inst✝⁶ : Algebra 𝕜 A
inst✝⁵ : LocallyCompactSpace X
inst✝⁴ : AddCommGroup X
inst✝³ : TopologicalAddGroup X
inst✝² : AddCommMonoid Y
inst✝¹ : ContinuousAdd Y
inst✝ : T2Space Y
f : C(X, Y)
p x : X
h : Summable fun n => comp f (ContinuousMap.addRight (n • p))
⊢ ↑(∑' (n : ℤ), comp f (ContinuousMap.addRight (n • p))) (x + p) =
    ↑(∑' (n : ℤ), comp f (ContinuousMap.addRight (n • p))) x

case neg
X : Type u_1
Y : Type u_2
Z : Type ?u.1698588
inst✝¹⁵ : TopologicalSpace X
inst✝¹⁴ : TopologicalSpace Y
inst✝¹³ : TopologicalSpace Z
𝕜 : Type ?u.1698600
inst✝¹² : CommSemiring 𝕜
A : Type ?u.1698606
inst✝¹¹ : TopologicalSpace A
inst✝¹⁰ : Semiring A
inst✝⁹ : TopologicalSemiring A
inst✝⁸ : StarRing A
inst✝⁷ : ContinuousStar A
inst✝⁶ : Algebra 𝕜 A
inst✝⁵ : LocallyCompactSpace X
inst✝⁴ : AddCommGroup X
inst✝³ : TopologicalAddGroup X
inst✝² : AddCommMonoid Y
inst✝¹ : ContinuousAdd Y
inst✝ : T2Space Y
f : C(X, Y)
p x : X
h : ¬Summable fun n => comp f (ContinuousMap.addRight (n • p))
⊢ ↑(∑' (n : ℤ), comp f (ContinuousMap.addRight (n • p))) (x + p) =
    ↑(∑' (n : ℤ), comp f (ContinuousMap.addRight (n • p))) x
X : Type u_1
Y : Type u_2
Z : Type ?u.1698588
inst✝¹⁵ : TopologicalSpace X
inst✝¹⁴ : TopologicalSpace Y
inst✝¹³ : TopologicalSpace Z
𝕜 : Type ?u.1698600
inst✝¹² : CommSemiring 𝕜
A : Type ?u.1698606
inst✝¹¹ : TopologicalSpace A
inst✝¹⁰ : Semiring A
inst✝⁹ : TopologicalSemiring A
inst✝⁸ : StarRing A
inst✝⁷ : ContinuousStar A
inst✝⁶ : Algebra 𝕜 A
inst✝⁵ : LocallyCompactSpace X
inst✝⁴ : AddCommGroup X
inst✝³ : TopologicalAddGroup X
inst✝² : AddCommMonoid Y
inst✝¹ : ContinuousAdd Y
inst✝ : T2Space Y
f : C(X, Y)
p x : X
⊢ ↑(∑' (n : ℤ), comp f (ContinuousMap.addRight (n • p))) (x + p) =
    ↑(∑' (n : ℤ), comp f (ContinuousMap.addRight (n • p))) x
by_cases h : Summable fun n : ℤ => f.comp (ContinuousMap.addRight (n • p))
case h.e'_2
X : Type u_1
Y : Type u_2
Z : Type ?u.1698588
inst✝¹⁵ : TopologicalSpace X
inst✝¹⁴ : TopologicalSpace Y
inst✝¹³ : TopologicalSpace Z
𝕜 : Type ?u.1698600
inst✝¹² : CommSemiring 𝕜
A : Type ?u.1698606
inst✝¹¹ : TopologicalSpace A
inst✝¹⁰ : Semiring A
inst✝⁹ : TopologicalSemiring A
inst✝⁸ : StarRing A
inst✝⁷ : ContinuousStar A
inst✝⁶ : Algebra 𝕜 A
inst✝⁵ : LocallyCompactSpace X
inst✝⁴ : AddCommGroup X
inst✝³ : TopologicalAddGroup X
inst✝² : AddCommMonoid Y
inst✝¹ : ContinuousAdd Y
inst✝ : T2Space Y
f : C(X, Y)
p x : X
h : Summable fun n => comp f (ContinuousMap.addRight (n • p))
⊢ ↑(∑' (n : ℤ), comp f (ContinuousMap.addRight (n • p))) (x + p) =
    ↑(∑' (c : ℤ), comp f (ContinuousMap.addRight (↑(Equiv.addRight 1) c • p))) x
case pos
X : Type u_1
Y : Type u_2
Z : Type ?u.1698588
inst✝¹⁵ : TopologicalSpace X
inst✝¹⁴ : TopologicalSpace Y
inst✝¹³ : TopologicalSpace Z
𝕜 : Type ?u.1698600
inst✝¹² : CommSemiring 𝕜
A : Type ?u.1698606
inst✝¹¹ : TopologicalSpace A
inst✝¹⁰ : Semiring A
inst✝⁹ : TopologicalSemiring A
inst✝⁸ : StarRing A
inst✝⁷ : ContinuousStar A
inst✝⁶ : Algebra 𝕜 A
inst✝⁵ : LocallyCompactSpace X
inst✝⁴ : AddCommGroup X
inst✝³ : TopologicalAddGroup X
inst✝² : AddCommMonoid Y
inst✝¹ : ContinuousAdd Y
inst✝ : T2Space Y
f : C(X, Y)
p x : X
h : Summable fun n => comp f (ContinuousMap.addRight (n • p))
⊢ ↑(∑' (n : ℤ), comp f (ContinuousMap.addRight (n • p))) (x + p) =
    ↑(∑' (n : ℤ), comp f (ContinuousMap.addRight (n • p))) x
convert congr_arg (fun f : C(X, Y) => f x) ((Equiv.addRight (1 : ℤ)).tsum_eq _) using 1
case h.e'_2
X : Type u_1
Y : Type u_2
Z : Type ?u.1698588
inst✝¹⁵ : TopologicalSpace X
inst✝¹⁴ : TopologicalSpace Y
inst✝¹³ : TopologicalSpace Z
𝕜 : Type ?u.1698600
inst✝¹² : CommSemiring 𝕜
A : Type ?u.1698606
inst✝¹¹ : TopologicalSpace A
inst✝¹⁰ : Semiring A
inst✝⁹ : TopologicalSemiring A
inst✝⁸ : StarRing A
inst✝⁷ : ContinuousStar A
inst✝⁶ : Algebra 𝕜 A
inst✝⁵ : LocallyCompactSpace X
inst✝⁴ : AddCommGroup X
inst✝³ : TopologicalAddGroup X
inst✝² : AddCommMonoid Y
inst✝¹ : ContinuousAdd Y
inst✝ : T2Space Y
f : C(X, Y)
p x : X
h : Summable fun n => comp f (ContinuousMap.addRight (n • p))
⊢ (∑' (i : ℤ), ↑(comp f (ContinuousMap.addRight (i • p))) (x + p)) =
    ↑(∑' (c : ℤ), comp f (ContinuousMap.addRight (↑(Equiv.addRight 1) c • p))) x
case h.e'_2
X : Type u_1
Y : Type u_2
Z : Type ?u.1698588
inst✝¹⁵ : TopologicalSpace X
inst✝¹⁴ : TopologicalSpace Y
inst✝¹³ : TopologicalSpace Z
𝕜 : Type ?u.1698600
inst✝¹² : CommSemiring 𝕜
A : Type ?u.1698606
inst✝¹¹ : TopologicalSpace A
inst✝¹⁰ : Semiring A
inst✝⁹ : TopologicalSemiring A
inst✝⁸ : StarRing A
inst✝⁷ : ContinuousStar A
inst✝⁶ : Algebra 𝕜 A
inst✝⁵ : LocallyCompactSpace X
inst✝⁴ : AddCommGroup X
inst✝³ : TopologicalAddGroup X
inst✝² : AddCommMonoid Y
inst✝¹ : ContinuousAdd Y
inst✝ : T2Space Y
f : C(X, Y)
p x : X
h : Summable fun n => comp f (ContinuousMap.addRight (n • p))
⊢ ↑(∑' (n : ℤ), comp f (ContinuousMap.addRight (n • p))) (x + p) =
    ↑(∑' (c : ℤ), comp f (ContinuousMap.addRight (↑(Equiv.addRight 1) c • p))) x
simp_rw [← tsum_apply h]
case h.e'_2
X : Type u_1
Y : Type u_2
Z : Type ?u.1698588
inst✝¹⁵ : TopologicalSpace X
inst✝¹⁴ : TopologicalSpace Y
inst✝¹³ : TopologicalSpace Z
𝕜 : Type ?u.1698600
inst✝¹² : CommSemiring 𝕜
A : Type ?u.1698606
inst✝¹¹ : TopologicalSpace A
inst✝¹⁰ : Semiring A
inst✝⁹ : TopologicalSemiring A
inst✝⁸ : StarRing A
inst✝⁷ : ContinuousStar A
inst✝⁶ : Algebra 𝕜 A
inst✝⁵ : LocallyCompactSpace X
inst✝⁴ : AddCommGroup X
inst✝³ : TopologicalAddGroup X
inst✝² : AddCommMonoid Y
inst✝¹ : ContinuousAdd Y
inst✝ : T2Space Y
f : C(X, Y)
p x : X
h : Summable fun n => comp f (ContinuousMap.addRight (n • p))
⊢ (∑' (i : ℤ), ↑(comp f (ContinuousMap.addRight (i • p))) (x + p)) =
    ∑' (i : ℤ), ↑(((fun n => comp f (ContinuousMap.addRight (n • p))) ∘ ↑(Equiv.addRight 1)) i) x
case h.e'_2
X : Type u_1
Y : Type u_2
Z : Type ?u.1698588
inst✝¹⁵ : TopologicalSpace X
inst✝¹⁴ : TopologicalSpace Y
inst✝¹³ : TopologicalSpace Z
𝕜 : Type ?u.1698600
inst✝¹² : CommSemiring 𝕜
A : Type ?u.1698606
inst✝¹¹ : TopologicalSpace A
inst✝¹⁰ : Semiring A
inst✝⁹ : TopologicalSemiring A
inst✝⁸ : StarRing A
inst✝⁷ : ContinuousStar A
inst✝⁶ : Algebra 𝕜 A
inst✝⁵ : LocallyCompactSpace X
inst✝⁴ : AddCommGroup X
inst✝³ : TopologicalAddGroup X
inst✝² : AddCommMonoid Y
inst✝¹ : ContinuousAdd Y
inst✝ : T2Space Y
f : C(X, Y)
p x : X
h : Summable fun n => comp f (ContinuousMap.addRight (n • p))
⊢ (∑' (i : ℤ), ↑(comp f (ContinuousMap.addRight (i • p))) (x + p)) =
    ↑(∑' (c : ℤ), comp f (ContinuousMap.addRight (↑(Equiv.addRight 1) c • p))) x
erw [← tsum_apply ((Equiv.addRight (1 : ℤ)).summable_iff.mpr h)]
no goals
case h.e'_2
X : Type u_1
Y : Type u_2
Z : Type ?u.1698588
inst✝¹⁵ : TopologicalSpace X
inst✝¹⁴ : TopologicalSpace Y
inst✝¹³ : TopologicalSpace Z
𝕜 : Type ?u.1698600
inst✝¹² : CommSemiring 𝕜
A : Type ?u.1698606
inst✝¹¹ : TopologicalSpace A
inst✝¹⁰ : Semiring A
inst✝⁹ : TopologicalSemiring A
inst✝⁸ : StarRing A
inst✝⁷ : ContinuousStar A
inst✝⁶ : Algebra 𝕜 A
inst✝⁵ : LocallyCompactSpace X
inst✝⁴ : AddCommGroup X
inst✝³ : TopologicalAddGroup X
inst✝² : AddCommMonoid Y
inst✝¹ : ContinuousAdd Y
inst✝ : T2Space Y
f : C(X, Y)
p x : X
h : Summable fun n => comp f (ContinuousMap.addRight (n • p))
⊢ (∑' (i : ℤ), ↑(comp f (ContinuousMap.addRight (i • p))) (x + p)) =
    ∑' (i : ℤ), ↑(((fun n => comp f (ContinuousMap.addRight (n • p))) ∘ ↑(Equiv.addRight 1)) i) x
simp [coe_addRight, add_one_zsmul, add_comm (_ • p) p, ← add_assoc]
case neg
X : Type u_1
Y : Type u_2
Z : Type ?u.1698588
inst✝¹⁵ : TopologicalSpace X
inst✝¹⁴ : TopologicalSpace Y
inst✝¹³ : TopologicalSpace Z
𝕜 : Type ?u.1698600
inst✝¹² : CommSemiring 𝕜
A : Type ?u.1698606
inst✝¹¹ : TopologicalSpace A
inst✝¹⁰ : Semiring A
inst✝⁹ : TopologicalSemiring A
inst✝⁸ : StarRing A
inst✝⁷ : ContinuousStar A
inst✝⁶ : Algebra 𝕜 A
inst✝⁵ : LocallyCompactSpace X
inst✝⁴ : AddCommGroup X
inst✝³ : TopologicalAddGroup X
inst✝² : AddCommMonoid Y
inst✝¹ : ContinuousAdd Y
inst✝ : T2Space Y
f : C(X, Y)
p x : X
h : ¬Summable fun n => comp f (ContinuousMap.addRight (n • p))
⊢ ↑0 (x + p) = ↑0 x
case neg
X : Type u_1
Y : Type u_2
Z : Type ?u.1698588
inst✝¹⁵ : TopologicalSpace X
inst✝¹⁴ : TopologicalSpace Y
inst✝¹³ : TopologicalSpace Z
𝕜 : Type ?u.1698600
inst✝¹² : CommSemiring 𝕜
A : Type ?u.1698606
inst✝¹¹ : TopologicalSpace A
inst✝¹⁰ : Semiring A
inst✝⁹ : TopologicalSemiring A
inst✝⁸ : StarRing A
inst✝⁷ : ContinuousStar A
inst✝⁶ : Algebra 𝕜 A
inst✝⁵ : LocallyCompactSpace X
inst✝⁴ : AddCommGroup X
inst✝³ : TopologicalAddGroup X
inst✝² : AddCommMonoid Y
inst✝¹ : ContinuousAdd Y
inst✝ : T2Space Y
f : C(X, Y)
p x : X
h : ¬Summable fun n => comp f (ContinuousMap.addRight (n • p))
⊢ ↑(∑' (n : ℤ), comp f (ContinuousMap.addRight (n • p))) (x + p) =
    ↑(∑' (n : ℤ), comp f (ContinuousMap.addRight (n • p))) x
rw [tsum_eq_zero_of_not_summable h]
no goals
case neg
X : Type u_1
Y : Type u_2
Z : Type ?u.1698588
inst✝¹⁵ : TopologicalSpace X
inst✝¹⁴ : TopologicalSpace Y
inst✝¹³ : TopologicalSpace Z
𝕜 : Type ?u.1698600
inst✝¹² : CommSemiring 𝕜
A : Type ?u.1698606
inst✝¹¹ : TopologicalSpace A
inst✝¹⁰ : Semiring A
inst✝⁹ : TopologicalSemiring A
inst✝⁸ : StarRing A
inst✝⁷ : ContinuousStar A
inst✝⁶ : Algebra 𝕜 A
inst✝⁵ : LocallyCompactSpace X
inst✝⁴ : AddCommGroup X
inst✝³ : TopologicalAddGroup X
inst✝² : AddCommMonoid Y
inst✝¹ : ContinuousAdd Y
inst✝ : T2Space Y
f : C(X, Y)
p x : X
h : ¬Summable fun n => comp f (ContinuousMap.addRight (n • p))
⊢ ↑0 (x + p) = ↑0 x
simp only [coe_zero, Pi.zero_apply]