Matematyka.pl

Do celów pewnego zadanka, znalazłem w necie taką oto fajną równość:
\(\displaystyle{ \sum_{i=1}^{n}\left[ \frac{n}{i} \right] = (2 \cdot \sum_{i=1}^{\left[ \sqrt{n} \right] } \left[ \frac{n}{i} \right] ) - \left[ \sqrt{n} \right] ^{2}}\)
Jako, że to było zadanie programistyczne, to wystarczyło, że 'widać, iż działa' i po prostu to zaklepać. Jednak ciekawi mnie, skąd ta równość się bierze. Sam nie potrafię do tego dojść. Mógłby zatem ktoś ją udowodnić?

Niech \(\displaystyle{ [\,\cdot\,]}\) będzie symbolem Iversona, tzn. \(\displaystyle{ [P]=0}\), gdy zdanie \(\displaystyle{ P}\) jest fałszywe i \(\displaystyle{ [P]=1}\), gdy \(\displaystyle{ P}\) jest prawdziwe. Tam, gdzie nie jest to wyraźnie zaznaczone, sumujemy po wszystkich liczbach naturalnych. Mamy

\(\displaystyle{ \sum_{i=1}^n\left\lfloor\frac{n}{i}\right\rfloor=\sum_i\sum_j\left[j\leq\frac{n}{i}\right]=\sum_{i,j}[ij\leq n]=\sum_{i\not=j}[ij\leq n]+\sum_{i=j}[ij\leq n]=}\)
\(\displaystyle{ =2\sum_{i<j}[ij\leq n]+\lfloor\sqrt{n}\rfloor=\bigl[\text{w naszej sumie musi być }i\leq\lfloor\sqrt{n}\rfloor,\text{ a jeżeli }j\leq i,\text{ to warunek }ij\leq n\text{ zachodzi }i\text{ razy, dla każdego }j\leq i\bigr]=}\)

\(\displaystyle{ =2\sum_{i\leq\lfloor\sqrt{n}\rfloor}\sum_j\left[j\leq\frac{n}{i}\right]-2\sum_{i\leq\lfloor\sqrt{n}\rfloor}i+\lfloor\sqrt{n}\rfloor=2\sum_{i\leq\lfloor\sqrt{n}\rfloor}\left\lfloor\frac{n}{i}\right\rfloor-\lfloor\sqrt{n}\rfloor^2}\).