Rounding

This file defines the round function, which uses the floor or ceil function to round a number to the nearest integer.

Main Definitions

• round a: Nearest integer to a. It rounds halves towards infinity.

Tags

rounding

Round

def round {α : Type u_2} [Ring α] [LinearOrder α] [FloorRing α] (x : α) : ℤ

round x rounds x to the nearest integer, breaking ties towards positive infinity.

round (0.5 : ℚ) = 1.

Equations

• round x = if 2 * Int.fract x < 1 then ⌊x⌋ else ⌈x⌉

@[simp]

theorem round_zero {α : Type u_2} [Ring α] [LinearOrder α] [FloorRing α] : round 0 = 0

@[simp]

theorem round_one {α : Type u_2} [Ring α] [LinearOrder α] [FloorRing α] : round 1 = 1

@[simp]

theorem round_natCast {α : Type u_2} [Ring α] [LinearOrder α] [FloorRing α] (n : ℕ) : round ↑n = ↑n

@[simp]

theorem round_ofNat {α : Type u_2} [Ring α] [LinearOrder α] [FloorRing α] (n : ℕ) [n.AtLeastTwo] : round (OfNat.ofNat n) = OfNat.ofNat n

@[simp]

theorem round_intCast {α : Type u_2} [Ring α] [LinearOrder α] [FloorRing α] (n : ℤ) : round ↑n = n

theorem round_eq_div {α : Type u_2} [Ring α] [LinearOrder α] [FloorRing α] [IsStrictOrderedRing α] (x : α) : round x = (⌊2 * x⌋ + 1) / 2

Formula for round in terms of Int.floor, a version that works over any ring.

TODO: decide if we want to use this as a definition. It may be slightly faster over ℚ.

theorem round_eq_half_ceil_two_mul {α : Type u_2} [Ring α] [LinearOrder α] [FloorRing α] [IsStrictOrderedRing α] {x : α} (hx : 2 * Int.fract x ≠ 1) : round x = ⌈2 * x⌉ / 2

Away from the points with fractional part 1 / 2, round x = ⌈2 * x⌉ / 2.

@[simp]

theorem round_add_intCast {α : Type u_2} [Ring α] [LinearOrder α] [FloorRing α] [IsStrictOrderedRing α] (x : α) (y : ℤ) : round (x + ↑y) = round x + y

@[simp]

theorem round_add_one {α : Type u_2} [Ring α] [LinearOrder α] [FloorRing α] [IsStrictOrderedRing α] (a : α) : round (a + 1) = round a + 1

@[simp]

theorem round_sub_intCast {α : Type u_2} [Ring α] [LinearOrder α] [FloorRing α] [IsStrictOrderedRing α] (x : α) (y : ℤ) : round (x - ↑y) = round x - y

@[simp]

theorem round_sub_one {α : Type u_2} [Ring α] [LinearOrder α] [FloorRing α] [IsStrictOrderedRing α] (a : α) : round (a - 1) = round a - 1

@[simp]

theorem round_add_natCast {α : Type u_2} [Ring α] [LinearOrder α] [FloorRing α] [IsStrictOrderedRing α] (x : α) (y : ℕ) : round (x + ↑y) = round x + ↑y

@[simp]

theorem round_add_ofNat {α : Type u_2} [Ring α] [LinearOrder α] [FloorRing α] [IsStrictOrderedRing α] (x : α) (n : ℕ) [n.AtLeastTwo] : round (x + OfNat.ofNat n) = round x + OfNat.ofNat n

@[simp]

theorem round_sub_natCast {α : Type u_2} [Ring α] [LinearOrder α] [FloorRing α] [IsStrictOrderedRing α] (x : α) (y : ℕ) : round (x - ↑y) = round x - ↑y

@[simp]

theorem round_sub_ofNat {α : Type u_2} [Ring α] [LinearOrder α] [FloorRing α] [IsStrictOrderedRing α] (x : α) (n : ℕ) [n.AtLeastTwo] : round (x - OfNat.ofNat n) = round x - OfNat.ofNat n

@[simp]

theorem round_intCast_add {α : Type u_2} [Ring α] [LinearOrder α] [FloorRing α] [IsStrictOrderedRing α] (x : α) (y : ℤ) : round (↑y + x) = y + round x

@[simp]

theorem round_natCast_add {α : Type u_2} [Ring α] [LinearOrder α] [FloorRing α] [IsStrictOrderedRing α] (x : α) (y : ℕ) : round (↑y + x) = ↑y + round x

@[simp]

theorem round_ofNat_add {α : Type u_2} [Ring α] [LinearOrder α] [FloorRing α] [IsStrictOrderedRing α] (n : ℕ) [n.AtLeastTwo] (x : α) : round (OfNat.ofNat n + x) = OfNat.ofNat n + round x

theorem abs_sub_round_eq_min {α : Type u_2} [Ring α] [LinearOrder α] [FloorRing α] [IsStrictOrderedRing α] (x : α) : |x - ↑(round x)| = min (Int.fract x) (1 - Int.fract x)

theorem round_le {α : Type u_2} [Ring α] [LinearOrder α] [FloorRing α] [IsStrictOrderedRing α] (x : α) (z : ℤ) : |x - ↑(round x)| ≤ |x - ↑z|

theorem round_eq {α : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] [FloorRing α] (x : α) : round x = ⌊x + 1 / 2⌋

theorem round_eq_iff {α : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] [FloorRing α] {x : α} {n : ℤ} : round x = n ↔ x ∈ Set.Ico (↑n - 1 / 2) (↑n + 1 / 2)

@[simp]

theorem round_two_inv {α : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] [FloorRing α] : round 2⁻¹ = 1

@[simp]

theorem round_neg_two_inv {α : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] [FloorRing α] : round (-2⁻¹) = 0

@[simp]

theorem round_eq_zero_iff {α : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] [FloorRing α] {x : α} : round x = 0 ↔ x ∈ Set.Ico (-(1 / 2)) (1 / 2)

theorem abs_sub_round {α : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] [FloorRing α] (x : α) : |x - ↑(round x)| ≤ 1 / 2

theorem abs_sub_round_div_natCast_eq {α : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] [FloorRing α] {m n : ℕ} : |↑m / ↑n - ↑(round (↑m / ↑n))| = ↑(min (m % n) (n - m % n)) / ↑n

theorem sub_half_lt_round {α : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] [FloorRing α] (x : α) : x - 1 / 2 < ↑(round x)

theorem round_le_add_half {α : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] [FloorRing α] (x : α) : ↑(round x) ≤ x + 1 / 2

theorem Int.map_round {F : Type u_1} {α : Type u_2} {β : Type u_3} [Field α] [LinearOrder α] [IsStrictOrderedRing α] [Field β] [LinearOrder β] [IsStrictOrderedRing β] [FloorRing α] [FloorRing β] [FunLike F α β] [RingHomClass F α β] (f : F) (hf : StrictMono ⇑f) (a : α) : round (f a) = round a