Oddness of the Dedekind sum: s(k-1,k)=-s(1,k)
ProveddedekindSum_natCast_sub_oneFor a natural number , write if the fractional part of the rational vanishes and otherwise, and for set
the sum being taken over in the range and computed in . The theorem asserts, for every natural number with no further hypotheses, the identity
where the first argument is the integer , so that for it is and both sides are the empty sum . Thus it is the special case at of the combination of periodicity of in modulo and oddness , stated here directly for the pair rather than through those two general properties.
This is the classical evaluation for Dedekind sums, reflecting their periodicity in the first argument and their oddness under . It is used in the computations of the Rademacher function at particular levels, where the witnesses for residues , and modulo invoke it.
import Definitions.Def_NumberTheory_DedekindSum set_option maxHeartbeats 4000000 set_option synthInstance.maxHeartbeats 400000 set_option backward.isDefEq.respectTransparency.types false
theorem dedekindSum_natCast_sub_one (k : ℕ) : dedekindSum ((k : ℤ) - 1) k = -dedekindSum 1 k := by sorry