English
For natural numbers m, n, |(m/n) − round(m/n)| equals a rational expression involving m mod n and n.
Русский
Для натуральных m, n выражение |(m/n) − round(m/n)| зависит от m mod n и n.
LaTeX
$$$\\\\forall m, n \\\\in \\mathbb{N}, \\\\text{... } |(m/n) - \\operatorname{round}(m/n)| = \\frac{\\min(m \\\\% \\\\ n, n - (m \\\\% \\\\ n))}{n}.$$$
Lean4
theorem abs_sub_round_div_natCast_eq {m n : ℕ} : |(m : α) / n - round ((m : α) / n)| = ↑(min (m % n) (n - m % n)) / n :=
by
rcases n.eq_zero_or_pos with (rfl | hn)
· simp
have hn' : 0 < (n : α) := by norm_cast
rw [abs_sub_round_eq_min, Nat.cast_min, ← min_div_div_right hn'.le, fract_div_natCast_eq_div_natCast_mod,
Nat.cast_sub (m.mod_lt hn).le, sub_div, div_self hn'.ne']
