Sums of translates of a continuous function is a period continuous function.

Summing translates of a function

theorem ContinuousMap.periodic_tsum_comp_add_zsmul {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [AddCommGroup X] [TopologicalAddGroup X] [AddCommMonoid Y] [ContinuousAdd Y] [T2Space Y] (f : C(X, Y)) (p : X) : Function.Periodic (⇑(∑' (n : ℤ), f.comp (ContinuousMap.addRight (n • p)))) p

Summing the translates of f by ℤ • p gives a map which is periodic with period p. (This is true without any convergence conditions, since if the sum doesn't converge it is taken to be the zero map, which is periodic.)