64-bit fixed point numbers

Fixed definitions and basics

@[unbox]

structure Fixed (s : Int64) : Type

A 64-bit fixed point number, corresponding to either

1. n * 2^s, if n ≠ Int64.min
2. Arbitrary, if n = Int64.min

• n : Int64

instance instDecidableEqFixed {s✝ : Int64} : DecidableEq (Fixed s✝)

Equations

• instDecidableEqFixed = instDecidableEqFixed.decEq

def instDecidableEqFixed.decEq {s✝ : Int64} (x✝ x✝¹ : Fixed s✝) : Decidable (x✝ = x✝¹)

Equations

• instDecidableEqFixed.decEq { n := a } { n := b } = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

instance instBEqFixed {s✝ : Int64} : BEq (Fixed s✝)

Equations

• instBEqFixed = { beq := instBEqFixed.beq }

def instBEqFixed.beq {s✝ : Int64} : Fixed s✝ → Fixed s✝ → Bool

Equations

• instBEqFixed.beq { n := a } { n := b } = (a == b)
• instBEqFixed.beq x✝¹ x✝ = false

instance instNanFixed {s : Int64} : Nan (Fixed s)

Sentinel value, indicating we don't know what the number is

Equations

• instNanFixed = { nan := { n := Int64.minValue } }

theorem Fixed.ext_iff {s : Int64} (x y : Fixed s) : x = y ↔ x.n = y.n

Reduce Fixed s equality to Int64 equality

instance instLawfulBEqFixed {s : Int64} : LawfulBEq (Fixed s)

Fixed s has nice equality

noncomputable def Fixed.val {s : Int64} (x : Fixed s) : ℝ

The ℝ that a Fixed represents, if it's not nan

Equations

• x.val = ↑↑x.n * 2 ^ ↑s

def Fixed.toFloat {s : Int64} (x : Fixed s) : Float

Approximate Fixed s by a Float

Equations

• x.toFloat = bif x == nan then Float.nan else x.n.toFloat.scaleB ↑s

instance instReprFixed {s : Int64} : Repr (Fixed s)

We print Fixed s as an approximate floating point number

Equations

• instReprFixed = { reprPrec := fun (x : Fixed s) (x_1 : ℕ) => Std.Format.text x.toFloat.toStringFull }

instance instZeroFixed {s : Int64} : Zero (Fixed s)

0 is easy regardless of s

Equations

• instZeroFixed = { zero := { n := 0 } }

theorem Fixed.zero_def {s : Int64} : 0 = { n := 0 }

theorem Fixed.nan_def {s : Int64} : nan = { n := Int64.minValue }

@[simp]

theorem Fixed.zero_n {s : Int64} : n 0 = 0

@[simp]

theorem Fixed.nan_n {s : Int64} : nan.n = Int64.minValue

@[simp]

theorem Fixed.val_zero {s : Int64} : val 0 = 0

theorem Fixed.val_of_s0 {x : Fixed 0} : x.val = ↑↑x.n

@[simp]

theorem Fixed.isNeg_nan {s : Int64} : nan.n < 0

@[simp]

theorem Fixed.zero_ne_nan {s : Int64} : 0 ≠ nan

theorem Fixed.val_eq_val {s : Int64} {x y : Fixed s} : x.val = y.val ↔ x = y

Additive group operations: add, sub, neg

def Fixed.neg {s : Int64} (x : Fixed s) : Fixed s

Fixed negation

Equations

• x.neg = { n := -x.n }

instance instNegFixed {s : Int64} : Neg (Fixed s)

Equations

• instNegFixed = { neg := fun (x : Fixed s) => x.neg }

theorem Fixed.neg_def {s : Int64} (x : Fixed s) : -x = x.neg

@[simp]

theorem Fixed.neg_nan {s : Int64} : -nan = nan

-nan = nan

@[simp]

theorem Fixed.ne_nan_of_neg {s : Int64} {x : Fixed s} (h : -x ≠ nan) : x ≠ nan

The contrapose of -nan = nan

@[irreducible]

def Fixed.add {s : Int64} (x y : Fixed s) : Fixed s

Fixed addition saturates to nan

Equations

• x.add y = bif x == nan || y == nan || x.n.isNeg == y.n.isNeg && x.n.isNeg != { n := x.n + y.n }.n.isNeg then nan else { n := x.n + y.n }

instance instAddFixed {s : Int64} : Add (Fixed s)

