English
In a field α with FloorRing, round x equals floor(x + 1/2).
Русский
В поле α с FloorRing округление x равно floor(x + 1/2).
LaTeX
$$$\\\\operatorname{round}(x) = \\left\\\\lfloor x + \\tfrac{1}{2} \\\\right\\\\rfloor.$$$
Lean4
theorem round_eq (x : α) : round x = ⌊x + 1 / 2⌋ :=
by
simp_rw [round, (by simp only [lt_div_iff₀', two_pos] : 2 * fract x < 1 ↔ fract x < 1 / 2)]
rcases lt_or_ge (fract x) (1 / 2) with hx | hx
· conv_rhs => rw [← fract_add_floor x, add_assoc, add_left_comm, floor_intCast_add]
rw [if_pos hx, left_eq_add, floor_eq_iff, cast_zero, zero_add]
constructor
· linarith [fract_nonneg x]
· linarith
· have : ⌊fract x + 1 / 2⌋ = 1 := by
rw [floor_eq_iff]
constructor
· norm_num
linarith
· norm_num
linarith [fract_lt_one x]
rw [if_neg (not_lt.mpr hx), ← fract_add_floor x, add_assoc, add_left_comm, floor_intCast_add, ceil_add_intCast,
add_comm _ ⌊x⌋, add_right_inj, ceil_eq_iff, this, cast_one, sub_self]
constructor
· linarith
· linarith [fract_lt_one x]
