Mathlib.Algebra.Order.Ring.Unbundled.Basic

add_one_le_two_mul theorem

[LE R] [NonAssocSemiring R] [AddLeftMono R] {a : R} (a1 : 1 ≤ a) : a + 1 ≤ 2 * a

Full source

theorem add_one_le_two_mul [LE R] [NonAssocSemiring R] [AddLeftMono R] {a : R}
    (a1 : 1 ≤ a) : a + 1 ≤ 2 * a :=
  calc
    a + 1 ≤ a + a := add_le_add_left a1 a
    _ = 2 * a := (two_mul _).symm

Inequality for elements greater than one in left-monotone semirings: $1 \leq a \implies a + 1 \leq 2a$

Informal description

Let $R$ be a non-associative semiring with a preorder relation $\leq$ where addition is left-monotone. For any element $a \in R$ satisfying $1 \leq a$, we have $a + 1 \leq 2 \cdot a$.

add_le_mul_two_add theorem

[ZeroLEOneClass R] [MulPosMono R] [AddLeftMono R] (a2 : 2 ≤ a) (b0 : 0 ≤ b) : a + (2 + b) ≤ a * (2 + b)

Full source

theorem add_le_mul_two_add [ZeroLEOneClass R] [MulPosMono R] [AddLeftMono R]
    (a2 : 2 ≤ a) (b0 : 0 ≤ b) : a + (2 + b) ≤ a * (2 + b) :=
  calc
    a + (2 + b) ≤ a + (a + a * b) :=
      add_le_add_left (add_le_add a2 <| le_mul_of_one_le_left b0 <| one_le_two.trans a2) a
    _ ≤ a * (2 + b) := by rw [mul_add, mul_two, add_assoc]

Inequality for elements ≥2 and nonnegative elements in monotone semirings: $a \geq 2 \land b \geq 0 \implies a + (2 + b) \leq a(2 + b)$

Informal description

Let $R$ be a preordered semiring with the following properties: 1. $0 \leq 1$ holds in $R$ (`ZeroLEOneClass`) 2. Right multiplication by nonnegative elements is monotone (`MulPosMono`) 3. Addition is left-monotone (`AddLeftMono`) Then for any elements $a, b \in R$ with $2 \leq a$ and $0 \leq b$, we have the inequality: $$a + (2 + b) \leq a \cdot (2 + b)$$

mul_le_mul_of_nonpos_left theorem

[ExistsAddOfLE R] [PosMulMono R] [AddRightMono R] [AddRightReflectLE R] (h : b ≤ a) (hc : c ≤ 0) : c * a ≤ c * b

Full source

theorem mul_le_mul_of_nonpos_left [ExistsAddOfLE R] [PosMulMono R]
    [AddRightMono R] [AddRightReflectLE R]
    (h : b ≤ a) (hc : c ≤ 0) : c * a ≤ c * b := by
  obtain ⟨d, hcd⟩ := exists_add_of_le hc
  refine le_of_add_le_add_right (a := d * b + d * a) ?_
  calc
    _ = d * b := by rw [add_left_comm, ← add_mul, ← hcd, zero_mul, add_zero]
    _ ≤ d * a := mul_le_mul_of_nonneg_left h <| hcd.trans_le <| add_le_of_nonpos_left hc
    _ = _ := by rw [← add_assoc, ← add_mul, ← hcd, zero_mul, zero_add]

Monotonicity of Left Multiplication by Nonpositive Elements: $c \leq 0 \implies (b \leq a \to c \cdot a \leq c \cdot b)$

Informal description

Let $R$ be a preordered semiring where: 1. The order relation has the "exists add of ≤" property (for any $a \leq b$, there exists $c$ such that $b = a + c$) 2. Left multiplication by nonnegative elements is monotone (`PosMulMono`) 3. Addition is right monotone (`AddRightMono`) 4. The order relation reflects addition on the right (`AddRightReflectLE`) Then for any elements $a, b, c \in R$ with $b \leq a$ and $c \leq 0$, we have $c \cdot a \leq c \cdot b$.

mul_le_mul_of_nonpos_right theorem

[ExistsAddOfLE R] [MulPosMono R] [AddRightMono R] [AddRightReflectLE R] (h : b ≤ a) (hc : c ≤ 0) : a * c ≤ b * c

Full source

theorem mul_le_mul_of_nonpos_right [ExistsAddOfLE R] [MulPosMono R]
    [AddRightMono R] [AddRightReflectLE R]
    (h : b ≤ a) (hc : c ≤ 0) : a * c ≤ b * c := by
  obtain ⟨d, hcd⟩ := exists_add_of_le hc
  refine le_of_add_le_add_right (a := b * d + a * d) ?_
  calc
    _ = b * d := by rw [add_left_comm, ← mul_add, ← hcd, mul_zero, add_zero]
    _ ≤ a * d := mul_le_mul_of_nonneg_right h <| hcd.trans_le <| add_le_of_nonpos_left hc
    _ = _ := by rw [← add_assoc, ← mul_add, ← hcd, mul_zero, zero_add]

Monotonicity of Right Multiplication by Nonpositive Elements: $c \leq 0 \implies (b \leq a \to a \cdot c \leq b \cdot c)$

Informal description

Let $R$ be a preordered semiring where: 1. The order relation has the "exists add of ≤" property (for any $a \leq b$, there exists $c$ such that $b = a + c$) 2. Right multiplication by nonnegative elements is monotone (`MulPosMono`) 3. Addition is right monotone (`AddRightMono`) 4. The order relation reflects addition on the right (`AddRightReflectLE`) Then for any elements $a, b, c \in R$ with $b \leq a$ and $c \leq 0$, we have $a \cdot c \leq b \cdot c$.

mul_nonneg_of_nonpos_of_nonpos theorem

[ExistsAddOfLE R] [MulPosMono R] [AddRightMono R] [AddRightReflectLE R] (ha : a ≤ 0) (hb : b ≤ 0) : 0 ≤ a * b

Full source

theorem mul_nonneg_of_nonpos_of_nonpos [ExistsAddOfLE R] [MulPosMono R]
    [AddRightMono R] [AddRightReflectLE R]
    (ha : a ≤ 0) (hb : b ≤ 0) : 0 ≤ a * b := by
  simpa only [zero_mul] using mul_le_mul_of_nonpos_right ha hb

Nonnegative Product of Nonpositive Elements in Preordered Semiring

Informal description

Let $R$ be a preordered semiring where: 1. The order relation has the "exists add of ≤" property (for any $a \leq b$, there exists $c$ such that $b = a + c$) 2. Right multiplication by nonnegative elements is monotone (`MulPosMono`) 3. Addition is right monotone (`AddRightMono`) 4. The order relation reflects addition on the right (`AddRightReflectLE`) Then for any elements $a, b \in R$ with $a \leq 0$ and $b \leq 0$, we have $0 \leq a \cdot b$.

mul_le_mul_of_nonneg_of_nonpos theorem

 [ExistsAddOfLE R] [MulPosMono R] [PosMulMono R] [AddRightMono R] [AddRightReflectLE R] (hca : c ≤ a) (hbd : b ≤ d)
  (hc : 0 ≤ c) (hb : b ≤ 0) : a * b ≤ c * d

Full source

theorem mul_le_mul_of_nonneg_of_nonpos [ExistsAddOfLE R] [MulPosMono R] [PosMulMono R]
    [AddRightMono R] [AddRightReflectLE R]
    (hca : c ≤ a) (hbd : b ≤ d) (hc : 0 ≤ c) (hb : b ≤ 0) : a * b ≤ c * d :=
  (mul_le_mul_of_nonpos_right hca hb).trans <| mul_le_mul_of_nonneg_left hbd hc

Inequality for Products with Nonnegative and Nonpositive Factors: $0 \leq c \leq a$ and $b \leq d \leq 0$ implies $a \cdot b \leq c \cdot d$

Informal description

Let $R$ be a preordered semiring where: 1. The order relation has the "exists add of ≤" property (for any $a \leq b$, there exists $c$ such that $b = a + c$) 2. Right multiplication by nonnegative elements is monotone (`MulPosMono`) 3. Left multiplication by nonnegative elements is monotone (`PosMulMono`) 4. Addition is right monotone (`AddRightMono`) 5. The order relation reflects addition on the right (`AddRightReflectLE`) Then for any elements $a, b, c, d \in R$ with $c \leq a$, $b \leq d$, $0 \leq c$, and $b \leq 0$, we have $a \cdot b \leq c \cdot d$.

mul_le_mul_of_nonneg_of_nonpos' theorem

 [ExistsAddOfLE R] [PosMulMono R] [MulPosMono R] [AddRightMono R] [AddRightReflectLE R] (hca : c ≤ a) (hbd : b ≤ d)
  (ha : 0 ≤ a) (hd : d ≤ 0) : a * b ≤ c * d

Full source

theorem mul_le_mul_of_nonneg_of_nonpos' [ExistsAddOfLE R] [PosMulMono R] [MulPosMono R]
    [AddRightMono R] [AddRightReflectLE R]
    (hca : c ≤ a) (hbd : b ≤ d) (ha : 0 ≤ a) (hd : d ≤ 0) : a * b ≤ c * d :=
  (mul_le_mul_of_nonneg_left hbd ha).trans <| mul_le_mul_of_nonpos_right hca hd

Inequality for Products with Nonnegative and Nonpositive Factors: $0 \leq a$ and $d \leq 0$ implies $a \cdot b \leq c \cdot d$ when $c \leq a$ and $b \leq d$

Informal description

Let $R$ be a preordered semiring where: 1. The order relation has the property that for any $a \leq b$, there exists $c$ such that $b = a + c$, 2. Left multiplication by nonnegative elements is monotone, 3. Right multiplication by nonnegative elements is monotone, 4. Addition is right monotone, 5. The order relation reflects addition on the right. Then for any elements $a, b, c, d \in R$ with $c \leq a$, $b \leq d$, $0 \leq a$, and $d \leq 0$, we have $a \cdot b \leq c \cdot d$.

mul_le_mul_of_nonpos_of_nonneg theorem

 [ExistsAddOfLE R] [MulPosMono R] [PosMulMono R] [AddRightMono R] [AddRightReflectLE R] (hac : a ≤ c) (hdb : d ≤ b)
  (hc : c ≤ 0) (hb : 0 ≤ b) : a * b ≤ c * d

Full source

theorem mul_le_mul_of_nonpos_of_nonneg [ExistsAddOfLE R] [MulPosMono R] [PosMulMono R]
    [AddRightMono R] [AddRightReflectLE R]
    (hac : a ≤ c) (hdb : d ≤ b) (hc : c ≤ 0) (hb : 0 ≤ b) : a * b ≤ c * d :=
  (mul_le_mul_of_nonneg_right hac hb).trans <| mul_le_mul_of_nonpos_left hdb hc

Inequality for Products with Nonpositive and Nonnegative Factors: $a \leq c \leq 0$ and $0 \leq b$ and $d \leq b$ implies $a \cdot b \leq c \cdot d$

Informal description

Let $R$ be a preordered semiring where: 1. The order relation has the property that for any $a \leq b$, there exists $c$ such that $b = a + c$, 2. Right multiplication by nonnegative elements is monotone, 3. Left multiplication by nonnegative elements is monotone, 4. Addition is right monotone, 5. The order relation reflects addition on the right. Then for any elements $a, b, c, d \in R$ with $a \leq c$, $d \leq b$, $c \leq 0$, and $0 \leq b$, we have $a \cdot b \leq c \cdot d$.

mul_le_mul_of_nonpos_of_nonneg' theorem

 [ExistsAddOfLE R] [PosMulMono R] [MulPosMono R] [AddRightMono R] [AddRightReflectLE R] (hca : c ≤ a) (hbd : b ≤ d)
  (ha : 0 ≤ a) (hd : d ≤ 0) : a * b ≤ c * d

Full source

theorem mul_le_mul_of_nonpos_of_nonneg' [ExistsAddOfLE R] [PosMulMono R] [MulPosMono R]
    [AddRightMono R] [AddRightReflectLE R]
    (hca : c ≤ a) (hbd : b ≤ d) (ha : 0 ≤ a) (hd : d ≤ 0) : a * b ≤ c * d :=
  (mul_le_mul_of_nonneg_left hbd ha).trans <| mul_le_mul_of_nonpos_right hca hd

Inequality for Products with Nonpositive and Nonnegative Factors: $c \leq a \geq 0$ and $b \leq d \leq 0$ implies $a \cdot b \leq c \cdot d$

Informal description

Let $R$ be a preordered semiring where: 1. The order relation has the "exists add of ≤" property (for any $a \leq b$, there exists $c$ such that $b = a + c$) 2. Left multiplication by nonnegative elements is monotone (`PosMulMono`) 3. Right multiplication by nonnegative elements is monotone (`MulPosMono`) 4. Addition is right monotone (`AddRightMono`) 5. The order relation reflects addition on the right (`AddRightReflectLE`) Then for any elements $a, b, c, d \in R$ with $c \leq a$, $b \leq d$, $a \geq 0$, and $d \leq 0$, we have $a \cdot b \leq c \cdot d$.

mul_le_mul_of_nonpos_of_nonpos theorem

 [ExistsAddOfLE R] [MulPosMono R] [PosMulMono R] [AddRightMono R] [AddRightReflectLE R] (hca : c ≤ a) (hdb : d ≤ b)
  (hc : c ≤ 0) (hb : b ≤ 0) : a * b ≤ c * d

Full source

theorem mul_le_mul_of_nonpos_of_nonpos [ExistsAddOfLE R] [MulPosMono R] [PosMulMono R]
    [AddRightMono R] [AddRightReflectLE R]
    (hca : c ≤ a) (hdb : d ≤ b) (hc : c ≤ 0) (hb : b ≤ 0) : a * b ≤ c * d :=
  (mul_le_mul_of_nonpos_right hca hb).trans <| mul_le_mul_of_nonpos_left hdb hc

Inequality for Products with Nonpositive Factors: $c \leq a$, $d \leq b$, $c \leq 0$, $b \leq 0$ implies $a \cdot b \leq c \cdot d$

Informal description

Let $R$ be a preordered semiring where: 1. The order relation has the "exists add of $\leq$" property (for any $a \leq b$, there exists $c$ such that $b = a + c$) 2. Right multiplication by nonnegative elements is monotone (`MulPosMono`) 3. Left multiplication by nonnegative elements is monotone (`PosMulMono`) 4. Addition is right monotone (`AddRightMono`) 5. The order relation reflects addition on the right (`AddRightReflectLE`) Then for any elements $a, b, c, d \in R$ with $c \leq a$, $d \leq b$, $c \leq 0$, and $b \leq 0$, we have $a \cdot b \leq c \cdot d$.

mul_le_mul_of_nonpos_of_nonpos' theorem

 [ExistsAddOfLE R] [PosMulMono R] [MulPosMono R] [AddRightMono R] [AddRightReflectLE R] (hca : c ≤ a) (hdb : d ≤ b)
  (ha : a ≤ 0) (hd : d ≤ 0) : a * b ≤ c * d

Full source

theorem mul_le_mul_of_nonpos_of_nonpos' [ExistsAddOfLE R] [PosMulMono R] [MulPosMono R]
    [AddRightMono R] [AddRightReflectLE R]
    (hca : c ≤ a) (hdb : d ≤ b) (ha : a ≤ 0) (hd : d ≤ 0) : a * b ≤ c * d :=
  (mul_le_mul_of_nonpos_left hdb ha).trans <| mul_le_mul_of_nonpos_right hca hd

Inequality for Products with Nonpositive Factors: $c \leq a \leq 0$ and $d \leq b$ with $d \leq 0$ implies $a \cdot b \leq c \cdot d$

Informal description

Let $R$ be a preordered semiring where: 1. The order relation has the "exists add of ≤" property (for any $a \leq b$, there exists $c$ such that $b = a + c$) 2. Left multiplication by nonnegative elements is monotone 3. Right multiplication by nonnegative elements is monotone 4. Addition is right monotone 5. The order relation reflects addition on the right Then for any elements $a, b, c, d \in R$ with $c \leq a$, $d \leq b$, $a \leq 0$, and $d \leq 0$, we have $a \cdot b \leq c \cdot d$.

le_mul_of_le_one_left theorem