Equations

• instAddFixed = { add := fun (x y : Fixed s) => x.add y }

theorem Fixed.add_def {s : Int64} (x y : Fixed s) : x + y = x.add y

@[irreducible]

def Fixed.sub {s : Int64} (x y : Fixed s) : Fixed s

Fixed subtraction saturates to nan

Equations

• x.sub y = bif x == nan || y == nan || x.n.isNeg != y.n.isNeg && x.n.isNeg != { n := x.n - y.n }.n.isNeg then nan else { n := x.n - y.n }

instance instSubFixed {s : Int64} : Sub (Fixed s)

Equations

• instSubFixed = { sub := fun (x y : Fixed s) => x.sub y }

theorem Fixed.sub_def {s : Int64} (x y : Fixed s) : x - y = x.sub y

theorem Fixed.add_as_eq {s : Int64} (x y : Fixed s) : x + y = have z := { n := x.n + y.n }; if x = nan ∨ y = nan ∨ x.n.isNeg = y.n.isNeg ∧ x.n.isNeg ≠ z.n.isNeg then nan else z

Fixed addition with fewer bools

instance instInvolutiveNegFixed {s : Int64} : InvolutiveNeg (Fixed s)

-(-x) = x

Equations

• instInvolutiveNegFixed = { toNeg := instNegFixed, neg_neg := ⋯ }

@[simp]

theorem Fixed.neg_eq_nan {s : Int64} {x : Fixed s} : -x = nan ↔ x = nan

Negation preserves nan

@[simp]

theorem Fixed.neg_ne_nan {s : Int64} {x : Fixed s} : -x ≠ nan ↔ x ≠ nan

Negation preserves nan

@[simp]

theorem Fixed.neg_beq_nan {s : Int64} {x : Fixed s} : (-x == nan) = (x == nan)

Negation preserves nan

theorem Fixed.isNeg_neg {s : Int64} {x : Fixed s} (x0 : x.n ≠ 0) (xn : x ≠ nan) : (-x.n).isNeg = !x.n.isNeg

Negation flips isNeg unless we're 0 or nan

theorem Fixed.sub_eq_add_neg {s : Int64} (x y : Fixed s) : x - y = x + -y

x - y = x + (-y)

theorem Fixed.add_comm {s : Int64} (x y : Fixed s) : x + y = y + x

@[simp]

theorem Fixed.nan_add {s : Int64} {x : Fixed s} : nan + x = nan

@[simp]

theorem Fixed.add_nan {s : Int64} {x : Fixed s} : x + nan = nan

@[simp]

theorem Fixed.nan_sub {s : Int64} {x : Fixed s} : nan - x = nan

@[simp]

theorem Fixed.sub_nan {s : Int64} {x : Fixed s} : x - nan = nan

theorem Fixed.ne_nan_of_add {s : Int64} {x y : Fixed s} (h : x + y ≠ nan) : x ≠ nan ∧ y ≠ nan

If x + y ≠ nan, neither x or y are nan

theorem Fixed.ne_nan_of_sub {s : Int64} {x y : Fixed s} (h : x - y ≠ nan) : x ≠ nan ∧ y ≠ nan

If x - y ≠ nan, neither x or y are nan

theorem Fixed.val_neg {s : Int64} {x : Fixed s} (xn : x ≠ nan) : (-x).val = -x.val

Fixed.val commutes with negation, except at nan

theorem Fixed.val_add_eq {s : Int64} {x y : Fixed s} (h : (x.n + y.n).isNeg = x.n.isNeg) : { n := x.n + y.n }.val = x.val + y.val

Fixed.val commutes with add if isNeg matches the left argument

theorem Fixed.val_add_ne {s : Int64} {x y : Fixed s} (h : x.n.isNeg ≠ y.n.isNeg) : { n := x.n + y.n }.val = x.val + y.val

Fixed.val commutes with add if the two arguments have different isNegs

instance instApproxFixedReal {s : Int64} : Approx (Fixed s) ℝ

Fixed approximates ℝ

Equations

• instApproxFixedReal = { approx := fun (x : Fixed s) (a : ℝ) => x = nan ∨ x.val = a }

instance instApproxNanFixedReal {s : Int64} : ApproxNan (Fixed s) ℝ

@[simp]

theorem Fixed.approx_nan {s : Int64} {a : ℝ} : approx nan a

theorem Fixed.approx_val {s : Int64} (x : Fixed s) : approx x x.val

