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{cases} -1 & \text{if } r < 0, \ ~~, 0 & \text{if } r = 0, \ ~~, 1 & \text{if } r > 0. \end{cases}$

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

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

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

theorem Real.sign_of_pos {r : ℝ} (hr : 0 < r) : Real.sign r = 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 : ℝ) : Real.sign r = -1 ∨ Real.sign r = 0 ∨ Real.sign r = 1

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

This lemma is useful for working with ℝˣ

@[simp]

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

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

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

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

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

@[simp]

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

@[simp]

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