[ExistsAddOfLE R] [MulPosMono R] [AddRightMono R] [AddRightReflectLE R] (hb : b ≤ 0) (h : a ≤ 1) : b ≤ a * b

Full source

/-- Variant of `mul_le_of_le_one_left` for `b` non-positive instead of non-negative. -/
theorem le_mul_of_le_one_left [ExistsAddOfLE R] [MulPosMono R]
    [AddRightMono R] [AddRightReflectLE R]
    (hb : b ≤ 0) (h : a ≤ 1) : b ≤ a * b := by
  simpa only [one_mul] using mul_le_mul_of_nonpos_right h hb

Lower Bound for Multiplication by Elements Less Than One on Nonpositive Elements: $b \leq 0 \land a \leq 1 \implies b \leq a \cdot b$

Informal description

Let $R$ be a preordered semiring where: 1. The order relation has the "exists add of ≤" property (for any $a \leq b$, there exists $c$ such that $b = a + c$) 2. Right multiplication by nonnegative elements is monotone (`MulPosMono`) 3. Addition is right monotone (`AddRightMono`) 4. The order relation reflects addition on the right (`AddRightReflectLE`) Then for any elements $a, b \in R$ with $b \leq 0$ and $a \leq 1$, we have $b \leq a \cdot b$.

mul_le_of_one_le_left theorem

[ExistsAddOfLE R] [MulPosMono R] [AddRightMono R] [AddRightReflectLE R] (hb : b ≤ 0) (h : 1 ≤ a) : a * b ≤ b

Full source

/-- Variant of `le_mul_of_one_le_left` for `b` non-positive instead of non-negative. -/
theorem mul_le_of_one_le_left [ExistsAddOfLE R] [MulPosMono R]
    [AddRightMono R] [AddRightReflectLE R]
    (hb : b ≤ 0) (h : 1 ≤ a) : a * b ≤ b := by
  simpa only [one_mul] using mul_le_mul_of_nonpos_right h hb

Left Multiplication Inequality for Nonpositive Elements: $b \leq 0 \land 1 \leq a \implies a \cdot b \leq b$

Informal description

Let $R$ be a preordered semiring where: 1. The order relation has the "exists add of ≤" property (for any $a \leq b$, there exists $c$ such that $b = a + c$) 2. Right multiplication by nonnegative elements is monotone 3. Addition is right monotone 4. The order relation reflects addition on the right Then for any elements $a, b \in R$ with $b \leq 0$ and $1 \leq a$, we have $a \cdot b \leq b$.

le_mul_of_le_one_right theorem

[ExistsAddOfLE R] [PosMulMono R] [AddRightMono R] [AddRightReflectLE R] (ha : a ≤ 0) (h : b ≤ 1) : a ≤ a * b

Full source

/-- Variant of `mul_le_of_le_one_right` for `a` non-positive instead of non-negative. -/
theorem le_mul_of_le_one_right [ExistsAddOfLE R] [PosMulMono R]
    [AddRightMono R] [AddRightReflectLE R]
    (ha : a ≤ 0) (h : b ≤ 1) : a ≤ a * b := by
  simpa only [mul_one] using mul_le_mul_of_nonpos_left h ha

Lower Bound for Right Multiplication by Elements Less Than One on Nonpositive Elements: $a \leq 0 \land b \leq 1 \implies a \leq a \cdot b$

Informal description

Let $R$ be a preordered semiring where: 1. The order relation has the "exists add of ≤" property (for any $a \leq b$, there exists $c$ such that $b = a + c$) 2. Left multiplication by nonnegative elements is monotone (`PosMulMono`) 3. Addition is right monotone (`AddRightMono`) 4. The order relation reflects addition on the right (`AddRightReflectLE`) Then for any elements $a, b \in R$ with $a \leq 0$ and $b \leq 1$, we have $a \leq a \cdot b$.

mul_le_of_one_le_right theorem

[ExistsAddOfLE R] [PosMulMono R] [AddRightMono R] [AddRightReflectLE R] (ha : a ≤ 0) (h : 1 ≤ b) : a * b ≤ a

Full source

/-- Variant of `le_mul_of_one_le_right` for `a` non-positive instead of non-negative. -/
theorem mul_le_of_one_le_right [ExistsAddOfLE R] [PosMulMono R]
    [AddRightMono R] [AddRightReflectLE R]
    (ha : a ≤ 0) (h : 1 ≤ b) : a * b ≤ a := by
  simpa only [mul_one] using mul_le_mul_of_nonpos_left h ha

Right Multiplication Inequality for Nonpositive Elements: $a \leq 0 \land 1 \leq b \implies a \cdot b \leq a$

Informal description

Let $R$ be a preordered semiring where: 1. The order relation has the "exists add of ≤" property (for any $a \leq b$, there exists $c$ such that $b = a + c$) 2. Left multiplication by nonnegative elements is monotone (`PosMulMono`) 3. Addition is right monotone (`AddRightMono`) 4. The order relation reflects addition on the right (`AddRightReflectLE`) Then for any elements $a, b \in R$ with $a \leq 0$ and $1 \leq b$, we have $a \cdot b \leq a$.

antitone_mul_left theorem

[ExistsAddOfLE R] [PosMulMono R] [AddRightMono R] [AddRightReflectLE R] {a : R} (ha : a ≤ 0) : Antitone (a * ·)

Full source

theorem antitone_mul_left [ExistsAddOfLE R] [PosMulMono R]
    [AddRightMono R] [AddRightReflectLE R]
    {a : R} (ha : a ≤ 0) : Antitone (a * ·) := fun _ _ b_le_c =>
  mul_le_mul_of_nonpos_left b_le_c ha

Antitonicity of Left Multiplication by Nonpositive Elements

Informal description

Let $R$ be a preordered semiring where: 1. The order relation has the "exists add of ≤" property (for any $a \leq b$, there exists $c$ such that $b = a + c$) 2. Left multiplication by nonnegative elements is monotone (`PosMulMono`) 3. Addition is right monotone (`AddRightMono`) 4. The order relation reflects addition on the right (`AddRightReflectLE`) Then for any element $a \in R$ with $a \leq 0$, the function $x \mapsto a \cdot x$ is antitone (order-reversing), meaning that for any $x_1 \leq x_2$ in $R$, we have $a \cdot x_2 \leq a \cdot x_1$.

antitone_mul_right theorem

 [ExistsAddOfLE R] [MulPosMono R] [AddRightMono R] [AddRightReflectLE R] {a : R} (ha : a ≤ 0) : Antitone fun x => x * a

Full source

theorem antitone_mul_right [ExistsAddOfLE R] [MulPosMono R]
    [AddRightMono R] [AddRightReflectLE R]
    {a : R} (ha : a ≤ 0) : Antitone fun x => x * a := fun _ _ b_le_c =>
  mul_le_mul_of_nonpos_right b_le_c ha

Antitonicity of Right Multiplication by Nonpositive Elements

Informal description

Let $R$ be a preordered semiring where: 1. The order relation has the "exists add of ≤" property (for any $a \leq b$, there exists $c$ such that $b = a + c$) 2. Right multiplication by nonnegative elements is monotone (`MulPosMono`) 3. Addition is right monotone (`AddRightMono`) 4. The order relation reflects addition on the right (`AddRightReflectLE`) Then for any element $a \in R$ with $a \leq 0$, the function $x \mapsto x \cdot a$ is antitone (order-reversing), meaning that for any $x_1 \leq x_2$ in $R$, we have $x_2 \cdot a \leq x_1 \cdot a$.

Monotone.const_mul_of_nonpos theorem

 [ExistsAddOfLE R] [PosMulMono R] [AddRightMono R] [AddRightReflectLE R] (hf : Monotone f) (ha : a ≤ 0) :
  Antitone fun x => a * f x

Full source

theorem Monotone.const_mul_of_nonpos [ExistsAddOfLE R] [PosMulMono R]
    [AddRightMono R] [AddRightReflectLE R]
    (hf : Monotone f) (ha : a ≤ 0) : Antitone fun x => a * f x :=
  (antitone_mul_left ha).comp_monotone hf

Antitonicity of Left Multiplication by Nonpositive Elements on Monotone Functions

Informal description

Let $R$ be a preordered semiring where: 1. The order relation has the "exists add of ≤" property (for any $a \leq b$, there exists $c$ such that $b = a + c$) 2. Left multiplication by nonnegative elements is monotone (`PosMulMono`) 3. Addition is right monotone (`AddRightMono`) 4. The order relation reflects addition on the right (`AddRightReflectLE`) Given a monotone function $f$ and an element $a \in R$ with $a \leq 0$, the function $x \mapsto a \cdot f(x)$ is antitone (order-reversing).

Monotone.mul_const_of_nonpos theorem

 [ExistsAddOfLE R] [MulPosMono R] [AddRightMono R] [AddRightReflectLE R] (hf : Monotone f) (ha : a ≤ 0) :
  Antitone fun x => f x * a

Full source

theorem Monotone.mul_const_of_nonpos [ExistsAddOfLE R] [MulPosMono R]
    [AddRightMono R] [AddRightReflectLE R]
    (hf : Monotone f) (ha : a ≤ 0) : Antitone fun x => f x * a :=
  (antitone_mul_right ha).comp_monotone hf

Antitonicity of Monotone Function Multiplied by Nonpositive Constant

Informal description

Let $R$ be a preordered semiring where: 1. The order relation has the "exists add of ≤" property (for any $a \leq b$, there exists $c$ such that $b = a + c$) 2. Right multiplication by nonnegative elements is monotone 3. Addition is right monotone 4. The order relation reflects addition on the right If $f : R \to R$ is a monotone function and $a \in R$ satisfies $a \leq 0$, then the function $x \mapsto f(x) \cdot a$ is antitone (order-reversing).

Antitone.const_mul_of_nonpos theorem

 [ExistsAddOfLE R] [PosMulMono R] [AddRightMono R] [AddRightReflectLE R] (hf : Antitone f) (ha : a ≤ 0) :
  Monotone fun x => a * f x

Full source

theorem Antitone.const_mul_of_nonpos [ExistsAddOfLE R] [PosMulMono R]
    [AddRightMono R] [AddRightReflectLE R]
    (hf : Antitone f) (ha : a ≤ 0) : Monotone fun x => a * f x :=
  (antitone_mul_left ha).comp hf

Monotonicity of Left Multiplication by Nonpositive Elements Applied to Antitone Functions

Informal description

Let $R$ be a preordered semiring where: 1. The order relation has the "exists add of ≤" property (for any $a \leq b$, there exists $c$ such that $b = a + c$) 2. Left multiplication by nonnegative elements is monotone 3. Addition is right monotone 4. The order relation reflects addition on the right If $f : R \to R$ is an antitone function and $a \in R$ satisfies $a \leq 0$, then the function $x \mapsto a \cdot f(x)$ is monotone.

Antitone.mul_const_of_nonpos theorem

 [ExistsAddOfLE R] [MulPosMono R] [AddRightMono R] [AddRightReflectLE R] (hf : Antitone f) (ha : a ≤ 0) :
  Monotone fun x => f x * a

Full source

theorem Antitone.mul_const_of_nonpos [ExistsAddOfLE R] [MulPosMono R]
    [AddRightMono R] [AddRightReflectLE R]
    (hf : Antitone f) (ha : a ≤ 0) : Monotone fun x => f x * a :=
  (antitone_mul_right ha).comp hf

Monotonicity of Right Multiplication by Nonpositive Elements for Antitone Functions

Informal description

Let $R$ be a preordered semiring where: 1. The order relation has the "exists add of ≤" property (for any $a \leq b$, there exists $c$ such that $b = a + c$) 2. Right multiplication by nonnegative elements is monotone (`MulPosMono`) 3. Addition is right monotone (`AddRightMono`) 4. The order relation reflects addition on the right (`AddRightReflectLE`) If $f : R \to R$ is an antitone function and $a \in R$ satisfies $a \leq 0$, then the function $x \mapsto f(x) \cdot a$ is monotone. That is, for any $x_1 \leq x_2$ in $R$, we have $f(x_1) \cdot a \leq f(x_2) \cdot a$.

Antitone.mul_monotone theorem

 [ExistsAddOfLE R] [PosMulMono R] [MulPosMono R] [AddRightMono R] [AddRightReflectLE R] (hf : Antitone f)
  (hg : Monotone g) (hf₀ : ∀ x, f x ≤ 0) (hg₀ : ∀ x, 0 ≤ g x) : Antitone (f * g)

Full source

theorem Antitone.mul_monotone [ExistsAddOfLE R] [PosMulMono R] [MulPosMono R]
    [AddRightMono R] [AddRightReflectLE R]
    (hf : Antitone f) (hg : Monotone g) (hf₀ : ∀ x, f x ≤ 0)
    (hg₀ : ∀ x, 0 ≤ g x) : Antitone (f * g) := fun _ _ h =>
  mul_le_mul_of_nonpos_of_nonneg (hf h) (hg h) (hf₀ _) (hg₀ _)

Antitone Product of Antitone and Monotone Functions with Nonpositive and Nonnegative Values

Informal description

Let $R$ be a preordered semiring where: 1. The order relation has the property that for any $a \leq b$, there exists $c$ such that $b = a + c$, 2. Left multiplication by nonnegative elements is monotone, 3. Right multiplication by nonnegative elements is monotone, 4. Addition is right monotone, 5. The order relation reflects addition on the right. If $f$ is an antitone function with $f(x) \leq 0$ for all $x$, and $g$ is a monotone function with $0 \leq g(x)$ for all $x$, then the pointwise product function $f \cdot g$ is antitone.

Monotone.mul_antitone theorem

 [ExistsAddOfLE R] [PosMulMono R] [MulPosMono R] [AddRightMono R] [AddRightReflectLE R] (hf : Monotone f)
  (hg : Antitone g) (hf₀ : ∀ x, 0 ≤ f x) (hg₀ : ∀ x, g x ≤ 0) : Antitone (f * g)

Full source

theorem Monotone.mul_antitone [ExistsAddOfLE R] [PosMulMono R] [MulPosMono R]
    [AddRightMono R] [AddRightReflectLE R]
    (hf : Monotone f) (hg : Antitone g) (hf₀ : ∀ x, 0 ≤ f x)
    (hg₀ : ∀ x, g x ≤ 0) : Antitone (f * g) := fun _ _ h =>
  mul_le_mul_of_nonneg_of_nonpos (hf h) (hg h) (hf₀ _) (hg₀ _)

Antitonicity of Product of Nonnegative Monotone and Nonpositive Antitone Functions

Informal description

Let $R$ be a preordered semiring where: 1. The order relation has the "exists add of ≤" property (for any $a \leq b$, there exists $c$ such that $b = a + c$) 2. Left multiplication by nonnegative elements is monotone (`PosMulMono`) 3. Right multiplication by nonnegative elements is monotone (`MulPosMono`) 4. Addition is right monotone (`AddRightMono`) 5. The order relation reflects addition on the right (`AddRightReflectLE`) If $f$ is a monotone function with $f(x) \geq 0$ for all $x$, and $g$ is an antitone function with $g(x) \leq 0$ for all $x$, then the product function $f \cdot g$ is antitone.

Antitone.mul theorem

 [ExistsAddOfLE R] [PosMulMono R] [MulPosMono R] [AddRightMono R] [AddRightReflectLE R] (hf : Antitone f)
  (hg : Antitone g) (hf₀ : ∀ x, f x ≤ 0) (hg₀ : ∀ x, g x ≤ 0) : Monotone (f * g)

Full source

theorem Antitone.mul [ExistsAddOfLE R] [PosMulMono R] [MulPosMono R]
    [AddRightMono R] [AddRightReflectLE R]
    (hf : Antitone f) (hg : Antitone g) (hf₀ : ∀ x, f x ≤ 0) (hg₀ : ∀ x, g x ≤ 0) :
    Monotone (f * g) := fun _ _ h => mul_le_mul_of_nonpos_of_nonpos (hf h) (hg h) (hf₀ _) (hg₀ _)

Monotonicity of Product of Antitone Nonpositive-Valued Functions

Informal description

Let $R$ be a preordered semiring where: 1. The order relation has the "exists add of $\leq$" property (for any $a \leq b$, there exists $c$ such that $b = a + c$) 2. Left multiplication by nonnegative elements is monotone (`PosMulMono`) 3. Right multiplication by nonnegative elements is monotone (`MulPosMono`) 4. Addition is right monotone (`AddRightMono`) 5. The order relation reflects addition on the right (`AddRightReflectLE`) If $f$ and $g$ are antitone functions from some type to $R$ such that $f(x) \leq 0$ and $g(x) \leq 0$ for all $x$, then their pointwise product $f \cdot g$ is monotone.

