Mathlib.Algebra.Order.Round

round definition

(x : α) : ℤ

Full source

/-- `round` rounds a number to the nearest integer. `round (1 / 2) = 1` -/
def round (x : α) : ℤ :=
  if 2 * fract x < 1 then ⌊x⌋ else ⌈x⌉

Rounding to the nearest integer

Informal description

The function `round` maps an element $x$ in a linearly ordered ring $\alpha$ to the nearest integer, rounding halves towards infinity. Specifically, if the fractional part of $x$ satisfies $2 \cdot \text{fract}(x) < 1$, then $\text{round}(x) = \lfloor x \rfloor$; otherwise, $\text{round}(x) = \lceil x \rceil$.

round_zero theorem

: round (0 : α) = 0

Full source

@[simp]
theorem round_zero : round (0 : α) = 0 := by simp [round]

Rounding Zero: $\text{round}(0) = 0$

Informal description

For any linearly ordered ring $\alpha$ with a rounding function, the rounding of the zero element is zero, i.e., $\text{round}(0) = 0$.

round_one theorem

: round (1 : α) = 1

Full source

@[simp]
theorem round_one : round (1 : α) = 1 := by simp [round]

Rounding of One: $\text{round}(1) = 1$

Informal description

For any linearly ordered ring $\alpha$ with a rounding function, the rounding of the multiplicative identity element is one, i.e., $\text{round}(1) = 1$.

round_natCast theorem

(n : ℕ) : round (n : α) = n

Full source

@[simp]
theorem round_natCast (n : ℕ) : round (n : α) = n := by simp [round]

Rounding Preserves Natural Numbers

Informal description

For any natural number $n$ and any linearly ordered ring $\alpha$ with a rounding function, the rounding of $n$ (viewed as an element of $\alpha$) equals $n$ itself, i.e., $\text{round}(n) = n$.

round_ofNat theorem

(n : ℕ) [n.AtLeastTwo] : round (ofNat(n) : α) = ofNat(n)

Full source

@[simp]
theorem round_ofNat (n : ℕ) [n.AtLeastTwo] : round (ofNat(n) : α) = ofNat(n) :=
  round_natCast n

Rounding Preserves Numerals $\geq 2$: $\text{round}(n) = n$ for $n \geq 2$

Informal description

For any natural number $n \geq 2$ and any linearly ordered ring $\alpha$ with a rounding function, the rounding of the canonical embedding of $n$ into $\alpha$ equals $n$ itself, i.e., $\text{round}(n) = n$.

round_intCast theorem

(n : ℤ) : round (n : α) = n

Full source

@[simp]
theorem round_intCast (n : ℤ) : round (n : α) = n := by simp [round]

Rounding Preserves Integers: $\text{round}(n) = n$ for $n \in \mathbb{Z}$

Informal description

For any integer $n$ in a linearly ordered ring $\alpha$, the rounding function satisfies $\text{round}(n) = n$.

round_add_intCast theorem

(x : α) (y : ℤ) : round (x + y) = round x + y

Full source

@[simp]
theorem round_add_intCast (x : α) (y : ℤ) : round (x + y) = round x + y := by
  rw [round, round, Int.fract_add_intCast, Int.floor_add_intCast, Int.ceil_add_intCast,
    ← apply_ite₂, ite_self]

Rounding Function Additivity with Integer Shift: $\text{round}(x + y) = \text{round}(x) + y$

Informal description

For any element $x$ in a linearly ordered ring $\alpha$ and any integer $y$, the rounding function satisfies $\text{round}(x + y) = \text{round}(x) + y$.

round_add_one theorem

(a : α) : round (a + 1) = round a + 1

Full source

@[simp]
theorem round_add_one (a : α) : round (a + 1) = round a + 1 := by
  rw [← round_add_intCast a 1, cast_one]

Rounding Function Additivity with Unit Shift: $\text{round}(a + 1) = \text{round}(a) + 1$

Informal description

For any element $a$ in a linearly ordered ring $\alpha$, the rounding function satisfies $\text{round}(a + 1) = \text{round}(a) + 1$.

round_sub_intCast theorem

(x : α) (y : ℤ) : round (x - y) = round x - y

Full source

@[simp]
theorem round_sub_intCast (x : α) (y : ℤ) : round (x - y) = round x - y := by
  rw [sub_eq_add_neg]
  norm_cast
  rw [round_add_intCast, sub_eq_add_neg]

Rounding Function Additivity with Integer Subtraction: $\text{round}(x - y) = \text{round}(x) - y$