@[simp]

theorem Fixed.approx_zero_iff {s : Int64} {a : ℝ} : approx 0 a ↔ a = 0

instance instApproxZeroFixedReal {s : Int64} : ApproxZero (Fixed s) ℝ

instance instApproxZeroIffFixedReal {s : Int64} : ApproxZeroIff (Fixed s) ℝ

@[simp]

theorem Fixed.approx_eq_singleton {s : Int64} {a : ℝ} {x : Fixed s} (n : x ≠ nan) : approx x a ↔ x.val = a

If we're not nan, approx is a singleton

instance instApproxNegFixedReal {s : Int64} : ApproxNeg (Fixed s) ℝ

Fixed negation respects approx

@[simp]

theorem Fixed.approx_neg {s : Int64} {a : ℝ} (x : Fixed s) : approx (-x) (-a) ↔ approx x a

For Fixed, - and approx commute

instance instApproxAddFixedReal {s : Int64} : ApproxAdd (Fixed s) ℝ

Fixed addition respects approx

theorem Fixed.val_add {s : Int64} {x y : Fixed s} (n : x + y ≠ nan) : (x + y).val = x.val + y.val

Fixed.val commutes with add if the result isn't nan

instance instApproxSubFixedReal {s : Int64} : ApproxSub (Fixed s) ℝ

Fixed subtraction respects approx

theorem Fixed.val_sub {s : Int64} {x y : Fixed s} (n : x - y ≠ nan) : (x - y).val = x.val - y.val

Fixed.val commutes with sub if the result isn't nan

theorem Fixed.neg_add {s : Int64} {x y : Fixed s} : -(x + y) = -y + -x

neg_add for Fixed s

theorem Fixed.neg_sub {s : Int64} {x y : Fixed s} : -(x - y) = y - x

neg_sub for Fixed s

instance instApproxAddGroupFixedReal {s : Int64} : ApproxAddGroup (Fixed s) ℝ

Fixed approximates ℝ as an additive group

Equations

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

theorem Fixed.rounds_iff {s : Int64} {a : ℝ} {x : Fixed s} {up : Bool} : Rounds x a up ↔ x ≠ nan → if up = true then a ≤ x.val else x.val ≤ a

Order operations on Fixed: min, max, abs

theorem Fixed.val_lt_zero {s : Int64} {x : Fixed s} : x.val < 0 ↔ x.n < 0

theorem Fixed.val_nonneg {s : Int64} {x : Fixed s} : 0 ≤ x.val ↔ ¬x.n < 0

theorem Fixed.val_nonpos {s : Int64} {x : Fixed s} : x.val ≤ 0 ↔ x.n ≤ 0

theorem Fixed.val_pos {s : Int64} {x : Fixed s} : 0 < x.val ↔ 0 < x.n

theorem Fixed.isNeg_eq {s : Int64} {x : Fixed s} : x.n < 0 ↔ x.val < 0

theorem Fixed.val_eq_zero_iff {s : Int64} {x : Fixed s} : x.val ≠ 0 ↔ x ≠ 0

x.val = 0 iff x = 0 is

theorem Fixed.val_ne_zero_iff {s : Int64} {x : Fixed s} : x.val ≠ 0 ↔ x ≠ 0

x.val is nonzero iff x is

instance instMinFixed {s : Int64} : Min (Fixed s)

Equations

• instMinFixed = { min := fun (x y : Fixed s) => { n := min x.n y.n } }

instance instMaxFixed {s : Int64} : Max (Fixed s)

Max.max can't propagate nan sincde it needs to be order consistent

Equations

• instMaxFixed = { max := fun (x y : Fixed s) => { n := max x.n y.n } }

@[irreducible]

def Fixed.max {s : Int64} (x y : Fixed s) : Fixed s

Fixed.max propagates nan

Equations

• x.max y = -min (-x) (-y)

def Fixed.abs {s : Int64} (x : Fixed s) : Fixed s

Unfortunately we can't use |x|, since that notation can't use our own implementation.

Equations

• x.abs = { n := x.n.uabs.toInt64 }

theorem Fixed.min_def {s : Int64} {x y : Fixed s} : min x y = { n := min x.n y.n }

theorem Fixed.max_def' {s : Int64} {x y : Fixed s} : Max.max x y = { n := Max.max x.n y.n }