lt_two_mul_self theorem

[ZeroLEOneClass R] [MulPosStrictMono R] [NeZero (1 : R)] [AddLeftStrictMono R] (ha : 0 < a) : a < 2 * a

Full source

theorem lt_two_mul_self [ZeroLEOneClass R] [MulPosStrictMono R] [NeZero (1 : R)]
    [AddLeftStrictMono R] (ha : 0 < a) : a < 2 * a :=
  lt_mul_of_one_lt_left ha one_lt_two

Strict inequality: $a < 2a$ for positive elements in ordered semirings

Informal description

Let $R$ be an ordered semiring where: 1. $0 \leq 1$ holds (`ZeroLEOneClass`), 2. right multiplication by positive elements is strictly monotone (`MulPosStrictMono`), 3. $1 \neq 0$ (`NeZero (1 : R)`), and 4. addition is strictly monotone on the left (`AddLeftStrictMono`). Then for any positive element $a > 0$ in $R$, we have $a < 2a$.

mul_lt_mul_of_neg_left theorem

 [ExistsAddOfLE R] [PosMulStrictMono R] [AddRightStrictMono R] [AddRightReflectLT R] (h : b < a) (hc : c < 0) :
  c * a < c * b

Full source

theorem mul_lt_mul_of_neg_left [ExistsAddOfLE R] [PosMulStrictMono R]
    [AddRightStrictMono R] [AddRightReflectLT R]
    (h : b < a) (hc : c < 0) : c * a < c * b := by
  obtain ⟨d, hcd⟩ := exists_add_of_le hc.le
  refine (add_lt_add_iff_right (d * b + d * a)).1 ?_
  calc
    _ = d * b := by rw [add_left_comm, ← add_mul, ← hcd, zero_mul, add_zero]
    _ < d * a := mul_lt_mul_of_pos_left h <| hcd.trans_lt <| add_lt_of_neg_left _ hc
    _ = _ := by rw [← add_assoc, ← add_mul, ← hcd, zero_mul, zero_add]

Strict Monotonicity of Left Multiplication by Negative Elements: $c < 0 \implies (b < a \to c \cdot a < c \cdot b)$

Informal description

Let $R$ be an ordered ring where: 1. Left multiplication by positive elements is strictly monotone (`PosMulStrictMono R`) 2. Addition is strictly monotone on the right (`AddRightStrictMono R`) 3. The order relation is reflected by right addition (`AddRightReflectLT R`) 4. For any $x \leq y$, there exists $z$ such that $y = x + z$ (`ExistsAddOfLE R`) Then for any elements $a, b \in R$ with $b < a$ and any negative element $c < 0$, we have $c \cdot a < c \cdot b$.

mul_lt_mul_of_neg_right theorem

 [ExistsAddOfLE R] [MulPosStrictMono R] [AddRightStrictMono R] [AddRightReflectLT R] (h : b < a) (hc : c < 0) :
  a * c < b * c

Full source

theorem mul_lt_mul_of_neg_right [ExistsAddOfLE R] [MulPosStrictMono R]
    [AddRightStrictMono R] [AddRightReflectLT R]
    (h : b < a) (hc : c < 0) : a * c < b * c := by
  obtain ⟨d, hcd⟩ := exists_add_of_le hc.le
  refine (add_lt_add_iff_right (b * d + a * d)).1 ?_
  calc
    _ = b * d := by rw [add_left_comm, ← mul_add, ← hcd, mul_zero, add_zero]
    _ < a * d := mul_lt_mul_of_pos_right h <| hcd.trans_lt <| add_lt_of_neg_left _ hc
    _ = _ := by rw [← add_assoc, ← mul_add, ← hcd, mul_zero, zero_add]

Strict Monotonicity of Right Multiplication by Negative Elements: $c < 0 \implies (b < a \to a \cdot c < b \cdot c)$

Informal description

Let $R$ be an ordered ring where: 1. Right multiplication by positive elements is strictly monotone (`MulPosStrictMono R`) 2. Addition is strictly monotone on the right (`AddRightStrictMono R`) 3. The order relation is reflected by right addition (`AddRightReflectLT R`) 4. For any $x \leq y$, there exists $z$ such that $y = x + z$ (`ExistsAddOfLE R`) Then for any elements $a, b \in R$ with $b < a$ and any negative element $c < 0$, we have $a \cdot c < b \cdot c$.

mul_pos_of_neg_of_neg theorem

 [ExistsAddOfLE R] [MulPosStrictMono R] [AddRightStrictMono R] [AddRightReflectLT R] {a b : R} (ha : a < 0)
  (hb : b < 0) : 0 < a * b

Full source

theorem mul_pos_of_neg_of_neg [ExistsAddOfLE R] [MulPosStrictMono R]
    [AddRightStrictMono R] [AddRightReflectLT R]
    {a b : R} (ha : a < 0) (hb : b < 0) : 0 < a * b := by
  simpa only [zero_mul] using mul_lt_mul_of_neg_right ha hb

Product of Two Negative Elements is Positive in Ordered Rings

Informal description

Let $R$ be an ordered ring where: 1. Right multiplication by positive elements is strictly monotone (`MulPosStrictMono R`) 2. Addition is strictly monotone on the right (`AddRightStrictMono R`) 3. The order relation is reflected by right addition (`AddRightReflectLT R`) 4. For any $x \leq y$, there exists $z$ such that $y = x + z$ (`ExistsAddOfLE R`) Then for any two negative elements $a, b \in R$ with $a < 0$ and $b < 0$, their product is positive, i.e., $0 < a \cdot b$.

lt_mul_of_lt_one_left theorem

 [ExistsAddOfLE R] [MulPosStrictMono R] [AddRightStrictMono R] [AddRightReflectLT R] (hb : b < 0) (h : a < 1) :
  b < a * b

Full source

/-- Variant of `mul_lt_of_lt_one_left` for `b` negative instead of positive. -/
theorem lt_mul_of_lt_one_left [ExistsAddOfLE R] [MulPosStrictMono R]
    [AddRightStrictMono R] [AddRightReflectLT R]
    (hb : b < 0) (h : a < 1) : b < a * b := by
  simpa only [one_mul] using mul_lt_mul_of_neg_right h hb

Inequality for Multiplication by Elements Less Than One with Negative Base: $b < 0 \land a < 1 \implies b < a \cdot b$

Informal description

Let $R$ be an ordered ring where: 1. Right multiplication by positive elements is strictly monotone, 2. Addition is strictly monotone on the right, 3. The order relation is reflected by right addition, 4. For any $x \leq y$, there exists $z$ such that $y = x + z$. Then for any negative element $b < 0$ and any element $a < 1$ in $R$, we have $b < a \cdot b$.

mul_lt_of_one_lt_left theorem

 [ExistsAddOfLE R] [MulPosStrictMono R] [AddRightStrictMono R] [AddRightReflectLT R] (hb : b < 0) (h : 1 < a) :
  a * b < b

Full source

/-- Variant of `lt_mul_of_one_lt_left` for `b` negative instead of positive. -/
theorem mul_lt_of_one_lt_left [ExistsAddOfLE R] [MulPosStrictMono R]
    [AddRightStrictMono R] [AddRightReflectLT R]
    (hb : b < 0) (h : 1 < a) : a * b < b := by
  simpa only [one_mul] using mul_lt_mul_of_neg_right h hb

Inequality for Multiplication by Elements Greater Than One with Negative Base: $b < 0 \land a > 1 \implies a \cdot b < b$

Informal description

Let $R$ be an ordered ring where: 1. Right multiplication by positive elements is strictly monotone, 2. Addition is strictly monotone on the right, 3. The order relation is reflected by right addition, 4. For any $x \leq y$, there exists $z$ such that $y = x + z$. Then for any negative element $b < 0$ and any element $a > 1$ in $R$, we have $a \cdot b < b$.

lt_mul_of_lt_one_right theorem

 [ExistsAddOfLE R] [PosMulStrictMono R] [AddRightStrictMono R] [AddRightReflectLT R] (ha : a < 0) (h : b < 1) :
  a < a * b

Full source

/-- Variant of `mul_lt_of_lt_one_right` for `a` negative instead of positive. -/
theorem lt_mul_of_lt_one_right [ExistsAddOfLE R] [PosMulStrictMono R]
    [AddRightStrictMono R] [AddRightReflectLT R]
    (ha : a < 0) (h : b < 1) : a < a * b := by
  simpa only [mul_one] using mul_lt_mul_of_neg_left h ha

Inequality for Left Multiplication by Elements Less Than One with Negative Base: $a < 0 \land b < 1 \implies a < a \cdot b$

Informal description

Let $R$ be an ordered ring where: 1. Left multiplication by positive elements is strictly monotone, 2. Addition is strictly monotone on the right, 3. The order relation is reflected by right addition, 4. For any $x \leq y$, there exists $z$ such that $y = x + z$. Then for any negative element $a < 0$ and any element $b < 1$ in $R$, we have $a < a \cdot b$.

mul_lt_of_one_lt_right theorem

 [ExistsAddOfLE R] [PosMulStrictMono R] [AddRightStrictMono R] [AddRightReflectLT R] (ha : a < 0) (h : 1 < b) :
  a * b < a

Full source

/-- Variant of `lt_mul_of_lt_one_right` for `a` negative instead of positive. -/
theorem mul_lt_of_one_lt_right [ExistsAddOfLE R] [PosMulStrictMono R]
    [AddRightStrictMono R] [AddRightReflectLT R]
    (ha : a < 0) (h : 1 < b) : a * b < a := by
  simpa only [mul_one] using mul_lt_mul_of_neg_left h ha

Inequality for Left Multiplication by Elements Greater Than One with Negative Base: $a < 0 \land b > 1 \implies a \cdot b < a$

Informal description

Let $R$ be an ordered ring where: 1. Left multiplication by positive elements is strictly monotone, 2. Addition is strictly monotone on the right, 3. The order relation is reflected by right addition, 4. For any $x \leq y$, there exists $z$ such that $y = x + z$. Then for any negative element $a < 0$ and any element $b > 1$ in $R$, we have $a \cdot b < a$.

strictAnti_mul_left theorem

 [ExistsAddOfLE R] [PosMulStrictMono R] [AddRightStrictMono R] [AddRightReflectLT R] {a : R} (ha : a < 0) :
  StrictAnti (a * ·)

Full source

theorem strictAnti_mul_left [ExistsAddOfLE R] [PosMulStrictMono R]
    [AddRightStrictMono R] [AddRightReflectLT R]
    {a : R} (ha : a < 0) : StrictAnti (a * ·) := fun _ _ b_lt_c =>
  mul_lt_mul_of_neg_left b_lt_c ha

Left Multiplication by Negative Elements is Strictly Antitone

Informal description

Let $R$ be an ordered ring where: 1. Left multiplication by positive elements is strictly monotone (`PosMulStrictMono R`) 2. Addition is strictly monotone on the right (`AddRightStrictMono R`) 3. The order relation is reflected by right addition (`AddRightReflectLT R`) 4. For any $x \leq y$, there exists $z$ such that $y = x + z$ (`ExistsAddOfLE R`) Then for any negative element $a < 0$ in $R$, the function $x \mapsto a \cdot x$ is strictly antitone (i.e., if $x < y$ then $a \cdot y < a \cdot x$).

strictAnti_mul_right theorem

 [ExistsAddOfLE R] [MulPosStrictMono R] [AddRightStrictMono R] [AddRightReflectLT R] {a : R} (ha : a < 0) :
  StrictAnti fun x => x * a

Full source

theorem strictAnti_mul_right [ExistsAddOfLE R] [MulPosStrictMono R]
    [AddRightStrictMono R] [AddRightReflectLT R]
    {a : R} (ha : a < 0) : StrictAnti fun x => x * a := fun _ _ b_lt_c =>
  mul_lt_mul_of_neg_right b_lt_c ha

Right Multiplication by Negative Elements is Strictly Antitone

Informal description

Let $R$ be an ordered ring where: 1. Right multiplication by positive elements is strictly monotone (`MulPosStrictMono R`) 2. Addition is strictly monotone on the right (`AddRightStrictMono R`) 3. The order relation is reflected by right addition (`AddRightReflectLT R`) 4. For any $x \leq y$, there exists $z$ such that $y = x + z$ (`ExistsAddOfLE R`) Then for any negative element $a < 0$ in $R$, the function $x \mapsto x \cdot a$ is strictly antitone (i.e., if $x < y$ then $y \cdot a < x \cdot a$).

StrictMono.const_mul_of_neg theorem

 [ExistsAddOfLE R] [PosMulStrictMono R] [AddRightStrictMono R] [AddRightReflectLT R] (hf : StrictMono f) (ha : a < 0) :
  StrictAnti fun x => a * f x

Full source

theorem StrictMono.const_mul_of_neg [ExistsAddOfLE R] [PosMulStrictMono R]
    [AddRightStrictMono R] [AddRightReflectLT R]
    (hf : StrictMono f) (ha : a < 0) : StrictAnti fun x => a * f x :=
  (strictAnti_mul_left ha).comp_strictMono hf

Strictly Increasing Function Composed with Negative Multiplication is Strictly Decreasing

Informal description

Let $R$ be an ordered ring where: 1. Left multiplication by positive elements is strictly monotone, 2. Addition is strictly monotone on the right, 3. The order relation is reflected by right addition, 4. For any $x \leq y$, there exists $z$ such that $y = x + z$. If $f : R \to R$ is a strictly increasing function and $a < 0$ is a negative element of $R$, then the function $x \mapsto a \cdot f(x)$ is strictly decreasing.

StrictMono.mul_const_of_neg theorem

 [ExistsAddOfLE R] [MulPosStrictMono R] [AddRightStrictMono R] [AddRightReflectLT R] (hf : StrictMono f) (ha : a < 0) :
  StrictAnti fun x => f x * a

Full source

theorem StrictMono.mul_const_of_neg [ExistsAddOfLE R] [MulPosStrictMono R]
    [AddRightStrictMono R] [AddRightReflectLT R]
    (hf : StrictMono f) (ha : a < 0) : StrictAnti fun x => f x * a :=
  (strictAnti_mul_right ha).comp_strictMono hf

Strictly monotone function composed with right multiplication by negative element is strictly antitone

Informal description

Let $R$ be an ordered ring where: 1. Right multiplication by positive elements is strictly monotone, 2. Addition is strictly monotone on the right, 3. The order relation is reflected by right addition, 4. For any $x \leq y$, there exists $z$ such that $y = x + z$. If $f : R \to R$ is a strictly monotone function and $a < 0$ is a negative element of $R$, then the function $x \mapsto f(x) \cdot a$ is strictly antitone (i.e., if $x < y$ then $f(y) \cdot a < f(x) \cdot a$).

StrictAnti.const_mul_of_neg theorem

 [ExistsAddOfLE R] [PosMulStrictMono R] [AddRightStrictMono R] [AddRightReflectLT R] (hf : StrictAnti f) (ha : a < 0) :
  StrictMono fun x => a * f x

Full source

theorem StrictAnti.const_mul_of_neg [ExistsAddOfLE R] [PosMulStrictMono R]
    [AddRightStrictMono R] [AddRightReflectLT R]
    (hf : StrictAnti f) (ha : a < 0) : StrictMono fun x => a * f x :=
  (strictAnti_mul_left ha).comp hf

Strictly Antitone Function Composed with Negative Multiplication is Strictly Monotone

Informal description

Let $R$ be an ordered ring where: 1. Left multiplication by positive elements is strictly monotone (`PosMulStrictMono R`) 2. Addition is strictly monotone on the right (`AddRightStrictMono R`) 3. The order relation is reflected by right addition (`AddRightReflectLT R`) 4. For any $x \leq y$, there exists $z$ such that $y = x + z$ (`ExistsAddOfLE R`) If $f$ is a strictly antitone function on $R$ and $a < 0$ is a negative element in $R$, then the function $x \mapsto a \cdot f(x)$ is strictly monotone (i.e., if $x < y$ then $a \cdot f(x) < a \cdot f(y)$).

