doc-next-gen

Mathlib.Algebra.Order.Group.Unbundled.Abs

Module docstring

{"# Absolute values in ordered groups

The absolute value of an element in a group which is also a lattice is its supremum with its negation. This generalizes the usual absolute value on real numbers (|x| = max x (-x)).

Notations

  • |a|: The absolute value of an element a of an additive lattice ordered group
  • |a|ₘ: The absolute value of an element a of a multiplicative lattice ordered group "}
mabs definition
(a : α) : α
Full source 
/-- `mabs a`, denoted `|a|ₘ`, is the absolute value of `a`. -/
@[to_additive "`abs a`, denoted `|a|`, is the absolute value of `a`"]
def mabs (a : α) : α := a ⊔ a⁻¹
Multiplicative absolute value
Informal description
The multiplicative absolute value of an element \( a \) in a multiplicative lattice ordered group is defined as the supremum of \( a \) and its multiplicative inverse \( a^{-1} \), denoted \( |a|_m \).
mabs.unexpander definition
: Lean.PrettyPrinter.Unexpander
Full source 
/-- Unexpander for the notation `|a|ₘ` for `mabs a`.
Tries to add discretionary parentheses in unparsable cases. -/
@[app_unexpander abs]
def mabs.unexpander : Lean.PrettyPrinter.Unexpander
  | `($_ $a) =>
    match a with
    | `(|$_|ₘ) | `(-$_) => `(|($a)|ₘ)
    | _ => `(|$a|ₘ)
  | _ => throw ()
Unexpander for multiplicative absolute value notation
Informal description
The unexpander for the notation `|a|ₘ` (representing the multiplicative absolute value of `a`) adds discretionary parentheses in cases where the expression would otherwise be unparsable. Specifically, it handles patterns like `|a|ₘ` and `-a` by ensuring proper parenthesization when needed.
abs.unexpander definition
: Lean.PrettyPrinter.Unexpander
Full source 
/-- Unexpander for the notation `|a|` for `abs a`.
Tries to add discretionary parentheses in unparsable cases. -/
@[app_unexpander abs]
def abs.unexpander : Lean.PrettyPrinter.Unexpander
  | `($_ $a) =>
    match a with
    | `(|$_|) | `(-$_) => `(|($a)|)
    | _ => `(|$a|)
  | _ => throw ()
Unexpander for absolute value notation
Informal description
The unexpander for the notation `|a|` (absolute value of `a`) adds discretionary parentheses in cases where the expression would otherwise be unparsable. Specifically, it wraps the argument in parentheses when it is already an absolute value or a negation.
mabs_le' theorem
: |a|ₘ ≤ b ↔ a ≤ b ∧ a⁻¹ ≤ b
Full source 
@[to_additive] lemma mabs_le' : |a|ₘ|a|ₘ ≤ b ↔ a ≤ b ∧ a⁻¹ ≤ b := sup_le_iff
Multiplicative Absolute Value Bound: $|a|_m \leq b \leftrightarrow (a \leq b \land a^{-1} \leq b)$
Informal description
For any element $a$ in a multiplicative lattice ordered group and any element $b$, the multiplicative absolute value $|a|_m$ is less than or equal to $b$ if and only if both $a \leq b$ and $a^{-1} \leq b$.
le_mabs_self theorem
(a : α) : a ≤ |a|ₘ
Full source 
@[to_additive] lemma le_mabs_self (a : α) : a ≤ |a|ₘ := le_sup_left
Element is Bounded by its Multiplicative Absolute Value: $a \leq |a|_m$
Informal description
For any element $a$ in a multiplicative lattice ordered group, $a$ is less than or equal to its multiplicative absolute value $|a|_m$.
inv_le_mabs theorem
(a : α) : a⁻¹ ≤ |a|ₘ
Full source 
@[to_additive] lemma inv_le_mabs (a : α) : a⁻¹ ≤ |a|ₘ := le_sup_right
Inverse is Bounded by Multiplicative Absolute Value
Informal description
For any element $a$ in a multiplicative lattice ordered group, the multiplicative inverse $a^{-1}$ is less than or equal to the multiplicative absolute value $|a|_m$.
mabs_le_mabs theorem
(h₀ : a ≤ b) (h₁ : a⁻¹ ≤ b) : |a|ₘ ≤ |b|ₘ
Full source 
@[to_additive] lemma mabs_le_mabs (h₀ : a ≤ b) (h₁ : a⁻¹ ≤ b) : |a|ₘ ≤ |b|ₘ :=
  (mabs_le'.2 ⟨h₀, h₁⟩).trans (le_mabs_self b)
Monotonicity of Multiplicative Absolute Value: $a \leq b \land a^{-1} \leq b \implies |a|_m \leq |b|_m$
Informal description
For any elements $a$ and $b$ in a multiplicative lattice ordered group, if $a \leq b$ and $a^{-1} \leq b$, then the multiplicative absolute value of $a$ is less than or equal to the multiplicative absolute value of $b$, i.e., $|a|_m \leq |b|_m$.
mabs_inv theorem
(a : α) : |a⁻¹|ₘ = |a|ₘ
Full source 
@[to_additive (attr := simp)] lemma mabs_inv (a : α) : |a⁻¹|ₘ = |a|ₘ := by simp [mabs, sup_comm]
Multiplicative Absolute Value of Inverse Equals Absolute Value
Informal description
For any element $a$ in a multiplicative lattice ordered group, the multiplicative absolute value of its inverse equals the multiplicative absolute value of $a$, i.e., $|a^{-1}|_m = |a|_m$.
mabs_div_comm theorem
(a b : α) : |a / b|ₘ = |b / a|ₘ
Full source 
@[to_additive] lemma mabs_div_comm (a b : α) : |a / b|ₘ = |b / a|ₘ := by rw [← mabs_inv, inv_div]
Multiplicative Absolute Value of Quotient is Commutative: $|a / b|_m = |b / a|_m$
Informal description
For any elements $a$ and $b$ in a multiplicative lattice ordered group, the multiplicative absolute value of the quotient $a / b$ equals the multiplicative absolute value of the reverse quotient $b / a$, i.e., $|a / b|_m = |b / a|_m$.
mabs_ite theorem
(p : Prop) [Decidable p] : |if p then a else b|ₘ = if p then |a|ₘ else |b|ₘ
Full source 
@[to_additive] lemma mabs_ite (p : Prop) [Decidable p] :
    |if p then a else b|ₘ = if p then |a|ₘ else |b|ₘ :=
  apply_ite _ _ _ _
Multiplicative Absolute Value Preserves Conditional Expression
Informal description
For any proposition $p$ with a decidability instance, and for any elements $a$ and $b$ in a multiplicative lattice ordered group, the multiplicative absolute value of the term $\text{if } p \text{ then } a \text{ else } b$ equals $\text{if } p \text{ then } |a|_m \text{ else } |b|_m$.
mabs_dite theorem
(p : Prop) [Decidable p] (a : p → α) (b : ¬p → α) : |if h : p then a h else b h|ₘ = if h : p then |a h|ₘ else |b h|ₘ
Full source 
@[to_additive] lemma mabs_dite (p : Prop) [Decidable p] (a : p → α) (b : ¬p → α) :
    |if h : p then a h else b h|ₘ = if h : p then |a h|ₘ else |b h|ₘ :=
  apply_dite _ _ _ _
Multiplicative Absolute Value of Dependent Conditional Expression
Informal description
For any proposition $p$ with a decidability instance, and for any functions $a : p \to \alpha$ and $b : \neg p \to \alpha$ in a multiplicative lattice ordered group, the multiplicative absolute value of the term $\text{if } h : p \text{ then } a(h) \text{ else } b(h)$ equals $\text{if } h : p \text{ then } |a(h)|_m \text{ else } |b(h)|_m$.
mabs_of_one_le theorem
(h : 1 ≤ a) : |a|ₘ = a
Full source 
@[to_additive] lemma mabs_of_one_le (h : 1 ≤ a) : |a|ₘ = a :=
  sup_eq_left.2 <| (inv_le_one'.2 h).trans h
Multiplicative Absolute Value of Elements Greater Than or Equal to One
Informal description
For any element $a$ in a multiplicative lattice ordered group, if $1 \leq a$, then the multiplicative absolute value of $a$ equals $a$ itself, i.e., $|a|_m = a$.
mabs_of_one_lt theorem
(h : 1 < a) : |a|ₘ = a
Full source 
@[to_additive] lemma mabs_of_one_lt (h : 1 < a) : |a|ₘ = a := mabs_of_one_le h.le
Multiplicative Absolute Value of Elements Greater Than One
Informal description
For any element $a$ in a multiplicative lattice ordered group, if $1 < a$, then the multiplicative absolute value of $a$ equals $a$ itself, i.e., $|a|_m = a$.
mabs_of_le_one theorem
(h : a ≤ 1) : |a|ₘ = a⁻¹
Full source 
@[to_additive] lemma mabs_of_le_one (h : a ≤ 1) : |a|ₘ = a⁻¹ :=
  sup_eq_right.2 <| h.trans (one_le_inv'.2 h)
Multiplicative Absolute Value of Elements Less Than or Equal to One
Informal description
For any element $a$ in a multiplicative lattice ordered group, if $a \leq 1$, then the multiplicative absolute value of $a$ equals its multiplicative inverse, i.e., $|a|_m = a^{-1}$.
mabs_of_lt_one theorem
(h : a < 1) : |a|ₘ = a⁻¹
Full source 
@[to_additive] lemma mabs_of_lt_one (h : a < 1) : |a|ₘ = a⁻¹ := mabs_of_le_one h.le
Multiplicative Absolute Value for Elements Below One: $|a|_m = a^{-1}$ when $a < 1$
Informal description
For any element $a$ in a multiplicative lattice ordered group, if $a < 1$, then the multiplicative absolute value of $a$ equals its multiplicative inverse, i.e., $|a|_m = a^{-1}$.
mabs_le_mabs_of_one_le theorem
(ha : 1 ≤ a) (hab : a ≤ b) : |a|ₘ ≤ |b|ₘ
Full source 
@[to_additive] lemma mabs_le_mabs_of_one_le (ha : 1 ≤ a) (hab : a ≤ b) : |a|ₘ ≤ |b|ₘ := by
  rwa [mabs_of_one_le ha, mabs_of_one_le (ha.trans hab)]
Monotonicity of Multiplicative Absolute Value for Elements Greater Than or Equal to One: $1 \leq a \leq b \Rightarrow |a|_m \leq |b|_m$
Informal description
For any elements $a$ and $b$ in a multiplicative lattice ordered group, if $1 \leq a$ and $a \leq b$, then the multiplicative absolute value of $a$ is less than or equal to the multiplicative absolute value of $b$, i.e., $|a|_m \leq |b|_m$.
mabs_one theorem
: |(1 : α)|ₘ = 1
Full source 
@[to_additive (attr := simp)] lemma mabs_one : |(1 : α)|ₘ = 1 := mabs_of_one_le le_rfl
Multiplicative Absolute Value of Identity: $|1|_m = 1$
Informal description
The multiplicative absolute value of the multiplicative identity element $1$ in a multiplicative lattice ordered group $\alpha$ is equal to $1$ itself, i.e., $|1|_m = 1$.
one_le_mabs theorem
(a : α) : 1 ≤ |a|ₘ
Full source 
@[to_additive (attr := simp) abs_nonneg] lemma one_le_mabs (a : α) : 1 ≤ |a|ₘ := by
  apply pow_two_semiclosed _
  rw [mabs, pow_two, mul_sup,  sup_mul, ← pow_two, inv_mul_cancel, sup_comm, ← sup_assoc]
  apply le_sup_right
Multiplicative Absolute Value Bounds: $1 \leq |a|_m$
Informal description
For any element $a$ in a multiplicative lattice ordered group, the multiplicative absolute value $|a|_m$ is greater than or equal to the multiplicative identity $1$.
mabs_mabs theorem
(a : α) : |(|a|ₘ)|ₘ = |a|ₘ
Full source 
@[to_additive (attr := simp)] lemma mabs_mabs (a : α) : |(|a|ₘ)|ₘ = |a|ₘ :=
  mabs_of_one_le <| one_le_mabs a
Idempotence of Multiplicative Absolute Value: $||a|_m|_m = |a|_m$
Informal description
For any element $a$ in a multiplicative lattice ordered group, the multiplicative absolute value of the multiplicative absolute value of $a$ equals the multiplicative absolute value of $a$, i.e., $||a|_m|_m = |a|_m$.
mabs_mul_le theorem
(a b : α) : |a * b|ₘ ≤ |a|ₘ * |b|ₘ
Full source 
/-- The absolute value satisfies the triangle inequality. -/
@[to_additive "The absolute value satisfies the triangle inequality."]
lemma mabs_mul_le (a b : α) : |a * b|ₘ ≤ |a|ₘ * |b|ₘ := by
  apply sup_le
  · exact mul_le_mul' (le_mabs_self a) (le_mabs_self b)
  · rw [mul_inv]
    exact mul_le_mul' (inv_le_mabs _) (inv_le_mabs _)
Triangle Inequality for Multiplicative Absolute Value: $|ab|_m \leq |a|_m |b|_m$
Informal description
For any elements $a$ and $b$ in a multiplicative lattice ordered group, the multiplicative absolute value of their product satisfies the inequality $|a \cdot b|_m \leq |a|_m \cdot |b|_m$.
mabs_mabs_div_mabs_le theorem
(a b : α) : |(|a|ₘ / |b|ₘ)|ₘ ≤ |a / b|ₘ
Full source 
@[to_additive]
lemma mabs_mabs_div_mabs_le (a b : α) : |(|a|ₘ / |b|ₘ)|ₘ ≤ |a / b|ₘ := by
  rw [mabs, sup_le_iff]
  constructor
  · apply div_le_iff_le_mul.2
    convert mabs_mul_le (a / b) b
    rw [div_mul_cancel]
  · rw [div_eq_mul_inv, mul_inv_rev, inv_inv, mul_inv_le_iff_le_mul, mabs_div_comm]
    convert mabs_mul_le (b / a) a
    · rw [div_mul_cancel]
Multiplicative Absolute Value Quotient Inequality: $\left|\frac{|a|_m}{|b|_m}\right|_m \leq \left|\frac{a}{b}\right|_m$
Informal description
For any elements $a$ and $b$ in a multiplicative lattice ordered group, 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., $$ \left|\frac{|a|_m}{|b|_m}\right|_m \leq \left|\frac{a}{b}\right|_m. $$
sup_div_inf_eq_mabs_div theorem
(a b : α) : (a ⊔ b) / (a ⊓ b) = |b / a|ₘ
Full source 
@[to_additive] lemma sup_div_inf_eq_mabs_div (a b : α) : (a ⊔ b) / (a ⊓ b) = |b / a|ₘ := by
  simp_rw [sup_div, div_inf, div_self', sup_comm, sup_sup_sup_comm, sup_idem]
  rw [← inv_div, sup_comm (b := _ / _), ← mabs, sup_eq_left]
  exact one_le_mabs _
Supremum-Infimum Quotient Equals Multiplicative Absolute Value of Reverse Quotient
Informal description
For any elements $a$ and $b$ in a multiplicative lattice ordered group, the quotient of their supremum and infimum equals the multiplicative absolute value of the quotient $b/a$, i.e., $$ \frac{a \sqcup b}{a \sqcap b} = \left|\frac{b}{a}\right|_m. $$
sup_sq_eq_mul_mul_mabs_div theorem
(a b : α) : (a ⊔ b) ^ 2 = a * b * |b / a|ₘ
Full source 
@[to_additive two_nsmul_sup_eq_add_add_abs_sub]
lemma sup_sq_eq_mul_mul_mabs_div (a b : α) : (a ⊔ b) ^ 2 = a * b * |b / a|ₘ := by
  rw [← inf_mul_sup a b, ← sup_div_inf_eq_mabs_div, div_eq_mul_inv, ← mul_assoc, mul_comm,
     mul_assoc, ← pow_two, inv_mul_cancel_left]
Square of Supremum Equals Product Times Multiplicative Absolute Value of Quotient
Informal description
For any elements $a$ and $b$ in a multiplicative lattice ordered group, the square of their supremum equals the product of $a$ and $b$ multiplied by the multiplicative absolute value of the quotient $b/a$, i.e., $$ (a \sqcup b)^2 = a \cdot b \cdot \left|\frac{b}{a}\right|_m. $$
inf_sq_eq_mul_div_mabs_div theorem
(a b : α) : (a ⊓ b) ^ 2 = a * b / |b / a|ₘ
Full source 
@[to_additive two_nsmul_inf_eq_add_sub_abs_sub]
lemma inf_sq_eq_mul_div_mabs_div (a b : α) : (a ⊓ b) ^ 2 = a * b / |b / a|ₘ := by
  rw [← inf_mul_sup a b, ← sup_div_inf_eq_mabs_div, div_eq_mul_inv, div_eq_mul_inv, mul_inv_rev,
    inv_inv, mul_assoc, mul_inv_cancel_comm_assoc, ← pow_two]
Square of Infimum Equals Product Divided by Multiplicative Absolute Value of Quotient
Informal description
For any elements $a$ and $b$ in a multiplicative lattice ordered group, the square of their infimum equals the product of $a$ and $b$ divided by the multiplicative absolute value of the quotient $b/a$, i.e., $$ (a \sqcap b)^2 = \frac{a \cdot b}{\left|\frac{b}{a}\right|_m}. $$
mabs_div_sup_mul_mabs_div_inf theorem
(a b c : α) : |(a ⊔ c) / (b ⊔ c)|ₘ * |(a ⊓ c) / (b ⊓ c)|ₘ = |a / b|ₘ
Full source 
@[to_additive]
lemma mabs_div_sup_mul_mabs_div_inf (a b c : α) :
    |(a ⊔ c) / (b ⊔ c)|ₘ * |(a ⊓ c) / (b ⊓ c)|ₘ = |a / b|ₘ := by
  letI : DistribLattice α := CommGroup.toDistribLattice α
  calc
    |(a ⊔ c) / (b ⊔ c)|ₘ * |(a ⊓ c) / (b ⊓ c)|ₘ =
        (b ⊔ cb ⊔ c ⊔ (a ⊔ c)) / ((b ⊔ c) ⊓ (a ⊔ c)) * |(a ⊓ c) / (b ⊓ c)|ₘ := by
        rw [sup_div_inf_eq_mabs_div]
    _ = (b ⊔ cb ⊔ c ⊔ (a ⊔ c)) / ((b ⊔ c) ⊓ (a ⊔ c)) * ((b ⊓ cb ⊓ c ⊔ a ⊓ c) / (b ⊓ cb ⊓ c ⊓ (a ⊓ c))) := by
        rw [sup_div_inf_eq_mabs_div (b ⊓ c) (a ⊓ c)]
    _ = (b ⊔ ab ⊔ a ⊔ c) / (b ⊓ ab ⊓ a ⊔ c) * (((b ⊔ a) ⊓ c) / (b ⊓ ab ⊓ a ⊓ c)) := by
        rw [← sup_inf_right, ← inf_sup_right, sup_assoc, sup_comm c (a ⊔ c), sup_right_idem,
          sup_assoc, inf_assoc, inf_comm c (a ⊓ c), inf_right_idem, inf_assoc]
    _ = (b ⊔ ab ⊔ a ⊔ c) * ((b ⊔ a) ⊓ c) / ((b ⊓ ab ⊓ a ⊔ c) * (b ⊓ ab ⊓ a ⊓ c)) := by rw [div_mul_div_comm]
    _ = (b ⊔ a) * c / ((b ⊓ a) * c) := by
        rw [mul_comm, inf_mul_sup, mul_comm (b ⊓ ab ⊓ a ⊔ c), inf_mul_sup]
    _ = (b ⊔ a) / (b ⊓ a) := by
        rw [div_eq_mul_inv, mul_inv_rev, mul_assoc, mul_inv_cancel_left, ← div_eq_mul_inv]
    _ = |a / b|ₘ := by rw [sup_div_inf_eq_mabs_div]
Product of Multiplicative Absolute Values of Supremum and Infimum Quotients Equals Multiplicative Absolute Value of Original Quotient
Informal description
For any elements $a$, $b$, and $c$ in a multiplicative lattice ordered group, the product of the multiplicative absolute values of the quotients $(a \sqcup c)/(b \sqcup c)$ and $(a \sqcap c)/(b \sqcap c)$ equals the multiplicative absolute value of the quotient $a/b$, i.e., \[ \left|\frac{a \sqcup c}{b \sqcup c}\right|_m \cdot \left|\frac{a \sqcap c}{b \sqcap c}\right|_m = \left|\frac{a}{b}\right|_m. \]
mabs_sup_div_sup_le_mabs theorem
(a b c : α) : |(a ⊔ c) / (b ⊔ c)|ₘ ≤ |a / b|ₘ
Full source 
@[to_additive] lemma mabs_sup_div_sup_le_mabs (a b c : α) : |(a ⊔ c) / (b ⊔ c)|ₘ ≤ |a / b|ₘ := by
  apply le_of_mul_le_of_one_le_left _ (one_le_mabs _); rw [mabs_div_sup_mul_mabs_div_inf]
Inequality for Multiplicative Absolute Value of Supremum Quotient: $\left|\frac{a \sqcup c}{b \sqcup c}\right|_m \leq \left|\frac{a}{b}\right|_m$
Informal description
For any elements $a$, $b$, and $c$ in a multiplicative lattice ordered group, the multiplicative absolute value of the quotient $(a \sqcup c)/(b \sqcup c)$ is less than or equal to the multiplicative absolute value of the quotient $a/b$, i.e., \[ \left|\frac{a \sqcup c}{b \sqcup c}\right|_m \leq \left|\frac{a}{b}\right|_m. \]
mabs_inf_div_inf_le_mabs theorem
(a b c : α) : |(a ⊓ c) / (b ⊓ c)|ₘ ≤ |a / b|ₘ
Full source 
@[to_additive] lemma mabs_inf_div_inf_le_mabs (a b c : α) : |(a ⊓ c) / (b ⊓ c)|ₘ ≤ |a / b|ₘ := by
  apply le_of_mul_le_of_one_le_right _ (one_le_mabs _); rw [mabs_div_sup_mul_mabs_div_inf]
Multiplicative Absolute Value Inequality for Infimum Quotients: $\left|\frac{a \sqcap c}{b \sqcap c}\right|_m \leq \left|\frac{a}{b}\right|_m$
Informal description
For any elements $a$, $b$, and $c$ in a multiplicative lattice ordered group, the multiplicative absolute value of the quotient $(a \sqcap c)/(b \sqcap c)$ is less than or equal to the multiplicative absolute value of the quotient $a/b$, i.e., \[ \left|\frac{a \sqcap c}{b \sqcap c}\right|_m \leq \left|\frac{a}{b}\right|_m. \]
m_Birkhoff_inequalities theorem
(a b c : α) : |(a ⊔ c) / (b ⊔ c)|ₘ ⊔ |(a ⊓ c) / (b ⊓ c)|ₘ ≤ |a / b|ₘ
Full source 
@[to_additive Birkhoff_inequalities]
lemma m_Birkhoff_inequalities (a b c : α) :
    |(a ⊔ c) / (b ⊔ c)|ₘ|(a ⊔ c) / (b ⊔ c)|ₘ ⊔ |(a ⊓ c) / (b ⊓ c)|ₘ ≤ |a / b|ₘ :=
  sup_le (mabs_sup_div_sup_le_mabs a b c) (mabs_inf_div_inf_le_mabs a b c)
Birkhoff's Inequality for Multiplicative Absolute Values: $\left|\frac{a \sqcup c}{b \sqcup c}\right|_m \sqcup \left|\frac{a \sqcap c}{b \sqcap c}\right|_m \leq \left|\frac{a}{b}\right|_m$
Informal description
For any elements $a$, $b$, and $c$ in a multiplicative lattice ordered group, the supremum of the multiplicative absolute values of the quotients $(a \sqcup c)/(b \sqcup c)$ and $(a \sqcap c)/(b \sqcap c)$ is less than or equal to the multiplicative absolute value of the quotient $a/b$, i.e., \[ \left|\frac{a \sqcup c}{b \sqcup c}\right|_m \sqcup \left|\frac{a \sqcap c}{b \sqcap c}\right|_m \leq \left|\frac{a}{b}\right|_m. \]
mabs_choice theorem
(x : α) : |x|ₘ = x ∨ |x|ₘ = x⁻¹
Full source 
@[to_additive] lemma mabs_choice (x : α) : |x|ₘ|x|ₘ = x ∨ |x|ₘ = x⁻¹ := max_choice _ _
Multiplicative Absolute Value is Either Element or Its Inverse
Informal description
For any element $x$ in a multiplicative lattice ordered group, the multiplicative absolute value $|x|_m$ is equal to either $x$ or its inverse $x^{-1}$.
le_mabs theorem
: a ≤ |b|ₘ ↔ a ≤ b ∨ a ≤ b⁻¹
Full source 
@[to_additive] lemma le_mabs : a ≤ |b|ₘ ↔ a ≤ b ∨ a ≤ b⁻¹ := le_max_iff
Characterization of Inequality with Multiplicative Absolute Value: $a \leq |b|_m \leftrightarrow a \leq b \lor a \leq b^{-1}$
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 $a \leq b$ or $a \leq b^{-1}$.
mabs_eq_max_inv theorem
: |a|ₘ = max a a⁻¹
Full source 
@[to_additive] lemma mabs_eq_max_inv : |a|ₘ = max a a⁻¹ := rfl
Multiplicative Absolute Value as Maximum of Element and Its Inverse: $|a|_m = \max(a, a^{-1})$
Informal description
For any element $a$ in a multiplicative lattice ordered group, the multiplicative absolute value $|a|_m$ is equal to the maximum of $a$ and its inverse $a^{-1}$.
lt_mabs theorem
: a < |b|ₘ ↔ a < b ∨ a < b⁻¹
Full source 
@[to_additive] lemma lt_mabs : a < |b|ₘ ↔ a < b ∨ a < b⁻¹ := lt_max_iff
Characterization of Strict Inequality with Multiplicative Absolute Value: $a < |b|_m \leftrightarrow a < b \lor a < b^{-1}$
Informal description
For any elements $a$ and $b$ in a multiplicative lattice ordered group, the strict inequality $a < |b|_m$ holds if and only if either $a < b$ or $a < b^{-1}$, where $|b|_m$ denotes the multiplicative absolute value of $b$.
mabs_by_cases theorem
(P : α → Prop) (h1 : P a) (h2 : P a⁻¹) : P |a|ₘ
Full source 
@[to_additive] lemma mabs_by_cases (P : α → Prop) (h1 : P a) (h2 : P a⁻¹) : P |a|ₘ :=
  sup_ind _ _ h1 h2
Case Analysis for Multiplicative Absolute Value
Informal description
Let $\alpha$ be a multiplicative lattice ordered group and $a \in \alpha$. For any predicate $P$ on $\alpha$, if $P(a)$ and $P(a^{-1})$ both hold, then $P(|a|_m)$ holds, where $|a|_m = \max(a, a^{-1})$ is the multiplicative absolute value of $a$.
mabs_eq_mabs theorem
: |a|ₘ = |b|ₘ ↔ a = b ∨ a = b⁻¹
Full source 
@[to_additive] lemma mabs_eq_mabs : |a|ₘ|a|ₘ = |b|ₘ ↔ a = b ∨ a = b⁻¹ := by
  refine ⟨fun h ↦ ?_, by rintro (h | h) <;> simp [h, abs_neg]⟩
  obtain rfl | rfl := eq_or_eq_inv_of_mabs_eq h <;>
    simpa only [inv_eq_iff_eq_inv (a := |b|ₘ), inv_inv, inv_inj, or_comm] using mabs_choice b
Multiplicative Absolute Value Equality Criterion: $|a|_m = |b|_m \leftrightarrow a = b \lor a = b^{-1}$
Informal description
For any elements $a$ and $b$ in a multiplicative lattice ordered group, the multiplicative absolute values $|a|_m$ and $|b|_m$ are equal if and only if $a$ equals $b$ or $a$ equals the inverse of $b$, i.e., $|a|_m = |b|_m \leftrightarrow (a = b \lor a = b^{-1})$.
isSquare_mabs theorem
: IsSquare |a|ₘ ↔ IsSquare a
Full source 
@[to_additive] lemma isSquare_mabs : IsSquareIsSquare |a|ₘ ↔ IsSquare a :=
  mabs_by_cases (IsSquareIsSquare · ↔ _) Iff.rfl isSquare_inv
Square Property of Multiplicative Absolute Value: $|a|_m$ is square iff $a$ is square
Informal description
For any element $a$ in a multiplicative lattice ordered group, the multiplicative absolute value $|a|_m$ is a square if and only if $a$ itself is a square, i.e., $|a|_m$ is a square $\leftrightarrow$ $a$ is a square.
lt_of_mabs_lt theorem
: |a|ₘ < b → a < b
Full source 
@[to_additive] lemma lt_of_mabs_lt : |a|ₘ < b → a < b := (le_mabs_self _).trans_lt
Strict Inequality from Multiplicative Absolute Value: $|a|_m < b \Rightarrow a < b$
Informal description
For any element $a$ in a multiplicative lattice ordered group and any element $b$, if the multiplicative absolute value $|a|_m$ is strictly less than $b$, then $a$ is strictly less than $b$.
one_lt_mabs theorem
: 1 < |a|ₘ ↔ a ≠ 1
Full source 
@[to_additive (attr := simp) abs_pos] lemma one_lt_mabs : 1 < |a|ₘ ↔ a ≠ 1 := by
  obtain ha | rfl | ha := lt_trichotomy a 1
  · simp [mabs_of_lt_one ha, neg_pos, ha.ne, ha]
  · simp
  · simp [mabs_of_one_lt ha, ha, ha.ne']
Characterization of Multiplicative Absolute Value Greater Than One: $1 < |a|_m \leftrightarrow a \neq 1$
Informal description
For any element $a$ in a multiplicative lattice ordered group, the multiplicative absolute value $|a|_m$ is greater than $1$ if and only if $a$ is not equal to $1$, i.e., $1 < |a|_m \leftrightarrow a \neq 1$.
one_lt_mabs_pos_of_one_lt theorem
(h : 1 < a) : 1 < |a|ₘ
Full source 
@[to_additive abs_pos_of_pos] lemma one_lt_mabs_pos_of_one_lt (h : 1 < a) : 1 < |a|ₘ :=
  one_lt_mabs.2 h.ne'
Multiplicative Absolute Value Greater Than One for Elements Greater Than One: $1 < a \Rightarrow 1 < |a|_m$
Informal description
For any element $a$ in a multiplicative lattice ordered group, if $1 < a$, then $1 < |a|_m$, where $|a|_m$ denotes the multiplicative absolute value of $a$.
one_lt_mabs_of_lt_one theorem
(h : a < 1) : 1 < |a|ₘ
Full source 
@[to_additive abs_pos_of_neg] lemma one_lt_mabs_of_lt_one (h : a < 1) : 1 < |a|ₘ :=
  one_lt_mabs.2 h.ne
Multiplicative Absolute Value Greater Than One for Elements Below One: $a < 1 \Rightarrow 1 < |a|_m$
Informal description
For any element $a$ in a multiplicative lattice ordered group, if $a < 1$, then the multiplicative absolute value $|a|_m$ satisfies $1 < |a|_m$.
inv_mabs_le theorem
(a : α) : |a|ₘ⁻¹ ≤ a
Full source 
@[to_additive] lemma inv_mabs_le (a : α) : |a|ₘ|a|ₘ⁻¹ ≤ a := by
  obtain h | h := le_total 1 a
  · simpa [mabs_of_one_le h] using (inv_le_one'.2 h).trans h
  · simp [mabs_of_le_one h]
Inverse of Multiplicative Absolute Value is Lower Bound: $|a|_m^{-1} \leq a$
Informal description
For any element $a$ in a multiplicative lattice ordered group, the multiplicative inverse of its absolute value is less than or equal to $a$, i.e., $|a|_m^{-1} \leq a$.
one_le_mul_mabs theorem
(a : α) : 1 ≤ a * |a|ₘ
Full source 
@[to_additive add_abs_nonneg] lemma one_le_mul_mabs (a : α) : 1 ≤ a * |a|ₘ := by
  rw [← mul_inv_cancel a]; exact mul_le_mul_left' (inv_le_mabs a) _
Product with Absolute Value Bounds Identity: $1 \leq a \cdot |a|_m$
Informal description
For any element $a$ in a multiplicative lattice ordered group, the product of $a$ with its multiplicative absolute value $|a|_m$ is greater than or equal to the identity element $1$, i.e., $1 \leq a \cdot |a|_m$.
inv_mabs_le_inv theorem
(a : α) : |a|ₘ⁻¹ ≤ a⁻¹
Full source 
@[to_additive] lemma inv_mabs_le_inv (a : α) : |a|ₘ|a|ₘ⁻¹ ≤ a⁻¹ := by simpa using inv_mabs_le a⁻¹
Inverse of Multiplicative Absolute Value Bounds Inverse: $|a|_m^{-1} \leq a^{-1}$
Informal description
For any element $a$ in a multiplicative lattice ordered group, the multiplicative inverse of its absolute value is less than or equal to the multiplicative inverse of $a$, i.e., $|a|_m^{-1} \leq a^{-1}$.
mabs_ne_one theorem
: |a|ₘ ≠ 1 ↔ a ≠ 1
Full source 
@[to_additive] lemma mabs_ne_one : |a|ₘ|a|ₘ ≠ 1|a|ₘ ≠ 1 ↔ a ≠ 1 :=
  (one_le_mabs a).gt_iff_ne.symm.trans one_lt_mabs
Characterization of Non-Unit Multiplicative Absolute Value: $|a|_m \neq 1 \leftrightarrow a \neq 1$
Informal description
For any element $a$ in a multiplicative lattice ordered group, the multiplicative absolute value $|a|_m$ is not equal to $1$ if and only if $a$ is not equal to $1$, i.e., $|a|_m \neq 1 \leftrightarrow a \neq 1$.
mabs_eq_one theorem
: |a|ₘ = 1 ↔ a = 1
Full source 
@[to_additive (attr := simp)] lemma mabs_eq_one : |a|ₘ|a|ₘ = 1 ↔ a = 1 := not_iff_not.1 mabs_ne_one
Characterization of Unit Multiplicative Absolute Value: $|a|_m = 1 \leftrightarrow a = 1$
Informal description
For any element $a$ in a multiplicative lattice ordered group, the multiplicative absolute value $|a|_m$ equals $1$ if and only if $a$ equals $1$, i.e., $|a|_m = 1 \leftrightarrow a = 1$.
mabs_le_one theorem
: |a|ₘ ≤ 1 ↔ a = 1
Full source 
@[to_additive (attr := simp) abs_nonpos_iff] lemma mabs_le_one : |a|ₘ|a|ₘ ≤ 1 ↔ a = 1 :=
  (one_le_mabs a).le_iff_eq.trans mabs_eq_one
Characterization of Multiplicative Absolute Value Bounded by One: $|a|_m \leq 1 \leftrightarrow a = 1$
Informal description
For any element $a$ in a multiplicative lattice ordered group, the multiplicative absolute value $|a|_m$ is less than or equal to $1$ if and only if $a$ equals $1$, i.e., $|a|_m \leq 1 \leftrightarrow a = 1$.
mabs_le_mabs_of_le_one theorem
(ha : a ≤ 1) (hab : b ≤ a) : |a|ₘ ≤ |b|ₘ
Full source 
@[to_additive] lemma mabs_le_mabs_of_le_one (ha : a ≤ 1) (hab : b ≤ a) : |a|ₘ ≤ |b|ₘ := by
  rw [mabs_of_le_one ha, mabs_of_le_one (hab.trans ha)]; exact inv_le_inv_iff.mpr hab
Monotonicity of Multiplicative Absolute Value for Elements Below One: $a \leq 1 \land b \leq a \Rightarrow |a|_m \leq |b|_m$
Informal description
For any elements $a$ and $b$ in a multiplicative lattice ordered group, if $a \leq 1$ and $b \leq a$, then the multiplicative absolute value of $a$ is less than or equal to the multiplicative absolute value of $b$, i.e., $|a|_m \leq |b|_m$.
mabs_lt theorem
: |a|ₘ < b ↔ b⁻¹ < a ∧ a < b
Full source 
@[to_additive] lemma mabs_lt : |a|ₘ|a|ₘ < b ↔ b⁻¹ < a ∧ a < b :=
  max_lt_iff.trans <| and_comm.trans <| by rw [inv_lt']
Characterization of Multiplicative Absolute Value Inequality: $|a|_m < b \leftrightarrow b^{-1} < a \land a < b$
Informal description
For an element $a$ in a multiplicative lattice ordered group and an element $b$, the multiplicative absolute value $|a|_m$ is less than $b$ if and only if both $b^{-1} < a$ and $a < b$ hold.
inv_lt_of_mabs_lt theorem
(h : |a|ₘ < b) : b⁻¹ < a
Full source 
@[to_additive] lemma inv_lt_of_mabs_lt (h : |a|ₘ < b) : b⁻¹ < a := (mabs_lt.mp h).1
Inverse Inequality from Multiplicative Absolute Value Bound: $|a|_m < b \Rightarrow b^{-1} < 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 $b$, then the multiplicative inverse of $b$ is less than $a$, i.e., $b^{-1} < a$.
max_div_min_eq_mabs' theorem
(a b : α) : max a b / min a b = |a / b|ₘ
Full source 
@[to_additive] lemma max_div_min_eq_mabs' (a b : α) : max a b / min a b = |a / b|ₘ := by
  rcases le_total a b with ab | ba
  · rw [max_eq_right ab, min_eq_left ab, mabs_of_le_one, inv_div]
    rwa [div_le_one']
  · rw [max_eq_left ba, min_eq_right ba, mabs_of_one_le]
    rwa [one_le_div']
Quotient of Max and Min Equals Multiplicative Absolute Value of Quotient
Informal description
For any elements $a$ and $b$ in a multiplicative lattice ordered group, the quotient of the maximum of $a$ and $b$ by their minimum equals the multiplicative absolute value of the quotient $a/b$, i.e., \[ \frac{\max(a,b)}{\min(a,b)} = \left|\frac{a}{b}\right|_m. \]
max_div_min_eq_mabs theorem
(a b : α) : max a b / min a b = |b / a|ₘ
Full source 
@[to_additive] lemma max_div_min_eq_mabs (a b : α) : max a b / min a b = |b / a|ₘ := by
  rw [mabs_div_comm, max_div_min_eq_mabs']
Quotient of Max and Min Equals Multiplicative Absolute Value of Reverse Quotient: $\frac{\max(a,b)}{\min(a,b)} = \left|\frac{b}{a}\right|_m$
Informal description
For any elements $a$ and $b$ in a multiplicative lattice ordered group, the quotient of the maximum of $a$ and $b$ by their minimum equals the multiplicative absolute value of the quotient $b/a$, i.e., \[ \frac{\max(a,b)}{\min(a,b)} = \left|\frac{b}{a}\right|_m. \]
LatticeOrderedAddCommGroup.IsSolid definition
(s : Set α) : Prop
Full source 
/-- A set `s` in a lattice ordered group is *solid* if for all `x ∈ s` and all `y ∈ α` such that
`|y| ≤ |x|`, then `y ∈ s`. -/
def IsSolid (s : Set α) : Prop := ∀ ⦃x⦄, x ∈ s → ∀ ⦃y⦄, |y| ≤ |x| → y ∈ s
Solid subset in a lattice-ordered additive commutative group
Informal description
A subset $s$ of a lattice-ordered additive commutative group $\alpha$ is called *solid* if for any element $x \in s$ and any element $y \in \alpha$ such that the absolute value $|y|$ is less than or equal to $|x|$, it follows that $y \in s$.
LatticeOrderedAddCommGroup.solidClosure definition
(s : Set α) : Set α
Full source 
/-- The solid closure of a subset `s` is the smallest superset of `s` that is solid. -/
def solidClosure (s : Set α) : Set α := {y | ∃ x ∈ s, |y| ≤ |x|}
Solid closure of a subset in a lattice-ordered additive commutative group
Informal description
The solid closure of a subset $s$ in a lattice-ordered additive commutative group $\alpha$ is the set of all elements $y \in \alpha$ for which there exists an element $x \in s$ such that the absolute value of $y$ is less than or equal to the absolute value of $x$. In other words, it is the smallest solid superset of $s$, where a set is called solid if it contains all elements whose absolute values are bounded by the absolute values of elements in the set.
LatticeOrderedAddCommGroup.isSolid_solidClosure theorem
(s : Set α) : IsSolid (solidClosure s)
Full source 
lemma isSolid_solidClosure (s : Set α) : IsSolid (solidClosure s) :=
  fun _ ⟨y, hy, hxy⟩ _ hzx ↦ ⟨y, hy, hzx.trans hxy⟩
Solidity of the Solid Closure in a Lattice-Ordered Additive Commutative Group
Informal description
For any subset $s$ of a lattice-ordered additive commutative group $\alpha$, the solid closure of $s$ is a solid set. That is, for any $y \in \alpha$ and $x \in \text{solidClosure}(s)$, if $|y| \leq |x|$, then $y \in \text{solidClosure}(s)$.
LatticeOrderedAddCommGroup.solidClosure_min theorem
(hst : s ⊆ t) (ht : IsSolid t) : solidClosure s ⊆ t
Full source 
lemma solidClosure_min (hst : s ⊆ t) (ht : IsSolid t) : solidClosuresolidClosure s ⊆ t :=
  fun _ ⟨_, hy, hxy⟩ ↦ ht (hst hy) hxy
Minimality of Solid Closure: $\text{solidClosure}(s) \subseteq t$ for Solid $t$ Containing $s$
Informal description
Let $\alpha$ be a lattice-ordered additive commutative group, and let $s$ and $t$ be subsets of $\alpha$. If $s \subseteq t$ and $t$ is solid, then the solid closure of $s$ is contained in $t$.
Pi.abs_apply theorem
(f : ∀ i, α i) (i : ι) : |f| i = |f i|
Full source 
@[simp] lemma abs_apply (f : ∀ i, α i) (i : ι) : |f| i = |f i| := rfl
Componentwise Absolute Value in Product Groups: $|f|_i = |f_i|$
Informal description
For any family of elements $f = (f_i)_{i \in \iota}$ in a product of lattice-ordered additive commutative groups, and for any index $i \in \iota$, the $i$-th component of the absolute value of $f$ equals the absolute value of the $i$-th component of $f$, i.e., $|f|_i = |f_i|$.
Pi.abs_def theorem
(f : ∀ i, α i) : |f| = fun i ↦ |f i|
Full source 
lemma abs_def (f : ∀ i, α i) : |f| = fun i ↦ |f i| := rfl
Componentwise Definition of Absolute Value in Product Groups: $|f| = (|f_i|)_{i \in \iota}$
Informal description
For any family of elements $f = (f_i)_{i \in \iota}$ in a product of lattice-ordered additive commutative groups, the absolute value of $f$ is the function that maps each index $i$ to the absolute value of $f_i$, i.e., $|f| = (|f_i|)_{i \in \iota}$.