Integer Rounding Functions

This module collects the integer-valued rounding primitives (round0, roundinf, roundup, rounddown, roundnearest) used to round a rational to a mantissa, together with their basic correctness properties such as round-to-even behaviour on half-integers.

@[reducible, inline]

abbrev IntRounder : Type

An integer-valued rounding rule taking a sign bit and a rational mantissa.

Equations

• IntRounder = (Bool → ℚ → ℕ)

def round0 (s : Bool) (q : ℚ) : ℕ

Round toward zero: the rounded mantissa is ⌊q⌋, ignoring the sign.

Equations

• round0 s q = if s = true then ⌊q⌋.natAbs else ⌊q⌋.natAbs

@[simp]

theorem round0_apply (s : Bool) (q : ℚ) : round0 s q = ⌊q⌋.natAbs

round0 ignores its sign argument.

def roundinf (s : Bool) (q : ℚ) : ℕ

Round away from zero: the rounded mantissa is ⌈q⌉, ignoring the sign.

Equations

• roundinf s q = if s = true then ⌈q⌉.natAbs else ⌈q⌉.natAbs

@[simp]

theorem roundinf_apply (s : Bool) (q : ℚ) : roundinf s q = ⌈q⌉.natAbs

roundinf ignores its sign argument.

def roundup (s : Bool) (q : ℚ) : ℕ

Round down (toward negative infinity), branching on the sign.

Equations

• roundup s q = if s = true then round0 s q else roundinf s q

def rounddown (s : Bool) (q : ℚ) : ℕ

Round up (toward positive infinity), branching on the sign.

Equations

• rounddown s q = if s = true then roundinf s q else round0 s q

def roundNearInt (q : ℚ) : ℤ

Round to the nearest integer, with ties broken to the even integer.

Equations

• roundNearInt q = if Int.fract q < 1 / 2 then ⌊q⌋ else if 1 / 2 < Int.fract q then ⌈q⌉ else if ⌊q⌋ % 2 = 0 then ⌊q⌋ else ⌈q⌉

def roundnearest (s : Bool) (q : ℚ) : ℕ

Round to nearest as an IntRounder: ties to even, ignoring the sign.

Equations

• roundnearest s q = if s = true then (roundNearInt q).natAbs else (roundNearInt q).natAbs

@[simp]

theorem roundnearest_apply (s : Bool) (q : ℚ) : roundnearest s q = (roundNearInt q).natAbs

roundnearest ignores its sign argument.

theorem round_near_int_of_nonneg {q : ℚ} (h : 0 ≤ q) : 0 ≤ roundNearInt q

theorem round_near_int_of_pos {q : ℚ} (h : 0 < q) : 0 ≤ roundNearInt q

theorem round_near_le_round_near {q1 q2 : ℚ} (h : q1 ≤ q2) : roundNearInt q1 ≤ roundNearInt q2

theorem round_near_eq_of (q : ℚ) (z : ℤ) : ↑z - 1 / 2 < q ∧ q < ↑z + 1 / 2 → z = roundNearInt q

theorem fract_eq_ceil_of_pos {q : ℚ} (h : 0 < Int.fract q) : Int.fract q = q + 1 - ↑⌈q⌉

theorem round_near_int_le (q : ℚ) : |↑(roundNearInt q) - q| ≤ 1 / 2

theorem round_near_int_of_int (z : ℤ) : roundNearInt ↑z = z

theorem round_near_add_half (z : ℤ) (h : z % 2 = 0) : roundNearInt (↑z + 1 / 2) = z

theorem round_near_sub_half (z : ℤ) (h : z % 2 = 0) : roundNearInt (↑z - 1 / 2) = z

theorem round_of_add_half (z : ℤ) : roundNearInt (↑z + 1 / 2) % 2 = 0

def floorInterval (z : ℤ) : Set ℚ

The set of rationals whose floor is z, namely [z, z + 1).

Equations

• floorInterval z = Set.Ico (↑z) (↑z + 1)