StrictAnti.mul_const_of_neg theorem

 [ExistsAddOfLE R] [MulPosStrictMono R] [AddRightStrictMono R] [AddRightReflectLT R] (hf : StrictAnti f) (ha : a < 0) :
  StrictMono fun x => f x * a

Full source

theorem StrictAnti.mul_const_of_neg [ExistsAddOfLE R] [MulPosStrictMono R]
    [AddRightStrictMono R] [AddRightReflectLT R]
    (hf : StrictAnti f) (ha : a < 0) : StrictMono fun x => f x * a :=
  (strictAnti_mul_right ha).comp hf

Strictly Antitone Function Multiplied by Negative Constant is Strictly Monotone

Informal description

Let $R$ be an ordered ring where: 1. Right multiplication by positive elements is strictly monotone, 2. Addition is strictly monotone on the right, 3. The order relation is reflected by right addition, 4. For any $x \leq y$, there exists $z$ such that $y = x + z$. If $f : R \to R$ is a strictly antitone function and $a < 0$ is a negative element of $R$, then the function $x \mapsto f(x) \cdot a$ is strictly monotone. That is, for any $x < y$ in $R$, we have $f(x) \cdot a < f(y) \cdot a$.

mul_add_mul_le_mul_add_mul theorem

 [ExistsAddOfLE R] [MulPosMono R] [AddLeftMono R] [AddLeftReflectLE R] (hab : a ≤ b) (hcd : c ≤ d) :
  a * d + b * c ≤ a * c + b * d

Full source

/-- Binary **rearrangement inequality**. -/
lemma mul_add_mul_le_mul_add_mul [ExistsAddOfLE R] [MulPosMono R]
    [AddLeftMono R] [AddLeftReflectLE R]
    (hab : a ≤ b) (hcd : c ≤ d) : a * d + b * c ≤ a * c + b * d := by
  obtain ⟨b, rfl⟩ := exists_add_of_le hab
  obtain ⟨d, hd, rfl⟩ := exists_nonneg_add_of_le hcd
  rw [mul_add, add_right_comm, mul_add, ← add_assoc]
  exact add_le_add_left (mul_le_mul_of_nonneg_right hab hd) _

Rearrangement Inequality: $a \leq b \land c \leq d \implies a \cdot d + b \cdot c \leq a \cdot c + b \cdot d$

Informal description

Let $R$ be an ordered semiring where right multiplication by nonnegative elements is monotone and addition is monotone in its left argument. For any elements $a, b, c, d \in R$ with $a \leq b$ and $c \leq d$, we have the inequality: $$ a \cdot d + b \cdot c \leq a \cdot c + b \cdot d $$

mul_add_mul_le_mul_add_mul' theorem

 [ExistsAddOfLE R] [MulPosMono R] [AddLeftMono R] [AddLeftReflectLE R] (hba : b ≤ a) (hdc : d ≤ c) :
  a * d + b * c ≤ a * c + b * d

Full source

/-- Binary **rearrangement inequality**. -/
lemma mul_add_mul_le_mul_add_mul' [ExistsAddOfLE R] [MulPosMono R]
    [AddLeftMono R] [AddLeftReflectLE R]
    (hba : b ≤ a) (hdc : d ≤ c) : a * d + b * c ≤ a * c + b * d := by
  rw [add_comm (a * d), add_comm (a * c)]; exact mul_add_mul_le_mul_add_mul hba hdc

Rearrangement Inequality (Reverse Order Variant): $b \leq a \land d \leq c \implies a \cdot d + b \cdot c \leq a \cdot c + b \cdot d$

Informal description

Let $R$ be an ordered semiring where right multiplication by nonnegative elements is monotone and addition is monotone in its left argument. For any elements $a, b, c, d \in R$ with $b \leq a$ and $d \leq c$, we have the inequality: $$ a \cdot d + b \cdot c \leq a \cdot c + b \cdot d $$

mul_add_mul_lt_mul_add_mul theorem

 [ExistsAddOfLE R] [MulPosStrictMono R] [AddLeftStrictMono R] (hab : a < b) (hcd : c < d) :
  a * d + b * c < a * c + b * d

Full source

/-- Binary strict **rearrangement inequality**. -/
lemma mul_add_mul_lt_mul_add_mul [ExistsAddOfLE R] [MulPosStrictMono R]
    [AddLeftStrictMono R]
    (hab : a < b) (hcd : c < d) : a * d + b * c < a * c + b * d := by
  obtain ⟨b, rfl⟩ := exists_add_of_le hab.le
  obtain ⟨d, hd, rfl⟩ := exists_pos_add_of_lt' hcd
  rw [mul_add, add_right_comm, mul_add, ← add_assoc]
  exact add_lt_add_left (mul_lt_mul_of_pos_right hab hd) _

Strict rearrangement inequality: $a < b \land c < d \implies a \cdot d + b \cdot c < a \cdot c + b \cdot d$

Informal description

Let $R$ be an ordered semiring where right multiplication by positive elements is strictly monotone and addition is strictly monotone in its left argument. For any elements $a, b, c, d \in R$ with $a < b$ and $c < d$, we have the strict inequality: $$ a \cdot d + b \cdot c < a \cdot c + b \cdot d $$

mul_add_mul_lt_mul_add_mul' theorem

 [ExistsAddOfLE R] [MulPosStrictMono R] [AddLeftStrictMono R] (hba : b < a) (hdc : d < c) :
  a * d + b * c < a * c + b * d

Full source

/-- Binary **rearrangement inequality**. -/
lemma mul_add_mul_lt_mul_add_mul' [ExistsAddOfLE R] [MulPosStrictMono R]
    [AddLeftStrictMono R]
    (hba : b < a) (hdc : d < c) : a * d + b * c < a * c + b * d := by
  rw [add_comm (a * d), add_comm (a * c)]
  exact mul_add_mul_lt_mul_add_mul hba hdc

Strict rearrangement inequality (reverse order variant): $b < a \land d < c \implies a \cdot d + b \cdot c < a \cdot c + b \cdot d$

Informal description

Let $R$ be an ordered semiring where right multiplication by positive elements is strictly monotone and addition is strictly monotone in its left argument. For any elements $a, b, c, d \in R$ with $b < a$ and $d < c$, we have the strict inequality: $$ a \cdot d + b \cdot c < a \cdot c + b \cdot d $$

nonneg_and_nonneg_or_nonpos_and_nonpos_of_mul_nonneg theorem

[MulPosStrictMono R] [PosMulStrictMono R] (hab : 0 ≤ a * b) : 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0

Full source

theorem nonneg_and_nonneg_or_nonpos_and_nonpos_of_mul_nonneg
    [MulPosStrictMono R] [PosMulStrictMono R]
    (hab : 0 ≤ a * b) : 0 ≤ a ∧ 0 ≤ b0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0 := by
  refine Decidable.or_iff_not_not_and_not.2 ?_
  simp only [not_and, not_le]; intro ab nab; apply not_lt_of_le hab _
  rcases lt_trichotomy 0 a with (ha | rfl | ha)
  · exact mul_neg_of_pos_of_neg ha (ab ha.le)
  · exact ((ab le_rfl).asymm (nab le_rfl)).elim
  · exact mul_neg_of_neg_of_pos ha (nab ha.le)

Nonnegative Product Implies Same Sign Factors: $ab \geq 0 \implies (a \geq 0 \land b \geq 0) \lor (a \leq 0 \land b \leq 0)$

Informal description

Let $R$ be an ordered semiring where both left and right multiplication by positive elements are strictly monotone. For any elements $a, b \in R$ such that their product satisfies $a \cdot b \geq 0$, either both $a \geq 0$ and $b \geq 0$, or both $a \leq 0$ and $b \leq 0$.

nonneg_of_mul_nonneg_left theorem

[MulPosStrictMono R] (h : 0 ≤ a * b) (hb : 0 < b) : 0 ≤ a

Full source

theorem nonneg_of_mul_nonneg_left [MulPosStrictMono R]
    (h : 0 ≤ a * b) (hb : 0 < b) : 0 ≤ a :=
  le_of_not_gt fun ha => (mul_neg_of_neg_of_pos ha hb).not_le h

Nonnegativity from Nonnegative Product on the Left: $0 \leq a \cdot b \land b > 0 \implies 0 \leq a$

Informal description

Let $R$ be an ordered semiring where right multiplication by positive elements is strictly monotone. For any elements $a, b \in R$, if $0 \leq a \cdot b$ and $0 < b$, then $0 \leq a$.

nonneg_of_mul_nonneg_right theorem

[PosMulStrictMono R] (h : 0 ≤ a * b) (ha : 0 < a) : 0 ≤ b

Full source

theorem nonneg_of_mul_nonneg_right [PosMulStrictMono R]
    (h : 0 ≤ a * b) (ha : 0 < a) : 0 ≤ b :=
  le_of_not_gt fun hb => (mul_neg_of_pos_of_neg ha hb).not_le h

Nonnegativity of Right Factor in Nonnegative Product under Left Monotonicity

Informal description

Let $R$ be a preordered type with multiplication such that left multiplication by positive elements is strictly monotone. For any elements $a, b \in R$, if $a \cdot b \geq 0$ and $a > 0$, then $b \geq 0$.

nonpos_of_mul_nonpos_left theorem

[PosMulStrictMono R] (h : a * b ≤ 0) (hb : 0 < b) : a ≤ 0

Full source

theorem nonpos_of_mul_nonpos_left [PosMulStrictMono R]
    (h : a * b ≤ 0) (hb : 0 < b) : a ≤ 0 :=
  le_of_not_gt fun ha : a > 0 => (mul_pos ha hb).not_le h

Nonpositivity from Left Multiplication with Positive Factor

Informal description

Let $R$ be a linearly ordered ring where left multiplication by positive elements is strictly monotone. For any elements $a, b \in R$, if $a \cdot b \leq 0$ and $b > 0$, then $a \leq 0$.

nonpos_of_mul_nonpos_right theorem

[PosMulStrictMono R] (h : a * b ≤ 0) (ha : 0 < a) : b ≤ 0

Full source

theorem nonpos_of_mul_nonpos_right [PosMulStrictMono R]
    (h : a * b ≤ 0) (ha : 0 < a) : b ≤ 0 :=
  le_of_not_gt fun hb : b > 0 => (mul_pos ha hb).not_le h

Nonpositivity from Right Multiplication by Positive Element

Informal description

Let $ R $ be a preordered ring where left multiplication by positive elements is strictly monotone. For any elements $ a, b \in R $, if $ a \cdot b \leq 0 $ and $ a > 0 $, then $ b \leq 0 $.

mul_nonneg_iff_of_pos_left theorem

[PosMulStrictMono R] (h : 0 < c) : 0 ≤ c * b ↔ 0 ≤ b

Full source

@[simp]
theorem mul_nonneg_iff_of_pos_left [PosMulStrictMono R]
    (h : 0 < c) : 0 ≤ c * b ↔ 0 ≤ b := by
  convert mul_le_mul_left h
  simp

Nonnegativity of Product with Positive Left Factor: $c > 0 \implies (0 \leq c \cdot b \leftrightarrow 0 \leq b)$

Informal description

Let $R$ be an ordered semiring where left multiplication by positive elements is strictly monotone. For any positive element $c > 0$ and any element $b \in R$, the product $c \cdot b$ is nonnegative if and only if $b$ is nonnegative.

mul_nonneg_iff_of_pos_right theorem

[MulPosStrictMono R] (h : 0 < c) : 0 ≤ b * c ↔ 0 ≤ b

Full source

@[simp]
theorem mul_nonneg_iff_of_pos_right [MulPosStrictMono R]
    (h : 0 < c) : 0 ≤ b * c ↔ 0 ≤ b := by
  simpa using (mul_le_mul_right h : 0 * c ≤ b * c ↔ 0 ≤ b)

Nonnegativity of Product via Right Factor Positivity: $c > 0 \implies (0 \leq b \cdot c \leftrightarrow 0 \leq b)$

Informal description

Let $R$ be a preordered ring where right multiplication by positive elements is strictly monotone. For any positive element $c > 0$ and any element $b \in R$, the product $b \cdot c$ is nonnegative if and only if $b$ is nonnegative. That is: \[ 0 \leq b \cdot c \leftrightarrow 0 \leq b. \]

add_le_mul_of_left_le_right theorem

 [ZeroLEOneClass R] [NeZero (1 : R)] [MulPosStrictMono R] [AddLeftMono R] (a2 : 2 ≤ a) (ab : a ≤ b) : a + b ≤ a * b

Full source

theorem add_le_mul_of_left_le_right [ZeroLEOneClass R] [NeZero (1 : R)]
    [MulPosStrictMono R] [AddLeftMono R]
    (a2 : 2 ≤ a) (ab : a ≤ b) : a + b ≤ a * b :=
  have : 0 < b :=
    calc
      0 < 2 := zero_lt_two
      _ ≤ a := a2
      _ ≤ b := ab
  calc
    a + b ≤ b + b := add_le_add_right ab b
    _ = 2 * b := (two_mul b).symm
    _ ≤ a * b := (mul_le_mul_right this).mpr a2

Sum Bound by Product for Ordered Semirings with $2 \leq a \leq b$

Informal description

Let $R$ be an ordered semiring with the following properties: 1. $0 \leq 1$ (ZeroLEOneClass) 2. $1 \neq 0$ (NeZero) 3. Right multiplication by positive elements is strictly monotone (MulPosStrictMono) 4. Addition is monotone in its left argument (AddLeftMono) For any elements $a, b \in R$ such that $2 \leq a$ and $a \leq b$, we have the inequality: \[ a + b \leq a \cdot b \]

add_le_mul_of_right_le_left theorem

 [ZeroLEOneClass R] [NeZero (1 : R)] [AddLeftMono R] [PosMulStrictMono R] (b2 : 2 ≤ b) (ba : b ≤ a) : a + b ≤ a * b

Full source

theorem add_le_mul_of_right_le_left [ZeroLEOneClass R] [NeZero (1 : R)]
    [AddLeftMono R] [PosMulStrictMono R]
    (b2 : 2 ≤ b) (ba : b ≤ a) : a + b ≤ a * b :=
  have : 0 < a :=
    calc 0
      _ < 2 := zero_lt_two
      _ ≤ b := b2
      _ ≤ a := ba
  calc
    a + b ≤ a + a := add_le_add_left ba a
    _ = a * 2 := (mul_two a).symm
    _ ≤ a * b := (mul_le_mul_left this).mpr b2

Sum Bound by Product for Ordered Elements: $2 \leq b \leq a \implies a + b \leq a \cdot b$

Informal description

Let $R$ be an ordered ring where: 1. $0 \leq 1$, 2. $1 \neq 0$, 3. addition is monotone in the left argument, 4. left multiplication by positive elements is strictly monotone. For any elements $a, b \in R$ such that $2 \leq b$ and $b \leq a$, we have $a + b \leq a \cdot b$.

add_le_mul theorem

 [ZeroLEOneClass R] [NeZero (1 : R)] [MulPosStrictMono R] [PosMulStrictMono R] [AddLeftMono R] (a2 : 2 ≤ a)
  (b2 : 2 ≤ b) : a + b ≤ a * b

Full source

theorem add_le_mul [ZeroLEOneClass R] [NeZero (1 : R)]
    [MulPosStrictMono R] [PosMulStrictMono R] [AddLeftMono R]
    (a2 : 2 ≤ a) (b2 : 2 ≤ b) : a + b ≤ a * b :=
  if hab : a ≤ b then add_le_mul_of_left_le_right a2 hab
  else add_le_mul_of_right_le_left b2 (le_of_not_le hab)

Sum Bound by Product for Ordered Semirings with $a, b \geq 2$

Informal description

Let $R$ be an ordered semiring with the following properties: 1. $0 \leq 1$, 2. $1 \neq 0$, 3. Right multiplication by positive elements is strictly monotone, 4. Left multiplication by positive elements is strictly monotone, 5. Addition is monotone in its left argument. For any elements $a, b \in R$ such that $2 \leq a$ and $2 \leq b$, we have the inequality: \[ a + b \leq a \cdot b \]

add_le_mul' theorem

 [ZeroLEOneClass R] [NeZero (1 : R)] [MulPosStrictMono R] [PosMulStrictMono R] [AddLeftMono R] (a2 : 2 ≤ a)
  (b2 : 2 ≤ b) : a + b ≤ b * a

Full source

