Utilities for decimal numbers

Decimal basics

structure Decimal : Type

`n * 10^s

• n : ℤ

  Coefficient

• s : ℤ

  Decimal integer exponent

def instDecidableEqDecimal.decEq (x✝ x✝¹ : Decimal) : Decidable (x✝ = x✝¹)

Equations

• instDecidableEqDecimal.decEq { n := a, s := a_1 } { n := b, s := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

instance instDecidableEqDecimal : DecidableEq Decimal

Equations

• instDecidableEqDecimal = instDecidableEqDecimal.decEq

instance Decimal.instZero : Zero Decimal

Equations

• Decimal.instZero = { zero := { n := 0, s := 0 } }

theorem Decimal.zero_def : 0 = { n := 0, s := 0 }

instance Decimal.instOfScientific : OfScientific Decimal

The obvious instance

Equations

• Decimal.instOfScientific = { ofScientific := fun (n : ℕ) (z : Bool) (s : ℕ) => { n := ↑n, s := if z = true then -↑s else ↑s } }

instance Decimal.instOfNatOfAtLeastTwo (n : ℕ) [n.AtLeastTwo] : OfNat Decimal n

Equations

• Decimal.instOfNatOfAtLeastTwo n = { ofNat := { n := ↑n, s := 0 } }

instance Decimal.instNeg : Neg Decimal

Equations

• Decimal.instNeg = { neg := fun (x : Decimal) => { n := -x.n, s := x.s } }

theorem Decimal.neg_eq (x : Decimal) : -x = { n := -x.n, s := x.s }

Negation of a Decimal number negates the coefficient

@[irreducible]

def Decimal.val (x : Decimal) : ℝ

Convert to ℝ

Equations

• x.val = bif decide (x.n < 0) then -OfScientific.ofScientific x.n.natAbs (decide (x.s < 0)) x.s.natAbs else OfScientific.ofScientific x.n.natAbs (decide (x.s < 0)) x.s.natAbs

@[irreducible]

def Decimal.valq (x : Decimal) : ℚ

Convert to ℚ

Equations

• x.valq = bif decide (x.n < 0) then -OfScientific.ofScientific x.n.natAbs (decide (x.s < 0)) x.s.natAbs else OfScientific.ofScientific x.n.natAbs (decide (x.s < 0)) x.s.natAbs

instance Decimal.instCoeTailReal : CoeTail Decimal ℝ

Convert to ℝ

Equations

• Decimal.instCoeTailReal = { coe := fun (x : Decimal) => x.val }

theorem Decimal.Rat.ofScientific_eq (n : ℕ) (neg : Bool) (e : ℕ) : OfScientific.ofScientific n neg e = ↑n * 10 ^ if neg = true then -↑e else ↑e

theorem Decimal.Real.ofScientific_eq (n : ℕ) (neg : Bool) (e : ℕ) : OfScientific.ofScientific n neg e = ↑↑n * 10 ^ if neg = true then -↑e else ↑e

theorem Decimal.val_eq (x : Decimal) : x.val = ↑x.n * 10 ^ x.s

Decimal.val in simple form

theorem Decimal.valq_eq (x : Decimal) : x.valq = ↑x.n * 10 ^ x.s

Decimal.valq in simple form

theorem Decimal.coe_valq (x : Decimal) : ↑x.valq = x.val

val and valq are related

@[simp]

theorem Decimal.val_neg (x : Decimal) : (-x).val = -x.val

Decimal.val commutes with negation for ℚ

@[simp]

theorem Decimal.val_zero : val 0 = 0

Decimal.val 0 = 0

instance Decimal.instRepr : Repr Decimal

Print Decimal exactly in Decimal notation

Equations

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

Exactly rounded precision reduction

def Decimal.prec (x : Decimal) (p : ℕ) (up : Bool) : Decimal

Round to at most p significant digits

Equations

• x.prec p up = bif decide (Nat.log 10 x.n.toNat ≤ p) then x else have t := Nat.log 10 x.n.toNat - p; { n := x.n.rdiv (10 ^ t) up, s := x.s + ↑t }

def Decimal.aprec (x : Decimal) (p : ℤ) (up : Bool) : Decimal

Round to absolute precision 10 ^ p

Equations

• x.aprec p up = bif decide (p ≤ x.s) then x else have t := (p - x.s).toNat; { n := x.n.rdiv (10 ^ t) up, s := x.s + ↑t }

theorem Decimal.prec_le (x : Decimal) (p : ℕ) : (x.prec p false).val ≤ x.val

prec rounds down if desired

theorem Decimal.le_prec (x : Decimal) (p : ℕ) : x.val ≤ (x.prec p true).val

prec rounds up if desired

theorem Decimal.aprec_le (x : Decimal) (p : ℤ) : (x.aprec p false).val ≤ x.val

aprec rounds down if desired

theorem Decimal.le_aprec (x : Decimal) (p : ℤ) : x.val ≤ (x.aprec p true).val

aprec rounds up if desired

Exactly rounded conversion from binary exponents to decimal

We start with n * 2^s and want to convert it to m * 10^t, rounding as desired. Say we're rounding down, and want to achieve precision prec: m * 10^t ≤ n * 2^s ∧ m < 10^(prec+1) m = ⌊n * 2^s / 10^t⌋ ∧ m < 10^(prec+1) m = ⌊n * 2^s / 10^t⌋ ∧ n * 2^s / 10^t < 10^(prec+1) m = ⌊n * 2^s / 10^t⌋ ∧ t = ⌈logb 10 (n * 2^s / 10^(prec+1))⌉ We'd like to compute the above without ever blowing up, say by computing a very large n * 2^s value. We can estimate t using approximate arithmetic, then shift it up or down a bit to get the minimal value that works. A t value works if f t = round (n * 2^s / 10^t) satisfies f t < 10^(prec+1) Meh, doing it without blowup seems involved: it . Let's just eat the blowup for now.

def Decimal.OfBinary.log_10_2_num : ℕ

Equations

• Decimal.OfBinary.log_10_2_num = 3010299956639812

def Decimal.OfBinary.log_10_2_den : ℕ

Equations

• Decimal.OfBinary.log_10_2_den = 10000000000000000

def Decimal.OfBinary.t_underestimate (n : ℕ) (s : ℤ) (prec : ℕ) : ℤ

We underestimate t, since we'll then increase it until we fit within prec

Equations

• Decimal.OfBinary.t_underestimate n s prec = ↑(Nat.log 10 n) + s * ↑Decimal.OfBinary.log_10_2_num / ↑Decimal.OfBinary.log_10_2_den - ↑prec - 2

def Decimal.OfBinary.m_of_t (n : ℕ) (s t : ℤ) (up : Bool) : ℕ

n * 2^s / 10^t, rounding as desired

Equations

• Decimal.OfBinary.m_of_t n s t up = if up = true then ⌈↑n * 2 ^ (s - t) / 5 ^ t⌉₊ else ⌊↑n * 2 ^ (s - t) / 5 ^ t⌋₊

theorem Decimal.OfBinary.m_of_t_le (n : ℕ) (s t : ℤ) : ↑(m_of_t n s t false) ≤ ↑n * 2 ^ s / 10 ^ t

m_of_t rounds down if desired

theorem Decimal.OfBinary.le_m_of_t (n : ℕ) (s t : ℤ) : ↑n * 2 ^ s / 10 ^ t ≤ ↑(m_of_t n s t true)

m_of_t rounds up if desired

theorem Decimal.OfBinary.antitone_m_of_t (n : ℕ) (s : ℤ) (up : Bool) : Antitone fun (x : ℤ) => m_of_t n s x up

m_of_t n s t is antitone in t

theorem Decimal.OfBinary.exists_t (n : ℕ) (s t : ℤ) (up : Bool) : ∃ (dt : ℕ), m_of_t n s (t + ↑dt) up ≤ 1

A sufficiently large t means m ≤ 1

theorem Decimal.OfBinary.exists_t' (n : ℕ) (s t : ℤ) (prec : ℕ) (up : Bool) : ∃ (dt : ℕ), m_of_t n s (t + ↑dt) up ≤ 10 ^ (prec + 1)

A sufficiently large t means m ≤ 10 ^ (prec + 1)

def Decimal.OfBinary.ofBinaryNat (n : ℕ) (s : ℤ) (prec : ℕ) (up : Bool) : Decimal

Convert binary to Decimal, rounding to a desired decimal precision

Equations

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

theorem Decimal.OfBinary.ofBinaryNat_le (n : ℕ) (s : ℤ) (prec : ℕ) : (ofBinaryNat n s prec false).val ≤ ↑n * 2 ^ s

ofBinaryNat rounds down if desired

theorem Decimal.OfBinary.le_ofBinaryNat (n : ℕ) (s : ℤ) (prec : ℕ) : ↑n * 2 ^ s ≤ (ofBinaryNat n s prec true).val

ofBinaryNat rounds up if desired

def Decimal.ofBinary (n s : ℤ) (prec : ℕ) (up : Bool) : Decimal

Convert binary to Decimal, rounding to a desired decimal precision

Equations

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

theorem Decimal.ofBinary_le (n s : ℤ) (prec : ℕ) : (ofBinary n s prec false).val ≤ ↑n * 2 ^ s

ofBinary rounds down if desired

theorem Decimal.le_ofBinary (n s : ℤ) (prec : ℕ) : ↑n * 2 ^ s ≤ (ofBinary n s prec true).val

ofBinary rounds up if desired

Comparison

For now we very lazily convert to ℚ, even though this can be very inefficient.

def Decimal.ble (x y : Decimal) : Bool

Comparison via (possibly very inefficient) conversion to ℚ

Equations

• x.ble y = decide (x.valq ≤ y.valq)

instance Decimal.instLE : LE Decimal

Equations

• Decimal.instLE = { le := fun (x y : Decimal) => x.ble y = true }

instance Decimal.instLT : LT Decimal

Equations

• Decimal.instLT = { lt := fun (x y : Decimal) => (!y.ble x) = true }

instance Decimal.instMin : Min Decimal

Equations

• Decimal.instMin = { min := fun (x y : Decimal) => bif x.ble y then x else y }

instance Decimal.instMax : Max Decimal

Equations

• Decimal.instMax = { max := fun (x y : Decimal) => bif x.ble y then y else x }

theorem Decimal.le_def (x y : Decimal) : x ≤ y ↔ x.ble y = true

theorem Decimal.lt_def (x y : Decimal) : x < y ↔ (!y.ble x) = true

theorem Decimal.le_iff (x y : Decimal) : x ≤ y ↔ x.val ≤ y.val

theorem Decimal.lt_iff (x y : Decimal) : x < y ↔ x.val < y.val

instance Decimal.instPreorder : Preorder Decimal

Equations

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

instance Decimal.instDecidableLe (x y : Decimal) : Decidable (x ≤ y)

Equations

• x.instDecidableLe y = ⋯.mpr ((x.ble y).decEq true)

theorem Decimal.min_def (x y : Decimal) : x ⊓ y = if x ≤ y then x else y

theorem Decimal.max_def (x y : Decimal) : x ⊔ y = if x ≤ y then y else x

@[simp]

theorem Decimal.val_min (x y : Decimal) : (x ⊓ y).val = min x.val y.val

@[simp]

theorem Decimal.val_max (x y : Decimal) : (x ⊔ y).val = max x.val y.val

Exact arithmetic

def Decimal.add (x y : Decimal) : Decimal

Exact addition of Decimal

Equations

• x.add y = { n := x.n * 10 ^ (x.s - min x.s y.s).natAbs + y.n * 10 ^ (y.s - min x.s y.s).natAbs, s := min x.s y.s }

def Decimal.div2 (x : Decimal) : Decimal

Exact division by 2 for Decimal

Equations

• x.div2 = { n := 5 * x.n, s := x.s - 1 }

instance Decimal.instAdd : Add Decimal

Equations

• Decimal.instAdd = { add := Decimal.add }

instance Decimal.instSub : Sub Decimal

Equations

• Decimal.instSub = { sub := fun (x y : Decimal) => x + -y }

theorem Decimal.add_def (x y : Decimal) : x + y = x.add y

theorem Decimal.sub_def (x y : Decimal) : x - y = x + -y

@[simp]

theorem Decimal.val_add {x y : Decimal} : (x + y).val = x.val + y.val

Decimal.add is exact

@[simp]

theorem Decimal.val_sub {x y : Decimal} : (x - y).val = x.val - y.val

Decimal.sub is exact

@[simp]

theorem Decimal.val_div2 {x : Decimal} : x.div2.val = x.val / 2

Decimal.div2 is exact

Decimal intervals and balls

structure Decimal.Interval : Type

A nonempty interval of Decimal

• lo : Decimal
• hi : Decimal
• le : self.lo.val ≤ self.hi.val

structure Decimal.Ball : Type

A nonempty ball of Decimal

• c : Decimal
• r : Decimal
• r0 : 0 ≤ self.r.val

instance Decimal.instApproxIntervalReal : Approx Interval ℝ

Equations

• Decimal.instApproxIntervalReal = { approx := fun (x : Decimal.Interval) (a : ℝ) => x.lo.val ≤ a ∧ a ≤ x.hi.val }

instance Decimal.instApproxBallReal : Approx Ball ℝ

Equations

• Decimal.instApproxBallReal = { approx := fun (x : Decimal.Ball) (a : ℝ) => x.c.val - x.r.val ≤ a ∧ a ≤ x.c.val + x.r.val }

instance Decimal.instZeroInterval : Zero Interval

Equations

• Decimal.instZeroInterval = { zero := { lo := 0, hi := 0, le := Decimal.instZeroInterval._proof_1 } }

instance Decimal.instZeroBall : Zero Ball

Equations

• Decimal.instZeroBall = { zero := { c := 0, r := 0, r0 := Decimal.instZeroBall._proof_1 } }

def Decimal.Interval.mk' (x y : Decimal) : Interval

Equations

• Decimal.Interval.mk' x y = if h : x ≤ y then { lo := x, hi := y, le := ⋯ } else { lo := y, hi := x, le := ⋯ }

instance Decimal.instReprBall : Repr Ball

Equations

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

def Decimal.Interval.ball (x : Interval) : Ball

Turn an interval into a ball, exactly

Equations

• x.ball = { c := (x.lo + x.hi).div2, r := (x.lo + x.hi).div2 - x.lo, r0 := ⋯ }

@[simp]

theorem Decimal.Interval.approx_ball (x : Interval) (x' : ℝ) : approx x.ball x' ↔ approx x x'

.ball commutes with approx

def Decimal.Ball.prec (x : Ball) (p : ℕ) : Ball

Precision reduce an Ball, growing it slightly if necessary

Equations

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

theorem Decimal.Ball.approx_prec (x : Ball) (p : ℕ) (y : ℝ) (m : approx x y) : approx (x.prec p) y

Ball.prec is conservative