Informal description

For any element $x$ in a linearly ordered ring $\alpha$ and any integer $y$, the rounding function satisfies $\text{round}(x - y) = \text{round}(x) - y$.

round_sub_one theorem

(a : α) : round (a - 1) = round a - 1

Full source

@[simp]
theorem round_sub_one (a : α) : round (a - 1) = round a - 1 := by
  rw [← round_sub_intCast a 1, cast_one]

Rounding Function Additivity with Unit Decrement: $\text{round}(a - 1) = \text{round}(a) - 1$

Informal description

For any element $a$ in a linearly ordered ring $\alpha$, the rounding function satisfies $\text{round}(a - 1) = \text{round}(a) - 1$.

round_add_natCast theorem

(x : α) (y : ℕ) : round (x + y) = round x + y

Full source

@[simp]
theorem round_add_natCast (x : α) (y : ℕ) : round (x + y) = round x + y :=
  mod_cast round_add_intCast x y

Rounding Function Additivity with Natural Number Shift: $\text{round}(x + y) = \text{round}(x) + y$

Informal description

For any element $x$ in a linearly ordered ring $\alpha$ and any natural number $y$, the rounding function satisfies $\text{round}(x + y) = \text{round}(x) + y$.

round_add_ofNat theorem

(x : α) (n : ℕ) [n.AtLeastTwo] : round (x + ofNat(n)) = round x + ofNat(n)

Full source

@[simp]
theorem round_add_ofNat (x : α) (n : ℕ) [n.AtLeastTwo] :
    round (x + ofNat(n)) = round x + ofNat(n) :=
  round_add_natCast x n

Rounding Function Additivity with Shift by $n \geq 2$: $\text{round}(x + n) = \text{round}(x) + n$

Informal description

For any element $x$ in a linearly ordered ring $\alpha$ and any natural number $n \geq 2$, the rounding function satisfies $\text{round}(x + n) = \text{round}(x) + n$.

round_sub_natCast theorem

(x : α) (y : ℕ) : round (x - y) = round x - y

Full source

@[simp]
theorem round_sub_natCast (x : α) (y : ℕ) : round (x - y) = round x - y :=
  mod_cast round_sub_intCast x y

Rounding Function Additivity with Natural Number Subtraction: $\text{round}(x - y) = \text{round}(x) - y$

Informal description

For any element $x$ in a linearly ordered ring $\alpha$ and any natural number $y$, the rounding function satisfies $\text{round}(x - y) = \text{round}(x) - y$.

round_sub_ofNat theorem

(x : α) (n : ℕ) [n.AtLeastTwo] : round (x - ofNat(n)) = round x - ofNat(n)

Full source

@[simp]
theorem round_sub_ofNat (x : α) (n : ℕ) [n.AtLeastTwo] :
    round (x - ofNat(n)) = round x - ofNat(n) :=
  round_sub_natCast x n

Rounding Function Additivity with Shift by $n \geq 2$: $\text{round}(x - n) = \text{round}(x) - n$

Informal description

For any element $x$ in a linearly ordered ring $\alpha$ and any natural number $n \geq 2$, the rounding function satisfies $\text{round}(x - n) = \text{round}(x) - n$.

round_intCast_add theorem

(x : α) (y : ℤ) : round ((y : α) + x) = y + round x

Full source

@[simp]
theorem round_intCast_add (x : α) (y : ℤ) : round ((y : α) + x) = y + round x := by
  rw [add_comm, round_add_intCast, add_comm]

Rounding Function Additivity with Integer Shift: $\text{round}(y + x) = y + \text{round}(x)$

Informal description

For any element $x$ in a linearly ordered ring $\alpha$ and any integer $y$, the rounding function satisfies $\text{round}(y + x) = y + \text{round}(x)$, where $y$ is first cast to an element of $\alpha$ before addition.

round_natCast_add theorem

(x : α) (y : ℕ) : round ((y : α) + x) = y + round x

Full source

@[simp]
theorem round_natCast_add (x : α) (y : ℕ) : round ((y : α) + x) = y + round x := by
  rw [add_comm, round_add_natCast, add_comm]

Rounding Function Additivity with Natural Number Shift: $\text{round}(y + x) = y + \text{round}(x)$

Informal description

For any element $x$ in a linearly ordered ring $\alpha$ and any natural number $y$, the rounding function satisfies $\text{round}(y + x) = y + \text{round}(x)$, where $y$ is first cast to an element of $\alpha$ before addition.

round_ofNat_add theorem

