Mathlib.Algebra.Order.Group.Abs

mabs_pow theorem

(n : ℕ) (a : G) : |a ^ n|ₘ = |a|ₘ ^ n

Full source

@[to_additive] lemma mabs_pow (n : ℕ) (a : G) : |a ^ n|ₘ = |a|ₘ ^ n := by
  obtain ha | ha := le_total a 1
  · rw [mabs_of_le_one ha, ← mabs_inv, ← inv_pow, mabs_of_one_le]
    exact one_le_pow_of_one_le' (one_le_inv'.2 ha) n
  · rw [mabs_of_one_le ha, mabs_of_one_le (one_le_pow_of_one_le' ha n)]

Power of Multiplicative Absolute Value Equals Absolute Value of Power

Informal description

For any natural number $n$ and any element $a$ in a multiplicative lattice ordered group $G$, the multiplicative absolute value of $a^n$ equals the $n$-th power of the multiplicative absolute value of $a$, i.e., $|a^n|_m = |a|_m^n$.

mabs_mul_eq_mul_mabs_iff theorem

(a b : G) : |a * b|ₘ = |a|ₘ * |b|ₘ ↔ 1 ≤ a ∧ 1 ≤ b ∨ a ≤ 1 ∧ b ≤ 1

Full source

@[to_additive] lemma mabs_mul_eq_mul_mabs_iff (a b : G) :
    |a * b|ₘ|a * b|ₘ = |a|ₘ * |b|ₘ ↔ 1 ≤ a ∧ 1 ≤ b ∨ a ≤ 1 ∧ b ≤ 1 := by
  obtain ab | ab := le_total a b
  · exact mabs_mul_eq_mul_mabs_le ab
  · simpa only [mul_comm, and_comm] using mabs_mul_eq_mul_mabs_le ab

Multiplicative Absolute Value Product Identity

Informal description

For any elements $a$ and $b$ in a multiplicative lattice ordered group $G$, the multiplicative absolute value of their product equals the product of their multiplicative absolute values if and only if either both $a$ and $b$ are greater than or equal to the identity element $1$, or both are less than or equal to $1$. In other words: $$|a \cdot b|_m = |a|_m \cdot |b|_m \iff (1 \leq a \land 1 \leq b) \lor (a \leq 1 \land b \leq 1).$$

mabs_le theorem

: |a|ₘ ≤ b ↔ b⁻¹ ≤ a ∧ a ≤ b

Full source

@[to_additive]
theorem mabs_le : |a|ₘ|a|ₘ ≤ b ↔ b⁻¹ ≤ a ∧ a ≤ b := by rw [mabs_le', and_comm, inv_le']

Multiplicative Absolute Value Bound: $|a|_m \leq b \leftrightarrow (b^{-1} \leq a \land a \leq b)$

Informal description

For any elements $a$ and $b$ in a multiplicative lattice ordered group, the multiplicative absolute value $|a|_m$ is less than or equal to $b$ if and only if both $b^{-1} \leq a$ and $a \leq b$ hold.

le_mabs' theorem

: a ≤ |b|ₘ ↔ b ≤ a⁻¹ ∨ a ≤ b

Full source

@[to_additive]
theorem le_mabs' : a ≤ |b|ₘ ↔ b ≤ a⁻¹ ∨ a ≤ b := by rw [le_mabs, or_comm, le_inv']

Characterization of Inequality with Multiplicative Absolute Value: $a \leq |b|_m \leftrightarrow b \leq a^{-1} \lor a \leq b$

Informal description

For any elements $a$ and $b$ in a multiplicative lattice ordered group, the inequality $a \leq |b|_m$ holds if and only if either $b \leq a^{-1}$ or $a \leq b$.

inv_le_of_mabs_le theorem

(h : |a|ₘ ≤ b) : b⁻¹ ≤ a

Full source

@[to_additive]
theorem inv_le_of_mabs_le (h : |a|ₘ ≤ b) : b⁻¹ ≤ a :=
  (mabs_le.mp h).1

Inverse Bound from Multiplicative Absolute Value Inequality: $|a|_m \leq b \Rightarrow b^{-1} \leq a$

Informal description

For any elements $a$ and $b$ in a multiplicative lattice ordered group, if the multiplicative absolute value $|a|_m$ is less than or equal to $b$, then the multiplicative inverse of $b$ is less than or equal to $a$.

le_of_mabs_le theorem

(h : |a|ₘ ≤ b) : a ≤ b

Full source

@[to_additive]
theorem le_of_mabs_le (h : |a|ₘ ≤ b) : a ≤ b :=
  (mabs_le.mp h).2

Upper Bound of Multiplicative Absolute Value Implies Upper Bound of Element

Informal description

For any elements $a$ and $b$ in a multiplicative lattice ordered group, if the multiplicative absolute value $|a|_m$ is less than or equal to $b$, then $a \leq b$.

mabs_mul theorem

(a b : G) : |a * b|ₘ ≤ |a|ₘ * |b|ₘ

Full source

/-- The **triangle inequality** in `LinearOrderedCommGroup`s. -/
@[to_additive "The **triangle inequality** in `LinearOrderedAddCommGroup`s."]
theorem mabs_mul (a b : G) : |a * b|ₘ ≤ |a|ₘ * |b|ₘ := by
  rw [mabs_le, mul_inv]
  constructor <;> gcongr <;> apply_rules [inv_mabs_le, le_mabs_self]

Multiplicative Triangle Inequality: $|ab|_m \leq |a|_m |b|_m$

Informal description

For any elements $a$ and $b$ in a multiplicative lattice ordered group $G$, the multiplicative absolute value of their product satisfies the inequality $|a \cdot b|_m \leq |a|_m \cdot |b|_m$.

mabs_mul' theorem

(a b : G) : |a|ₘ ≤ |b|ₘ * |b * a|ₘ

Full source

@[to_additive]
theorem mabs_mul' (a b : G) : |a|ₘ ≤ |b|ₘ * |b * a|ₘ := by simpa using mabs_mul b⁻¹ (b * a)

Multiplicative Absolute Value Inequality: $|a|_m \leq |b|_m \cdot |b a|_m$

Informal description

For any elements $a$ and $b$ in a multiplicative lattice ordered group $G$, the multiplicative absolute value of $a$ satisfies the inequality $|a|_m \leq |b|_m \cdot |b \cdot a|_m$.

mabs_div theorem

(a b : G) : |a / b|ₘ ≤ |a|ₘ * |b|ₘ

Full source

@[to_additive]
theorem mabs_div (a b : G) : |a / b|ₘ ≤ |a|ₘ * |b|ₘ := by
  rw [div_eq_mul_inv, ← mabs_inv b]
  exact mabs_mul a _

Multiplicative Absolute Value Inequality for Quotients: $|a/b|_m \leq |a|_m |b|_m$

Informal description

For any elements $a$ and $b$ in a multiplicative lattice ordered group $G$, the multiplicative absolute value of their quotient satisfies the inequality $|a / b|_m \leq |a|_m \cdot |b|_m$.

mabs_div_le_iff theorem

: |a / b|ₘ ≤ c ↔ a / b ≤ c ∧ b / a ≤ c

Full source

@[to_additive]
theorem mabs_div_le_iff : |a / b|ₘ|a / b|ₘ ≤ c ↔ a / b ≤ c ∧ b / a ≤ c := by
  rw [mabs_le, inv_le_div_iff_le_mul, div_le_iff_le_mul', and_comm, div_le_iff_le_mul']

Multiplicative Absolute Value of Quotient Bound: $|a/b|_m \leq c \leftrightarrow (a/b \leq c \land b/a \leq c)$

Informal description

For elements $a$, $b$, and $c$ in a multiplicative lattice ordered group, the multiplicative absolute value of the quotient $a/b$ satisfies $|a/b|_m \leq c$ if and only if both $a/b \leq c$ and $b/a \leq c$ hold.

mabs_div_lt_iff theorem

: |a / b|ₘ < c ↔ a / b < c ∧ b / a < c

Full source

@[to_additive]
theorem mabs_div_lt_iff : |a / b|ₘ|a / b|ₘ < c ↔ a / b < c ∧ b / a < c := by
  rw [mabs_lt, inv_lt_div_iff_lt_mul', div_lt_iff_lt_mul', and_comm, div_lt_iff_lt_mul']

Multiplicative Absolute Value of Quotient Inequality: $|a/b|_m < c \leftrightarrow (a/b < c \land b/a < c)$

Informal description

For elements $a$, $b$, and $c$ in a multiplicative lattice ordered group, the multiplicative absolute value of the quotient $a/b$ is less than $c$ if and only if both $a/b < c$ and $b/a < c$ hold.

div_le_of_mabs_div_le_left theorem

(h : |a / b|ₘ ≤ c) : b / c ≤ a

Full source

@[to_additive]
theorem div_le_of_mabs_div_le_left (h : |a / b|ₘ ≤ c) : b / c ≤ a :=
  div_le_comm.1 <| (mabs_div_le_iff.1 h).2

Left Division Inequality from Multiplicative Absolute Value Bound: $|a/b|_m \leq c \implies b/c \leq a$

Informal description

For elements $a$, $b$, and $c$ in a multiplicative lattice ordered group, if the multiplicative absolute value of the quotient $a/b$ satisfies $|a/b|_m \leq c$, then $b/c \leq a$.

div_le_of_mabs_div_le_right theorem

(h : |a / b|ₘ ≤ c) : a / c ≤ b

Full source

@[to_additive]
theorem div_le_of_mabs_div_le_right (h : |a / b|ₘ ≤ c) : a / c ≤ b :=
  div_le_of_mabs_div_le_left (mabs_div_comm a b ▸ h)

Right Division Inequality from Multiplicative Absolute Value Bound: $|a/b|_m \leq c \implies a/c \leq b$

Informal description

For elements $a$, $b$, and $c$ in a multiplicative lattice ordered group, if the multiplicative absolute value of the quotient $a/b$ satisfies $|a/b|_m \leq c$, then $a/c \leq b$.

div_lt_of_mabs_div_lt_left theorem

(h : |a / b|ₘ < c) : b / c < a

Full source

@[to_additive]
theorem div_lt_of_mabs_div_lt_left (h : |a / b|ₘ < c) : b / c < a :=
  div_lt_comm.1 <| (mabs_div_lt_iff.1 h).2

Left Division Inequality from Multiplicative Absolute Value: $|a/b|_m < c \implies b/c < a$

Informal description

For elements $a$, $b$, and $c$ in a multiplicative lattice ordered group, if the multiplicative absolute value of the quotient $a/b$ is less than $c$, then $b/c$ is less than $a$.

div_lt_of_mabs_div_lt_right theorem

(h : |a / b|ₘ < c) : a / c < b

Full source

@[to_additive]
theorem div_lt_of_mabs_div_lt_right (h : |a / b|ₘ < c) : a / c < b :=
  div_lt_of_mabs_div_lt_left (mabs_div_comm a b ▸ h)

Right Division Inequality from Multiplicative Absolute Value: $|a/b|_m < c \implies a/c < b$

Informal description

For elements $a$, $b$, and $c$ in a multiplicative lattice ordered group, if the multiplicative absolute value of the quotient $a/b$ is less than $c$, then $a/c$ is less than $b$.

mabs_div_mabs_le_mabs_div theorem

(a b : G) : |a|ₘ / |b|ₘ ≤ |a / b|ₘ

Full source

@[to_additive]
theorem mabs_div_mabs_le_mabs_div (a b : G) : |a|ₘ / |b|ₘ ≤ |a / b|ₘ :=
  div_le_iff_le_mul.2 <|
    calc
      |a|ₘ = |a / b * b|ₘ := by rw [div_mul_cancel]
      _ ≤ |a / b|ₘ * |b|ₘ := mabs_mul _ _

Quotient of Absolute Values Inequality: $|a|_m / |b|_m \leq |a / b|_m$

Informal description

For any elements $a$ and $b$ in a multiplicative lattice ordered group $G$, the quotient of their multiplicative absolute values is bounded above by the multiplicative absolute value of their quotient, i.e., $|a|_m / |b|_m \leq |a / b|_m$.

mabs_mabs_div_mabs_le_mabs_div theorem

(a b : G) : |(|a|ₘ / |b|ₘ)|ₘ ≤ |a / b|ₘ

Full source

@[to_additive]
theorem mabs_mabs_div_mabs_le_mabs_div (a b : G) : |(|a|ₘ / |b|ₘ)|ₘ ≤ |a / b|ₘ :=
  mabs_div_le_iff.2
    ⟨mabs_div_mabs_le_mabs_div _ _, by rw [mabs_div_comm]; apply mabs_div_mabs_le_mabs_div⟩

Absolute Value Quotient Inequality: $\big||a|_m / |b|_m\big|_m \leq |a / b|_m$

Informal description

For any elements $a$ and $b$ in a multiplicative lattice ordered group $G$, the multiplicative absolute value of the quotient of their multiplicative absolute values is bounded above by the multiplicative absolute value of their quotient, i.e., $\big||a|_m / |b|_m\big|_m \leq |a / b|_m$.

mabs_div_le_of_one_le_of_le theorem

{a b n : G} (one_le_a : 1 ≤ a) (a_le_n : a ≤ n) (one_le_b : 1 ≤ b) (b_le_n : b ≤ n) : |a / b|ₘ ≤ n

Full source

/-- `|a / b|ₘ ≤ n` if `1 ≤ a ≤ n` and `1 ≤ b ≤ n`. -/
@[to_additive "`|a - b| ≤ n` if `0 ≤ a ≤ n` and `0 ≤ b ≤ n`."]
theorem mabs_div_le_of_one_le_of_le {a b n : G} (one_le_a : 1 ≤ a) (a_le_n : a ≤ n)
    (one_le_b : 1 ≤ b) (b_le_n : b ≤ n) : |a / b|ₘ ≤ n := by
  rw [mabs_div_le_iff, div_le_iff_le_mul, div_le_iff_le_mul]
  exact ⟨le_mul_of_le_of_one_le a_le_n one_le_b, le_mul_of_le_of_one_le b_le_n one_le_a⟩

Multiplicative Absolute Value of Quotient Bounded by Common Upper Bound: $|a/b|_m \leq n$ under $1 \leq a, b \leq n$

Informal description

For elements $a$, $b$, and $n$ in a multiplicative lattice ordered group, if $1 \leq a \leq n$ and $1 \leq b \leq n$, then the multiplicative absolute value of the quotient $a / b$ satisfies $|a / b|_m \leq n$.

mabs_div_lt_of_one_le_of_lt theorem

{a b n : G} (one_le_a : 1 ≤ a) (a_lt_n : a < n) (one_le_b : 1 ≤ b) (b_lt_n : b < n) : |a / b|ₘ < n

Full source

/-- `|a - b| < n` if `0 ≤ a < n` and `0 ≤ b < n`. -/
@[to_additive "`|a / b|ₘ < n` if `1 ≤ a < n` and `1 ≤ b < n`."]
theorem mabs_div_lt_of_one_le_of_lt {a b n : G} (one_le_a : 1 ≤ a) (a_lt_n : a < n)
    (one_le_b : 1 ≤ b) (b_lt_n : b < n) : |a / b|ₘ < n := by
  rw [mabs_div_lt_iff, div_lt_iff_lt_mul, div_lt_iff_lt_mul]
  exact ⟨lt_mul_of_lt_of_one_le a_lt_n one_le_b, lt_mul_of_lt_of_one_le b_lt_n one_le_a⟩

Multiplicative Absolute Value of Quotient Bounded by Common Upper Bound: $|a/b|_m < n$ under $1 \leq a, b < n$

Informal description

For elements $a$, $b$, and $n$ in a multiplicative lattice ordered group, if $1 \leq a$ and $a < n$, and $1 \leq b$ and $b < n$, then the multiplicative absolute value of the quotient $a / b$ satisfies $|a / b|_m < n$.

mabs_eq theorem

(hb : 1 ≤ b) : |a|ₘ = b ↔ a = b ∨ a = b⁻¹

Full source

@[to_additive]
theorem mabs_eq (hb : 1 ≤ b) : |a|ₘ|a|ₘ = b ↔ a = b ∨ a = b⁻¹ := by
  refine ⟨eq_or_eq_inv_of_mabs_eq, ?_⟩
  rintro (rfl | rfl) <;> simp only [mabs_inv, mabs_of_one_le hb]

Characterization of Multiplicative Absolute Value: $|a|_m = b \leftrightarrow (a = b \lor a = b^{-1})$

Informal description

For any element $b$ in a multiplicative lattice ordered group with $1 \leq b$, the multiplicative absolute value of an element $a$ equals $b$ if and only if $a$ is equal to $b$ or its inverse $b^{-1}$. That is, $|a|_m = b \leftrightarrow (a = b \lor a = b^{-1})$.

mabs_le_max_mabs_mabs theorem

(hab : a ≤ b) (hbc : b ≤ c) : |b|ₘ ≤ max |a|ₘ |c|ₘ

Full source

@[to_additive]
theorem mabs_le_max_mabs_mabs (hab : a ≤ b) (hbc : b ≤ c) : |b|ₘ ≤ max |a|ₘ |c|ₘ :=
  mabs_le'.2
    ⟨by simp [hbc.trans (le_mabs_self c)], by
      simp [(inv_le_inv_iff.mpr hab).trans (inv_le_mabs a)]⟩

Multiplicative Absolute Value Bounded by Maximum of Extremes: $|b|_m \leq \max(|a|_m, |c|_m)$

Informal description

For any elements $a, b, c$ in a multiplicative lattice ordered group such that $a \leq b$ and $b \leq c$, the multiplicative absolute value of $b$ is less than or equal to the maximum of the multiplicative absolute values of $a$ and $c$, i.e., $|b|_m \leq \max(|a|_m, |c|_m)$.

min_mabs_mabs_le_mabs_max theorem

: min |a|ₘ |b|ₘ ≤ |max a b|ₘ

Full source

@[to_additive]
theorem min_mabs_mabs_le_mabs_max : min |a|ₘ |b|ₘ ≤ |max a b|ₘ :=
  (le_total a b).elim (fun h => (min_le_right _ _).trans_eq <| congr_arg _ (max_eq_right h).symm)
    fun h => (min_le_left _ _).trans_eq <| congr_arg _ (max_eq_left h).symm

Inequality for Minimum of Absolute Values and Absolute Value of Maximum in Multiplicative Lattice Ordered Groups

Informal description

For any elements $a$ and $b$ in a multiplicative lattice ordered group, the minimum of their multiplicative absolute values is less than or equal to the multiplicative absolute value of their maximum, i.e., $\min(|a|_m, |b|_m) \leq |\max(a, b)|_m$.

min_mabs_mabs_le_mabs_min theorem

: min |a|ₘ |b|ₘ ≤ |min a b|ₘ

Full source

@[to_additive]
theorem min_mabs_mabs_le_mabs_min : min |a|ₘ |b|ₘ ≤ |min a b|ₘ :=
  (le_total a b).elim (fun h => (min_le_left _ _).trans_eq <| congr_arg _ (min_eq_left h).symm)
    fun h => (min_le_right _ _).trans_eq <| congr_arg _ (min_eq_right h).symm

Inequality for Minimum of Multiplicative Absolute Values

Informal description

For any elements $a$ and $b$ in a multiplicative lattice ordered group, the minimum of their multiplicative absolute values $|a|_m$ and $|b|_m$ is less than or equal to the multiplicative absolute value of their minimum, i.e., $\min(|a|_m, |b|_m) \leq |\min(a, b)|_m$.

mabs_max_le_max_mabs_mabs theorem

: |max a b|ₘ ≤ max |a|ₘ |b|ₘ

Full source

@[to_additive]
theorem mabs_max_le_max_mabs_mabs : |max a b|ₘ ≤ max |a|ₘ |b|ₘ :=
  (le_total a b).elim (fun h => (congr_arg _ <| max_eq_right h).trans_le <| le_max_right _ _)
    fun h => (congr_arg _ <| max_eq_left h).trans_le <| le_max_left _ _

Multiplicative Absolute Value of Maximum is Bounded by Maximum of Absolute Values

Informal description

For any elements $a$ and $b$ in a multiplicative lattice ordered group, the multiplicative absolute value of their maximum satisfies the inequality $|\max(a, b)|_m \leq \max(|a|_m, |b|_m)$.

mabs_min_le_max_mabs_mabs theorem

: |min a b|ₘ ≤ max |a|ₘ |b|ₘ

Full source

@[to_additive]
theorem mabs_min_le_max_mabs_mabs : |min a b|ₘ ≤ max |a|ₘ |b|ₘ :=
  (le_total a b).elim (fun h => (congr_arg _ <| min_eq_left h).trans_le <| le_max_left _ _) fun h =>
    (congr_arg _ <| min_eq_right h).trans_le <| le_max_right _ _

Multiplicative Absolute Value Inequality for Minimum and Maximum

Informal description

For any elements $a$ and $b$ in a multiplicative lattice ordered group, the multiplicative absolute value of their minimum is less than or equal to the maximum of their multiplicative absolute values, i.e., $|\min(a, b)|_m \leq \max(|a|_m, |b|_m)$.

mabs_div_le theorem

(a b c : G) : |a / c|ₘ ≤ |a / b|ₘ * |b / c|ₘ

Full source

@[to_additive]
theorem mabs_div_le (a b c : G) : |a / c|ₘ ≤ |a / b|ₘ * |b / c|ₘ :=
  calc
    |a / c|ₘ = |a / b * (b / c)|ₘ := by rw [div_mul_div_cancel]
    _ ≤ |a / b|ₘ * |b / c|ₘ := mabs_mul _ _

Multiplicative Absolute Value Inequality for Division: $|a/c|_m \leq |a/b|_m \cdot |b/c|_m$

Informal description

For any elements $a, b, c$ in a multiplicative lattice ordered group $G$, the multiplicative absolute value of $a / c$ satisfies the inequality $|a / c|_m \leq |a / b|_m \cdot |b / c|_m$.

mabs_mul_three theorem

(a b c : G) : |a * b * c|ₘ ≤ |a|ₘ * |b|ₘ * |c|ₘ

Full source

@[to_additive]
theorem mabs_mul_three (a b c : G) : |a * b * c|ₘ ≤ |a|ₘ * |b|ₘ * |c|ₘ :=
  (mabs_mul _ _).trans (mul_le_mul_right' (mabs_mul _ _) _)

Multiplicative Triangle Inequality for Three Elements: $|abc|_m \leq |a|_m |b|_m |c|_m$

Informal description

For any elements $a$, $b$, and $c$ in a multiplicative lattice ordered group $G$, the multiplicative absolute value of their product satisfies the inequality $|a \cdot b \cdot c|_m \leq |a|_m \cdot |b|_m \cdot |c|_m$.

mabs_div_le_of_le_of_le theorem

{a b lb ub : G} (hal : lb ≤ a) (hau : a ≤ ub) (hbl : lb ≤ b) (hbu : b ≤ ub) : |a / b|ₘ ≤ ub / lb

Full source

@[to_additive]
theorem mabs_div_le_of_le_of_le {a b lb ub : G} (hal : lb ≤ a) (hau : a ≤ ub) (hbl : lb ≤ b)
    (hbu : b ≤ ub) : |a / b|ₘ ≤ ub / lb :=
  mabs_div_le_iff.2 ⟨div_le_div'' hau hbl, div_le_div'' hbu hal⟩

Bound on Multiplicative Absolute Value of Quotient in Ordered Groups

Informal description

For any elements $a, b, lb, ub$ in a multiplicative lattice ordered group $G$ such that $lb \leq a \leq ub$ and $lb \leq b \leq ub$, the multiplicative absolute value of the quotient $a/b$ satisfies $|a/b|_m \leq ub/lb$.

mabs_div_le_one theorem

: |a / b|ₘ ≤ 1 ↔ a = b

Full source

@[to_additive]
theorem mabs_div_le_one : |a / b|ₘ|a / b|ₘ ≤ 1 ↔ a = b :=
  ⟨eq_of_mabs_div_le_one, by rintro rfl; rw [div_self', mabs_one]⟩

Multiplicative Absolute Value of Quotient Bounded by One iff Elements are Equal

Informal description

For elements $a$ and $b$ in a multiplicative lattice ordered group, the multiplicative absolute value of $a / b$ is less than or equal to $1$ if and only if $a = b$. That is, $|a / b|_m \leq 1 \leftrightarrow a = b$.

mabs_div_pos theorem

: 1 < |a / b|ₘ ↔ a ≠ b

Full source

@[to_additive]
theorem mabs_div_pos : 1 < |a / b|ₘ ↔ a ≠ b :=
  not_le.symm.trans mabs_div_le_one.not

Multiplicative Absolute Value of Quotient Greater Than One iff Elements are Distinct: $1 < |a/b|_m \leftrightarrow a \neq b$

Informal description

For any elements $a$ and $b$ in a multiplicative lattice ordered group, the multiplicative absolute value of $a/b$ is greater than $1$ if and only if $a$ and $b$ are distinct, i.e., $1 < |a/b|_m \leftrightarrow a \neq b$.

mabs_eq_self theorem

: |a|ₘ = a ↔ 1 ≤ a

Full source

@[to_additive (attr := simp)]
theorem mabs_eq_self : |a|ₘ|a|ₘ = a ↔ 1 ≤ a := by
  rw [mabs_eq_max_inv, max_eq_left_iff, inv_le_self_iff]

Multiplicative Absolute Value Equals Element if and Only if Element is Greater Than or Equal to One: $|a|_m = a \leftrightarrow 1 \leq a$

Informal description

For any element $a$ in a multiplicative lattice ordered group, the multiplicative absolute value $|a|_m$ equals $a$ if and only if $1 \leq a$.

mabs_eq_inv_self theorem

: |a|ₘ = a⁻¹ ↔ a ≤ 1

Full source

@[to_additive (attr := simp)]
theorem mabs_eq_inv_self : |a|ₘ|a|ₘ = a⁻¹ ↔ a ≤ 1 := by
  rw [mabs_eq_max_inv, max_eq_right_iff, le_inv_self_iff]

Multiplicative Absolute Value Equals Inverse iff Element is at Most One: $|a|_m = a^{-1} \leftrightarrow a \leq 1$

Informal description

For any element $a$ in a multiplicative lattice ordered group, the multiplicative absolute value $|a|_m$ is equal to the inverse $a^{-1}$ if and only if $a \leq 1$.

mabs_cases theorem

(a : G) : |a|ₘ = a ∧ 1 ≤ a ∨ |a|ₘ = a⁻¹ ∧ a < 1

Full source

/-- For an element `a` of a multiplicative linear ordered group,
either `|a|ₘ = a` and `1 ≤ a`, or `|a|ₘ = a⁻¹` and `a < 1`. -/
@[to_additive
  "For an element `a` of an additive linear ordered group,
  either `|a| = a` and `0 ≤ a`, or `|a| = -a` and `a < 0`.
  Use cases on this lemma to automate linarith in inequalities"]
theorem mabs_cases (a : G) : |a|ₘ|a|ₘ = a ∧ 1 ≤ a|a|ₘ = a ∧ 1 ≤ a ∨ |a|ₘ = a⁻¹ ∧ a < 1 := by
  cases le_or_lt 1 a <;> simp [*, le_of_lt]

Cases for Multiplicative Absolute Value in Ordered Groups

Informal description

For any element $a$ in a multiplicative linearly ordered group, the multiplicative absolute value $|a|_m$ satisfies exactly one of the following: 1. $|a|_m = a$ and $1 \leq a$, or 2. $|a|_m = a^{-1}$ and $a < 1$.

max_one_mul_max_inv_one_eq_mabs_self theorem

(a : G) : max a 1 * max a⁻¹ 1 = |a|ₘ

Full source

@[to_additive (attr := simp)]
theorem max_one_mul_max_inv_one_eq_mabs_self (a : G) : max a 1 * max a⁻¹ 1 = |a|ₘ := by
  symm
  rcases le_total 1 a with (ha | ha) <;> simp [ha]

Product of Maxima Equals Multiplicative Absolute Value

Informal description

For any element $a$ in a multiplicative lattice ordered group $G$, the product of $\max(a, 1)$ and $\max(a^{-1}, 1)$ equals the multiplicative absolute value of $a$, i.e., \[ \max(a, 1) \cdot \max(a^{-1}, 1) = |a|_m. \]

apply_abs_le_mul_of_one_le' theorem

 {H : Type*} [MulOneClass H] [LE H] [MulLeftMono H] [MulRightMono H] {f : G → H} {a : G} (h₁ : 1 ≤ f a)
  (h₂ : 1 ≤ f (-a)) : f |a| ≤ f a * f (-a)

Full source

@[to_additive]
theorem apply_abs_le_mul_of_one_le' {H : Type*} [MulOneClass H] [LE H]
    [MulLeftMono H] [MulRightMono H] {f : G → H}
    {a : G} (h₁ : 1 ≤ f a) (h₂ : 1 ≤ f (-a)) : f |a| ≤ f a * f (-a) :=
  (le_total a 0).rec (fun ha => (abs_of_nonpos ha).symm ▸ le_mul_of_one_le_left' h₁) fun ha =>
    (abs_of_nonneg ha).symm ▸ le_mul_of_one_le_right' h₂

Inequality for Monotone Functions on Absolute Values: $f(|a|) \leq f(a) \cdot f(-a)$ under $1 \leq f(a), f(-a)$

Informal description

Let $H$ be a multiplicative monoid with a partial order, where multiplication is monotone in both arguments. Given a function $f \colon G \to H$ and an element $a \in G$ such that $1 \leq f(a)$ and $1 \leq f(-a)$, then the image of the absolute value of $a$ under $f$ satisfies $f(|a|) \leq f(a) \cdot f(-a)$.

apply_abs_le_mul_of_one_le theorem

 {H : Type*} [MulOneClass H] [LE H] [MulLeftMono H] [MulRightMono H] {f : G → H} (h : ∀ x, 1 ≤ f x) (a : G) :
  f |a| ≤ f a * f (-a)

Full source

@[to_additive]
theorem apply_abs_le_mul_of_one_le {H : Type*} [MulOneClass H] [LE H]
    [MulLeftMono H] [MulRightMono H] {f : G → H}
    (h : ∀ x, 1 ≤ f x) (a : G) : f |a| ≤ f a * f (-a) :=
  apply_abs_le_mul_of_one_le' (h _) (h _)

Inequality for Monotone Functions on Absolute Values: $f(|a|) \leq f(a) \cdot f(-a)$ under $1 \leq f(x)$ for all $x$

Informal description

Let $H$ be a multiplicative monoid with a partial order, where multiplication is monotone in both arguments. Given a function $f \colon G \to H$ such that $1 \leq f(x)$ for all $x \in G$, then for any element $a \in G$, the image of the absolute value of $a$ under $f$ satisfies $f(|a|) \leq f(a) \cdot f(-a)$.

Notations