theorem Fixed.max_def {s : Int64} {x y : Fixed s} : x.max y = -min (-x) (-y)

theorem Fixed.abs_def {s : Int64} {x : Fixed s} : x.abs = { n := x.n.uabs.toInt64 }

@[simp]

theorem Fixed.min_nan {s : Int64} {x : Fixed s} : min x nan = nan

@[simp]

theorem Fixed.nan_min {s : Int64} {x : Fixed s} : min nan x = nan

@[simp]

theorem Fixed.max_nan {s : Int64} {x : Fixed s} : x.max nan = nan

@[simp]

theorem Fixed.nan_max {s : Int64} {x : Fixed s} : nan.max x = nan

@[simp]

theorem Fixed.abs_nan {s : Int64} : nan.abs = nan

@[simp]

theorem Fixed.abs_zero {s : Int64} : abs 0 = 0

@[simp]

theorem Fixed.abs_eq_nan {s : Int64} {x : Fixed s} : x.abs = nan ↔ x = nan

@[simp]

theorem Fixed.abs_ne_nan {s : Int64} {x : Fixed s} : x.abs ≠ nan ↔ x ≠ nan

@[simp]

theorem Fixed.isNeg_abs {s : Int64} {x : Fixed s} : x.abs.n < 0 ↔ x = nan

theorem Fixed.val_abs {s : Int64} {x : Fixed s} (n : x ≠ nan) : x.abs.val = |x.val|

theorem Fixed.approx_abs_eq {s : Int64} {a : ℝ} {x : Fixed s} (n : x ≠ nan) : approx x.abs a ↔ |x.val| = a

theorem Fixed.approx_abs {s : Int64} {a : ℝ} {x : Fixed s} (m : approx x a) : approx x.abs |a|

@[simp]

theorem Fixed.min_eq_nan {s : Int64} {x y : Fixed s} : min x y = nan ↔ x = nan ∨ y = nan

@[simp]

theorem Fixed.max_eq_nan {s : Int64} {x y : Fixed s} : x.max y = nan ↔ x = nan ∨ y = nan

theorem Fixed.val_lt_val {s : Int64} {x y : Fixed s} : x.val < y.val ↔ x.n < y.n

theorem Fixed.val_le_val {s : Int64} {x y : Fixed s} : x.val ≤ y.val ↔ x.n ≤ y.n

@[simp]

theorem Fixed.val_min {s : Int64} {x y : Fixed s} : (min x y).val = min x.val y.val

theorem Fixed.val_max {s : Int64} {x y : Fixed s} (nx : x ≠ nan) (ny : y ≠ nan) : (x.max y).val = Max.max x.val y.val

theorem Fixed.min_comm {s : Int64} {x y : Fixed s} : min x y = min y x

theorem Fixed.max_comm {s : Int64} {x y : Fixed s} : x.max y = y.max x

Order lemmas about nan

theorem Fixed.val_nan {s : Int64} : nan.val = -2 ^ (↑s + 63)

nan.val is very negative

@[simp]

theorem Fixed.val_nan_neg {s : Int64} : nan.val < 0

nan.val < 0

@[simp]

theorem Fixed.not_val_nan_nonneg {s : Int64} : ¬0 ≤ nan.val

¬0 ≤ nan.val

@[simp]

theorem Fixed.not_val_nan_pos {s : Int64} : ¬0 < nan.val

¬0 < nan.val

theorem Fixed.ne_nan_of_pos {s : Int64} {x : Fixed s} (h : 0 < x.val) : x ≠ nan

Positive Fixeds are ≠ nan

Fixed multiplication, rounding up or down

def Fixed.of_raw_uint128 {s : Int64} (n : UInt128) : Fixed s

Cast a UInt128 to Fixed s, ignoring s. Too large values become nan.

Equations

• Fixed.of_raw_uint128 n = bif n.hi != 0 || n.lo.toInt64.isNeg then nan else { n := n.lo.toInt64 }

theorem Fixed.lt_of_of_raw_uint128_ne_nan {n : UInt128} {s : Int64} (h : of_raw_uint128 n ≠ nan) : n.toNat < 2 ^ 63

If of_raw_uint128 ≠ nan, the input is small

@[irreducible]

def Fixed.mul_of_pos {s t : Int64} (x : Fixed s) (y : Fixed t) (u : Int64) (up : Bool) : Fixed u

Multiply two positive, non-nan Fixeds

Equations

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

@[irreducible]

