Theorem: Replicative Function of x minus Floor of x is Replicative

Let $f: \R \to \R$ be a real function.
Let $f$ be a replicative function.
Let $g: \R \to \R$ be the real function defined as:
:$\map g x = \map f {x - \floor x}$
Then $g$ is also a replicative function.

Proof:
=== Lemma ===
{{:Replicative Function of x minus Floor of x is Replicative/Lemma}}{{qed|lemma}}
First observe:
:$\ds \sum_{k \mathop = 0}^{n - 1} \map g {x + \frac k n} = \sum_{k \mathop = 0}^{n - 1} \map f {x + \frac k n - \floor {x + \frac k n} }$
{{begin-eqn}}
{{eqn | l = \map g {n x}
      | r = \map f {n x - \floor {n x} }
}}
{{eqn | r = \sum_{k \mathop = 0}^{n - 1} \map f {\frac {n x - \floor {n x} } n + \frac k n}
      | c = {{Defof|Replicative Function}}
}}
{{eqn | r = \sum_{k \mathop = 0}^{n - 1} \map f {x - \frac {\floor {n x} } n + \frac k n}
      | c = 
}}
{{end-eqn}}
We need to show that the two final sums are equal.
Suppose:
:$\dfrac j n \le x - \floor x < \dfrac {j + 1} n$
for some integer $j$.
By Real Number minus Floor:
:$0 \le x - \floor x < 1$
This gives:
:$0 \le j \le n - 1$
Let $y = x - \dfrac j n$.
Then:
:$\floor x \le x - \dfrac j n = y$
By Number not less than Integer iff Floor not less than Integer:
:$\floor x \le \floor y$
On the other hand:
:$y \le x$
which gives
:$\floor y \le \floor x$
So $\floor y = \floor x$.
We now have:
:$\dfrac j n \le x - \floor x = y + \dfrac j n - \floor y < \dfrac {j + 1} n$
which gives:
:$0 \le y - \floor y < \dfrac 1 n$
which satisfies the condition for the lemma.
Hence:
{{begin-eqn}}
{{eqn | l = \map f {y + \frac k n - \floor {y + \frac k n} }
      | r = \map f {y - \frac {\floor {n y} } n + \frac k n}
      | c = by the lemma
}}
{{eqn | r = \map f {x - \dfrac j n - \frac {\floor {n x - j} } n + \frac k n}
      | c =
}}
{{eqn | r = \map f {x - \dfrac j n - \frac {\floor {n x} } n + \dfrac j n + \frac k n}
      | c = Floor of Number plus Integer
}}
{{eqn | r = \map f {x - \frac {\floor {n x} } n + \frac k n}
}}
{{end-eqn}}
We also have:
{{begin-eqn}}
{{eqn | l = \sum_{k \mathop = 0}^{n - 1} \map f {y + \frac k n - \floor {y + \frac k n} }
      | r = \sum_{k \mathop = 0}^{n - 1} \map f {x - \frac j n + \frac k n - \floor {x - \frac j n + \frac k n} }
}}
{{eqn | r = \sum_{k \mathop = 0}^{j - 1} \map f {x + \frac {k - j} n - \floor {x + \frac {k - j} n} } + \sum_{k \mathop = j}^{n - 1} \map f {x + \frac {k - j} n - \floor {x + \frac {k - j} n} }
}}
{{eqn | r = \sum_{k \mathop = 0}^{j - 1} \map f {x + \frac {k - j} n + 1 - \floor {x + \frac {k - j} n} - 1} + \sum_{k \mathop = 0}^{n - j - 1} \map f {x + \frac k n - \floor {x + \frac k n} }
      | c = Translation of Index Variable of Summation
}}
{{eqn | r = \sum_{k \mathop = 0}^{j - 1} \map f {x + \frac {k - j} n + 1 - \floor {x + \frac {k - j} n + 1} } + \sum_{k \mathop = 0}^{n - j - 1} \map f {x + \frac k n - \floor {x + \frac k n} }
      | c = Floor of Number plus Integer
}}
{{eqn | r = \sum_{k \mathop = 0}^{j - 1} \map f {x + \frac {n - j + k} n + 1 - \floor {x + \frac {n - j + k} n} } + \sum_{k \mathop = 0}^{n - j - 1} \map f {x + \frac k n - \floor {x + \frac k n} }
      | c = 
}}
{{eqn | r = \sum_{k \mathop = n - j}^{n - 1} \map f {x + \frac k n + 1 - \floor {x + \frac k n} } + \sum_{k \mathop = 0}^{n - j - 1} \map f {x + \frac k n - \floor {x + \frac k n} }
      | c = Translation of Index Variable of Summation
}}
{{eqn | r = \sum_{k \mathop = 0}^{n - 1} \map f {x + \frac k n - \floor {x + \frac k n} }
}}
{{end-eqn}}
Hence the result.
{{qed}}