English
The distance from x to round x equals the minimum of fract(x) and 1 − fract(x): |x − round x| = min(fract x, 1 − fract x).
Русский
Расстояние до округления равно минимуму дробной части и единицы минус дробная часть: |x − round x| = min(fract x, 1 − fract x).
LaTeX
$$$|x - \\operatorname{round} x| = \\min(\\operatorname{fract} x, 1 - \\operatorname{fract} x).$$$
Lean4
theorem abs_sub_round_eq_min (x : α) : |x - round x| = min (fract x) (1 - fract x) :=
by
simp_rw [round, min_def_lt, two_mul, ← lt_tsub_iff_left]
rcases lt_or_ge (fract x) (1 - fract x) with hx | hx
· rw [if_pos hx, if_pos hx, self_sub_floor, abs_fract]
· have : 0 < fract x :=
by
replace hx : 0 < fract x + fract x := lt_of_lt_of_le zero_lt_one (tsub_le_iff_left.mp hx)
simpa only [← two_mul, mul_pos_iff_of_pos_left, zero_lt_two] using hx
rw [if_neg (not_lt.mpr hx), if_neg (not_lt.mpr hx), abs_sub_comm, ceil_sub_self_eq this.ne.symm, abs_one_sub_fract]
