Floating point scaling by changing the exponent

@[irreducible]

def Floating.scaleB (x : Floating) (t : Int64) : Floating

Scale by changing the exponent

Equations

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

@[irreducible]

def Floating.scaleB' (x : Floating) (t : Fixed 0) : Floating

Scale by changing the exponent

Equations

• x.scaleB' t = bif t == nan then nan else x.scaleB t.n

theorem Floating.approx_scaleB {x' : ℝ} {x : Floating} (t : Int64) (xm : approx x x') : approx (x.scaleB t) (x' * 2 ^ ↑t)

scaleB is conservative

theorem Floating.val_scaleB {x : Floating} {t : Int64} (n : x.scaleB t ≠ nan) : (x.scaleB t).val = x.val * 2 ^ ↑t

scaleB _ _ is exact if not nan

@[simp]

theorem Floating.nan_scaleB {t : Int64} : nan.scaleB t = nan

scaleB propagates nan

@[simp]

theorem Floating.ne_nan_of_scaleB {x : Floating} {t : Int64} (n : x.scaleB t ≠ nan) : x ≠ nan

scaleB propagates nan

@[simp]

theorem Floating.scaleB_zero {t : Int64} : scaleB 0 t = 0

Dividing by two

@[irreducible]

def Floating.div2 (x : Floating) : Floating

Equations

• x.div2 = x.scaleB (-1)

instance Floating.instDiv2 : Div2 Floating

Equations

• Floating.instDiv2 = { div2 := Floating.div2 }

theorem Floating.div2_def (x : Floating) : Div2.div2 x = x.div2

theorem Floating.approx_div2 {x : Floating} {x' : ℝ} (xm : approx x x') : approx x.div2 (x' / 2)

div2 is conservative

instance Floating.instApproxDiv2Real : ApproxDiv2 Floating ℝ

theorem Floating.val_div2 {x : Floating} (n : x.div2 ≠ nan) : x.div2.val = x.val / 2

div2 is exact if not nan

@[simp]

theorem Floating.nan_div2 : nan.div2 = nan

div2 propagates nan

@[simp]

theorem Floating.ne_nan_of_div2 {x : Floating} (n : x.div2 ≠ nan) : x ≠ nan

div2 propagates nan

instance Floating.instDiv2Zero : Div2Zero Floating