Rounding to the nearest multiple

Mirror of Mathlib/Algebra/Order/Round.lean: the additions a PR there would make. [UPSTREAM]

Rounding to the nearest multiple of ε sends d to round (d / ε) • ε. Mathlib bounds x - round x and shows round x is the nearest integer; this file transfers both facts to multiples of ε, and shows that round of a quotient by an odd natural factors through round.

Main results

• abs_sub_round_div_zsmul_le: rounding to the nearest multiple of ε moves a point by at most ε / 2.
• abs_sub_round_div_zsmul_le_abs_sub_zsmul: no multiple of ε is nearer.
• abs_sub_round_eq_half_iff: the points moved by exactly a half are the half-integers.
• round_div_two_mul_add_one: round (x / (2 * j + 1)) is (round x + j) / (2 * j + 1).

theorem abs_sub_round_div_zsmul_le {α : Type u_1} [Field α] {ε : α} [LinearOrder α] [IsStrictOrderedRing α] [FloorRing α] (hε : 0 < ε) (d : α) : |d - round (d / ε) • ε| ≤ ε / 2

Rounding to the nearest multiple of ε moves a point by at most ε / 2, the sibling of abs_sub_round for multiples.

theorem abs_sub_round_div_zsmul_le_abs_sub_zsmul {α : Type u_1} [Field α] {ε : α} [LinearOrder α] [IsStrictOrderedRing α] [FloorRing α] (hε : ε ≠ 0) (d : α) (n : ℤ) : |d - round (d / ε) • ε| ≤ |d - n • ε|

The nearest multiple of ε is no farther from d than any multiple, the sibling of round_le for multiples.

theorem abs_sub_round_eq_half_iff {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] [FloorRing α] {x : α} : |x - ↑(round x)| = 1 / 2 ↔ ∃ (k : ℤ), x = ↑k + 1 / 2

Rounding moves a point by exactly a half at the half-integers, the equality case of abs_sub_round.

theorem round_div_two_mul_add_one {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] [FloorRing α] (x : α) (j : ℕ) : round (x / ↑(2 * j + 1)) = (round x + ↑j) / ↑(2 * j + 1)

Rounding a quotient by an odd natural factors through rounding, since the half-integers k * (2 * j + 1) + j + 1 / 2 at which round (x / (2 * j + 1)) jumps are among those at which round x jumps.