def Fixed.mul {s t : Int64} (x : Fixed s) (y : Fixed t) (u : Int64) (up : Bool) : Fixed u

Multiply, changing s and rounding up or down. We have z = x * y z.n * 2^u = x.n * y.n * 2^(s + t) z.n = x.n * y.n * 2^(s + t - u)

Equations

• x.mul y u up = bif x == nan || y == nan then nan else have p := x.n.isNeg != y.n.isNeg; have z := x.abs.mul_of_pos y.abs u (up ^^ p); bif p then -z else z

theorem Fixed.of_raw_uint128_val {s : Int64} {n : UInt128} (h : of_raw_uint128 n ≠ nan) : (of_raw_uint128 n).val = ↑n * 2 ^ ↑s

theorem Fixed.toNat_shiftLeftSaturate_of_ne_nan {x : UInt128} {s : UInt64} {t : Int64} (h : of_raw_uint128 (x.shiftLeftSaturate s) ≠ nan) : (x.shiftLeftSaturate s).toNat = x.toNat * 2 ^ s.toNat

If we're not nan, shiftLeftSaturate is nice

@[simp]

theorem Fixed.nan_mul {s t : Int64} {y : Fixed t} {u : Int64} {up : Bool} : nan.mul y u up = nan

Fixed.mul nan _ _ _ = nan

@[simp]

theorem Fixed.mul_nan {s t : Int64} {x : Fixed s} {u : Int64} {up : Bool} : x.mul nan u up = nan

Fixed.mul nan _ _ _ = nan

theorem extract_exists_cond {α : Type} {c : Prop} {y : α} {e : α → Prop} : (∃ (x : α), (c → x = y) ∧ e x) ↔ if c then e y else ∃ (x : α), e x

theorem Fixed.approx_mul_of_pos {s t : Int64} {x : Fixed s} {y : Fixed t} {u : Int64} {up : Bool} (xn : x ≠ nan) (yn : y ≠ nan) (xp : ¬x.n < 0) (yp : ¬y.n < 0) {x' y' : ℝ} (ax : approx x x') (ay : approx y y') : Rounds (x.mul_of_pos y u up) (x' * y') up

Fixed.mul_of_pos respects approx

theorem Fixed.approx_mul {s t : Int64} (x : Fixed s) (y : Fixed t) (u : Int64) (up : Bool) {x' y' : ℝ} (ax : approx x x') (ay : approx y y') : Rounds (x.mul y u up) (x' * y') up

Fixed.mul respects approx

theorem Fixed.mul_le {s t : Int64} {x : Fixed s} {y : Fixed t} {u : Int64} (n : x.mul y u false ≠ nan) : (x.mul y u false).val ≤ x.val * y.val

Fixed.approx_mul in plainer form (down version)

theorem Fixed.le_mul {s t : Int64} {x : Fixed s} {y : Fixed t} {u : Int64} (n : x.mul y u true ≠ nan) : x.val * y.val ≤ (x.mul y u true).val

Fixed.approx_mul in plainer form (up version)

Conversion from ℕ, ℤ, ℚ, Float

@[irreducible]

def Fixed.ofNat {s : Int64} (n : ℕ) (up : Bool) : Fixed s

Conversion from ℕ literals to Fixed s, rounding up or down

Equations

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

@[irreducible]

def Fixed.ofNat0 (n : ℕ) : Fixed 0

Conversion from ℕ to Fixed 0, not rounding

Equations

• Fixed.ofNat0 n = bif decide (n.log2 < 63) then { n := ↑n } else nan

@[irreducible]

def Fixed.ofInt0 (n : ℤ) : Fixed 0

Conversion from ℤ to Fixed 0, not rounding

Equations

• Fixed.ofInt0 n = bif decide (n.natAbs.log2 < 63) then { n := ↑n } else nan

instance Fixed.instOne {s : Int64} : One (Fixed s)

We use the general .ofNat routine even for 1, to handle overflow, rounding down arbitrarily

Equations

• Fixed.instOne = { one := Fixed.ofNat 1 false }

instance instOfNatFixedOfAtLeastTwo {s : Int64} {n : ℕ} [n.AtLeastTwo] : OfNat (Fixed s) n

Conversion from ℕ literals to Fixed s

Equations

• instOfNatFixedOfAtLeastTwo = { ofNat := Fixed.ofNat n false }

@[irreducible]

