Absolute value, sign, inversion and division on extended real numbers

This file defines an absolute value and sign function on EReal and uses them to provide a CommMonoidWithZero instance, based on the absolute value and sign characterising all EReals. Then it defines the inverse of an EReal as ⊤⁻¹ = ⊥⁻¹ = 0, which leads to a DivInvMonoid instance and division.

Absolute value

def EReal.abs : EReal → ENNReal

The absolute value from EReal to ℝ≥0∞, mapping ⊥ and ⊤ to ⊤ and a real x to |x|.

Equations

• EReal.abs none = ⊤
• EReal.abs (some none) = ⊤
• EReal.abs (some (some x_1)) = ENNReal.ofReal |x_1|

@[simp]

theorem EReal.abs_top : ⊤.abs = ⊤

@[simp]

theorem EReal.abs_bot : ⊥.abs = ⊤

theorem EReal.abs_def (x : ℝ) : (↑x).abs = ENNReal.ofReal |x|

theorem EReal.abs_coe_lt_top (x : ℝ) : (↑x).abs < ⊤

@[simp]

theorem EReal.abs_eq_zero_iff {x : EReal} : x.abs = 0 ↔ x = 0

@[simp]

theorem EReal.abs_zero : EReal.abs 0 = 0

@[simp]

theorem EReal.coe_abs (x : ℝ) : ↑(↑x).abs = ↑|x|

@[simp]

theorem EReal.abs_neg (x : EReal) : (-x).abs = x.abs

@[simp]

theorem EReal.abs_mul (x y : EReal) : (x * y).abs = x.abs * y.abs

Sign

theorem EReal.sign_top : SignType.sign ⊤ = 1

theorem EReal.sign_bot : SignType.sign ⊥ = -1

@[simp]

theorem EReal.sign_coe (x : ℝ) : SignType.sign ↑x = SignType.sign x

@[simp]

theorem EReal.coe_coe_sign (x : SignType) : ↑↑x = ↑x

@[simp]

theorem EReal.sign_neg (x : EReal) : SignType.sign (-x) = -SignType.sign x

@[simp]

theorem EReal.sign_mul (x y : EReal) : SignType.sign (x * y) = SignType.sign x * SignType.sign y

@[simp]

theorem EReal.sign_mul_abs (x : EReal) : ↑(SignType.sign x) * ↑x.abs = x

@[simp]

theorem EReal.abs_mul_sign (x : EReal) : ↑x.abs * ↑(SignType.sign x) = x

theorem EReal.sign_eq_and_abs_eq_iff_eq {x y : EReal} : x.abs = y.abs ∧ SignType.sign x = SignType.sign y ↔ x = y

theorem EReal.le_iff_sign {x y : EReal} : x ≤ y ↔ SignType.sign x < SignType.sign y ∨ SignType.sign x = SignType.neg ∧ SignType.sign y = SignType.neg ∧ y.abs ≤ x.abs ∨ SignType.sign x = SignType.zero ∧ SignType.sign y = SignType.zero ∨ SignType.sign x = SignType.pos ∧ SignType.sign y = SignType.pos ∧ x.abs ≤ y.abs

instance EReal.instCommMonoidWithZero : CommMonoidWithZero EReal

Equations

• EReal.instCommMonoidWithZero = CommMonoidWithZero.mk ⋯ ⋯

instance EReal.instPosMulMono : PosMulMono EReal

instance EReal.instMulPosMono : MulPosMono EReal

instance EReal.instPosMulReflectLT : PosMulReflectLT EReal

instance EReal.instMulPosReflectLT : MulPosReflectLT EReal

theorem EReal.mul_le_mul_of_nonpos_right {a b c : EReal} (h : b ≤ a) (hc : c ≤ 0) : a * c ≤ b * c

@[simp]

theorem EReal.coe_pow (x : ℝ) (n : ℕ) : ↑(x ^ n) = ↑x ^ n

@[simp]

theorem EReal.coe_ennreal_pow (x : ENNReal) (n : ℕ) : ↑(x ^ n) = ↑x ^ n

theorem EReal.exists_nat_ge_mul {a : EReal} (ha : a ≠ ⊤) (n : ℕ) : ∃ (m : ℕ), a * ↑n ≤ ↑m

Min and Max

theorem EReal.min_neg_neg (x y : EReal) : -x ⊓ -y = -(x ⊔ y)

theorem EReal.max_neg_neg (x y : EReal) : -x ⊔ -y = -(x ⊓ y)

Inverse

def EReal.inv : EReal → EReal

Multiplicative inverse of an EReal. We choose 0⁻¹ = 0 to guarantee several good properties, for instance (a * b)⁻¹ = a⁻¹ * b⁻¹.

Equations