theorem add_le_mul' [ZeroLEOneClass R] [NeZero (1 : R)]
    [MulPosStrictMono R] [PosMulStrictMono R] [AddLeftMono R]
    (a2 : 2 ≤ a) (b2 : 2 ≤ b) : a + b ≤ b * a :=
  (le_of_eq (add_comm _ _)).trans (add_le_mul b2 a2)

Sum Bound by Product (Commutative Version) for Ordered Semirings with $a, b \geq 2$

Informal description

Let $R$ be an ordered semiring with the following properties: 1. $0 \leq 1$, 2. $1 \neq 0$, 3. Right multiplication by positive elements is strictly monotone, 4. Left multiplication by positive elements is strictly monotone, 5. Addition is monotone in its left argument. For any elements $a, b \in R$ such that $2 \leq a$ and $2 \leq b$, we have the inequality: \[ a + b \leq b \cdot a \]

mul_nonneg_iff_right_nonneg_of_pos theorem

[PosMulStrictMono R] (ha : 0 < a) : 0 ≤ a * b ↔ 0 ≤ b

Full source

theorem mul_nonneg_iff_right_nonneg_of_pos [PosMulStrictMono R]
    (ha : 0 < a) : 0 ≤ a * b ↔ 0 ≤ b :=
  ⟨fun h => nonneg_of_mul_nonneg_right h ha, mul_nonneg ha.le⟩

Nonnegativity of Product Equivalent to Nonnegativity of Right Factor for Positive Left Factor

Informal description

Let $R$ be a preordered type with multiplication such that left multiplication by positive elements is strictly monotone. For any elements $a, b \in R$ with $a > 0$, the product $a \cdot b$ is nonnegative if and only if $b$ is nonnegative, i.e., $0 \leq a \cdot b \leftrightarrow 0 \leq b$.

mul_nonneg_iff_left_nonneg_of_pos theorem

[PosMulStrictMono R] [MulPosStrictMono R] (hb : 0 < b) : 0 ≤ a * b ↔ 0 ≤ a

Full source

theorem mul_nonneg_iff_left_nonneg_of_pos [PosMulStrictMono R] [MulPosStrictMono R]
    (hb : 0 < b) : 0 ≤ a * b ↔ 0 ≤ a :=
  ⟨fun h => nonneg_of_mul_nonneg_left h hb, fun h => mul_nonneg h hb.le⟩

Nonnegativity of Product with Positive Factor: $0 \leq a \cdot b \leftrightarrow 0 \leq a$ when $b > 0$

Informal description

Let $R$ be an ordered semiring where left and right multiplication by positive elements are strictly monotone. For any elements $a, b \in R$ with $b > 0$, the product $a \cdot b$ is nonnegative if and only if $a$ is nonnegative, i.e., $0 \leq a \cdot b \leftrightarrow 0 \leq a$.

nonpos_of_mul_nonneg_left theorem

[PosMulStrictMono R] (h : 0 ≤ a * b) (hb : b < 0) : a ≤ 0

Full source

theorem nonpos_of_mul_nonneg_left [PosMulStrictMono R]
    (h : 0 ≤ a * b) (hb : b < 0) : a ≤ 0 :=
  le_of_not_gt fun ha => absurd h (mul_neg_of_pos_of_neg ha hb).not_le

Nonpositivity from Nonnegative Product with Negative Factor

Informal description

Let $R$ be a preordered ring where left multiplication by positive elements is strictly monotone. For any elements $a, b \in R$, if $0 \leq a \cdot b$ and $b < 0$, then $a \leq 0$.

nonpos_of_mul_nonneg_right theorem

[MulPosStrictMono R] (h : 0 ≤ a * b) (ha : a < 0) : b ≤ 0

Full source

theorem nonpos_of_mul_nonneg_right [MulPosStrictMono R]
    (h : 0 ≤ a * b) (ha : a < 0) : b ≤ 0 :=
  le_of_not_gt fun hb => absurd h (mul_neg_of_neg_of_pos ha hb).not_le

Nonpositivity from Nonnegative Product with Negative Factor: $a < 0 \land 0 \leq a \cdot b \implies b \leq 0$

Informal description

Let $R$ be a preordered ring where right multiplication by positive elements is strictly monotone. If $a \cdot b$ is nonnegative and $a$ is negative, then $b$ is nonpositive. That is, for $a < 0$ and $0 \leq a \cdot b$, we have $b \leq 0$.

Units.inv_pos theorem

[ZeroLEOneClass R] [NeZero (1 : R)] [PosMulStrictMono R] {u : Rˣ} : (0 : R) < ↑u⁻¹ ↔ (0 : R) < u

Full source

@[simp]
theorem Units.inv_pos
    [ZeroLEOneClass R] [NeZero (1 : R)] [PosMulStrictMono R]
    {u : Rˣ} : (0 : R) < ↑u⁻¹ ↔ (0 : R) < u :=
  have : ∀ {u : Rˣ}, (0 : R) < u → (0 : R) < ↑u⁻¹ := @fun u h =>
    (mul_pos_iff_of_pos_left h).mp <| u.mul_inv.symm ▸ zero_lt_one
  ⟨this, this⟩

Positivity of Unit Inverses in Ordered Rings

Informal description

Let $R$ be a ring with a zero element $0$, a one element $1$, and a partial order $\leq$ such that $0 \leq 1$ and $1 \neq 0$. Suppose that left multiplication by positive elements is strictly monotone. For any unit $u \in R^\times$, the inverse $u^{-1}$ is positive if and only if $u$ is positive, i.e., \[ 0 < u^{-1} \leftrightarrow 0 < u. \]

Units.inv_neg theorem

[ZeroLEOneClass R] [NeZero (1 : R)] [MulPosMono R] [PosMulMono R] {u : Rˣ} : ↑u⁻¹ < (0 : R) ↔ ↑u < (0 : R)

Full source

@[simp]
theorem Units.inv_neg
    [ZeroLEOneClass R] [NeZero (1 : R)] [MulPosMono R] [PosMulMono R]
    {u : Rˣ} : ↑u⁻¹ < (0 : R) ↔ ↑u < (0 : R) :=
  have : ∀ {u : Rˣ}, ↑u < (0 : R) → ↑u⁻¹ < (0 : R) := @fun u h =>
    neg_of_mul_pos_right (u.mul_inv.symm ▸ zero_lt_one) h.le
  ⟨this, this⟩

Negativity of Unit Inverses in Ordered Rings

Informal description

Let $R$ be a ring with a zero element $0$, a one element $1$, and a partial order $\leq$ such that $0 \leq 1$ and $1 \neq 0$. Suppose that both left and right multiplication by nonnegative elements are monotone. For any unit $u \in R^\times$, the inverse $u^{-1}$ is negative if and only if $u$ is negative, i.e., \[ u^{-1} < 0 \leftrightarrow u < 0. \]

cmp_mul_pos_left theorem

[PosMulStrictMono R] (ha : 0 < a) (b c : R) : cmp (a * b) (a * c) = cmp b c

Full source

theorem cmp_mul_pos_left [PosMulStrictMono R]
    (ha : 0 < a) (b c : R) : cmp (a * b) (a * c) = cmp b c :=
  (strictMono_mul_left_of_pos ha).cmp_map_eq b c

Comparison Preservation under Left Multiplication by Positive Elements: $\text{cmp}(a \cdot b, a \cdot c) = \text{cmp}(b, c)$ for $a > 0$

Informal description

Let $R$ be a preordered type with multiplication and zero, where left multiplication by positive elements is strictly monotone. For any positive element $a > 0$ in $R$ and any elements $b, c \in R$, the comparison of $a \cdot b$ and $a \cdot c$ is equal to the comparison of $b$ and $c$. That is, $\text{cmp}(a \cdot b, a \cdot c) = \text{cmp}(b, c)$.

cmp_mul_pos_right theorem

[MulPosStrictMono R] (ha : 0 < a) (b c : R) : cmp (b * a) (c * a) = cmp b c

Full source

theorem cmp_mul_pos_right [MulPosStrictMono R]
    (ha : 0 < a) (b c : R) : cmp (b * a) (c * a) = cmp b c :=
  (strictMono_mul_right_of_pos ha).cmp_map_eq b c

Order-Preserving Property of Right Multiplication by Positive Elements: $\text{cmp}(b \cdot a, c \cdot a) = \text{cmp}(b, c)$ for $a > 0$

Informal description

Let $R$ be a preordered type with multiplication and zero, where right multiplication by positive elements is strictly monotone (i.e., the typeclass `MulPosStrictMono R` holds). Then for any positive element $a > 0$ in $R$, and for any elements $b, c \in R$, the comparison of $b \cdot a$ and $c \cdot a$ is the same as the comparison of $b$ and $c$. In other words, the function $x \mapsto x \cdot a$ preserves the order relation when $a > 0$.

mul_max_of_nonneg theorem

[PosMulMono R] (b c : R) (ha : 0 ≤ a) : a * max b c = max (a * b) (a * c)

Full source

theorem mul_max_of_nonneg [PosMulMono R]
    (b c : R) (ha : 0 ≤ a) : a * max b c = max (a * b) (a * c) :=
  (monotone_mul_left_of_nonneg ha).map_max

Distributivity of Nonnegative Multiplication over Maximum: $a \cdot \max(b, c) = \max(a \cdot b, a \cdot c)$ for $a \geq 0$

Informal description

Let $R$ be a type with a multiplication operation and a preorder, such that left multiplication by nonnegative elements is monotone (i.e., `PosMulMono R` holds). Then for any nonnegative element $a \geq 0$ and any elements $b, c \in R$, we have the equality: \[ a \cdot \max(b, c) = \max(a \cdot b, a \cdot c). \]

mul_min_of_nonneg theorem

[PosMulMono R] (b c : R) (ha : 0 ≤ a) : a * min b c = min (a * b) (a * c)

Full source

theorem mul_min_of_nonneg [PosMulMono R]
    (b c : R) (ha : 0 ≤ a) : a * min b c = min (a * b) (a * c) :=
  (monotone_mul_left_of_nonneg ha).map_min

Left Multiplication Preserves Minimum for Nonnegative Elements: $a \cdot \min(b, c) = \min(a \cdot b, a \cdot c)$

Informal description

Let $R$ be a type with a multiplication operation and a preorder, such that left multiplication by nonnegative elements is monotone (i.e., `PosMulMono R` holds). Then for any nonnegative element $a \geq 0$ and any elements $b, c \in R$, we have: $$a \cdot \min(b, c) = \min(a \cdot b, a \cdot c)$$

max_mul_of_nonneg theorem

[MulPosMono R] (a b : R) (hc : 0 ≤ c) : max a b * c = max (a * c) (b * c)

Full source

theorem max_mul_of_nonneg [MulPosMono R]
    (a b : R) (hc : 0 ≤ c) : max a b * c = max (a * c) (b * c) :=
  (monotone_mul_right_of_nonneg hc).map_max

Distributivity of Maximum over Nonnegative Multiplication: $\max(a, b) \cdot c = \max(a \cdot c, b \cdot c)$ for $c \geq 0$

Informal description

Let $R$ be a type with a multiplication operation and a preorder, such that right multiplication by nonnegative elements is monotone (i.e., `MulPosMono R` holds). Then for any nonnegative element $c \geq 0$ and any elements $a, b \in R$, we have the equality: \[ \max(a, b) \cdot c = \max(a \cdot c, b \cdot c). \]

min_mul_of_nonneg theorem

[MulPosMono R] (a b : R) (hc : 0 ≤ c) : min a b * c = min (a * c) (b * c)

Full source

theorem min_mul_of_nonneg [MulPosMono R]
    (a b : R) (hc : 0 ≤ c) : min a b * c = min (a * c) (b * c) :=
  (monotone_mul_right_of_nonneg hc).map_min

Right Multiplication Preserves Minimum for Nonnegative Elements: $\min(a, b) \cdot c = \min(a \cdot c, b \cdot c)$

Informal description

Let $R$ be a type with a multiplication operation and a preorder, such that right multiplication by nonnegative elements is monotone (i.e., `MulPosMono R` holds). Then for any nonnegative element $c \geq 0$ and any elements $a, b \in R$, we have: $$\min(a, b) \cdot c = \min(a \cdot c, b \cdot c)$$

le_of_mul_le_of_one_le theorem

 [ZeroLEOneClass R] [NeZero (1 : R)] [MulPosStrictMono R] [PosMulMono R] {a b c : R} (h : a * c ≤ b) (hb : 0 ≤ b)
  (hc : 1 ≤ c) : a ≤ b

Full source

theorem le_of_mul_le_of_one_le
    [ZeroLEOneClass R] [NeZero (1 : R)] [MulPosStrictMono R] [PosMulMono R]
    {a b c : R} (h : a * c ≤ b) (hb : 0 ≤ b) (hc : 1 ≤ c) : a ≤ b :=
  le_of_mul_le_mul_right (h.trans <| le_mul_of_one_le_right hb hc) <| zero_lt_one.trans_le hc

Order comparison via multiplication by elements greater than or equal to one: $a \cdot c \leq b \land b \geq 0 \land c \geq 1 \implies a \leq b$

Informal description

Let $R$ be an ordered structure with zero and one elements, where $0 \leq 1$ and $1 \neq 0$. Assume that right multiplication by positive elements is strictly monotone and left multiplication by nonnegative elements is monotone. For any elements $a, b, c \in R$ with $b \geq 0$ and $c \geq 1$, if $a \cdot c \leq b$, then $a \leq b$.

nonneg_le_nonneg_of_sq_le_sq theorem

[PosMulStrictMono R] [MulPosMono R] {a b : R} (hb : 0 ≤ b) (h : a * a ≤ b * b) : a ≤ b

Full source

theorem nonneg_le_nonneg_of_sq_le_sq [PosMulStrictMono R] [MulPosMono R]
    {a b : R} (hb : 0 ≤ b) (h : a * a ≤ b * b) : a ≤ b :=
  le_of_not_gt fun hab => (mul_self_lt_mul_self hb hab).not_le h

Nonnegative elements comparison via squares: $a^2 \leq b^2 \implies a \leq b$ for $b \geq 0$

Informal description

Let $R$ be an ordered structure where left multiplication by positive elements is strictly monotone and right multiplication by nonnegative elements is monotone. For any elements $a, b \in R$ with $b \geq 0$, if $a^2 \leq b^2$, then $a \leq b$.

mul_self_le_mul_self_iff theorem

[PosMulStrictMono R] [MulPosMono R] {a b : R} (h1 : 0 ≤ a) (h2 : 0 ≤ b) : a ≤ b ↔ a * a ≤ b * b

Full source

theorem mul_self_le_mul_self_iff [PosMulStrictMono R] [MulPosMono R]
    {a b : R} (h1 : 0 ≤ a) (h2 : 0 ≤ b) : a ≤ b ↔ a * a ≤ b * b :=
  ⟨mul_self_le_mul_self h1, nonneg_le_nonneg_of_sq_le_sq h2⟩

Nonnegative Elements Comparison via Squares: $a \leq b \leftrightarrow a^2 \leq b^2$ for $a, b \geq 0$

Informal description

Let $R$ be an ordered structure where left multiplication by positive elements is strictly monotone and right multiplication by nonnegative elements is monotone. For any nonnegative elements $a, b \in R$ (i.e., $a \geq 0$ and $b \geq 0$), we have $a \leq b$ if and only if $a^2 \leq b^2$.

mul_self_lt_mul_self_iff theorem

[PosMulStrictMono R] [MulPosMono R] {a b : R} (h1 : 0 ≤ a) (h2 : 0 ≤ b) : a < b ↔ a * a < b * b

Full source

theorem mul_self_lt_mul_self_iff [PosMulStrictMono R] [MulPosMono R]
    {a b : R} (h1 : 0 ≤ a) (h2 : 0 ≤ b) : a < b ↔ a * a < b * b :=
  ((@strictMonoOn_mul_self R _).lt_iff_lt h1 h2).symm

Square preserves strict order for nonnegative elements: $a < b \leftrightarrow a^2 < b^2$ when $a, b \geq 0$

Informal description

Let $R$ be an ordered structure where left multiplication by positive elements is strictly monotone and right multiplication by nonnegative elements is monotone. For any nonnegative elements $a, b \in R$ (i.e., $a \geq 0$ and $b \geq 0$), we have $a < b$ if and only if $a^2 < b^2$.

