Floating point negation

theorem Floating.valid_neg {x : Floating} : Valid (-x.n) x.s

instance Floating.instNeg : Neg Floating

Equations

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

@[simp]

theorem Floating.n_neg {x : Floating} : (-x).n = -x.n

@[simp]

theorem Floating.s_neg {x : Floating} : (-x).s = x.s

@[simp]

theorem Floating.neg_nan : -nan = nan

Negation propagates nan

@[simp]

theorem Floating.neg_eq_nan_iff {x : Floating} : -x = nan ↔ x = nan

Negation preserves nan

@[simp]

theorem Floating.neg_zero : -0 = 0

-0 = 0

@[simp]

theorem Floating.neg_eq_zero_iff {x : Floating} : -x = 0 ↔ x = 0

Negation preserves 0

@[simp]

theorem Floating.val_neg {x : Floating} (n : x ≠ nan) : (-x).val = -x.val

Negation flips .val, except at nan

@[simp]

theorem Floating.approx_neg {x : Floating} {a : ℝ} : approx (-x) a = approx x (-a)

Negation negates approx

instance Floating.instApproxNegReal : ApproxNeg Floating ℝ

- is conservative

instance Floating.instInvolutiveNeg : InvolutiveNeg Floating

- -x = x

Equations

• Floating.instInvolutiveNeg = { toNeg := Floating.instNeg, neg_neg := Floating.instInvolutiveNeg._proof_1 }