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 rounds a number to the nearest integer. round (1 / 2) = 1

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[deprecated round_add_intCast (since := "2025-03-23")]

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

Alias of round_add_intCast.

@[simp]

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

@[simp]

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

@[deprecated round_sub_intCast (since := "2025-03-23")]

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

Alias of round_sub_intCast.

@[simp]

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

@[simp]

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

@[deprecated round_add_natCast (since := "2025-03-23")]

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

Alias of round_add_natCast.

@[simp]

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

@[simp]

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

@[deprecated round_sub_natCast (since := "2025-03-23")]

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

Alias of round_sub_natCast.

@[simp]

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

@[simp]

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

@[deprecated round_intCast_add (since := "2025-03-23")]

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

Alias of round_intCast_add.

@[simp]

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

@[deprecated round_natCast_add (since := "2025-03-23")]

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

Alias of round_natCast_add.

@[simp]

theorem round_ofNat_add {α : Type u_2} [Ring α] [LinearOrder α] [IsStrictOrderedRing α] [FloorRing α] (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 α] [IsStrictOrderedRing α] [FloorRing α] (x : α) : |x - ↑(round x)| = Int.fract x ⊓ (1 - Int.fract x)

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

theorem round_eq {α : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] [FloorRing α] (x : α) : round x = ⌊x + 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))| = ↑(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