mul_self_inj theorem

[PosMulStrictMono R] [MulPosMono R] {a b : R} (h1 : 0 ≤ a) (h2 : 0 ≤ b) : a * a = b * b ↔ a = b

Full source

theorem mul_self_inj [PosMulStrictMono R] [MulPosMono R]
    {a b : R} (h1 : 0 ≤ a) (h2 : 0 ≤ b) : a * a = b * b ↔ a = b :=
  (@strictMonoOn_mul_self R _).eq_iff_eq h1 h2

Injectivity of Squaring on Nonnegative Elements: $a^2 = b^2 \leftrightarrow a = b$ for $a, b \geq 0$

Informal description

Let $R$ be a preordered type with multiplication such that left multiplication by positive elements is strictly monotone and right multiplication by nonnegative elements is monotone. For any nonnegative elements $a, b \in R$ (i.e., $0 \leq a$ and $0 \leq b$), the squares of $a$ and $b$ are equal if and only if $a$ and $b$ are equal, i.e., $a^2 = b^2 \leftrightarrow a = b$.

sign_cases_of_C_mul_pow_nonneg theorem

[PosMulStrictMono R] (h : ∀ n, 0 ≤ a * b ^ n) : a = 0 ∨ 0 < a ∧ 0 ≤ b

Full source

lemma sign_cases_of_C_mul_pow_nonneg [PosMulStrictMono R]
    (h : ∀ n, 0 ≤ a * b ^ n) : a = 0 ∨ 0 < a ∧ 0 ≤ b := by
  have : 0 ≤ a := by simpa only [pow_zero, mul_one] using h 0
  refine this.eq_or_gt.imp_right fun ha ↦ ⟨ha, nonneg_of_mul_nonneg_right ?_ ha⟩
  simpa only [pow_one] using h 1

Sign Analysis of Nonnegative Products $a \cdot b^n$: $a = 0$ or ($a > 0$ and $b \geq 0$)

Informal description

Let $R$ be a preordered type with multiplication such that left multiplication by positive elements is strictly monotone. For any elements $a, b \in R$, if for all natural numbers $n$, the product $a \cdot b^n$ is nonnegative, then either $a = 0$ or $a > 0$ and $b \geq 0$.

mul_pos_iff theorem

 [ExistsAddOfLE R] [PosMulStrictMono R] [MulPosStrictMono R] [AddLeftStrictMono R] [AddLeftReflectLT R] :
  0 < a * b ↔ 0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0

Full source

theorem mul_pos_iff [ExistsAddOfLE R] [PosMulStrictMono R] [MulPosStrictMono R]
    [AddLeftStrictMono R] [AddLeftReflectLT R] :
    0 < a * b ↔ 0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0 :=
  ⟨pos_and_pos_or_neg_and_neg_of_mul_pos, fun h =>
    h.elim (and_imp.2 mul_pos) (and_imp.2 mul_pos_of_neg_of_neg)⟩

Characterization of Positive Products in Ordered Rings: $0 < a \cdot b \leftrightarrow (0 < a \land 0 < b) \lor (a < 0 \land b < 0)$

Informal description

Let $R$ be an ordered ring where: 1. Left multiplication by positive elements is strictly monotone (`PosMulStrictMono R`) 2. Right multiplication by positive elements is strictly monotone (`MulPosStrictMono R`) 3. Addition is strictly monotone on the left (`AddLeftStrictMono R`) 4. The order relation is reflected by left addition (`AddLeftReflectLT R`) 5. For any $x \leq y$, there exists $z$ such that $y = x + z$ (`ExistsAddOfLE R`) Then for any elements $a, b \in R$, the product $a \cdot b$ is positive ($0 < a \cdot b$) if and only if either both $a$ and $b$ are positive ($0 < a$ and $0 < b$) or both are negative ($a < 0$ and $b < 0$).

mul_nonneg_iff theorem

 [ExistsAddOfLE R] [MulPosStrictMono R] [PosMulStrictMono R] [AddLeftReflectLE R] [AddLeftMono R] :
  0 ≤ a * b ↔ 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0

Full source

theorem mul_nonneg_iff [ExistsAddOfLE R] [MulPosStrictMono R] [PosMulStrictMono R]
    [AddLeftReflectLE R] [AddLeftMono R]:
    0 ≤ a * b ↔ 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0 :=
  ⟨nonneg_and_nonneg_or_nonpos_and_nonpos_of_mul_nonneg, fun h =>
    h.elim (and_imp.2 mul_nonneg) (and_imp.2 mul_nonneg_of_nonpos_of_nonpos)⟩

Characterization of Nonnegative Products in Ordered Semirings: $0 \leq a \cdot b \leftrightarrow (0 \leq a \land 0 \leq b) \lor (a \leq 0 \land b \leq 0)$

Informal description

Let $R$ be an ordered semiring where: 1. Right multiplication by positive elements is strictly monotone (`MulPosStrictMono`) 2. Left multiplication by positive elements is strictly monotone (`PosMulStrictMono`) 3. Addition is monotone on the left (`AddLeftMono`) 4. The order relation is reflected by left addition (`AddLeftReflectLE`) 5. For any $x \leq y$, there exists $z$ such that $y = x + z$ (`ExistsAddOfLE`) Then for any elements $a, b \in R$, the product $a \cdot b$ is nonnegative ($0 \leq a \cdot b$) if and only if either both $a$ and $b$ are nonnegative ($0 \leq a$ and $0 \leq b$) or both are nonpositive ($a \leq 0$ and $b \leq 0$).

mul_nonneg_of_three theorem

 [ExistsAddOfLE R] [MulPosStrictMono R] [PosMulStrictMono R] [AddLeftMono R] [AddLeftReflectLE R] (a b c : R) :
  0 ≤ a * b ∨ 0 ≤ b * c ∨ 0 ≤ c * a

Full source

/-- Out of three elements of a `LinearOrderedRing`, two must have the same sign. -/
theorem mul_nonneg_of_three [ExistsAddOfLE R] [MulPosStrictMono R] [PosMulStrictMono R]
    [AddLeftMono R] [AddLeftReflectLE R]
    (a b c : R) : 0 ≤ a * b ∨ 0 ≤ b * c ∨ 0 ≤ c * a := by
  iterate 3 rw [mul_nonneg_iff]
  have or_a := le_total 0 a
  have or_b := le_total 0 b
  have or_c := le_total 0 c
  aesop

Sign Agreement Among Three Elements in a Linearly Ordered Ring

Informal description

Let $R$ be a linearly ordered ring where: 1. Right multiplication by positive elements is strictly monotone (`MulPosStrictMono`) 2. Left multiplication by positive elements is strictly monotone (`PosMulStrictMono`) 3. Addition is monotone on the left (`AddLeftMono`) 4. The order relation is reflected by left addition (`AddLeftReflectLE`) 5. For any $x \leq y$, there exists $z$ such that $y = x + z$ (`ExistsAddOfLE`) Then for any three elements $a, b, c \in R$, at least one of the following products must be nonnegative: \[ 0 \leq a \cdot b \quad \text{or} \quad 0 \leq b \cdot c \quad \text{or} \quad 0 \leq c \cdot a. \]

mul_nonneg_iff_pos_imp_nonneg theorem

 [ExistsAddOfLE R] [PosMulStrictMono R] [MulPosStrictMono R] [AddLeftMono R] [AddLeftReflectLE R] :
  0 ≤ a * b ↔ (0 < a → 0 ≤ b) ∧ (0 < b → 0 ≤ a)

Full source

lemma mul_nonneg_iff_pos_imp_nonneg [ExistsAddOfLE R] [PosMulStrictMono R] [MulPosStrictMono R]
    [AddLeftMono R] [AddLeftReflectLE R] :
    0 ≤ a * b ↔ (0 < a → 0 ≤ b) ∧ (0 < b → 0 ≤ a) := by
  refine mul_nonneg_iff.trans ?_
  simp_rw [← not_le, ← or_iff_not_imp_left]
  have := le_total a 0
  have := le_total b 0
  tauto

Nonnegativity of Product via Positive Implications: $0 \leq a \cdot b \leftrightarrow (0 < a \to 0 \leq b) \land (0 < b \to 0 \leq a)$

Informal description

Let $R$ be an ordered semiring where: 1. Left multiplication by positive elements is strictly monotone (`PosMulStrictMono`) 2. Right multiplication by positive elements is strictly monotone (`MulPosStrictMono`) 3. Addition is monotone on the left (`AddLeftMono`) 4. The order relation is reflected by left addition (`AddLeftReflectLE`) 5. For any $x \leq y$, there exists $z$ such that $y = x + z$ (`ExistsAddOfLE`) Then for any elements $a, b \in R$, the product $a \cdot b$ is nonnegative ($0 \leq a \cdot b$) if and only if both implications hold: - If $a$ is positive ($0 < a$), then $b$ is nonnegative ($0 \leq b$) - If $b$ is positive ($0 < b$), then $a$ is nonnegative ($0 \leq a$).

mul_le_mul_left_of_neg theorem

 [ExistsAddOfLE R] [PosMulStrictMono R] [AddRightMono R] [AddRightReflectLE R] {a b c : R} (h : c < 0) :
  c * a ≤ c * b ↔ b ≤ a

Full source

@[simp]
theorem mul_le_mul_left_of_neg [ExistsAddOfLE R] [PosMulStrictMono R]
    [AddRightMono R] [AddRightReflectLE R]
    {a b c : R} (h : c < 0) : c * a ≤ c * b ↔ b ≤ a :=
  (strictAnti_mul_left h).le_iff_le

Left Multiplication by Negative Elements Reverses Inequality

Informal description

Let $R$ be an ordered ring where: 1. Left multiplication by positive elements is strictly monotone (`PosMulStrictMono R`) 2. Addition is monotone on the right (`AddRightMono R`) 3. The order relation is reflected by right addition (`AddRightReflectLE R`) 4. For any $x \leq y$, there exists $z$ such that $y = x + z$ (`ExistsAddOfLE R`) Then for any negative element $c < 0$ in $R$, and any elements $a, b \in R$, we have the equivalence: \[ c \cdot a \leq c \cdot b \quad \text{if and only if} \quad b \leq a. \]

mul_le_mul_right_of_neg theorem

 [ExistsAddOfLE R] [MulPosStrictMono R] [AddRightMono R] [AddRightReflectLE R] {a b c : R} (h : c < 0) :
  a * c ≤ b * c ↔ b ≤ a

Full source

@[simp]
theorem mul_le_mul_right_of_neg [ExistsAddOfLE R] [MulPosStrictMono R]
    [AddRightMono R] [AddRightReflectLE R]
    {a b c : R} (h : c < 0) : a * c ≤ b * c ↔ b ≤ a :=
  (strictAnti_mul_right h).le_iff_le

Right Multiplication by Negative Elements Reverses Inequality

Informal description

Let $R$ be an ordered ring where: 1. Right multiplication by positive elements is strictly monotone (`MulPosStrictMono R`) 2. Addition is monotone on the right (`AddRightMono R`) 3. The order relation is reflected by right addition (`AddRightReflectLE R`) 4. For any $x \leq y$, there exists $z$ such that $y = x + z$ (`ExistsAddOfLE R`) Then for any negative element $c < 0$ in $R$, and any elements $a, b \in R$, we have the equivalence: \[ a \cdot c \leq b \cdot c \quad \text{if and only if} \quad b \leq a. \]

mul_lt_mul_left_of_neg theorem

 [ExistsAddOfLE R] [PosMulStrictMono R] [AddRightStrictMono R] [AddRightReflectLT R] {a b c : R} (h : c < 0) :
  c * a < c * b ↔ b < a

Full source

@[simp]
theorem mul_lt_mul_left_of_neg [ExistsAddOfLE R] [PosMulStrictMono R]
    [AddRightStrictMono R] [AddRightReflectLT R]
    {a b c : R} (h : c < 0) : c * a < c * b ↔ b < a :=
  (strictAnti_mul_left h).lt_iff_lt

Reversed Inequality Under Left Multiplication by Negative Elements: $c \cdot a < c \cdot b \leftrightarrow b < a$

Informal description

Let $R$ be an ordered ring where: 1. Left multiplication by positive elements is strictly monotone, 2. Addition is strictly monotone on the right, 3. The order relation is reflected by right addition, 4. For any $x \leq y$, there exists $z$ such that $y = x + z$. Then for any negative element $c < 0$ in $R$ and any elements $a, b \in R$, we have the equivalence: $$c \cdot a < c \cdot b \quad \text{if and only if} \quad b < a.$$

mul_lt_mul_right_of_neg theorem

 [ExistsAddOfLE R] [MulPosStrictMono R] [AddRightStrictMono R] [AddRightReflectLT R] {a b c : R} (h : c < 0) :
  a * c < b * c ↔ b < a

Full source

@[simp]
theorem mul_lt_mul_right_of_neg [ExistsAddOfLE R] [MulPosStrictMono R]
    [AddRightStrictMono R] [AddRightReflectLT R]
    {a b c : R} (h : c < 0) : a * c < b * c ↔ b < a :=
  (strictAnti_mul_right h).lt_iff_lt

Inequality Reversal for Right Multiplication by Negative Elements

Informal description

Let $R$ be an ordered ring where: 1. For any $x \leq y$, there exists $z$ such that $y = x + z$ (`ExistsAddOfLE R`), 2. Right multiplication by positive elements is strictly monotone (`MulPosStrictMono R`), 3. Addition is strictly monotone on the right (`AddRightStrictMono R`), 4. The order relation is reflected by right addition (`AddRightReflectLT R`). Then for any elements $a, b, c \in R$ with $c < 0$, the inequality $a \cdot c < b \cdot c$ holds if and only if $b < a$.

lt_of_mul_lt_mul_of_nonpos_left theorem

[ExistsAddOfLE R] [PosMulMono R] [AddRightMono R] [AddRightReflectLE R] (h : c * a < c * b) (hc : c ≤ 0) : b < a

Full source

theorem lt_of_mul_lt_mul_of_nonpos_left [ExistsAddOfLE R] [PosMulMono R]
    [AddRightMono R] [AddRightReflectLE R]
    (h : c * a < c * b) (hc : c ≤ 0) : b < a :=
  (antitone_mul_left hc).reflect_lt h

Inequality Reversal for Left Multiplication by Nonpositive Elements

Informal description

Let $R$ be a preordered semiring where: 1. The order relation has the "exists add of ≤" property (for any $a \leq b$, there exists $c$ such that $b = a + c$) 2. Left multiplication by nonnegative elements is monotone (`PosMulMono`) 3. Addition is right monotone (`AddRightMono`) 4. The order relation reflects addition on the right (`AddRightReflectLE`) For any elements $a, b, c \in R$ with $c \leq 0$, if $c \cdot a < c \cdot b$, then $b < a$.

lt_of_mul_lt_mul_of_nonpos_right theorem

[ExistsAddOfLE R] [MulPosMono R] [AddRightMono R] [AddRightReflectLE R] (h : a * c < b * c) (hc : c ≤ 0) : b < a

Full source

theorem lt_of_mul_lt_mul_of_nonpos_right [ExistsAddOfLE R] [MulPosMono R]
    [AddRightMono R] [AddRightReflectLE R]
    (h : a * c < b * c) (hc : c ≤ 0) : b < a :=
  (antitone_mul_right hc).reflect_lt h

Inequality Reversal for Right Multiplication by Nonpositive Elements

Informal description

Let $R$ be a preordered semiring where: 1. The order relation has the "exists add of ≤" property (for any $a \leq b$, there exists $c$ such that $b = a + c$) 2. Right multiplication by nonnegative elements is monotone (`MulPosMono`) 3. Addition is right monotone (`AddRightMono`) 4. The order relation reflects addition on the right (`AddRightReflectLE`) For any elements $a, b, c \in R$ with $c \leq 0$, if $a \cdot c < b \cdot c$, then $b < a$.

cmp_mul_neg_left theorem

 [ExistsAddOfLE R] [PosMulStrictMono R] [AddRightReflectLT R] [AddRightStrictMono R] {a : R} (ha : a < 0) (b c : R) :
  cmp (a * b) (a * c) = cmp c b

Full source

theorem cmp_mul_neg_left [ExistsAddOfLE R] [PosMulStrictMono R]
    [AddRightReflectLT R] [AddRightStrictMono R]
    {a : R} (ha : a < 0) (b c : R) : cmp (a * b) (a * c) = cmp c b :=
  (strictAnti_mul_left ha).cmp_map_eq b c