• EReal.inv none = 0
• EReal.inv (some none) = 0
• EReal.inv (some (some x_1)) = ↑x_1⁻¹

instance EReal.instInv : Inv EReal

Equations

• EReal.instInv = { inv := EReal.inv }

noncomputable instance EReal.instDivInvMonoid : DivInvMonoid EReal

Equations

• EReal.instDivInvMonoid = DivInvMonoid.mk EReal.instDivInvMonoid.proof_1 zpowRec EReal.instDivInvMonoid.proof_2 EReal.instDivInvMonoid.proof_3 EReal.instDivInvMonoid.proof_4

@[simp]

theorem EReal.inv_bot : ⊥⁻¹ = 0

@[simp]

theorem EReal.inv_top : ⊤⁻¹ = 0

theorem EReal.coe_inv (x : ℝ) : ↑x⁻¹ = (↑x)⁻¹

@[simp]

theorem EReal.inv_zero : 0⁻¹ = 0

noncomputable instance EReal.instDivInvOneMonoid : DivInvOneMonoid EReal

Equations

• EReal.instDivInvOneMonoid = DivInvOneMonoid.mk EReal.instDivInvOneMonoid.proof_1

theorem EReal.inv_neg (a : EReal) : (-a)⁻¹ = -a⁻¹