def Fixed.ofInt {s : Int64} (n : ℤ) (up : Bool) : Fixed s

Conversion from ℤ

Equations

• Fixed.ofInt n up = bif decide (n < 0) then -Fixed.ofNat (-n).toNat !up else Fixed.ofNat n.toNat up

@[irreducible]

def Fixed.ofRat {s : Int64} (x : ℚ) (up : Bool) : Fixed s

Conversion from ℚ, rounding up or down

Equations

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

@[irreducible]

def Fixed.ofFloat {s : Int64} (x : Float) : Fixed s

Convert a Float to Fixed s

Equations

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

theorem Fixed.approx_ofNat {s : Int64} (n : ℕ) (up : Bool) : Rounds (ofNat n up) (↑n) up

Fixed.ofNat rounds the desired way

theorem Real.cast_natCast (n : ℤ) (n0 : 0 ≤ n) : ↑n = ↑n.toNat

theorem Fixed.approx_ofInt0 (n : ℤ) : approx (ofInt0 n) ↑n

Fixed.ofInt0 is conservative

@[simp]

theorem Fixed.ofInt0_natCast (n : ℕ) : ofInt0 ↑n = ofNat0 n

theorem Fixed.approx_ofNat0 (n : ℕ) : approx (ofNat0 n) ↑n

Fixed.ofNat0 is conservative

theorem Fixed.ofNat_le {s : Int64} {n : ℕ} (h : ofNat n false ≠ nan) : (ofNat n false).val ≤ ↑n

Fixed.approx_ofNat, down version

theorem Fixed.le_ofNat {s : Int64} {n : ℕ} (h : ofNat n true ≠ nan) : ↑n ≤ (ofNat n true).val

Fixed.approx_ofNat, up version

theorem Fixed.approx_ofInt {s : Int64} (n : ℤ) (up : Bool) : Rounds (ofInt n up) (↑n) up

Fixed.ofInt rounds the desired way

theorem Fixed.ofInt_le {s : Int64} {n : ℤ} (h : ofInt n false ≠ nan) : (ofInt n false).val ≤ ↑n

Fixed.approx_ofInt, down version

theorem Fixed.le_ofInt {s : Int64} {n : ℤ} (h : ofInt n true ≠ nan) : ↑n ≤ (ofInt n true).val

Fixed.approx_ofInt, up version

theorem Fixed.approx_ofRat {s : Int64} (x : ℚ) (up : Bool) : Rounds (ofRat x up) (↑x) up

Fixed.ofRat rounds the desired way

theorem Fixed.ofRat_le {s : Int64} {x : ℚ} (h : ofRat x false ≠ nan) : (ofRat x false).val ≤ ↑x

Fixed.approx_ofRat, down version

theorem Fixed.le_ofRat {s : Int64} {x : ℚ} (h : ofRat x true ≠ nan) : ↑x ≤ (ofRat x true).val

Fixed.approx_ofRat, up version

@[simp]

theorem Fixed.val_one_of_s0 : val 1 = 1

2^n and log2

@[irreducible]

def Fixed.log2 {s : Int64} (x : Fixed s) : Fixed 0

Find n s.t. 2^n ≤ x.val < 2^(n+1), or nan

Equations

• x.log2 = bif decide (x.n ≤ 0) then nan else { n := x.n.toUInt64.log2.toInt64 } + { n := s }

@[irreducible]

def Fixed.two_pow {s : Int64} (n : Fixed 0) (up : Bool) : Fixed s

2^n : Fixed s, rounded up or down

Equations

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

theorem Fixed.val_mem_log2 {s : Int64} {x : Fixed s} (h : x.log2 ≠ nan) : x.val ∈ Set.Ico (2 ^ ↑x.log2.n) (2 ^ (↑x.log2.n + 1))

x.log2 gives us a bracketing interval of two powers around x.val

theorem Fixed.approx_two_pow {s : Int64} (n : Fixed 0) (up : Bool) : Rounds (n.two_pow up) (2 ^ ↑n.n) up

Fixed.two_pow is correctly rounded

@[simp]

theorem Fixed.log2_eq_nan_of_nonpos {s : Int64} {x : Fixed s} (x0 : x.val ≤ 0) : x.log2 = nan

Fixed.log2 = nan if we're nonpos

@[simp]

theorem Fixed.log2_nan {s : Int64} : nan.log2 = nan

Fixed.log2 propagates nan

@[simp]