(n : ℕ) [n.AtLeastTwo] (x : α) : round (ofNat(n) + x) = ofNat(n) + round x

Full source

@[simp]
theorem round_ofNat_add (n : ℕ) [n.AtLeastTwo] (x : α) :
    round (ofNat(n) + x) = ofNat(n) + round x :=
  round_natCast_add x n

Rounding Additivity with Shift by Natural Number $\geq 2$: $\text{round}(n + x) = n + \text{round}(x)$

Informal description

For any natural number $n \geq 2$ and any element $x$ in a linearly ordered ring $\alpha$, the rounding function satisfies $\text{round}(n + x) = n + \text{round}(x)$, where $n$ is interpreted as an element of $\alpha$ via the canonical homomorphism from $\mathbb{N}$.

abs_sub_round_eq_min theorem

(x : α) : |x - round x| = min (fract x) (1 - fract x)

Full source

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]

Minimal Distance Property of Rounding: $|x - \text{round}(x)| = \min(\text{fract}(x), 1 - \text{fract}(x))$

Informal description

For any element $x$ in a linearly ordered ring $\alpha$, the absolute difference between $x$ and its rounded value $\text{round}(x)$ equals the minimum between the fractional part $\text{fract}(x)$ and $1 - \text{fract}(x)$. That is: $$ |x - \text{round}(x)| = \min(\text{fract}(x), 1 - \text{fract}(x)) $$

round_le theorem

(x : α) (z : ℤ) : |x - round x| ≤ |x - z|

Full source

theorem round_le (x : α) (z : ℤ) : |x - round x| ≤ |x - z| := by
  rw [abs_sub_round_eq_min, min_le_iff]
  rcases le_or_lt (z : α) x with (hx | hx) <;> [left; right]
  · conv_rhs => rw [abs_eq_self.mpr (sub_nonneg.mpr hx), ← fract_add_floor x, add_sub_assoc]
    simpa only [le_add_iff_nonneg_right, sub_nonneg, cast_le] using le_floor.mpr hx
  · rw [abs_eq_neg_self.mpr (sub_neg.mpr hx).le]
    conv_rhs => rw [← fract_add_floor x]
    rw [add_sub_assoc, add_comm, neg_add, neg_sub, le_add_neg_iff_add_le, sub_add_cancel,
      le_sub_comm]
    norm_cast
    exact floor_le_sub_one_iff.mpr hx

Optimality of Rounding: $|x - \text{round}(x)| \leq |x - z|$ for all integers $z$

Informal description

For any element $x$ in a linearly ordered ring $\alpha$ and any integer $z$, the absolute difference between $x$ and its rounded value $\text{round}(x)$ is less than or equal to the absolute difference between $x$ and $z$, i.e., $$ |x - \text{round}(x)| \leq |x - z|. $$

round_eq theorem

(x : α) : round x = ⌊x + 1 / 2⌋

Full source

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_le (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]

Rounding as Floor of Shifted Value: $\text{round}(x) = \lfloor x + \frac{1}{2} \rfloor$

Informal description

For any element $x$ in a linearly ordered ring $\alpha$, the nearest integer to $x$ (rounding halves towards infinity) is equal to the floor of $x + \frac{1}{2}$, i.e., $\text{round}(x) = \lfloor x + \frac{1}{2} \rfloor$.

round_two_inv theorem

: round (2⁻¹ : α) = 1

Full source

@[simp]
theorem round_two_inv : round (2⁻¹ : α) = 1 := by
  simp only [round_eq, ← one_div, add_halves, floor_one]

Rounding of Half: $\text{round}(\frac{1}{2}) = 1$

Informal description

For any element $\alpha$ in a linearly ordered ring with a floor function, the rounding of the multiplicative inverse of $2$ is equal to $1$, i.e., $\text{round}(\frac{1}{2}) = 1$.

round_neg_two_inv theorem

: round (-2⁻¹ : α) = 0

Full source

@[simp]
theorem round_neg_two_inv : round (-2⁻¹ : α) = 0 := by
  simp only [round_eq, ← one_div, neg_add_cancel, floor_zero]

Rounding of Negative Half: $\text{round}(-1/2) = 0$

Informal description

For any linearly ordered ring $\alpha$ with a floor function, the rounding of $-1/2$ is $0$, i.e., $\text{round}(-1/2) = 0$.

round_eq_zero_iff theorem

{x : α} : round x = 0 ↔ x ∈ Ico (-(1 / 2)) ((1 : α) / 2)

