# Absolute values #

This file defines a bundled type of absolute values AbsoluteValue R S.

## Main definitions #

• AbsoluteValue R S is the type of absolute values on R mapping to S.
• AbsoluteValue.abs is the "standard" absolute value on S, mapping negative x to -x.
• AbsoluteValue.toMonoidWithZeroHom: absolute values mapping to a linear ordered field preserve 0, * and 1
• IsAbsoluteValue: a type class stating that f : β → α satisfies the axioms of an absolute value
structure AbsoluteValue (R : Type u_5) (S : Type u_6) [] [] extends :
Type (max u_5 u_6)

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 equality.

• toFun : RS
• map_mul' : ∀ (x y : R), self.toFun (x * y) = self.toFun x * self.toFun y
• nonneg' : ∀ (x : R), 0 self.toFun x

The absolute value is nonnegative

• eq_zero' : ∀ (x : R), self.toFun x = 0 x = 0

The absolute value is positive definitive

• add_le' : ∀ (x y : R), self.toFun (x + y) self.toFun x + self.toFun y

The absolute value satisfies the triangle inequality

Instances For
theorem AbsoluteValue.nonneg' {R : Type u_5} {S : Type u_6} [] [] (self : ) (x : R) :
0 self.toFun x

The absolute value is nonnegative

theorem AbsoluteValue.eq_zero' {R : Type u_5} {S : Type u_6} [] [] (self : ) (x : R) :
self.toFun x = 0 x = 0

The absolute value is positive definitive

theorem AbsoluteValue.add_le' {R : Type u_5} {S : Type u_6} [] [] (self : ) (x : R) (y : R) :
self.toFun (x + y) self.toFun x + self.toFun y

The absolute value satisfies the triangle inequality

