Mathlib.Algebra.Order.AbsoluteValue.Basic

AbsoluteValue structure

(R S : Type*) [Semiring R] [Semiring S] [PartialOrder S]
    extends R →ₙ* S

Full source

/-- `AbsoluteValue R S` is the type of absolute values on `R` mapping to `S`:
the maps that preserve `*`, are nonnegative, positive definite and satisfy
the triangle inequality. -/
structure AbsoluteValue (R S : Type*) [Semiring R] [Semiring S] [PartialOrder S]
    extends R →ₙ* S where
  /-- The absolute value is nonnegative -/
  nonneg' : ∀ x, 0 ≤ toFun x
  /-- The absolute value is positive definitive -/
  eq_zero' : ∀ x, toFun x = 0 ↔ x = 0
  /-- The absolute value satisfies the triangle inequality -/
  add_le' : ∀ x y, toFun (x + y) ≤ toFun x + toFun y

Absolute Value on Semirings

Informal description

An `AbsoluteValue R S` is a structure representing an absolute value function from a semiring `R` to a partially ordered semiring `S`. It extends the notion of a non-unital multiplicative homomorphism (`R →ₙ* S`) and satisfies the following properties: 1. Nonnegativity: For all `x ∈ R`, the value `f(x) ≥ 0` in `S`. 2. Positive definiteness: `f(x) = 0` if and only if `x = 0`. 3. Triangle inequality: For all `x, y ∈ R`, `f(x + y) ≤ f(x) + f(y)` in `S`. 4. Multiplicativity: For all `x, y ∈ R`, `f(x * y) = f(x) * f(y)` in `S`.

AbsoluteValue.funLike instance

: FunLike (AbsoluteValue R S) R S

Full source

instance funLike : FunLike (AbsoluteValue R S) R S where
  coe f := f.toFun
  coe_injective' f g h := by obtain ⟨⟨_, _⟩, _⟩ := f; obtain ⟨⟨_, _⟩, _⟩ := g; congr

Absolute Values as Function-Like Objects

Informal description

For any semiring $R$ and partially ordered semiring $S$, an absolute value function from $R$ to $S$ can be treated as a function-like object, meaning it can be coerced to a function from $R$ to $S$ in a way that preserves the function application operation.

AbsoluteValue.zeroHomClass instance

: ZeroHomClass (AbsoluteValue R S) R S

Full source