def ceilInterval (z : ℤ) : Set ℚ

The set of rationals whose ceiling is z, namely (z - 1, z].

Equations

• ceilInterval z = Set.Ioc (↑z - 1) ↑z

theorem floor_eq_iff_interval (z : ℤ) (q : ℚ) : ⌊q⌋ = z ↔ q ∈ floorInterval z

theorem ceil_eq_iff_interval (z : ℤ) (q : ℚ) : ⌈q⌉ = z ↔ q ∈ ceilInterval z

def roundNearInterval (z : ℤ) : Set ℚ

The set of rationals that round to nearest z: a closed interval when z is even (ties round to it) and an open interval otherwise.

Equations

• roundNearInterval z = if z % 2 = 0 then Set.Icc (↑z - 1 / 2) (↑z + 1 / 2) else Set.Ioo (↑z - 1 / 2) (↑z + 1 / 2)

theorem Icc_of_Ioo {α : Type} [PartialOrder α] {q x y : α} (h : q ∈ Set.Icc x y) (not_x : q ≠ x) (not_y : q ≠ y) : q ∈ Set.Ioo x y

theorem round_near_eq_iff (q : ℚ) (z : ℤ) : roundNearInt q = z ↔ q ∈ roundNearInterval z

def evalRoundNearInt : Mathlib.Meta.Positivity.PositivityExt

A positivity extension proving 0 ≤ roundNearInt q from 0 ≤ q.

Equations

• One or more equations did not get rendered due to their size.

class ValidRounder (f : Bool → ℚ → ℕ) : Prop

A rounding rule is valid if it is monotone on nonnegative inputs and is a left inverse of the cast ℕ → ℚ (so it fixes integer mantissas).

• le_iff_le (s : Bool) (q1 q2 : ℚ) : 0 ≤ q1 → q1 ≤ q2 → f s q1 ≤ f s q2

  The rounder is monotone in the mantissa on nonnegative inputs.

• leftInverse (s : Bool) : Function.LeftInverse (f s) Nat.cast

  The rounder fixes integer mantissas: it left-inverts the cast ℕ → ℚ.

instance instValidRounderRound0 : ValidRounder round0

instance instValidRounderRoundinf : ValidRounder roundinf

instance instValidRounderRoundup : ValidRounder roundup

instance instValidRounderRounddown : ValidRounder rounddown

instance instValidRounderRoundnearest : ValidRounder roundnearest

def IntRounder.neg (r : IntRounder) : IntRounder

The rounder obtained by flipping the sign bit, used to relate rounding of q and -q.

Equations

• r.neg s = r !s

theorem neg_neg_r (r : IntRounder) : r.neg.neg = r

theorem ValidRounder.neg {r : IntRounder} (rh : ValidRounder r) : ValidRounder r.neg

theorem neg_valid_rounder (r : IntRounder) : ValidRounder r.neg ↔ ValidRounder r

theorem roundnearest_neg : IntRounder.neg roundnearest = roundnearest

theorem round_eq_or (r : IntRounder) [rh : ValidRounder r] (b : Bool) {q : ℚ} (h : 0 ≤ q) : r b q = round0 b q ∨ r b q = roundinf b q

theorem round_eq_or' (r : IntRounder) [rh : ValidRounder r] (b : Bool) {q : ℚ} (h : 0 ≤ q) : r b q = rounddown b q ∨ r b q = roundup b q

theorem roundr_le (r : IntRounder) [rh : ValidRounder r] {b : Bool} {n : ℕ} {q : ℚ} (h : 0 ≤ q) (h' : q ≤ ↑n) : r b q ≤ n

theorem le_roundr (r : IntRounder) [rh : ValidRounder r] {b : Bool} {n : ℕ} {q : ℚ} (h' : ↑n ≤ q) : n ≤ r b q

theorem roundup_neg : IntRounder.neg roundup = rounddown

theorem rounddown_neg : IntRounder.neg rounddown = roundup