instance AbsoluteValue.funLike {R : Type u_5} {S : Type u_6} [] [] :
FunLike () R S
Equations
• AbsoluteValue.funLike = { coe := fun (f : ) => f.toFun, coe_injective' := }
instance AbsoluteValue.zeroHomClass {R : Type u_5} {S : Type u_6} [] [] :
Equations
• =
instance AbsoluteValue.mulHomClass {R : Type u_5} {S : Type u_6} [] [] :
Equations
• =
instance AbsoluteValue.nonnegHomClass {R : Type u_5} {S : Type u_6} [] [] :
Equations
• =
instance AbsoluteValue.subadditiveHomClass {R : Type u_5} {S : Type u_6} [] [] :
Equations
• =
@[simp]
theorem AbsoluteValue.coe_mk {R : Type u_5} {S : Type u_6} [] [] (f : R →ₙ* S) {h₁ : ∀ (x : R), 0 f.toFun x} {h₂ : ∀ (x : R), f.toFun x = 0 x = 0} {h₃ : ∀ (x y : R), f.toFun (x + y) f.toFun x + f.toFun y} :
{ toMulHom := f, nonneg' := h₁, eq_zero' := h₂, add_le' := h₃ } = f
theorem AbsoluteValue.ext {R : Type u_5} {S : Type u_6} [] [] ⦃f : ⦃g : :
(∀ (x : R), f x = g x)f = g
def AbsoluteValue.Simps.apply {R : Type u_5} {S : Type u_6} [] [] (f : ) :
RS

See Note [custom simps projection].

Equations
Instances For
instance AbsoluteValue.instCoeFunForall {R : Type u_5} {S : Type u_6} [] [] :
CoeFun () fun (x : ) => RS

Helper instance for when there's too many metavariables to apply DFunLike.has_coe_to_fun directly.

Equations
• AbsoluteValue.instCoeFunForall = DFunLike.hasCoeToFun
@[simp]
theorem AbsoluteValue.coe_toMulHom {R : Type u_5} {S : Type u_6} [] [] (abv : ) :
abv.toMulHom = abv
theorem AbsoluteValue.nonneg {R : Type u_5} {S : Type u_6} [] [] (abv : ) (x : R) :
0 abv x
@[simp]
theorem AbsoluteValue.eq_zero {R : Type u_5} {S : Type u_6} [] [] (abv : ) {x : R} :
abv x = 0 x = 0
theorem AbsoluteValue.add_le {R : Type u_5} {S : Type u_6} [] [] (abv : ) (x : R) (y : R) :
abv (x + y) abv x + abv y
theorem AbsoluteValue.map_mul {R : Type u_5} {S : Type u_6} [] [] (abv : ) (x : R) (y : R) :
abv (x * y) = abv x * abv y
theorem AbsoluteValue.ne_zero_iff {R : Type u_5} {S : Type u_6} [] [] (abv : ) {x : R} :
abv x 0 x 0
theorem AbsoluteValue.pos {R : Type u_5} {S : Type u_6} [] [] (abv : ) {x : R} (hx : x 0) :
0 < abv x
@[simp]
theorem AbsoluteValue.pos_iff {R : Type u_5} {S : Type u_6} [] [] (abv : ) {x : R} :
0 < abv x x 0
theorem AbsoluteValue.ne_zero {R : Type u_5} {S : Type u_6} [] [] (abv : ) {x : R} (hx : x 0) :
abv x 0
theorem AbsoluteValue.map_one_of_isLeftRegular {R : Type u_5} {S : Type u_6} [] [] (abv : ) (h : IsLeftRegular (abv 1)) :
abv 1 = 1
theorem AbsoluteValue.map_zero {R : Type u_5} {S : Type u_6} [] [] (abv : ) :
abv 0 = 0
theorem AbsoluteValue.sub_le {R : Type u_5} {S : Type u_6} [Ring R] [] (abv : ) (a : R) (b : R) (c : R) :
abv (a - c) abv (a - b) + abv (b - c)
@[simp]
theorem AbsoluteValue.map_sub_eq_zero_iff {R : Type u_5} {S : Type u_6} [Ring R] [] (abv : ) (a : R) (b : R) :
abv (a - b) = 0 a = b
theorem AbsoluteValue.map_one {R : Type u_5} {S : Type u_6} [] [] (abv : ) [] [] :
abv 1 = 1
instance AbsoluteValue.monoidWithZeroHomClass {R : Type u_5} {S : Type u_6} [] [] [] [] :
Equations
• =
def AbsoluteValue.toMonoidWithZeroHom {R : Type u_5} {S : Type u_6} [] [] (abv : ) [] [] :

Absolute values from a nontrivial R to a linear ordered ring preserve *, 0 and 1.

Equations
• abv.toMonoidWithZeroHom = abv
Instances For
@[simp]
theorem AbsoluteValue.coe_toMonoidWithZeroHom {R : Type u_5} {S : Type u_6} [] [] (abv : ) [] [] :
abv.toMonoidWithZeroHom = abv
def AbsoluteValue.toMonoidHom {R : Type u_5} {S : Type u_6} [] [] (abv : ) [] [] :
R →* S

Absolute values from a nontrivial R to a linear ordered ring preserve * and 1.

Equations
• abv.toMonoidHom = abv
Instances For
@[simp]
theorem AbsoluteValue.coe_toMonoidHom {R : Type u_5} {S : Type u_6} [] [] (abv : ) [] [] :
abv.toMonoidHom = abv
theorem AbsoluteValue.map_pow {R : Type u_5} {S : Type u_6} [] [] (abv : ) [] [] (a : R) (n : ) :
abv (a ^ n) = abv a ^ n
theorem AbsoluteValue.le_sub {R : Type u_5} {S : Type u_6} [Ring R] [] (abv : ) (a : R) (b : R) :
abv a - abv b abv (a - b)
@[simp]
theorem AbsoluteValue.map_neg {R : Type u_3} {S : Type u_4} [] [Ring R] (abv : ) [] (a : R) :
abv (-a) = abv a
theorem AbsoluteValue.map_sub {R : Type u_3} {S : Type u_4} [] [Ring R] (abv : ) [] (a : R) (b : R) :
abv (a - b) = abv (b - a)
theorem AbsoluteValue.le_add {R : Type u_3} {S : Type u_4} [] [Ring R] (abv : ) [] (a : R) (b : R) :
abv a - abv b abv (a + b)

Bound abv (a + b) from below

theorem AbsoluteValue.sub_le_add {R : Type u_3} {S : Type u_4} [] [Ring R] (abv : ) [] (a : R) (b : R) :
abv (a - b) abv a + abv b

Bound abv (a - b) from above

instance AbsoluteValue.instMulRingNormClassOfNontrivialOfIsDomain {R : Type u_3} {S : Type u_4} [] [Ring R] [] [] [] :
Equations
• =
@[simp]
theorem AbsoluteValue.abs_toFun {S : Type u_6} (a : S) :
AbsoluteValue.abs a = |a|
@[simp]
theorem AbsoluteValue.abs_apply {S : Type u_6} (a : S) :
AbsoluteValue.abs a = |a|
def AbsoluteValue.abs {S : Type u_6} :

AbsoluteValue.abs is abs as a bundled AbsoluteValue.

Equations
• AbsoluteValue.abs = { toFun := abs, map_mul' := , nonneg' := , eq_zero' := , add_le' := }
Instances For
Equations
• AbsoluteValue.instInhabited = { default := AbsoluteValue.abs }
theorem AbsoluteValue.abs_abv_sub_le_abv_sub {R : Type u_5} {S : Type u_6} [Ring R] (abv : ) (a : R) (b : R) :
|abv a - abv b| abv (a - b)
class IsAbsoluteValue {S : Type u_5} [] {R : Type u_6} [] (f : RS) :

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.

• abv_nonneg' : ∀ (x : R), 0 f x

The absolute value is nonnegative

• abv_eq_zero' : ∀ {x : R}, f x = 0 x = 0

The absolute value is positive definitive

• abv_add' : ∀ (x y : R), f (x + y) f x + f y

The absolute value satisfies the triangle inequality

• abv_mul' : ∀ (x y : R), f (x * y) = f x * f y

The absolute value is multiplicative

Instances
theorem IsAbsoluteValue.abv_nonneg' {S : Type u_5} [] {R : Type u_6} [] {f : RS} [self : ] (x : R) :
0 f x

The absolute value is nonnegative

theorem IsAbsoluteValue.abv_eq_zero' {S : Type u_5} [] {R : Type u_6} [] {f : RS} [self : ] {x : R} :
f x = 0 x = 0

The absolute value is positive definitive

theorem IsAbsoluteValue.abv_add' {S : Type u_5} [] {R : Type u_6} [] {f : RS} [self : ] (x : R) (y : R) :
f (x + y) f x + f y

The absolute value satisfies the triangle inequality

theorem IsAbsoluteValue.abv_mul' {S : Type u_5} [] {R : Type u_6} [] {f : RS} [self : ] (x : R) (y : R) :
f (x * y) = f x * f y

The absolute value is multiplicative

theorem IsAbsoluteValue.abv_nonneg {S : Type u_5} [] {R : Type u_6} [] (abv : RS) [] (x : R) :
0 abv x

The positivity extension which identifies expressions of the form abv a.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem IsAbsoluteValue.abv_eq_zero {S : Type u_5} [] {R : Type u_6} [] (abv : RS) [] {x : R} :
abv x = 0 x = 0
theorem IsAbsoluteValue.abv_add {S : Type u_5} [] {R : Type u_6} [] (abv : RS) [] (x : R) (y : R) :
abv (x + y) abv x + abv y
theorem IsAbsoluteValue.abv_mul {S : Type u_5} [] {R : Type u_6} [] (abv : RS) [] (x : R) (y : R) :
abv (x * y) = abv x * abv y
instance AbsoluteValue.isAbsoluteValue {S : Type u_5} [] {R : Type u_6} [] (abv : ) :

A bundled absolute value is an absolute value.

Equations
• =
@[simp]
theorem IsAbsoluteValue.toAbsoluteValue_apply {S : Type u_5} [] {R : Type u_6} [] (abv : RS) [] :
∀ (a : R), = abv a
@[simp]
theorem IsAbsoluteValue.toAbsoluteValue_toFun {S : Type u_5} [] {R : Type u_6} [] (abv : RS) [] :
∀ (a : R), = abv a
def IsAbsoluteValue.toAbsoluteValue {S : Type u_5} [] {R : Type u_6} [] (abv : RS) [] :

Convert an unbundled IsAbsoluteValue to a bundled AbsoluteValue.

Equations
• = { toFun := abv, map_mul' := , nonneg' := , eq_zero' := , add_le' := }
Instances For
theorem IsAbsoluteValue.abv_zero {S : Type u_5} [] {R : Type u_6} [] (abv : RS) [] :
abv 0 = 0
theorem IsAbsoluteValue.abv_pos {S : Type u_5} [] {R : Type u_6} [] (abv : RS) [] {a : R} :
0 < abv a a 0
Equations
• =
theorem IsAbsoluteValue.abv_one {S : Type u_5} [] {R : Type u_6} [] (abv : RS) [] [] [] :
abv 1 = 1
def IsAbsoluteValue.abvHom {S : Type u_5} [] {R : Type u_6} [] (abv : RS) [] [] [] :

abv as a MonoidWithZeroHom.

Equations
• = .toMonoidWithZeroHom
Instances For
theorem IsAbsoluteValue.abv_pow {S : Type u_5} [] {R : Type u_6} [] [] [] (abv : RS) [] (a : R) (n : ) :
abv (a ^ n) = abv a ^ n
theorem IsAbsoluteValue.abv_sub_le {S : Type u_5} [] {R : Type u_6} [Ring R] (abv : RS) [] (a : R) (b : R) (c : R) :
abv (a - c) abv (a - b) + abv (b - c)
theorem IsAbsoluteValue.sub_abv_le_abv_sub {S : Type u_5} [] {R : Type u_6} [Ring R] (abv : RS) [] (a : R) (b : R) :
abv a - abv b abv (a - b)
theorem IsAbsoluteValue.abv_neg {R : Type u_3} {S : Type u_4} [] [] [Ring R] (abv : RS) [] (a : R) :
abv (-a) = abv a
theorem IsAbsoluteValue.abv_sub {R : Type u_3} {S : Type u_4} [] [] [Ring R] (abv : RS) [] (a : R) (b : R) :
abv (a - b) = abv (b - a)
theorem IsAbsoluteValue.abs_abv_sub_le_abv_sub {S : Type u_5} {R : Type u_6} [Ring R] (abv : RS) [] (a : R) (b : R) :
|abv a - abv b| abv (a - b)
theorem IsAbsoluteValue.abv_one' {S : Type u_5} {R : Type u_6} [] [] (abv : RS) [] :
abv 1 = 1
def IsAbsoluteValue.abvHom' {S : Type u_5} {R : Type u_6} [] [] (abv : RS) [] :

An absolute value as a monoid with zero homomorphism, assuming the target is a semifield.

Equations
• = { toFun := abv, map_zero' := , map_one' := , map_mul' := }
Instances For
theorem IsAbsoluteValue.abv_inv {S : Type u_5} {R : Type u_6} [] (abv : RS) [] (a : R) :
abv a⁻¹ = (abv a)⁻¹
theorem IsAbsoluteValue.abv_div {S : Type u_5} {R : Type u_6} [] (abv : RS) [] (a : R) (b : R) :
abv (a / b) = abv a / abv b