Real sign function

This file introduces and contains some results about Real.sign which maps negative real numbers to -1, positive real numbers to 1, and 0 to 0.

Main definitions

• Real.sign r is $\{\begin{array}{ll}-1& \text{if }r<0,\\ 0& \text{if }r=0,\\ 1& \text{if }r>0.\end{array}$

Tags

sign function

noncomputable def Real.sign (r : ℝ) : ℝ

The sign function that maps negative real numbers to -1, positive numbers to 1, and 0 otherwise.

Equations

• r.sign = if r < 0 then -1 else if 0 < r then 1 else 0

theorem Real.sign_of_neg {r : ℝ} (hr : r < 0) : r.sign = -1

theorem Real.sign_of_pos {r : ℝ} (hr : 0 < r) : r.sign = 1

@[simp]

theorem Real.sign_zero : Real.sign 0 = 0

@[simp]

theorem Real.sign_one : Real.sign 1 = 1

theorem Real.sign_apply_eq (r : ℝ) : r.sign = -1 ∨ r.sign = 0 ∨ r.sign = 1

theorem Real.sign_apply_eq_of_ne_zero (r : ℝ) (h : r ≠ 0) : r.sign = -1 ∨ r.sign = 1

This lemma is useful for working with ℝˣ

@[simp]

theorem Real.sign_eq_zero_iff {r : ℝ} : r.sign = 0 ↔ r = 0

theorem Real.sign_intCast (z : ℤ) : (↑z).sign = ↑z.sign

@[deprecated Real.sign_intCast]

theorem Real.sign_int_cast (z : ℤ) : (↑z).sign = ↑z.sign

Alias of Real.sign_intCast.

theorem Real.sign_neg {r : ℝ} : (-r).sign = -r.sign

theorem Real.sign_mul_nonneg (r : ℝ) : 0 ≤ r.sign * r

theorem Real.sign_mul_pos_of_ne_zero (r : ℝ) (hr : r ≠ 0) : 0 < r.sign * r

@[simp]

theorem Real.inv_sign (r : ℝ) : r.sign⁻¹ = r.sign

@[simp]

theorem Real.sign_inv (r : ℝ) : r⁻¹.sign = r.sign