Comparison Reversal for Left Multiplication by Negative Elements

Informal description

Let $R$ be an ordered ring where: 1. Left multiplication by positive elements is strictly monotone (`PosMulStrictMono R`) 2. The order relation is reflected by right addition (`AddRightReflectLT R`) 3. Addition is strictly monotone on the right (`AddRightStrictMono R`) 4. For any $x \leq y$, there exists $z$ such that $y = x + z$ (`ExistsAddOfLE R`) Then for any negative element $a < 0$ in $R$ and any elements $b, c \in R$, the comparison of $a \cdot b$ and $a \cdot c$ is equal to the comparison of $c$ and $b$, i.e., $\text{cmp}(a \cdot b, a \cdot c) = \text{cmp}(c, b)$.

cmp_mul_neg_right theorem

 [ExistsAddOfLE R] [MulPosStrictMono R] [AddRightReflectLT R] [AddRightStrictMono R] {a : R} (ha : a < 0) (b c : R) :
  cmp (b * a) (c * a) = cmp c b

Full source

theorem cmp_mul_neg_right [ExistsAddOfLE R] [MulPosStrictMono R]
    [AddRightReflectLT R] [AddRightStrictMono R]
    {a : R} (ha : a < 0) (b c : R) : cmp (b * a) (c * a) = cmp c b :=
  (strictAnti_mul_right ha).cmp_map_eq b c

Comparison Reversal under Right Multiplication by Negative Elements

Informal description

Let $R$ be an ordered ring where: 1. Right multiplication by positive elements is strictly monotone, 2. The order relation is reflected by right addition, 3. Addition is strictly monotone on the right, and 4. For any $x \leq y$, there exists $z$ such that $y = x + z$. Then for any negative element $a < 0$ in $R$ and any elements $b, c \in R$, the comparison of $b \cdot a$ and $c \cdot a$ is equal to the comparison of $c$ and $b$, i.e., $$\text{cmp}(b \cdot a, c \cdot a) = \text{cmp}(c, b).$$

mul_self_pos theorem

 [ExistsAddOfLE R] [PosMulStrictMono R] [MulPosStrictMono R] [AddLeftStrictMono R] [AddLeftReflectLT R] {a : R} :
  0 < a * a ↔ a ≠ 0

Full source

@[simp]
theorem mul_self_pos [ExistsAddOfLE R] [PosMulStrictMono R] [MulPosStrictMono R]
    [AddLeftStrictMono R] [AddLeftReflectLT R]
    {a : R} : 0 < a * a ↔ a ≠ 0 := by
  constructor
  · rintro h rfl
    rw [mul_zero] at h
    exact h.false
  · intro h
    rcases h.lt_or_lt with h | h
    exacts [mul_pos_of_neg_of_neg h h, mul_pos h h]

Positivity of Squares in Ordered Rings: $0 < a^2 \leftrightarrow a \neq 0$

Informal description

Let $R$ be an ordered ring where: 1. Right multiplication by positive elements is strictly monotone (`MulPosStrictMono R`) 2. Left multiplication by positive elements is strictly monotone (`PosMulStrictMono R`) 3. Addition is strictly monotone on the left (`AddLeftStrictMono R`) 4. The order relation is reflected by left addition (`AddLeftReflectLT R`) 5. For any $x \leq y$, there exists $z$ such that $y = x + z$ (`ExistsAddOfLE R`) Then for any element $a \in R$, the square $a^2$ is positive if and only if $a$ is nonzero, i.e., $0 < a^2 \leftrightarrow a \neq 0$.

nonneg_of_mul_nonpos_left theorem

 [ExistsAddOfLE R] [MulPosStrictMono R] [AddRightMono R] [AddRightReflectLE R] {a b : R} (h : a * b ≤ 0) (hb : b < 0) :
  0 ≤ a

Full source

theorem nonneg_of_mul_nonpos_left [ExistsAddOfLE R] [MulPosStrictMono R]
    [AddRightMono R] [AddRightReflectLE R]
    {a b : R} (h : a * b ≤ 0) (hb : b < 0) : 0 ≤ a :=
  le_of_not_gt fun ha => absurd h (mul_pos_of_neg_of_neg ha hb).not_le

Nonnegativity from Left Nonpositive Product with Negative Factor

Informal description

Let $R$ be an ordered ring where: 1. Right multiplication by positive elements is strictly monotone (`MulPosStrictMono R`) 2. Addition is monotone on the right (`AddRightMono R`) 3. The order relation is reflected by right addition (`AddRightReflectLE R`) 4. For any $x \leq y$, there exists $z$ such that $y = x + z$ (`ExistsAddOfLE R`) Then for any elements $a, b \in R$ with $a \cdot b \leq 0$ and $b < 0$, we have $0 \leq a$.

nonneg_of_mul_nonpos_right theorem

 [ExistsAddOfLE R] [MulPosStrictMono R] [AddRightMono R] [AddRightReflectLE R] {a b : R} (h : a * b ≤ 0) (ha : a < 0) :
  0 ≤ b

Full source

theorem nonneg_of_mul_nonpos_right [ExistsAddOfLE R] [MulPosStrictMono R]
    [AddRightMono R] [AddRightReflectLE R]
    {a b : R} (h : a * b ≤ 0) (ha : a < 0) : 0 ≤ b :=
  le_of_not_gt fun hb => absurd h (mul_pos_of_neg_of_neg ha hb).not_le

Nonnegativity of Second Factor from Nonpositive Product with Negative First Factor in Ordered Rings

Informal description

Let $R$ be an ordered ring where: 1. Right multiplication by positive elements is strictly monotone (`MulPosStrictMono R`), 2. Addition is monotone on the right (`AddRightMono R`), 3. The order relation is reflected by right addition (`AddRightReflectLE R`), 4. For any $x \leq y$, there exists $z$ such that $y = x + z$ (`ExistsAddOfLE R`). If $a, b \in R$ satisfy $a \cdot b \leq 0$ and $a < 0$, then $0 \leq b$.

pos_of_mul_neg_left theorem

 [ExistsAddOfLE R] [MulPosMono R] [AddRightMono R] [AddRightReflectLE R] {a b : R} (h : a * b < 0) (hb : b ≤ 0) : 0 < a

Full source

theorem pos_of_mul_neg_left [ExistsAddOfLE R] [MulPosMono R]
    [AddRightMono R] [AddRightReflectLE R]
    {a b : R} (h : a * b < 0) (hb : b ≤ 0) : 0 < a :=
  lt_of_not_ge fun ha => absurd h (mul_nonneg_of_nonpos_of_nonpos ha hb).not_lt

Positivity from Left Factor in Negative Product with Nonpositive Right Factor

Informal description

Let $R$ be a preordered semiring where: 1. The order relation has the "exists add of ≤" property (for any $a \leq b$, there exists $c$ such that $b = a + c$) 2. Right multiplication by nonnegative elements is monotone 3. Addition is right monotone 4. The order relation reflects addition on the right For any elements $a, b \in R$, if $a \cdot b < 0$ and $b \leq 0$, then $0 < a$.

pos_of_mul_neg_right theorem

 [ExistsAddOfLE R] [MulPosMono R] [AddRightMono R] [AddRightReflectLE R] {a b : R} (h : a * b < 0) (ha : a ≤ 0) : 0 < b

Full source

theorem pos_of_mul_neg_right [ExistsAddOfLE R] [MulPosMono R]
    [AddRightMono R] [AddRightReflectLE R]
    {a b : R} (h : a * b < 0) (ha : a ≤ 0) : 0 < b :=
  lt_of_not_ge fun hb => absurd h (mul_nonneg_of_nonpos_of_nonpos ha hb).not_lt

Positivity of Right Factor in Negative Product with Nonpositive Left Factor

Informal description

Let $R$ be a preordered semiring where: 1. The order relation has the "exists add of ≤" property (for any $a \leq b$, there exists $c$ such that $b = a + c$) 2. Right multiplication by nonnegative elements is monotone 3. Addition is right monotone 4. The order relation reflects addition on the right For any elements $a, b \in R$, if $a \cdot b < 0$ and $a \leq 0$, then $0 < b$.

neg_iff_pos_of_mul_neg theorem

 [ExistsAddOfLE R] [PosMulMono R] [MulPosMono R] [AddRightMono R] [AddRightReflectLE R] (hab : a * b < 0) :
  a < 0 ↔ 0 < b

Full source

theorem neg_iff_pos_of_mul_neg [ExistsAddOfLE R] [PosMulMono R] [MulPosMono R]
    [AddRightMono R] [AddRightReflectLE R]
    (hab : a * b < 0) : a < 0 ↔ 0 < b :=
  ⟨pos_of_mul_neg_right hab ∘ le_of_lt, neg_of_mul_neg_left hab ∘ le_of_lt⟩

Sign Criterion for Negative Product: $a < 0 \leftrightarrow 0 < b$ when $a \cdot b < 0$

Informal description

Let $R$ be a preordered semiring where: 1. For any $a \leq b$, there exists $c$ such that $b = a + c$, 2. Left and right multiplication by nonnegative elements are monotone, 3. Addition is right monotone, 4. The order relation reflects addition on the right. For any elements $a, b \in R$ with $a \cdot b < 0$, we have $a < 0$ if and only if $0 < b$.

pos_iff_neg_of_mul_neg theorem

 [ExistsAddOfLE R] [PosMulMono R] [MulPosMono R] [AddRightMono R] [AddRightReflectLE R] (hab : a * b < 0) :
  0 < a ↔ b < 0

Full source

theorem pos_iff_neg_of_mul_neg [ExistsAddOfLE R] [PosMulMono R] [MulPosMono R]
    [AddRightMono R] [AddRightReflectLE R]
    (hab : a * b < 0) : 0 < a ↔ b < 0 :=
  ⟨neg_of_mul_neg_right hab ∘ le_of_lt, pos_of_mul_neg_left hab ∘ le_of_lt⟩

Positivity-Negativity Equivalence for Factors in Negative Product

Informal description

Let $R$ be a preordered semiring where: 1. The order relation has the "exists add of ≤" property (for any $a \leq b$, there exists $c$ such that $b = a + c$) 2. Left and right multiplication by nonnegative elements are monotone 3. Addition is right monotone 4. The order relation reflects addition on the right For any elements $a, b \in R$ such that $a \cdot b < 0$, we have $0 < a$ if and only if $b < 0$.

sq_nonneg theorem

[IsRightCancelAdd R] [ZeroLEOneClass R] [ExistsAddOfLE R] [PosMulMono R] [AddLeftStrictMono R] (a : R) : 0 ≤ a ^ 2

Full source

lemma sq_nonneg [IsRightCancelAdd R]
    [ZeroLEOneClass R] [ExistsAddOfLE R] [PosMulMono R] [AddLeftStrictMono R]
    (a : R) : 0 ≤ a ^ 2 := by
  obtain ha | ha := le_total 0 a
  · exact pow_nonneg ha _
  obtain ⟨b, hab⟩ := exists_add_of_le ha
  calc
    0 ≤ b ^ 2 := pow_nonneg (not_lt.1 fun hb ↦ hab.not_gt <| add_neg_of_nonpos_of_neg ha hb) _
    _ = a ^ 2 := add_left_injective (a * b) ?_
  calc
    b ^ 2 + a * b = (a + b) * b := by rw [add_comm, sq, add_mul]
    _ = a * (a + b) := by simp [← hab]
    _ = a ^ 2 + a * b := by rw [sq, mul_add]

Nonnegativity of Squares in Ordered Structures

Informal description

Let $R$ be a type with the following properties: - Addition is right-cancellative ($\text{IsRightCancelAdd}$) - $0 \leq 1$ ($\text{ZeroLEOneClass}$) - For any $a \leq b$, there exists $c$ such that $b = a + c$ ($\text{ExistsAddOfLE}$) - Left multiplication by nonnegative elements is monotone ($\text{PosMulMono}$) - Addition is strictly monotone on the left ($\text{AddLeftStrictMono}$) Then for any element $a \in R$, the square of $a$ is nonnegative, i.e., $0 \leq a^2$.

sq_nonpos_iff theorem

 [IsRightCancelAdd R] [ZeroLEOneClass R] [ExistsAddOfLE R] [PosMulMono R] [AddLeftStrictMono R] [NoZeroDivisors R]
  (r : R) : r ^ 2 ≤ 0 ↔ r = 0

Full source

@[simp]
lemma sq_nonpos_iff [IsRightCancelAdd R] [ZeroLEOneClass R] [ExistsAddOfLE R]
    [PosMulMono R] [AddLeftStrictMono R] [NoZeroDivisors R] (r : R) :
    r ^ 2 ≤ 0 ↔ r = 0 := by
  trans r ^ 2 = 0
  · rw [le_antisymm_iff, and_iff_left (sq_nonneg r)]
  · exact sq_eq_zero_iff

Square Nonpositivity Criterion in Ordered Structures with No Zero Divisors

Informal description

Let $R$ be a type with the following properties: - Addition is right-cancellative - $0 \leq 1$ - For any $a \leq b$, there exists $c$ such that $b = a + c$ - Left multiplication by nonnegative elements is monotone - Addition is strictly monotone on the left - $R$ has no zero divisors Then for any element $r \in R$, the square of $r$ is nonpositive if and only if $r$ is zero, i.e., $r^2 \leq 0 \leftrightarrow r = 0$.

mul_self_nonneg theorem

[IsRightCancelAdd R] [ZeroLEOneClass R] [ExistsAddOfLE R] [PosMulMono R] [AddLeftStrictMono R] (a : R) : 0 ≤ a * a

Full source

lemma mul_self_nonneg [IsRightCancelAdd R]
    [ZeroLEOneClass R] [ExistsAddOfLE R] [PosMulMono R] [AddLeftStrictMono R]
    (a : R) : 0 ≤ a * a := by simpa only [sq] using sq_nonneg a

Nonnegativity of Self-Multiplication in Ordered Structures

Informal description

Let $R$ be a type with the following properties: - Addition is right-cancellative - $0 \leq 1$ - For any $a \leq b$, there exists $c$ such that $b = a + c$ - Left multiplication by nonnegative elements is monotone - Addition is strictly monotone on the left Then for any element $a \in R$, the product $a \cdot a$ is nonnegative, i.e., $0 \leq a \cdot a$.

mul_self_add_mul_self_eq_zero theorem

 [IsRightCancelAdd R] [NoZeroDivisors R] [ZeroLEOneClass R] [ExistsAddOfLE R] [PosMulMono R] [AddLeftMono R]
  [AddLeftStrictMono R] : a * a + b * b = 0 ↔ a = 0 ∧ b = 0

Full source

/-- The sum of two squares is zero iff both elements are zero. -/
lemma mul_self_add_mul_self_eq_zero [IsRightCancelAdd R] [NoZeroDivisors R]
    [ZeroLEOneClass R] [ExistsAddOfLE R] [PosMulMono R]
    [AddLeftMono R] [AddLeftStrictMono R] :
    a * a + b * b = 0 ↔ a = 0 ∧ b = 0 := by
  rw [add_eq_zero_iff_of_nonneg, mul_self_eq_zero (M₀ := R), mul_self_eq_zero (M₀ := R)] <;>
    apply mul_self_nonneg

Sum of Squares Vanishes if and only if Both Elements are Zero

Informal description

Let $R$ be an ordered algebraic structure with the following properties: - Addition is right-cancellative - $0 \leq 1$ - For any $a \leq b$, there exists $c$ such that $b = a + c$ - Left multiplication by nonnegative elements is monotone - Addition is monotone and strictly monotone on the left - $R$ has no zero divisors Then for any elements $a, b \in R$, the sum of their squares equals zero if and only if both elements are zero, i.e., \[ a^2 + b^2 = 0 \leftrightarrow a = 0 \text{ and } b = 0. \]

max_mul_mul_le_max_mul_max theorem

[PosMulMono R] [MulPosMono R] (b c : R) (ha : 0 ≤ a) (hd : 0 ≤ d) : max (a * b) (d * c) ≤ max a c * max d b

Full source