theorem EReal.inv_inv {a : EReal} (h : a ≠ ⊥) (h' : a ≠ ⊤) : a⁻¹⁻¹ = a

theorem EReal.mul_inv (a b : EReal) : (a * b)⁻¹ = a⁻¹ * b⁻¹

Inversion and Absolute Value

theorem EReal.sign_mul_inv_abs (a : EReal) : ↑(SignType.sign a) * (↑a.abs)⁻¹ = a⁻¹

theorem EReal.sign_mul_inv_abs' (a : EReal) : ↑(SignType.sign a) * ↑a.abs⁻¹ = a⁻¹

Inversion and Positivity

theorem EReal.bot_lt_inv (x : EReal) : ⊥ < x⁻¹

theorem EReal.inv_lt_top (x : EReal) : x⁻¹ < ⊤

theorem EReal.inv_nonneg_of_nonneg {a : EReal} (h : 0 ≤ a) : 0 ≤ a⁻¹

theorem EReal.inv_nonpos_of_nonpos {a : EReal} (h : a ≤ 0) : a⁻¹ ≤ 0

theorem EReal.inv_pos_of_pos_ne_top {a : EReal} (h : 0 < a) (h' : a ≠ ⊤) : 0 < a⁻¹

theorem EReal.inv_neg_of_neg_ne_bot {a : EReal} (h : a < 0) (h' : a ≠ ⊥) : a⁻¹ < 0

theorem EReal.inv_strictAntiOn : StrictAntiOn (fun (x : EReal) => x⁻¹) (Set.Ioi 0)

Division

theorem EReal.div_eq_inv_mul (a b : EReal) : a / b = b⁻¹ * a

theorem EReal.coe_div (a b : ℝ) : ↑(a / b) = ↑a / ↑b

theorem EReal.natCast_div_le (m n : ℕ) : ↑(m / n) ≤ ↑m / ↑n

@[simp]

theorem EReal.div_bot {a : EReal} : a / ⊥ = 0

@[simp]

theorem EReal.div_top {a : EReal} : a / ⊤ = 0

@[simp]

theorem EReal.div_zero {a : EReal} : a / 0 = 0

@[simp]

theorem EReal.zero_div {a : EReal} : 0 / a = 0

theorem EReal.top_div_of_pos_ne_top {a : EReal} (h : 0 < a) (h' : a ≠ ⊤) : ⊤ / a = ⊤

theorem EReal.top_div_of_neg_ne_bot {a : EReal} (h : a < 0) (h' : a ≠ ⊥) : ⊤ / a = ⊥

theorem EReal.bot_div_of_pos_ne_top {a : EReal} (h : 0 < a) (h' : a ≠ ⊤) : ⊥ / a = ⊥

theorem EReal.bot_div_of_neg_ne_bot {a : EReal} (h : a < 0) (h' : a ≠ ⊥) : ⊥ / a = ⊤

Division and Multiplication

theorem EReal.div_self {a : EReal} (h₁ : a ≠ ⊥) (h₂ : a ≠ ⊤) (h₃ : a ≠ 0) : a / a = 1

theorem EReal.mul_div (a b c : EReal) : a * (b / c) = a * b / c

theorem EReal.mul_div_right (a b c : EReal) : a / b * c = a * c / b

theorem EReal.mul_div_left_comm (a b c : EReal) : a * (b / c) = b * (a / c)

theorem EReal.div_div (a b c : EReal) : a / b / c = a / (b * c)

theorem EReal.div_mul_div_comm (a b c d : EReal) : a / b * (c / d) = a * c / (b * d)

theorem EReal.div_mul_cancel {a b : EReal} (h₁ : b ≠ ⊥) (h₂ : b ≠ ⊤) (h₃ : b ≠ 0) : a / b * b = a

theorem EReal.mul_div_cancel {a b : EReal} (h₁ : b ≠ ⊥) (h₂ : b ≠ ⊤) (h₃ : b ≠ 0) : b * (a / b) = a

theorem EReal.mul_div_mul_cancel {a b c : EReal} (h₁ : c ≠ ⊥) (h₂ : c ≠ ⊤) (h₃ : c ≠ 0) : a * c / (b * c) = a / b

theorem EReal.div_eq_iff {a b c : EReal} (hbot : b ≠ ⊥) (htop : b ≠ ⊤) (hzero : b ≠ 0) : c / b = a ↔ c = a * b

Division and Order

theorem EReal.monotone_div_right_of_nonneg {b : EReal} (h : 0 ≤ b) : Monotone fun (a : EReal) => a / b

theorem EReal.div_le_div_right_of_nonneg {a b c : EReal} (h : 0 ≤ c) (h' : a ≤ b) : a / c ≤ b / c

theorem EReal.strictMono_div_right_of_pos {b : EReal} (h : 0 < b) (h' : b ≠ ⊤) : StrictMono fun (a : EReal) => a / b

theorem EReal.div_lt_div_right_of_pos {a b c : EReal} (h₁ : 0 < c) (h₂ : c ≠ ⊤) (h₃ : a < b) : a / c < b / c

theorem EReal.antitone_div_right_of_nonpos {b : EReal} (h : b ≤ 0) : Antitone fun (a : EReal) => a / b

theorem EReal.div_le_div_right_of_nonpos {a b c : EReal} (h : c ≤ 0) (h' : a ≤ b) : b / c ≤ a / c

theorem EReal.strictAnti_div_right_of_neg {b : EReal} (h : b < 0) (h' : b ≠ ⊥) : StrictAnti fun (a : EReal) => a / b

theorem EReal.div_lt_div_right_of_neg {a b c : EReal} (h₁ : c < 0) (h₂ : c ≠ ⊥) (h₃ : a < b) : b / c < a / c

theorem EReal.le_div_iff_mul_le {a b c : EReal} (h : b > 0) (h' : b ≠ ⊤) : a ≤ c / b ↔ a * b ≤ c

theorem EReal.div_le_iff_le_mul {a b c : EReal} (h : 0 < b) (h' : b ≠ ⊤) : a / b ≤ c ↔ a ≤ b * c

theorem EReal.lt_div_iff {a b c : EReal} (h : 0 < b) (h' : b ≠ ⊤) : a < c / b ↔ a * b < c

theorem EReal.div_lt_iff {a b c : EReal} (h : 0 < c) (h' : c ≠ ⊤) : b / c < a ↔ b < a * c

theorem EReal.div_nonneg {a b : EReal} (h : 0 ≤ a) (h' : 0 ≤ b) : 0 ≤ a / b

theorem EReal.div_pos {a b : EReal} (ha : 0 < a) (hb : 0 < b) (hb' : b ≠ ⊤) : 0 < a / b

theorem EReal.div_nonpos_of_nonpos_of_nonneg {a b : EReal} (h : a ≤ 0) (h' : 0 ≤ b) : a / b ≤ 0

theorem EReal.div_nonpos_of_nonneg_of_nonpos {a b : EReal} (h : 0 ≤ a) (h' : b ≤ 0) : a / b ≤ 0

theorem EReal.div_nonneg_of_nonpos_of_nonpos {a b : EReal} (h : a ≤ 0) (h' : b ≤ 0) : 0 ≤ a / b

theorem EReal.le_mul_of_forall_lt {a b c : EReal} (h₁ : 0 < a ∨ b ≠ ⊤) (h₂ : a ≠ ⊤ ∨ 0 < b) (h : ∀ a' > a, ∀ b' > b, c ≤ a' * b') : c ≤ a * b

theorem EReal.mul_le_of_forall_lt_of_nonneg {a b c : EReal} (ha : 0 ≤ a) (hc : 0 ≤ c) (h : ∀ a' ∈ Set.Ioo 0 a, ∀ b' ∈ Set.Ioo 0 b, a' * b' ≤ c) : a * b ≤ c

Division Distributivity

theorem EReal.div_right_distrib_of_nonneg {a b c : EReal} (h : 0 ≤ a) (h' : 0 ≤ b) : (a + b) / c = a / c + b / c

theorem EReal.add_div_of_nonneg_right {a b c : EReal} (h : 0 ≤ c) : (a + b) / c = a / c + b / c