Full source

@[simp]
theorem round_eq_zero_iff {x : α} : roundround x = 0 ↔ x ∈ Ico (-(1 / 2)) ((1 : α) / 2) := by
  rw [round_eq, floor_eq_zero_iff, add_mem_Ico_iff_left]
  norm_num

Characterization of Zero Rounding: $\text{round}(x) = 0 \leftrightarrow x \in [-\frac{1}{2}, \frac{1}{2})$

Informal description

For any element $x$ in a linearly ordered ring $\alpha$, the nearest integer to $x$ (rounding halves towards infinity) is zero if and only if $x$ lies in the interval $[-\frac{1}{2}, \frac{1}{2})$. That is, $\text{round}(x) = 0 \leftrightarrow x \in [-\frac{1}{2}, \frac{1}{2})$.

abs_sub_round theorem

(x : α) : |x - round x| ≤ 1 / 2

Full source

theorem abs_sub_round (x : α) : |x - round x| ≤ 1 / 2 := by
  rw [round_eq, abs_sub_le_iff]
  have := floor_le (x + 1 / 2)
  have := lt_floor_add_one (x + 1 / 2)
  constructor <;> linarith

Bound on Rounding Error: $|x - \text{round}(x)| \leq \frac{1}{2}$

Informal description

For any element $x$ in a linearly ordered ring $\alpha$, the absolute difference between $x$ and its rounded value $\text{round}(x)$ is at most $\frac{1}{2}$, i.e., $|x - \text{round}(x)| \leq \frac{1}{2}$.

abs_sub_round_div_natCast_eq theorem

{m n : ℕ} : |(m : α) / n - round ((m : α) / n)| = ↑(min (m % n) (n - m % n)) / n

Full source

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']

Rounding Error for Natural Number Division: $\left| \frac{m}{n} - \text{round}\left(\frac{m}{n}\right) \right| = \frac{\min(m \bmod n, n - m \bmod n)}{n}$

Informal description

For any natural numbers $m$ and $n$, and any linearly ordered ring $\alpha$, the absolute difference between the division $\frac{m}{n}$ and its rounded value $\text{round}\left(\frac{m}{n}\right)$ equals $\frac{\min(m \bmod n, n - m \bmod n)}{n}$. That is, $$\left| \frac{m}{n} - \text{round}\left(\frac{m}{n}\right) \right| = \frac{\min(m \bmod n, n - m \bmod n)}{n}.$$

sub_half_lt_round theorem

(x : α) : x - 1 / 2 < round x

Full source

@[bound]
theorem sub_half_lt_round (x : α) : x - 1 / 2 < round x := by
  rw [round_eq x, show x - 1 / 2 = x + 1 / 2 - 1 by linarith]
  exact Int.sub_one_lt_floor (x + 1 / 2)

Lower Bound for Rounding: $x - \frac{1}{2} < \text{round}(x)$

Informal description

For any element $x$ in a linearly ordered ring $\alpha$, the value $x - \frac{1}{2}$ is strictly less than the nearest integer to $x$ (rounding halves towards infinity), i.e., $x - \frac{1}{2} < \text{round}(x)$.

round_le_add_half theorem

(x : α) : round x ≤ x + 1 / 2

Full source

@[bound]
theorem round_le_add_half (x : α) : round x ≤ x + 1 / 2 := by
  rw [round_eq x]
  exact Int.floor_le (x + 1 / 2)

Upper Bound for Rounding: $\text{round}(x) \leq x + \frac{1}{2}$

Informal description

For any element $x$ in a linearly ordered ring $\alpha$, the rounded value of $x$ satisfies $\text{round}(x) \leq x + \frac{1}{2}$.

Int.map_round theorem

(f : F) (hf : StrictMono f) (a : α) : round (f a) = round a

Full source

theorem map_round (f : F) (hf : StrictMono f) (a : α) : round (f a) = round a := by
  simp_rw [round_eq, ← map_floor _ hf, map_add, one_div, map_inv₀, map_ofNat]

Rounding Preservation under Strictly Monotone Functions: $\text{round}(f(a)) = \text{round}(a)$

Informal description

Let $\alpha$ be a linearly ordered ring with a floor function, and let $F$ be a function-like type. For any strictly monotone function $f \colon \alpha \to \alpha$ and any element $a \in \alpha$, the rounding of $f(a)$ is equal to the rounding of $a$, i.e., $\text{round}(f(a)) = \text{round}(a)$.

Mathlib.Algebra.Order.Round

Main Definitions

Tags