theorem Fixed.two_pow_nan {s : Int64} {up : Bool} : nan.two_pow up = nan

Fixed.two_pow propagates nan

@[simp]

theorem Fixed.ne_nan_of_two_pow {s : Int64} {n : Fixed 0} {up : Bool} (h : n.two_pow up ≠ nan) : n ≠ nan

Fixed.two_pow ≠ nan implies the argument ≠ nan

theorem Fixed.two_pow_le {s : Int64} {n : Fixed 0} (h : n.two_pow false ≠ nan) : (n.two_pow false).val ≤ 2 ^ ↑n.n

Fixed.approx_two_pow, down version

theorem Fixed.le_two_pow {s : Int64} {n : Fixed 0} (h : n.two_pow true ≠ nan) : 2 ^ ↑n.n ≤ (n.two_pow true).val

Fixed.approx_ofNat, up version

Exponent changes: Fixed s → Fixed t

@[irreducible]

def Fixed.repoint {s : Int64} (x : Fixed s) (t : Int64) (up : Bool) : Fixed t

Change Fixed s to Fixed t, rounding up or down as desired

Equations

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

@[simp]

theorem Fixed.repoint_nan {s : Int64} (t : Int64) (up : Bool) : nan.repoint t up = nan

Fixed.repoint propagates nan

theorem two_pow_coe_sub {s t : Int64} {k : Fixed 0} (st : s ≤ t) (e : { n := t } - { n := s } = k) (kn : k ≠ nan) : 2 ^ ↑t / 2 ^ ↑s = ↑(2 ^ k.n.toUInt64.toNat)

Special case of pow_sub involving UInt64s

theorem Fixed.approx_repoint {s : Int64} (x : Fixed s) (t : Int64) (up : Bool) {x' : ℝ} (ax : approx x x') : Rounds (x.repoint t up) x' up

Fixed.repoint is conservative

theorem Fixed.repoint_le {s : Int64} {x : Fixed s} {t : Int64} (n : x.repoint t false ≠ nan) : (x.repoint t false).val ≤ x.val

Fixed.repoint _ _ false rounds down

theorem Fixed.le_repoint {s : Int64} {x : Fixed s} {t : Int64} (n : x.repoint t true ≠ nan) : x.val ≤ (x.repoint t true).val

Fixed.repoint _ _ true rounds up

Ordering on Fixed s

@[irreducible]

def Fixed.ble {s : Int64} (x y : Fixed s) : Bool

Equations

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

@[irreducible]

def Fixed.blt {s : Int64} (x y : Fixed s) : Bool

Equations

• x.blt y = decide (x.n < y.n)

instance Fixed.instLE {s : Int64} : LE (Fixed s)

Equations

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

instance Fixed.instLT {s : Int64} : LT (Fixed s)

Equations

• Fixed.instLT = { lt := fun (x y : Fixed s) => x.blt y = true }

theorem Fixed.le_def {s : Int64} (x y : Fixed s) : x ≤ y ↔ x.n ≤ y.n

theorem Fixed.lt_def {s : Int64} (x y : Fixed s) : x < y ↔ x.n < y.n

instance Fixed.decidableLT {s : Int64} : DecidableRel fun (x1 x2 : Fixed s) => x1 < x2

Equations

• x✝¹.decidableLT x✝ = id inferInstance

instance Fixed.decidableLE {s : Int64} : DecidableRel fun (x1 x2 : Fixed s) => x1 ≤ x2

Equations

• x✝¹.decidableLE x✝ = id inferInstance

theorem Fixed.blt_eq_decide_lt {s : Int64} (x y : Fixed s) : x.blt y = decide (x < y)

theorem Fixed.ble_eq_decide_le {s : Int64} (x y : Fixed s) : x.ble y = decide (x ≤ y)

@[simp]

theorem Fixed.le_iff {s : Int64} {x y : Fixed s} : x ≤ y ↔ x.val ≤ y.val

The order is consistent with .val

@[simp]

theorem Fixed.lt_iff {s : Int64} {x y : Fixed s} : x < y ↔ x.val < y.val

The order is consistent with .val

instance instLinearOrderFixed {s : Int64} : LinearOrder (Fixed s)

Equations

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

@[simp]

theorem Fixed.nan_le {s : Int64} (x : Fixed s) : nan ≤ x

@[simp]

theorem Fixed.val_nan_le {s : Int64} (x : Fixed s) : nan.val ≤ x.val