lemma max_mul_mul_le_max_mul_max [PosMulMono R] [MulPosMono R] (b c : R) (ha : 0 ≤ a) (hd : 0 ≤ d) :
    max (a * b) (d * c) ≤ max a c * max d b :=
  have ba : b * a ≤ max d b * max c a :=
    mul_le_mul (le_max_right d b) (le_max_right c a) ha (le_trans hd (le_max_left d b))
  have cd : c * d ≤ max a c * max b d :=
    mul_le_mul (le_max_right a c) (le_max_right b d) hd (le_trans ha (le_max_left a c))
  max_le (by simpa [mul_comm, max_comm] using ba) (by simpa [mul_comm, max_comm] using cd)

Inequality for Maximum of Products: $\max(ab, dc) \leq \max(a, c) \cdot \max(d, b)$

Informal description

Let $R$ be an ordered semiring where left and right multiplication by nonnegative elements are monotone. For any elements $a, b, c, d \in R$ with $a \geq 0$ and $d \geq 0$, we have \[ \max(a \cdot b, d \cdot c) \leq \max(a, c) \cdot \max(d, b). \]

two_mul_le_add_sq theorem

[ExistsAddOfLE R] [MulPosStrictMono R] [AddLeftReflectLE R] [AddLeftMono R] (a b : R) : 2 * a * b ≤ a ^ 2 + b ^ 2

Full source

/-- Binary, squared, and division-free **arithmetic mean-geometric mean inequality**
(aka AM-GM inequality) for linearly ordered commutative semirings. -/
lemma two_mul_le_add_sq [ExistsAddOfLE R] [MulPosStrictMono R]
    [AddLeftReflectLE R] [AddLeftMono R]
    (a b : R) : 2 * a * b ≤ a ^ 2 + b ^ 2 := by
  simpa [fn_min_add_fn_max (fun x ↦ x * x), sq, two_mul, add_mul]
    using mul_add_mul_le_mul_add_mul (@min_le_max _ _ a b) (@min_le_max _ _ a b)

Inequality: $2ab \leq a^2 + b^2$ in ordered semirings

Informal description

Let $R$ be an ordered semiring where right multiplication by positive elements is strictly monotone, addition is monotone in its left argument, and the order relation is reflected by addition on the left. For any elements $a, b \in R$, the following inequality holds: $$ 2ab \leq a^2 + b^2 $$

four_mul_le_sq_add theorem

[ExistsAddOfLE R] [MulPosStrictMono R] [AddLeftReflectLE R] [AddLeftMono R] (a b : R) : 4 * a * b ≤ (a + b) ^ 2

Full source

/-- Binary, squared, and division-free **arithmetic mean-geometric mean inequality**
(aka AM-GM inequality) for linearly ordered commutative semirings. -/
lemma four_mul_le_sq_add [ExistsAddOfLE R] [MulPosStrictMono R]
    [AddLeftReflectLE R] [AddLeftMono R]
    (a b : R) : 4 * a * b ≤ (a + b) ^ 2 := by
  calc 4 * a * b
    _ = 2 * a * b + 2 * a * b := by rw [mul_assoc, two_add_two_eq_four.symm, add_mul, mul_assoc]
    _ ≤ a ^ 2 + b ^ 2 + 2 * a * b := by gcongr; exact two_mul_le_add_sq _ _
    _ = a ^ 2 + 2 * a * b + b ^ 2 := by rw [add_right_comm]
    _ = (a + b) ^ 2 := (add_sq a b).symm

Inequality: $4ab \leq (a + b)^2$ in ordered semirings

Informal description

Let $R$ be an ordered semiring where right multiplication by positive elements is strictly monotone, addition is monotone in its left argument, and the order relation is reflected by addition on the left. For any elements $a, b \in R$, the following inequality holds: $$ 4ab \leq (a + b)^2 $$

two_mul_le_add_of_sq_eq_mul theorem

 [ExistsAddOfLE R] [MulPosStrictMono R] [PosMulStrictMono R] [AddLeftReflectLE R] [AddLeftMono R] {a b r : R}
  (ha : 0 ≤ a) (hb : 0 ≤ b) (ht : r ^ 2 = a * b) : 2 * r ≤ a + b

Full source

/-- Binary and division-free **arithmetic mean-geometric mean inequality**
(aka AM-GM inequality) for linearly ordered commutative semirings. -/
lemma two_mul_le_add_of_sq_eq_mul [ExistsAddOfLE R] [MulPosStrictMono R] [PosMulStrictMono R]
    [AddLeftReflectLE R] [AddLeftMono R] {a b r : R}
    (ha : 0 ≤ a) (hb : 0 ≤ b) (ht : r ^ 2 = a * b) : 2 * r ≤ a + b := by
  apply nonneg_le_nonneg_of_sq_le_sq (Left.add_nonneg ha hb)
  conv_rhs => rw [← pow_two]
  convert four_mul_le_sq_add a b using 1
  rw [mul_mul_mul_comm, two_mul, two_add_two_eq_four, ← pow_two, ht, mul_assoc]

Arithmetic Mean-Geometric Mean Inequality for Ordered Semirings: $2\sqrt{ab} \leq a + b$ for $a, b \geq 0$

Informal description

Let $R$ be an ordered semiring where: 1. Right multiplication by positive elements is strictly monotone (`MulPosStrictMono R`) 2. Left multiplication by positive elements is strictly monotone (`PosMulStrictMono R`) 3. Addition is monotone on the left (`AddLeftMono R`) 4. The order relation is reflected by left addition (`AddLeftReflectLE R`) For any nonnegative elements $a, b \in R$ (i.e., $a \geq 0$ and $b \geq 0$) and any element $r \in R$ such that $r^2 = a \cdot b$, the following inequality holds: $$ 2r \leq a + b $$

mul_neg_iff theorem

 [PosMulStrictMono R] [MulPosStrictMono R] [AddLeftReflectLT R] [AddLeftStrictMono R] :
  a * b < 0 ↔ 0 < a ∧ b < 0 ∨ a < 0 ∧ 0 < b

Full source

lemma mul_neg_iff [PosMulStrictMono R] [MulPosStrictMono R]
    [AddLeftReflectLT R] [AddLeftStrictMono R] :
    a * b < 0 ↔ 0 < a ∧ b < 0 ∨ a < 0 ∧ 0 < b := by
  rw [← neg_pos, neg_mul_eq_mul_neg, mul_pos_iff (R := R), neg_pos, neg_lt_zero]

Characterization of Negative Products in Ordered Rings: $a \cdot b < 0 \leftrightarrow (0 < a \land b < 0) \lor (a < 0 \land 0 < b)$

Informal description

Let $R$ be an ordered ring where: 1. Left multiplication by positive elements is strictly monotone (`PosMulStrictMono R`) 2. Right multiplication by positive elements is strictly monotone (`MulPosStrictMono R`) 3. The order relation is reflected by left addition (`AddLeftReflectLT R`) 4. Addition is strictly monotone on the left (`AddLeftStrictMono R`) Then for any elements $a, b \in R$, the product $a \cdot b$ is negative ($a \cdot b < 0$) if and only if either $a$ is positive and $b$ is negative ($0 < a$ and $b < 0$) or $a$ is negative and $b$ is positive ($a < 0$ and $0 < b$).

mul_nonpos_iff theorem

 [MulPosStrictMono R] [PosMulStrictMono R] [AddLeftReflectLE R] [AddLeftMono R] :
  a * b ≤ 0 ↔ 0 ≤ a ∧ b ≤ 0 ∨ a ≤ 0 ∧ 0 ≤ b

Full source

lemma mul_nonpos_iff [MulPosStrictMono R] [PosMulStrictMono R]
    [AddLeftReflectLE R] [AddLeftMono R] :
    a * b ≤ 0 ↔ 0 ≤ a ∧ b ≤ 0 ∨ a ≤ 0 ∧ 0 ≤ b := by
  rw [← neg_nonneg, neg_mul_eq_mul_neg, mul_nonneg_iff (R := R), neg_nonneg, neg_nonpos]

Characterization of Nonpositive Products in Ordered Semirings: $a \cdot b \leq 0 \leftrightarrow (0 \leq a \land b \leq 0) \lor (a \leq 0 \land 0 \leq b)$

Informal description

Let $R$ be an ordered semiring where: 1. Right multiplication by positive elements is strictly monotone (`MulPosStrictMono R`) 2. Left multiplication by positive elements is strictly monotone (`PosMulStrictMono R`) 3. Addition is monotone on the left (`AddLeftMono R`) 4. The order relation is reflected by left addition (`AddLeftReflectLE R`) Then for any elements $a, b \in R$, the product $a \cdot b$ is nonpositive ($a \cdot b \leq 0$) if and only if either $a$ is nonnegative and $b$ is nonpositive ($0 \leq a$ and $b \leq 0$) or $a$ is nonpositive and $b$ is nonnegative ($a \leq 0$ and $0 \leq b$).

mul_nonneg_iff_neg_imp_nonpos theorem

 [PosMulStrictMono R] [MulPosStrictMono R] [AddLeftMono R] [AddLeftReflectLE R] :
  0 ≤ a * b ↔ (a < 0 → b ≤ 0) ∧ (b < 0 → a ≤ 0)

Full source

lemma mul_nonneg_iff_neg_imp_nonpos [PosMulStrictMono R] [MulPosStrictMono R]
    [AddLeftMono R] [AddLeftReflectLE R] :
    0 ≤ a * b ↔ (a < 0 → b ≤ 0) ∧ (b < 0 → a ≤ 0) := by
  rw [← neg_mul_neg, mul_nonneg_iff_pos_imp_nonneg (R := R)]; simp only [neg_pos, neg_nonneg]

Nonnegativity of Product via Negative Implications: $0 \leq a \cdot b \leftrightarrow (a < 0 \to b \leq 0) \land (b < 0 \to a \leq 0)$

Informal description

Let $R$ be an ordered semiring where: 1. Left multiplication by positive elements is strictly monotone (`PosMulStrictMono`) 2. Right multiplication by positive elements is strictly monotone (`MulPosStrictMono`) 3. Addition is monotone on the left (`AddLeftMono`) 4. The order relation is reflected by left addition (`AddLeftReflectLE`) Then for any elements $a, b \in R$, the product $a \cdot b$ is nonnegative ($0 \leq a \cdot b$) if and only if both implications hold: - If $a$ is negative ($a < 0$), then $b$ is nonpositive ($b \leq 0$) - If $b$ is negative ($b < 0$), then $a$ is nonpositive ($a \leq 0$).

mul_nonpos_iff_pos_imp_nonpos theorem

 [PosMulStrictMono R] [MulPosStrictMono R] [AddLeftMono R] [AddLeftReflectLE R] :
  a * b ≤ 0 ↔ (0 < a → b ≤ 0) ∧ (b < 0 → 0 ≤ a)

Full source

lemma mul_nonpos_iff_pos_imp_nonpos [PosMulStrictMono R] [MulPosStrictMono R]
    [AddLeftMono R] [AddLeftReflectLE R] :
    a * b ≤ 0 ↔ (0 < a → b ≤ 0) ∧ (b < 0 → 0 ≤ a) := by
  rw [← neg_nonneg, ← mul_neg, mul_nonneg_iff_pos_imp_nonneg (R := R)]
  simp only [neg_pos, neg_nonneg]

Characterization of Nonpositive Products via Positive Implications: $a \cdot b \leq 0 \leftrightarrow (0 < a \to b \leq 0) \land (b < 0 \to 0 \leq a)$

Informal description

Let $R$ be an ordered semiring where: 1. Left multiplication by positive elements is strictly monotone (`PosMulStrictMono`) 2. Right multiplication by positive elements is strictly monotone (`MulPosStrictMono`) 3. Addition is monotone on the left (`AddLeftMono`) 4. The order relation is reflected by left addition (`AddLeftReflectLE`) Then for any elements $a, b \in R$, the product $a \cdot b$ is nonpositive ($a \cdot b \leq 0$) if and only if both implications hold: - If $a$ is positive ($0 < a$), then $b$ is nonpositive ($b \leq 0$) - If $b$ is negative ($b < 0$), then $a$ is nonnegative ($0 \leq a$).

mul_nonpos_iff_neg_imp_nonneg theorem

 [PosMulStrictMono R] [MulPosStrictMono R] [AddLeftMono R] [AddLeftReflectLE R] :
  a * b ≤ 0 ↔ (a < 0 → 0 ≤ b) ∧ (0 < b → a ≤ 0)

Full source

lemma mul_nonpos_iff_neg_imp_nonneg [PosMulStrictMono R] [MulPosStrictMono R]
    [AddLeftMono R] [AddLeftReflectLE R] :
    a * b ≤ 0 ↔ (a < 0 → 0 ≤ b) ∧ (0 < b → a ≤ 0) := by
  rw [← neg_nonneg, ← neg_mul, mul_nonneg_iff_pos_imp_nonneg (R := R)]
  simp only [neg_pos, neg_nonneg]

Nonpositivity of Product via Negative and Positive Implications: $a \cdot b \leq 0 \leftrightarrow (a < 0 \to 0 \leq b) \land (0 < b \to a \leq 0)$

Informal description

Let $R$ be an ordered semiring where: 1. Left multiplication by positive elements is strictly monotone (`PosMulStrictMono`) 2. Right multiplication by positive elements is strictly monotone (`MulPosStrictMono`) 3. Addition is monotone on the left (`AddLeftMono`) 4. The order relation is reflected by left addition (`AddLeftReflectLE`) Then for any elements $a, b \in R$, the product $a \cdot b$ is nonpositive ($a \cdot b \leq 0$) if and only if both implications hold: - If $a$ is negative ($a < 0$), then $b$ is nonnegative ($0 \leq b$) - If $b$ is positive ($0 < b$), then $a$ is nonpositive ($a \leq 0$).

neg_one_lt_zero theorem

[ZeroLEOneClass R] [NeZero (1 : R)] [AddLeftStrictMono R] : -1 < (0 : R)

Full source

lemma neg_one_lt_zero
    [ZeroLEOneClass R] [NeZero (1 : R)] [AddLeftStrictMono R] :
    -1 < (0 : R) := neg_lt_zero.2 zero_lt_one

Negative One is Less Than Zero in Ordered Rings

Informal description

For any ordered ring $R$ where $0 \leq 1$, $1 \neq 0$, and addition is strictly monotone, the inequality $-1 < 0$ holds.

sub_one_lt theorem

[ZeroLEOneClass R] [NeZero (1 : R)] [AddLeftStrictMono R] (a : R) : a - 1 < a

Full source

lemma sub_one_lt [ZeroLEOneClass R] [NeZero (1 : R)]
    [AddLeftStrictMono R]
    (a : R) : a - 1 < a := sub_lt_iff_lt_add.2 <| lt_add_one a

Subtracting One Decreases the Value in Ordered Rings

Informal description

Let $R$ be an ordered ring where $0 \leq 1$, $1 \neq 0$, and addition is strictly monotone. Then for any element $a \in R$, we have $a - 1 < a$.

mul_self_le_mul_self_of_le_of_neg_le theorem

[MulPosMono R] [PosMulMono R] [AddLeftMono R] (h₁ : a ≤ b) (h₂ : -a ≤ b) : a * a ≤ b * b

Full source

lemma mul_self_le_mul_self_of_le_of_neg_le
    [MulPosMono R] [PosMulMono R] [AddLeftMono R]
    (h₁ : a ≤ b) (h₂ : -a ≤ b) : a * a ≤ b * b :=
  (le_total 0 a).elim (mul_self_le_mul_self · h₁) fun h ↦
    (neg_mul_neg a a).symm.trans_le <|
      mul_le_mul h₂ h₂ (neg_nonneg.2 h) <| (neg_nonneg.2 h).trans h₂

Squared Inequality Under Boundedness: $a \leq b$ and $-a \leq b$ implies $a^2 \leq b^2$

Informal description

Let $R$ be an ordered ring where: 1. Right multiplication by nonnegative elements is monotone (`MulPosMono`), 2. Left multiplication by nonnegative elements is monotone (`PosMulMono`), 3. Addition is monotone (`AddLeftMono`). For any elements $a, b \in R$ such that $a \leq b$ and $-a \leq b$, we have $a^2 \leq b^2$.

Mathlib.Algebra.Order.Ring.Unbundled.Basic

Typeclasses found in `Algebra.Order.Ring.Defs`

Hierarchy

Generality

Typeclasses found in Algebra.Order.Ring.Defs

Hierarchy

Generality

Typeclasses found in `Algebra.Order.Ring.Defs`