Documentation

Interval.Fixed

64-bit fixed point numbers #

`Fixed` definitions and basics #

@[unbox]

structure Fixed (s : Int64) :

A 64-bit fixed point number, corresponding to either

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

n : Int64

Instances For

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 ⋯

Instances For

@[instance_reducible]

instance instDecidableEqFixed {s✝ : Int64} :

DecidableEq (Fixed s✝)

Equations

instDecidableEqFixed = instDecidableEqFixed.decEq

@[instance_reducible]

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

Instances For

@[instance_reducible]

instance instNanFixed {s : Int64} :

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

Instances For

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

Approximate Fixed s by a Float

Equations

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

Instances For

@[instance_reducible]

instance instReprFixed {s : Int64} :

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_reducible]

instance instZeroFixed {s : Int64} :

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} :

@[simp]

theorem Fixed.zero_ne_nan {s : Int64} :

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 negation

Equations

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

Instances For

@[instance_reducible]

instance instNegFixed {s : Int64} :

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

@[simp]

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

The contrapose of -nan = nan

@[irreducible]

def Fixed.add {s : Int64} (x y : 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 }

Instances For

@[instance_reducible]

instance instAddFixed {s : Int64} :

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 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 }

Instances For

@[instance_reducible]

instance instSubFixed {s : Int64} :

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_reducible]

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} :

@[simp]

theorem Fixed.add_nan {s : Int64} {x : Fixed s} :

@[simp]

theorem Fixed.nan_sub {s : Int64} {x : Fixed s} :

@[simp]

theorem Fixed.sub_nan {s : Int64} {x : Fixed s} :

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_reducible]

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 : ℝ} :

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

@[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_reducible]

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_reducible]

instance instMinFixed {s : Int64} :

Equations

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

@[instance_reducible]

instance instMaxFixed {s : Int64} :

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.max propagates nan

Equations

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

Instances For

def Fixed.abs {s : Int64} (x : 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 }

Instances For

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} :

@[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

@[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

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

Positive Fixeds are ≠ nan

`Fixed` multiplication, rounding up or down #

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

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 }

Instances For

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) :

Multiply two positive, non-nan Fixeds

Equations

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

Instances For

@[irreducible]

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

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

Instances For

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) :

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

Equations

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

Instances For

@[irreducible]

def Fixed.ofNat0 (n : ℕ) :

Conversion from ℕ to Fixed 0, not rounding

Equations

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

Instances For

@[irreducible]

def Fixed.ofInt0 (n : ℤ) :

Conversion from ℤ to Fixed 0, not rounding

Equations

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

Instances For

@[instance_reducible]

instance Fixed.instOne {s : Int64} :

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

Equations

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

@[instance_reducible]

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) :

Conversion from ℤ

Equations

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

Instances For

@[irreducible]

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

Conversion from ℚ, rounding up or down

Equations

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

Instances For

@[irreducible]

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

Convert a Float to Fixed s

Equations

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

Instances For

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) :

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 }

Instances For

@[irreducible]

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

2^n : Fixed s, rounded up or down

Equations

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

Instances For

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) :

Fixed.log2 = nan if we're nonpos

@[simp]

theorem Fixed.log2_nan {s : Int64} :

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) :

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) :

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.

Instances For

@[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) :

Equations

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

Instances For

@[irreducible]

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

Equations

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

Instances For

@[instance_reducible]

instance Fixed.instLE {s : Int64} :

Equations

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

@[instance_reducible]

instance Fixed.instLT {s : Int64} :

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_reducible]

instance Fixed.decidableLT {s : Int64} :

DecidableRel fun (x1 x2 : Fixed s) => x1 < x2

Equations

x✝¹.decidableLT x✝ = id inferInstance

@[instance_reducible]

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_reducible]

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) :

@[simp]

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

nan.val ≤ x.val