Floating point absolute value

theorem Floating.valid_abs {x : Floating} : Valid x.n.uabs.toInt64 x.s

abs is valid

@[irreducible]

def Floating.abs (x : Floating) : Floating

Absolute value

Equations

• x.abs = { n := x.n.uabs.toInt64, s := x.s, v := ⋯ }

@[simp]

theorem Floating.n_abs {x : Floating} : x.abs.n = x.n.uabs.toInt64

@[simp]

theorem Floating.s_abs {x : Floating} : x.abs.s = x.s

@[simp]

theorem Floating.abs_nan : nan.abs = nan

abs preserves nan

@[simp]

theorem Floating.abs_eq_nan {x : Floating} : x.abs = nan ↔ x = nan

abs preserves nan

@[simp]

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

abs is exact away from nan

@[simp]

theorem Floating.abs_nonneg {x : Floating} (n : x ≠ nan) : 0 ≤ x.abs.val

abs is nonnegative away from nan

@[simp]

theorem Floating.abs_of_nonneg {x : Floating} (x0 : 0 ≤ x.val) : x.abs = x

abs is the identity for nonnegatives (since nan < 0)

@[simp]

theorem Floating.abs_of_nonpos {x : Floating} (x0 : x.val ≤ 0) : x.abs = -x

abs is negates nonpositives (since -nan = nan)

theorem Floating.approx_abs {a : ℝ} {x : Floating} (ax : approx x a) : approx x.abs |a|

abs is conservative