instance zeroHomClass : ZeroHomClass (AbsoluteValue R S) R S where
  map_zero f := (f.eq_zero' _).2 rfl

Absolute Values Preserve Zero

Informal description

For any semiring $R$ and partially ordered semiring $S$, the type of absolute values from $R$ to $S$ forms a `ZeroHomClass`. This means that every absolute value function $f : R \to S$ preserves zero, i.e., $f(0) = 0$.

AbsoluteValue.mulHomClass instance

: MulHomClass (AbsoluteValue R S) R S

Full source

instance mulHomClass : MulHomClass (AbsoluteValue R S) R S :=
  { AbsoluteValue.zeroHomClass (R := R) (S := S) with map_mul := fun f => f.map_mul' }

Absolute Values Preserve Multiplication

Informal description

For any semiring $R$ and partially ordered semiring $S$, the type of absolute values from $R$ to $S$ forms a `MulHomClass`. This means that every absolute value function $f : R \to S$ preserves multiplication, i.e., $f(x * y) = f(x) * f(y)$ for all $x, y \in R$.

AbsoluteValue.nonnegHomClass instance

: NonnegHomClass (AbsoluteValue R S) R S

Full source

instance nonnegHomClass : NonnegHomClass (AbsoluteValue R S) R S :=
  { AbsoluteValue.zeroHomClass (R := R) (S := S) with apply_nonneg := fun f => f.nonneg' }

Nonnegativity of Absolute Values

Informal description

For any semiring $R$ and partially ordered semiring $S$, the type of absolute values from $R$ to $S$ forms a `NonnegHomClass`. This means that every absolute value function $f \colon R \to S$ is nonnegative, i.e., $f(x) \geq 0$ for all $x \in R$.

AbsoluteValue.subadditiveHomClass instance

: SubadditiveHomClass (AbsoluteValue R S) R S

Full source

instance subadditiveHomClass : SubadditiveHomClass (AbsoluteValue R S) R S :=
  { AbsoluteValue.zeroHomClass (R := R) (S := S) with map_add_le_add := fun f => f.add_le' }

Absolute Values are Subadditive Homomorphisms

Informal description

For any semiring $R$ and partially ordered semiring $S$, the type of absolute values from $R$ to $S$ forms a `SubadditiveHomClass`. This means that every absolute value function $f : R \to S$ satisfies the subadditivity property, i.e., $f(x + y) \leq f(x) + f(y)$ for all $x, y \in R$.

AbsoluteValue.coe_mk theorem

(f : R →ₙ* S) {h₁ h₂ h₃} : (AbsoluteValue.mk f h₁ h₂ h₃ : R → S) = f

Full source

@[simp]
theorem coe_mk (f : R →ₙ* S) {h₁ h₂ h₃} : (AbsoluteValue.mk f h₁ h₂ h₃ : R → S) = f :=
  rfl

Underlying Function of Constructed Absolute Value Equals Original Homomorphism

Informal description

For any non-unital multiplicative homomorphism $f \colon R \to S$ and properties $h_1, h_2, h_3$ defining an absolute value, the underlying function of the constructed absolute value $\text{AbsoluteValue.mk}(f, h_1, h_2, h_3)$ is equal to $f$.

AbsoluteValue.ext theorem

⦃f g : AbsoluteValue R S⦄ : (∀ x, f x = g x) → f = g

Full source

@[ext]
theorem ext ⦃f g : AbsoluteValue R S⦄ : (∀ x, f x = g x) → f = g :=
  DFunLike.ext _ _

Extensionality of Absolute Values

Informal description

For any two absolute value functions $f, g \colon R \to S$ from a semiring $R$ to a partially ordered semiring $S$, if $f(x) = g(x)$ for all $x \in R$, then $f = g$.

AbsoluteValue.Simps.apply definition

(f : AbsoluteValue R S) : R → S

Full source

/-- See Note [custom simps projection]. -/
def Simps.apply (f : AbsoluteValue R S) : R → S :=
  f

Underlying map of an absolute value

Informal description

The function that extracts the underlying map from an absolute value structure, which takes an element of the semiring $R$ and returns its absolute value in the partially ordered semiring $S$.

AbsoluteValue.coe_toMulHom theorem

: ⇑abv.toMulHom = abv

Full source

@[simp]
theorem coe_toMulHom : ⇑abv.toMulHom = abv :=
  rfl

Coercion of Absolute Value to Multiplicative Homomorphism Preserves Function

Informal description

For any absolute value function `abv` from a semiring `R` to a partially ordered semiring `S`, the underlying function of the associated multiplicative homomorphism `abv.toMulHom` is equal to `abv` itself. In other words, the coercion of `abv.toMulHom` to a function coincides with `abv`.

AbsoluteValue.nonneg theorem

(x : R) : 0 ≤ abv x

Full source

@[bound]
protected theorem nonneg (x : R) : 0 ≤ abv x :=
  abv.nonneg' x

Nonnegativity of Absolute Values

Informal description

For any absolute value function $abv$ from a semiring $R$ to a partially ordered semiring $S$, and for any element $x \in R$, the value $abv(x)$ is nonnegative, i.e., $0 \leq abv(x)$.

AbsoluteValue.add_le theorem

(x y : R) : abv (x + y) ≤ abv x + abv y

Full source

@[bound]
protected theorem add_le (x y : R) : abv (x + y) ≤ abv x + abv y :=
  abv.add_le' x y

Triangle Inequality for Absolute Values

Informal description

For any absolute value function $abv$ from a semiring $R$ to a partially ordered semiring $S$, and for any elements $x, y \in R$, the triangle inequality holds: \[ abv(x + y) \leq abv(x) + abv(y). \]

AbsoluteValue.listSum_le theorem

[AddLeftMono S] (l : List R) : abv l.sum ≤ (l.map abv).sum

Full source

/-- The triangle inequality for an `AbsoluteValue` applied to a list. -/
lemma listSum_le [AddLeftMono S] (l : List R) : abv l.sum ≤ (l.map abv).sum := by
  induction l with
  | nil => simp
  | cons head tail ih => exact (abv.add_le ..).trans <| add_le_add_left ih (abv head)

Triangle Inequality for Absolute Values on Lists

Informal description

Let $R$ be a semiring and $S$ be a partially ordered semiring with the property that addition is monotone on the left (i.e., $a \leq b$ implies $a + c \leq b + c$ for all $a, b, c \in S$). For any absolute value function $\text{abv} : R \to S$ and any list $l$ of elements in $R$, the absolute value of the sum of the list is less than or equal to the sum of the absolute values of its elements: \[ \text{abv}\left(\sum_{x \in l} x\right) \leq \sum_{x \in l} \text{abv}(x). \]

AbsoluteValue.map_mul theorem

(x y : R) : abv (x * y) = abv x * abv y

Full source

@[simp]
protected theorem map_mul (x y : R) : abv (x * y) = abv x * abv y :=
  abv.map_mul' x y

Multiplicativity of Absolute Values: $\text{abv}(xy) = \text{abv}(x)\text{abv}(y)$

Informal description

For any absolute value function $\text{abv} : R \to S$ from a semiring $R$ to a partially ordered semiring $S$, and for any elements $x, y \in R$, the absolute value of the product $x \cdot y$ equals the product of the absolute values: \[ \text{abv}(x \cdot y) = \text{abv}(x) \cdot \text{abv}(y). \]

AbsoluteValue.ne_zero_iff theorem

{x : R} : abv x ≠ 0 ↔ x ≠ 0

Full source

protected theorem ne_zero_iff {x : R} : abv x ≠ 0abv x ≠ 0 ↔ x ≠ 0 :=
  abv.eq_zero.not

Nonzero Absolute Value iff Nonzero Element

Informal description

For any element $x$ in a semiring $R$ and an absolute value function $\text{abv} : R \to S$ where $S$ is a partially ordered semiring, the value $\text{abv}(x)$ is nonzero if and only if $x$ is nonzero.

AbsoluteValue.pos_iff theorem

{x : R} : 0 < abv x ↔ x ≠ 0

Full source

@[simp]
protected theorem pos_iff {x : R} : 0 < abv x ↔ x ≠ 0 :=
  (abv.nonneg x).gt_iff_ne.trans abv.ne_zero_iff

Positivity of Absolute Values: $0 < \text{abv}(x) \leftrightarrow x \neq 0$

Informal description

For any element $x$ in a semiring $R$ and an absolute value function $\text{abv} : R \to S$ where $S$ is a partially ordered semiring, the value $\text{abv}(x)$ is strictly positive if and only if $x$ is nonzero, i.e., \[ 0 < \text{abv}(x) \leftrightarrow x \neq 0. \]

AbsoluteValue.map_one_of_isLeftRegular theorem

(h : IsLeftRegular (abv 1)) : abv 1 = 1

Full source

theorem map_one_of_isLeftRegular (h : IsLeftRegular (abv 1)) : abv 1 = 1 :=
  h <| by simp [← abv.map_mul]

Absolute Value of One Equals One under Left Regularity Condition

Informal description

For any absolute value function $\text{abv} : R \to S$ from a semiring $R$ to a partially ordered semiring $S$, if the value $\text{abv}(1)$ is left regular (i.e., left multiplication by $\text{abv}(1)$ is injective), then $\text{abv}(1) = 1$.

AbsoluteValue.map_zero theorem

: abv 0 = 0

Full source

@[simp]
protected theorem map_zero : abv 0 = 0 :=
  abv.eq_zero.2 rfl

Absolute Value Vanishes at Zero

Informal description

For any absolute value function $abv$ from a semiring $R$ to a partially ordered semiring $S$, the value of $abv$ at $0$ is $0$, i.e., $abv(0) = 0$.

AbsoluteValue.sub_le theorem

(a b c : R) : abv (a - c) ≤ abv (a - b) + abv (b - c)

Full source

protected theorem sub_le (a b c : R) : abv (a - c) ≤ abv (a - b) + abv (b - c) := by
  simpa [sub_eq_add_neg, add_assoc] using abv.add_le (a - b) (b - c)

Triangle Inequality for Differences under Absolute Value

Informal description

For any absolute value function $abv$ from a semiring $R$ to a partially ordered semiring $S$, and for any elements $a, b, c \in R$, the following inequality holds: \[ abv(a - c) \leq abv(a - b) + abv(b - c). \]

AbsoluteValue.map_sub_eq_zero_iff theorem

(a b : R) : abv (a - b) = 0 ↔ a = b

Full source

@[simp high] -- added `high` to apply it before `AbsoluteValue.eq_zero`
theorem map_sub_eq_zero_iff (a b : R) : abv (a - b) = 0 ↔ a = b :=
  abv.eq_zero.trans sub_eq_zero

Absolute Value of Difference Vanishes if and only if Elements are Equal

Informal description

For any elements $a, b$ in a semiring $R$ with an absolute value function $abv$ mapping to a partially ordered semiring $S$, the absolute value of their difference is zero if and only if $a = b$, i.e., $abv(a - b) = 0 \leftrightarrow a = b$.

AbsoluteValue.map_one theorem

: abv 1 = 1

Full source

@[simp]
protected theorem map_one : abv 1 = 1 :=
  abv.map_one_of_isLeftRegular (isRegular_of_ne_zero <| abv.ne_zero one_ne_zero).left

Absolute Value of One: $\text{abv}(1) = 1$

Informal description

For any absolute value function $\text{abv} : R \to S$ from a semiring $R$ to a partially ordered semiring $S$, the value of $\text{abv}$ at the multiplicative identity $1$ is equal to $1$, i.e., $\text{abv}(1) = 1$.

AbsoluteValue.monoidWithZeroHomClass instance

: MonoidWithZeroHomClass (AbsoluteValue R S) R S

Full source

instance monoidWithZeroHomClass : MonoidWithZeroHomClass (AbsoluteValue R S) R S :=
  { AbsoluteValue.mulHomClass with
    map_zero := fun f => f.map_zero
    map_one := fun f => f.map_one }

Absolute Values as Monoid with Zero Homomorphisms

Informal description

For any semiring $R$ and partially ordered semiring $S$, the type of absolute values from $R$ to $S$ forms a `MonoidWithZeroHomClass`. This means that every absolute value function $f : R \to S$ preserves the multiplicative identity, the zero element, and multiplication, i.e., $f(1) = 1$, $f(0) = 0$, and $f(x * y) = f(x) * f(y)$ for all $x, y \in R$.

AbsoluteValue.toMonoidWithZeroHom definition

: R →*₀ S

Full source

/-- Absolute values from a nontrivial `R` to a linear ordered ring preserve `*`, `0` and `1`. -/
def toMonoidWithZeroHom : R →*₀ S :=
  abv

Absolute value as a monoid with zero homomorphism

Informal description

The function converts an absolute value $\text{abv} : R \to S$ from a semiring $R$ to a partially ordered semiring $S$ into a monoid with zero homomorphism from $R$ to $S$, preserving the multiplicative structure, the identity element, and the zero element.

AbsoluteValue.coe_toMonoidWithZeroHom theorem

: ⇑abv.toMonoidWithZeroHom = abv

Full source

@[simp]
theorem coe_toMonoidWithZeroHom : ⇑abv.toMonoidWithZeroHom = abv :=
  rfl

Coercion of Absolute Value to Monoid with Zero Homomorphism Preserves Function

Informal description

For any absolute value function $\text{abv} \colon R \to S$ from a semiring $R$ to a partially ordered semiring $S$, the underlying function of the monoid with zero homomorphism $\text{abv.toMonoidWithZeroHom}$ is equal to $\text{abv}$ itself. In other words, the coercion of $\text{abv.toMonoidWithZeroHom}$ to a function coincides with $\text{abv}$.

AbsoluteValue.toMonoidHom definition

: R →* S

Full source

/-- Absolute values from a nontrivial `R` to a linear ordered ring preserve `*` and `1`. -/
def toMonoidHom : R →* S :=
  abv

Absolute value as a monoid homomorphism

Informal description

The function converts an absolute value `abv` from a semiring `R` to a partially ordered semiring `S` into a monoid homomorphism from `R` to `S`, preserving the multiplicative structure and the identity element.

AbsoluteValue.coe_toMonoidHom theorem

: ⇑abv.toMonoidHom = abv

Full source

@[simp]
theorem coe_toMonoidHom : ⇑abv.toMonoidHom = abv :=
  rfl

Coercion of Absolute Value to Monoid Homomorphism Preserves Function

Informal description

For any absolute value function $\text{abv} \colon R \to S$ from a semiring $R$ to a partially ordered semiring $S$, the underlying function of the monoid homomorphism $\text{abv.toMonoidHom}$ is equal to $\text{abv}$ itself. In other words, the coercion of $\text{abv.toMonoidHom}$ to a function coincides with $\text{abv}$.

AbsoluteValue.map_pow theorem

(a : R) (n : ℕ) : abv (a ^ n) = abv a ^ n

Full source

@[simp]
protected theorem map_pow (a : R) (n : ℕ) : abv (a ^ n) = abv a ^ n :=
  abv.toMonoidHom.map_pow a n

Power Preservation under Absolute Values: $\text{abv}(a^n) = \text{abv}(a)^n$

Informal description

For any absolute value function $\text{abv} \colon R \to S$ from a semiring $R$ to a partially ordered semiring $S$, and for any element $a \in R$ and natural number $n$, the absolute value of $a^n$ equals the $n$-th power of the absolute value of $a$, i.e., \[ \text{abv}(a^n) = (\text{abv}(a))^n. \]

AbsoluteValue.apply_nat_le_self theorem

[IsOrderedRing S] (n : ℕ) : abv n ≤ n

Full source

/-- An absolute value satisfies `f (n : R) ≤ n` for every `n : ℕ`. -/
lemma apply_nat_le_self [IsOrderedRing S] (n : ℕ) : abv n ≤ n := by
  cases subsingleton_or_nontrivial R
  · simp [Subsingleton.eq_zero (n : R)]
  induction n with
  | zero => simp
  | succ n hn =>
    simp only [Nat.cast_succ]
    calc
      abv (n + 1) ≤ abv n + abv 1 := abv.add_le ..
      _ = abv n + 1 := congrArg (abv n + ·) abv.map_one
      _ ≤ n + 1 := add_le_add_right hn 1

Absolute Value Bound on Natural Numbers: $\text{abv}(n) \leq n$

Informal description

For any absolute value function $\text{abv} : R \to S$ from a semiring $R$ to an ordered ring $S$, and for any natural number $n$, the value of $\text{abv}$ at $n$ is less than or equal to $n$, i.e., $\text{abv}(n) \leq n$.

AbsoluteValue.le_sub theorem

(a b : R) : abv a - abv b ≤ abv (a - b)

Full source

@[bound]
protected theorem le_sub (a b : R) : abv a - abv b ≤ abv (a - b) :=
  sub_le_iff_le_add.2 <| by simpa using abv.add_le (a - b) b

Reverse Triangle Inequality for Absolute Values

Informal description

For any absolute value function $abv$ from a semiring $R$ to a partially ordered semiring $S$, and for any elements $a, b \in R$, the following inequality holds: \[ abv(a) - abv(b) \leq abv(a - b). \]

AbsoluteValue.map_neg theorem

(a : R) : abv (-a) = abv a

Full source

@[simp]
protected theorem map_neg (a : R) : abv (-a) = abv a := by
  by_cases ha : a = 0; · simp [ha]
  refine
    (mul_self_eq_mul_self_iff.mp (by rw [← abv.map_mul, neg_mul_neg, abv.map_mul])).resolve_right ?_
  exact ((neg_lt_zero.mpr (abv.pos ha)).trans (abv.pos (neg_ne_zero.mpr ha))).ne'

Absolute Value of Negative Element: $\text{abv}(-a) = \text{abv}(a)$

Informal description

For any absolute value function $\text{abv} : R \to S$ from a semiring $R$ to a partially ordered semiring $S$, and for any element $a \in R$, the absolute value of $-a$ equals the absolute value of $a$, i.e., \[ \text{abv}(-a) = \text{abv}(a). \]

AbsoluteValue.map_sub theorem

(a b : R) : abv (a - b) = abv (b - a)

Full source

protected theorem map_sub (a b : R) : abv (a - b) = abv (b - a) := by rw [← neg_sub, abv.map_neg]

Absolute Value of Difference is Symmetric: $\text{abv}(a - b) = \text{abv}(b - a)$

Informal description

For any absolute value function $\text{abv} : R \to S$ from a semiring $R$ to a partially ordered semiring $S$, and for any elements $a, b \in R$, the absolute value of $a - b$ equals the absolute value of $b - a$, i.e., \[ \text{abv}(a - b) = \text{abv}(b - a). \]

AbsoluteValue.le_add theorem

(a b : R) : abv a - abv b ≤ abv (a + b)

Full source

/-- Bound `abv (a + b)` from below -/
@[bound]
protected theorem le_add (a b : R) : abv a - abv b ≤ abv (a + b) := by
  simpa only [tsub_le_iff_right, add_neg_cancel_right, abv.map_neg] using abv.add_le (a + b) (-b)

Lower Bound for Absolute Value of Sum: $\text{abv}(a) - \text{abv}(b) \leq \text{abv}(a + b)$

Informal description

For any absolute value function $\text{abv} : R \to S$ from a semiring $R$ to a partially ordered semiring $S$, and for any elements $a, b \in R$, the following inequality holds: \[ \text{abv}(a) - \text{abv}(b) \leq \text{abv}(a + b). \]

AbsoluteValue.sub_le_add theorem

(a b : R) : abv (a - b) ≤ abv a + abv b

Full source

/-- Bound `abv (a - b)` from above -/
@[bound]
lemma sub_le_add (a b : R) : abv (a - b) ≤ abv a + abv b := by
  simpa only [← sub_eq_add_neg, AbsoluteValue.map_neg] using abv.add_le a (-b)

Triangle Inequality for Absolute Value of Differences: $\text{abv}(a - b) \leq \text{abv}(a) + \text{abv}(b)$

Informal description

For any absolute value function $\text{abv} : R \to S$ from a semiring $R$ to a partially ordered semiring $S$, and for any elements $a, b \in R$, the following inequality holds: \[ \text{abv}(a - b) \leq \text{abv}(a) + \text{abv}(b). \]

AbsoluteValue.instMulRingNormClassOfNontrivialOfIsDomain instance

[Nontrivial R] [IsDomain S] : MulRingNormClass (AbsoluteValue R S) R S

Full source

instance [Nontrivial R] [IsDomain S] : MulRingNormClass (AbsoluteValue R S) R S :=
  { AbsoluteValue.subadditiveHomClass,
    AbsoluteValue.monoidWithZeroHomClass with
    map_neg_eq_map := fun f => f.map_neg
    eq_zero_of_map_eq_zero := fun f _ => f.eq_zero.1 }

Absolute Values as Multiplicative Ring Norms

Informal description

For any nontrivial semiring $R$ and domain $S$, the type of absolute values from $R$ to $S$ forms a `MulRingNormClass`. This means that every absolute value function $f : R \to S$ satisfies the properties of a multiplicative ring norm, including multiplicativity, subadditivity, and positive definiteness.

AbsoluteValue.apply_natAbs_eq theorem

(x : ℤ) : abv (natAbs x) = abv x

Full source

lemma apply_natAbs_eq (x : ℤ) : abv (natAbs x) = abv x := by
  obtain ⟨_, rfl | rfl⟩ := Int.eq_nat_or_neg x <;> simp

Absolute Value Preserves Integer Absolute Value: $\text{abv}(\text{natAbs}(x)) = \text{abv}(x)$

Informal description

For any absolute value function $\text{abv} : \mathbb{Z} \to S$ from the integers to a partially ordered semiring $S$, and for any integer $x \in \mathbb{Z}$, the absolute value of the natural number obtained by taking the absolute value of $x$ equals the absolute value of $x$ itself, i.e., \[ \text{abv}(\text{natAbs}(x)) = \text{abv}(x). \]

AbsoluteValue.abs definition

: AbsoluteValue S S

Full source

/-- `AbsoluteValue.abs` is `abs` as a bundled `AbsoluteValue`. -/
@[simps]
protected def abs : AbsoluteValue S S where
  toFun := abs
  nonneg' := abs_nonneg
  eq_zero' _ := abs_eq_zero
  add_le' := abs_add
  map_mul' := abs_mul

Standard absolute value as bundled absolute value structure

Informal description

The function `AbsoluteValue.abs` is the standard absolute value function, viewed as an `AbsoluteValue` structure from a semiring `S` to itself. It maps each element $x$ to its absolute value $|x|$ and satisfies the following properties: 1. Nonnegativity: $|x| \geq 0$ for all $x \in S$. 2. Positive definiteness: $|x| = 0$ if and only if $x = 0$. 3. Triangle inequality: $|x + y| \leq |x| + |y|$ for all $x, y \in S$. 4. Multiplicativity: $|x \cdot y| = |x| \cdot |y|$ for all $x, y \in S$.

AbsoluteValue.instInhabited instance

: Inhabited (AbsoluteValue S S)

Full source

instance : Inhabited (AbsoluteValue S S) :=
  ⟨AbsoluteValue.abs⟩

Standard Absolute Value as a Canonical Instance

Informal description

For any semiring $S$, there exists a canonical absolute value structure on $S$ given by the standard absolute value function $x \mapsto |x|$.

AbsoluteValue.abs_abv_sub_le_abv_sub theorem

(a b : R) : abs (abv a - abv b) ≤ abv (a - b)

Full source

@[bound]
theorem abs_abv_sub_le_abv_sub (a b : R) : abs (abv a - abv b) ≤ abv (a - b) :=
  abs_sub_le_iff.2 ⟨abv.le_sub _ _, by rw [abv.map_sub]; apply abv.le_sub⟩

Reverse Triangle Inequality for Absolute Values: $|\text{abv}(a) - \text{abv}(b)| \leq \text{abv}(a - b)$

Informal description

For any absolute value function $\text{abv} : R \to S$ from a semiring $R$ to a partially ordered semiring $S$, and for any elements $a, b \in R$, the following inequality holds: \[ |\text{abv}(a) - \text{abv}(b)| \leq \text{abv}(a - b). \]

AbsoluteValue.trivial definition

: AbsoluteValue R S

Full source

/-- The *trivial* absolute value takes the value `1` on all nonzero elements. -/
protected
def trivial : AbsoluteValue R S where
  toFun x := if x = 0 then 0 else 1
  map_mul' x y := by
    rcases eq_or_ne x 0 with rfl | hx
    · simp
    rcases eq_or_ne y 0 with rfl | hy
    · simp
    simp [hx, hy]
  nonneg' x := by rcases eq_or_ne x 0 with hx | hx <;> simp [hx]
  eq_zero' x := by rcases eq_or_ne x 0 with hx | hx <;> simp [hx]
  add_le' x y := by
    rcases eq_or_ne x 0 with rfl | hx
    · simp
    rcases eq_or_ne y 0 with rfl | hy
    · simp
    simp only [hx, ↓reduceIte, hy, one_add_one_eq_two]
    rcases eq_or_ne (x + y) 0 with hxy | hxy <;> simp [hxy, one_le_two]

Trivial absolute value

Informal description

The trivial absolute value on a semiring $ R $ with values in a partially ordered semiring $ S $ is defined by mapping every nonzero element $ x \in R $ to $ 1 \in S $ and zero to zero. Formally, it is the function $ f \colon R \to S $ given by \[ f(x) = \begin{cases} 0 & \text{if } x = 0, \\ 1 & \text{otherwise.} \end{cases} \] This function satisfies the properties of an absolute value, including nonnegativity, positive definiteness, the triangle inequality, and multiplicativity.

AbsoluteValue.trivial_apply theorem

{x : R} (hx : x ≠ 0) : AbsoluteValue.trivial (S := S) x = 1

Full source

@[simp]
lemma trivial_apply {x : R} (hx : x ≠ 0) : AbsoluteValue.trivial (S := S) x = 1 :=
  if_neg hx

Trivial Absolute Value Maps Nonzero Elements to One

Informal description

For any nonzero element $x$ in a semiring $R$, the trivial absolute value function on $R$ with values in a partially ordered semiring $S$ maps $x$ to $1$, i.e., $\text{trivial}(x) = 1$.

AbsoluteValue.IsNontrivial definition

(v : AbsoluteValue R S) : Prop

Full source

/-- An absolute value on a semiring `R` without zero divisors is *nontrivial* if it takes
a value `≠ 1` on a nonzero element.

This has the advantage over `v ≠ .trivial` that it does not require decidability
of `· = 0` in `R`. -/
def IsNontrivial (v : AbsoluteValue R S) : Prop :=
  ∃ x ≠ 0, v x ≠ 1

Nontrivial absolute value

Informal description

An absolute value $ v $ on a semiring $ R $ is called *nontrivial* if there exists a nonzero element $ x \in R $ such that $ v(x) \neq 1 $.

AbsoluteValue.isNontrivial_iff_ne_trivial theorem

 [DecidablePred fun x : R ↦ x = 0] [NoZeroDivisors R] [Nontrivial S] (v : AbsoluteValue R S) :
  v.IsNontrivial ↔ v ≠ .trivial

Full source

lemma isNontrivial_iff_ne_trivial [DecidablePred fun x : R ↦ x = 0] [NoZeroDivisors R]
    [Nontrivial S] (v : AbsoluteValue R S) :
    v.IsNontrivial ↔ v ≠ .trivial := by
  refine ⟨fun ⟨x, hx₀, hx₁⟩ h ↦ hx₁ <| h.symm ▸ trivial_apply hx₀, fun H ↦ ?_⟩
  simp only [IsNontrivial]
  contrapose! H
  ext1 x
  rcases eq_or_ne x 0 with rfl | hx
  · simp
  · simp [H, hx]

Nontrivial Absolute Value Characterization: $v$ is Nontrivial $\leftrightarrow$ $v \neq \text{trivial}$

Informal description

Let $R$ be a semiring with no zero divisors, $S$ a nontrivial partially ordered semiring, and $v \colon R \to S$ an absolute value. Then $v$ is nontrivial if and only if $v$ is not equal to the trivial absolute value.

AbsoluteValue.not_isNontrivial_iff theorem

(v : AbsoluteValue R S) : ¬v.IsNontrivial ↔ ∀ x ≠ 0, v x = 1

Full source

lemma not_isNontrivial_iff (v : AbsoluteValue R S) :
    ¬ v.IsNontrivial¬ v.IsNontrivial ↔ ∀ x ≠ 0, v x = 1 := by
  simp only [IsNontrivial]
  push_neg
  rfl

Characterization of Trivial Absolute Values: $\neg\text{IsNontrivial}(v) \leftrightarrow \forall x \neq 0, v(x) = 1$

Informal description

For an absolute value $v$ on a semiring $R$ mapping to a partially ordered semiring $S$, the statement that $v$ is not nontrivial is equivalent to the condition that for every nonzero element $x \in R$, the value $v(x)$ equals $1$.

AbsoluteValue.not_isNontrivial_apply theorem

{v : AbsoluteValue R S} (hv : ¬v.IsNontrivial) {x : R} (hx : x ≠ 0) : v x = 1

Full source

@[simp]
lemma not_isNontrivial_apply {v : AbsoluteValue R S} (hv : ¬ v.IsNontrivial) {x : R} (hx : x ≠ 0) :
    v x = 1 :=
  v.not_isNontrivial_iff.mp hv _ hx

Trivial Absolute Values Evaluate to One on Nonzero Elements

Informal description

Let $v$ be an absolute value from a semiring $R$ to a partially ordered semiring $S$. If $v$ is not nontrivial, then for any nonzero element $x \in R$, we have $v(x) = 1$.

AbsoluteValue.IsNontrivial.exists_abv_gt_one theorem

(h : v.IsNontrivial) : ∃ x, 1 < v x

Full source

lemma IsNontrivial.exists_abv_gt_one (h : v.IsNontrivial) : ∃ x, 1 < v x := by
  obtain ⟨x, hx₀, hx₁⟩ := h
  rcases hx₁.lt_or_lt with h | h
  · refine ⟨x⁻¹, ?_⟩
    rw [map_inv₀]
    exact (one_lt_inv₀ <| v.pos hx₀).mpr h
  · exact ⟨x, h⟩

Existence of Element with Absolute Value Greater Than One for Nontrivial Absolute Values

Informal description

For any nontrivial absolute value $v$ on a semiring $R$ mapping to a partially ordered semiring $S$, there exists an element $x \in R$ such that $v(x) > 1$.

AbsoluteValue.IsNontrivial.exists_abv_lt_one theorem

(h : v.IsNontrivial) : ∃ x ≠ 0, v x < 1

Full source

lemma IsNontrivial.exists_abv_lt_one (h : v.IsNontrivial) : ∃ x ≠ 0, v x < 1 := by
  obtain ⟨y, hy⟩ := h.exists_abv_gt_one
  have hy₀ := v.ne_zero_iff.mp <| (zero_lt_one.trans hy).ne'
  refine ⟨y⁻¹, inv_ne_zero hy₀, ?_⟩
  rw [map_inv₀]
  exact (inv_lt_one₀ <| v.pos hy₀).mpr hy

Existence of Element with Absolute Value Less Than One for Nontrivial Absolute Values

Informal description

For any nontrivial absolute value $v$ from a semiring $R$ to a partially ordered semiring $S$, there exists a nonzero element $x \in R$ such that $v(x) < 1$.

IsAbsoluteValue structure

{S} [Semiring S] [PartialOrder S] {R} [Semiring R] (f : R → S)

Full source

/-- A function `f` is an absolute value if it is nonnegative, zero only at 0, additive, and
multiplicative.

See also the type `AbsoluteValue` which represents a bundled version of absolute values.
-/
class IsAbsoluteValue {S} [Semiring S] [PartialOrder S] {R} [Semiring R] (f : R → S) : Prop where
  /-- The absolute value is nonnegative -/
  abv_nonneg' : ∀ x, 0 ≤ f x
  /-- The absolute value is positive definitive -/
  abv_eq_zero' : ∀ {x}, f x = 0 ↔ x = 0
  /-- The absolute value satisfies the triangle inequality -/
  abv_add' : ∀ x y, f (x + y) ≤ f x + f y
  /-- The absolute value is multiplicative -/
  abv_mul' : ∀ x y, f (x * y) = f x * f y

Absolute value on a semiring

Informal description

A function $f: R \to S$ between semirings is called an absolute value if it satisfies the following properties: 1. Nonnegativity: $f(x) \geq 0$ for all $x \in R$. 2. Definiteness: $f(x) = 0$ if and only if $x = 0$. 3. Additivity: $f(x + y) \leq f(x) + f(y)$ for all $x, y \in R$. 4. Multiplicativity: $f(xy) = f(x)f(y)$ for all $x, y \in R$. Here, $R$ and $S$ are semirings, and $S$ is equipped with a partial order.

IsAbsoluteValue.abv_nonneg theorem

(x) : 0 ≤ abv x

Full source

lemma abv_nonneg (x) : 0 ≤ abv x := abv_nonneg' x

Nonnegativity of Absolute Values: $0 \leq f(x)$

Informal description

For any absolute value function $f$ on a semiring $R$ and any element $x \in R$, we have $0 \leq f(x)$.

IsAbsoluteValue.Mathlib.Meta.Positivity.evalAbv definition

: PositivityExt

Full source

/-- The `positivity` extension which identifies expressions of the form `abv a`. -/
@[positivity _]
def Mathlib.Meta.Positivity.evalAbv : PositivityExt where eval {_ _α} _zα _pα e := do
  let (.app f a) ← whnfR e | throwError "not abv ·"
  let pa' ← mkAppM ``abv_nonneg #[f, a]
  pure (.nonnegative pa')

Positivity extension for absolute values

Informal description

The `positivity` extension identifies expressions of the form `abv a` where `abv` is an absolute value function, and proves that `abv a` is nonnegative for any input `a`.

IsAbsoluteValue.abv_eq_zero theorem

{x} : abv x = 0 ↔ x = 0

Full source

lemma abv_eq_zero {x} : abv x = 0 ↔ x = 0 := abv_eq_zero'

Definiteness of Absolute Values: $f(x) = 0 \iff x = 0$

Informal description

For any absolute value function $f$ on a semiring $R$ and any element $x \in R$, we have $f(x) = 0$ if and only if $x = 0$.

IsAbsoluteValue.abv_add theorem

(x y) : abv (x + y) ≤ abv x + abv y

Full source

lemma abv_add (x y) : abv (x + y) ≤ abv x + abv y := abv_add' x y

Triangle Inequality for Absolute Values

Informal description

For any absolute value function $f$ on a semiring $R$ and any elements $x, y \in R$, the triangle inequality holds: \[ f(x + y) \leq f(x) + f(y). \]

IsAbsoluteValue.abv_mul theorem

(x y) : abv (x * y) = abv x * abv y

Full source

lemma abv_mul (x y) : abv (x * y) = abv x * abv y := abv_mul' x y

Multiplicativity of Absolute Values: $f(xy) = f(x)f(y)$

Informal description

For any absolute value function $f$ on a semiring $R$ and any elements $x, y \in R$, the multiplicativity property holds: \[ f(xy) = f(x)f(y). \]

AbsoluteValue.isAbsoluteValue instance

(abv : AbsoluteValue R S) : IsAbsoluteValue abv

Full source

/-- A bundled absolute value is an absolute value. -/
instance _root_.AbsoluteValue.isAbsoluteValue (abv : AbsoluteValue R S) : IsAbsoluteValue abv where
  abv_nonneg' := abv.nonneg
  abv_eq_zero' := abv.eq_zero
  abv_add' := abv.add_le
  abv_mul' := abv.map_mul

Bundled Absolute Values Satisfy Absolute Value Axioms

Informal description

For any absolute value function $abv : R \to S$ from a semiring $R$ to a partially ordered semiring $S$, $abv$ satisfies the axioms of an absolute value. Specifically: 1. Nonnegativity: $abv(x) \geq 0$ for all $x \in R$. 2. Definiteness: $abv(x) = 0$ if and only if $x = 0$. 3. Triangle inequality: $abv(x + y) \leq abv(x) + abv(y)$ for all $x, y \in R$. 4. Multiplicativity: $abv(xy) = abv(x)abv(y)$ for all $x, y \in R$.

IsAbsoluteValue.toAbsoluteValue definition

: AbsoluteValue R S

Full source

/-- Convert an unbundled `IsAbsoluteValue` to a bundled `AbsoluteValue`. -/
@[simps]
def toAbsoluteValue : AbsoluteValue R S where
  toFun := abv
  add_le' := abv_add'
  eq_zero' _ := abv_eq_zero'
  nonneg' := abv_nonneg'
  map_mul' := abv_mul'

Conversion from unbundled to bundled absolute value

Informal description

Given a function `abv : R → S` between semirings that satisfies the properties of an absolute value (nonnegativity, definiteness, additivity, and multiplicativity), this definition constructs a bundled `AbsoluteValue R S` structure from the unbundled `IsAbsoluteValue` type class.

IsAbsoluteValue.abv_zero theorem

: abv 0 = 0

Full source

theorem abv_zero : abv 0 = 0 :=
  (toAbsoluteValue abv).map_zero

Absolute Value Vanishes at Zero

Informal description

For any absolute value function $abv$ from a semiring $R$ to a partially ordered semiring $S$, the value of $abv$ at $0$ is $0$, i.e., $abv(0) = 0$.

IsAbsoluteValue.abv_pos theorem

{a : R} : 0 < abv a ↔ a ≠ 0

Full source

theorem abv_pos {a : R} : 0 < abv a ↔ a ≠ 0 :=
  (toAbsoluteValue abv).pos_iff

Positivity of Absolute Values: $0 < \text{abv}(a) \leftrightarrow a \neq 0$

Informal description

For any element $a$ in a semiring $R$ and an absolute value function $\text{abv} : R \to S$ where $S$ is a partially ordered semiring, the value $\text{abv}(a)$ is strictly positive if and only if $a$ is nonzero, i.e., \[ 0 < \text{abv}(a) \leftrightarrow a \neq 0. \]

IsAbsoluteValue.abs_isAbsoluteValue instance

: IsAbsoluteValue (abs : S → S)

Full source

instance abs_isAbsoluteValue : IsAbsoluteValue (abs : S → S) :=
  AbsoluteValue.abs.isAbsoluteValue

Standard Absolute Value is an Absolute Value

Informal description

The standard absolute value function $\text{abs} : S \to S$ on a semiring $S$ satisfies the axioms of an absolute value. Specifically: 1. Nonnegativity: $|x| \geq 0$ for all $x \in S$. 2. Definiteness: $|x| = 0$ if and only if $x = 0$. 3. Triangle inequality: $|x + y| \leq |x| + |y|$ for all $x, y \in S$. 4. Multiplicativity: $|xy| = |x||y|$ for all $x, y \in S$.

IsAbsoluteValue.abv_one theorem

[Nontrivial R] : abv 1 = 1

Full source

theorem abv_one [Nontrivial R] : abv 1 = 1 :=
  (toAbsoluteValue abv).map_one

Absolute Value of One: $\text{abv}(1) = 1$

Informal description

For any absolute value function $\text{abv} : R \to S$ from a nontrivial semiring $R$ to a partially ordered semiring $S$, the value of $\text{abv}$ at the multiplicative identity $1$ is equal to $1$, i.e., $\text{abv}(1) = 1$.

IsAbsoluteValue.abvHom definition

[Nontrivial R] : R →*₀ S

Full source

/-- `abv` as a `MonoidWithZeroHom`. -/
def abvHom [Nontrivial R] : R →*₀ S :=
  (toAbsoluteValue abv).toMonoidWithZeroHom

Absolute value as a monoid with zero homomorphism

Informal description

Given a nontrivial semiring $R$ and a partially ordered semiring $S$, the function converts an absolute value $\text{abv} : R \to S$ into a monoid with zero homomorphism from $R$ to $S$, preserving the multiplicative structure, the identity element, and the zero element.

IsAbsoluteValue.abv_pow theorem

[Nontrivial R] (abv : R → S) [IsAbsoluteValue abv] (a : R) (n : ℕ) : abv (a ^ n) = abv a ^ n

Full source

theorem abv_pow [Nontrivial R] (abv : R → S) [IsAbsoluteValue abv] (a : R) (n : ℕ) :
    abv (a ^ n) = abv a ^ n :=
  (toAbsoluteValue abv).map_pow a n

Power Preservation under Absolute Values: $\text{abv}(a^n) = \text{abv}(a)^n$

Informal description

For any absolute value function $\text{abv} \colon R \to S$ on a nontrivial semiring $R$ with values in a partially ordered semiring $S$, and for any element $a \in R$ and natural number $n$, the absolute value of $a^n$ equals the $n$-th power of the absolute value of $a$, i.e., \[ \text{abv}(a^n) = (\text{abv}(a))^n. \]

IsAbsoluteValue.abv_sub_le theorem

(a b c : R) : abv (a - c) ≤ abv (a - b) + abv (b - c)

Full source

theorem abv_sub_le (a b c : R) : abv (a - c) ≤ abv (a - b) + abv (b - c) := by
  simpa [sub_eq_add_neg, add_assoc] using abv_add abv (a - b) (b - c)

Triangle Inequality for Differences under Absolute Value

Informal description

For any absolute value function $f$ on a semiring $R$ and any elements $a, b, c \in R$, the following inequality holds: \[ f(a - c) \leq f(a - b) + f(b - c). \]

IsAbsoluteValue.sub_abv_le_abv_sub theorem

[IsOrderedRing S] (a b : R) : abv a - abv b ≤ abv (a - b)

Full source

theorem sub_abv_le_abv_sub [IsOrderedRing S] (a b : R) : abv a - abv b ≤ abv (a - b) :=
  (toAbsoluteValue abv).le_sub a b

Reverse Triangle Inequality for Absolute Values on Ordered Rings

Informal description

For any absolute value function $abv: R \to S$ where $S$ is an ordered ring, and for any elements $a, b \in R$, the following inequality holds: \[ abv(a) - abv(b) \leq abv(a - b). \]

IsAbsoluteValue.abv_neg theorem

(a : R) : abv (-a) = abv a

Full source

theorem abv_neg (a : R) : abv (-a) = abv a :=
  (toAbsoluteValue abv).map_neg a

Absolute Value of Negative Element: $f(-a) = f(a)$

Informal description

For any absolute value function $f: R \to S$ on a semiring $R$ and any element $a \in R$, we have $f(-a) = f(a)$.

IsAbsoluteValue.abv_sub theorem

(a b : R) : abv (a - b) = abv (b - a)

Full source

theorem abv_sub (a b : R) : abv (a - b) = abv (b - a) :=
  (toAbsoluteValue abv).map_sub a b

Symmetry of Absolute Value of Differences: $f(a - b) = f(b - a)$

Informal description

For any absolute value function $f: R \to S$ on a semiring $R$ and any elements $a, b \in R$, the absolute value of the difference $a - b$ equals the absolute value of the difference $b - a$, i.e., \[ f(a - b) = f(b - a). \]

IsAbsoluteValue.abs_abv_sub_le_abv_sub theorem

(a b : R) : abs (abv a - abv b) ≤ abv (a - b)

Full source

theorem abs_abv_sub_le_abv_sub (a b : R) : abs (abv a - abv b) ≤ abv (a - b) :=
  (toAbsoluteValue abv).abs_abv_sub_le_abv_sub a b

Reverse Triangle Inequality for Absolute Values: $|f(a) - f(b)| \leq f(a - b)$

Informal description

For any absolute value function $f \colon R \to S$ on a semiring $R$ and any elements $a, b \in R$, the following inequality holds: \[ |f(a) - f(b)| \leq f(a - b). \]

IsAbsoluteValue.abv_one' theorem

: abv 1 = 1

Full source

theorem abv_one' : abv 1 = 1 :=
  (toAbsoluteValue abv).map_one_of_isLeftRegular <|
    (isRegular_of_ne_zero <| (toAbsoluteValue abv).ne_zero one_ne_zero).left

Absolute Value of One: $f(1) = 1$

Informal description

For any absolute value function $f: R \to S$ between semirings, the value of $f$ at the multiplicative identity $1$ is equal to $1$, i.e., $f(1) = 1$.

IsAbsoluteValue.abvHom' definition

: R →*₀ S

Full source

/-- An absolute value as a monoid with zero homomorphism, assuming the target is a semifield. -/
def abvHom' : R →*₀ S where
  toFun := abv; map_zero' := abv_zero abv; map_one' := abv_one' abv; map_mul' := abv_mul abv

Absolute value as a monoid with zero homomorphism

Informal description

The function `abvHom'` is a monoid with zero homomorphism from a semiring $R$ to a partially ordered semiring $S$, defined by an absolute value function `abv` that satisfies: 1. $f(0) = 0$, 2. $f(1) = 1$, 3. $f(xy) = f(x)f(y)$ for all $x, y \in R$.

IsAbsoluteValue.abv_inv theorem

(a : R) : abv a⁻¹ = (abv a)⁻¹

Full source

theorem abv_inv (a : R) : abv a⁻¹ = (abv a)⁻¹ :=
  map_inv₀ (abvHom' abv) a

Inverse Preservation Property of Absolute Values: $f(a^{-1}) = (f(a))^{-1}$

Informal description

For any absolute value function $f: R \to S$ between semirings and any invertible element $a \in R$, the value of $f$ at the inverse of $a$ is equal to the inverse of $f(a)$, i.e., $f(a^{-1}) = (f(a))^{-1}$.

IsAbsoluteValue.abv_div theorem

(a b : R) : abv (a / b) = abv a / abv b

Full source

theorem abv_div (a b : R) : abv (a / b) = abv a / abv b :=
  map_div₀ (abvHom' abv) a b

Absolute Value Preserves Division: $\text{abv}(a / b) = \text{abv}(a) / \text{abv}(b)$

Informal description

For any elements $a, b$ in a semiring $R$ equipped with an absolute value function $\text{abv} : R \to S$, where $S$ is a partially ordered semiring, the absolute value of the division $a / b$ is equal to the division of the absolute values, i.e., \[ \text{abv}(a / b) = \text{abv}(a) / \text{abv}(b). \]

Main definitions