Floor function properties: $[2x] = [x] + [ x + \frac12 ]$ and $[nx] = \sum_{k = 0}^{n - 1} [ x + \frac{k}{n} ] $

This is one of my favourite exercises, because of the following neat solution:

Fix $n$. Let

$$ f(x) := \sum\limits_{k=0}^{n-1} \Biggl[x + \frac{k}{n}\Biggr] - [nx] \,.$$

Then $f(x) =0 \forall x \in [0,\frac{1}{n})$ since all terms are zero, and it is easy to prove that $f(x+\frac{1}{n})=f(x)$.

It follows imediately that $f$ is identically 0.

Let $n=\lfloor x\rfloor$, and let $\alpha=x-n$; clearly either $0\le\alpha<\frac12$, or $\frac12\le\alpha<1$. Then

$$\lfloor 2x\rfloor=\lfloor 2n+2\alpha\rfloor=2n+\lfloor 2\alpha\rfloor=\begin{cases} 2n,&\text{if }0\le\alpha<\frac12\\ 2n+1,&\text{if }\frac12\le\alpha<1\;, \end{cases}$$

and

$$\left\lfloor x+\frac12\right\rfloor=\left\lfloor n+\alpha+\frac12\right\rfloor=n+\left\lfloor\alpha+\frac12\right\rfloor=\begin{cases} n,&\text{if }0\le\alpha<\frac12\\ n+1&\text{if }\frac12\le\alpha<1\;; \end{cases}$$

since $\lfloor x\rfloor=n$, the first result is immediate.

The general case is handled similarly, except that there are $n$ cases; for $k=0,\dots,n-1$, case $k$ is $$\frac kn\le\alpha<\frac{k+1}n\;.$$

Both sides are equal since they count the same set: the RHS counts naturals $\rm\:\le n\:x\:$. The LHS counts them in a unique mod $\rm\ n\ $ representation, $\:$ viz. $\rm\ \: j \:\le\: x+k/n\: \iff \ j\:n-k \:\le\: n\:x\:,\ \ j>0 \le k < n\:$.

REMARK $\:$ That every natural has a unique representation of form $\rm \: j\:n-k \ \ \:$ where $\rm\ \ \: j>0 \le k < n\ \ \ $ is simply a slight variant of the Division Algorithm where one utilizes negative (vs. positive) remainders.$\ \ $ To derive this negative form, simply perform the following transformation on the positive remainder form $\rm\ q\: n + r\ \to\ (q+1)\:n + r-n\ $ if $\rm\ r\ne 0\:$, i.e. inc the quotient, dec the remainder by the dividend.

Thus the result is equivalent to the Division Algorithm, whose normal proof is indeed by induction. One could give a direct inductive proof of the result if, instead of invoking the Division Algorithm by name, one unwinds or inlines this inductive proof directly into the proof of the result - much as the same way that the classic Lindenmann - Zermelo direct proof of unique factorization of naturals inlines a division / Euclidean algorithm based descent proof of the fundamental Prime Divisor property $\rm\ p|ab\ \Rightarrow\ p|a\ \ or\ \ p|b\:$.