Dedekind Sums (Q7361248)

For integers $h$, $k$, the Dedekind sum is defined as \[s(h,k) = \sum_{r=1}^{k-1} \frac{r}{k} \left(\left\{\frac{hr}{k}\right\} - \frac{1}{2}\right) \] where $\{x\} = x - \lfloor x\rfloor$ denotes the fractional part of $x$. These sums occur in various contexts in analytic number theory, e.g. in the functional equation of the Dedekind $\eta$ function or in the study of modular forms. We give the definition of $s(h,k)$ and prove its basic properties, including the reciprocity law \[s(h,k) + s(k,h) = \frac{1}{12hk} + \frac{h}{12k} + \frac{k}{12h} - \frac{1}{4} \] and various congruence results. Our formalisation follows Chapter 3 of Apostol's Modular Functions and Dirichlet Series in Number Theory and contains all facts related to Dedekind sums from it (without the exercises).