algebra.order.absolute_value

structure absolute_value (R : Type u_1) (S : Type u_2) [semiring R] [ordered_semiring S] :

Type (max u_1 u_2)

to_mul_hom : R →ₙ* S
nonneg' : ∀ (x : R), 0 ≤ self.to_mul_hom.to_fun x
eq_zero' : ∀ (x : R), self.to_mul_hom.to_fun x = 0 ↔ x = 0
add_le' : ∀ (x y : R), self.to_mul_hom.to_fun (x + y) ≤ self.to_mul_hom.to_fun x + self.to_mul_hom.to_fun y

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

Instances for absolute_value

absolute_value.has_sizeof_inst
absolute_value.zero_hom_class
absolute_value.mul_hom_class
absolute_value.nonneg_hom_class
absolute_value.subadditive_hom_class
absolute_value.has_coe_to_fun
absolute_value.monoid_with_zero_hom_class
absolute_value.mul_ring_norm_class
absolute_value.inhabited

source

@[protected, instance]

def absolute_value.zero_hom_class {R : Type u_1} {S : Type u_2} [semiring R] [ordered_semiring S] :

zero_hom_class (absolute_value R S) R S

Equations

absolute_value.zero_hom_class = {coe := λ (f : absolute_value R S), f.to_mul_hom.to_fun, coe_injective' := _, map_zero := _}

source

@[protected, instance]

def absolute_value.mul_hom_class {R : Type u_1} {S : Type u_2} [semiring R] [ordered_semiring S] :

mul_hom_class (absolute_value R S) R S

Equations

absolute_value.mul_hom_class = {coe := zero_hom_class.coe absolute_value.zero_hom_class, coe_injective' := _, map_mul := _}

source

@[protected, instance]

def absolute_value.nonneg_hom_class {R : Type u_1} {S : Type u_2} [semiring R] [ordered_semiring S] :

nonneg_hom_class (absolute_value R S) R S

Equations

absolute_value.nonneg_hom_class = {coe := zero_hom_class.coe absolute_value.zero_hom_class, coe_injective' := _, map_nonneg := _}

source

@[protected, instance]

def absolute_value.subadditive_hom_class {R : Type u_1} {S : Type u_2} [semiring R] [ordered_semiring S] :

subadditive_hom_class (absolute_value R S) R S

Equations

absolute_value.subadditive_hom_class = {coe := zero_hom_class.coe absolute_value.zero_hom_class, coe_injective' := _, map_add_le_add := _}

source

@[simp]

theorem absolute_value.coe_mk {R : Type u_1} {S : Type u_2} [semiring R] [ordered_semiring S] (f : R →ₙ* S) {h₁ : ∀ (x : R), 0 ≤ f.to_fun x} {h₂ : ∀ (x : R), f.to_fun x = 0 ↔ x = 0} {h₃ : ∀ (x y : R), f.to_fun (x + y) ≤ f.to_fun x + f.to_fun y} :

⇑{to_mul_hom := f, nonneg' := h₁, eq_zero' := h₂, add_le' := h₃} = ⇑f

source

@[ext]

theorem absolute_value.ext {R : Type u_1} {S : Type u_2} [semiring R] [ordered_semiring S] ⦃f g : absolute_value R S⦄ :

(∀ (x : R), ⇑f x = ⇑g x) → f = g

source

def absolute_value.simps.apply {R : Type u_1} {S : Type u_2} [semiring R] [ordered_semiring S] (f : absolute_value R S) :

R → S

See Note [custom simps projection].

Equations

absolute_value.simps.apply f = ⇑f

source

@[protected, instance]

def absolute_value.has_coe_to_fun {R : Type u_1} {S : Type u_2} [semiring R] [ordered_semiring S] :

has_coe_to_fun (absolute_value R S) (λ (f : absolute_value R S), R → S)

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

Equations

absolute_value.has_coe_to_fun = fun_like.has_coe_to_fun

source

@[simp]

theorem absolute_value.coe_to_mul_hom {R : Type u_1} {S : Type u_2} [semiring R] [ordered_semiring S] (abv : absolute_value R S) :

⇑(abv.to_mul_hom) = ⇑abv

source

@[protected]

theorem absolute_value.nonneg {R : Type u_1} {S : Type u_2} [semiring R] [ordered_semiring S] (abv : absolute_value R S) (x : R) :

0 ≤ ⇑abv x

source

@[protected, simp]

theorem absolute_value.eq_zero {R : Type u_1} {S : Type u_2} [semiring R] [ordered_semiring S] (abv : absolute_value R S) {x : R} :

⇑abv x = 0 ↔ x = 0

source

@[protected]

theorem absolute_value.add_le {R : Type u_1} {S : Type u_2} [semiring R] [ordered_semiring S] (abv : absolute_value R S) (x y : R) :

⇑abv (x + y) ≤ ⇑abv x + ⇑abv y

source

@[protected, simp]

theorem absolute_value.map_mul {R : Type u_1} {S : Type u_2} [semiring R] [ordered_semiring S] (abv : absolute_value R S) (x y : R) :

⇑abv (x * y) = ⇑abv x * ⇑abv y

source

@[protected]

theorem absolute_value.ne_zero_iff {R : Type u_1} {S : Type u_2} [semiring R] [ordered_semiring S] (abv : absolute_value R S) {x : R} :

⇑abv x ≠ 0 ↔ x ≠ 0

source

@[protected]

theorem absolute_value.pos {R : Type u_1} {S : Type u_2} [semiring R] [ordered_semiring S] (abv : absolute_value R S) {x : R} (hx : x ≠ 0) :

0 < ⇑abv x

source

@[protected, simp]

theorem absolute_value.pos_iff {R : Type u_1} {S : Type u_2} [semiring R] [ordered_semiring S] (abv : absolute_value R S) {x : R} :

0 < ⇑abv x ↔ x ≠ 0

source

@[protected]

theorem absolute_value.ne_zero {R : Type u_1} {S : Type u_2} [semiring R] [ordered_semiring S] (abv : absolute_value R S) {x : R} (hx : x ≠ 0) :

⇑abv x ≠ 0

source

theorem absolute_value.map_one_of_is_regular {R : Type u_1} {S : Type u_2} [semiring R] [ordered_semiring S] (abv : absolute_value R S) (h : is_left_regular (⇑abv 1)) :

⇑abv 1 = 1

source

@[protected, simp]

theorem absolute_value.map_zero {R : Type u_1} {S : Type u_2} [semiring R] [ordered_semiring S] (abv : absolute_value R S) :

⇑abv 0 = 0

source

@[protected]

theorem absolute_value.sub_le {R : Type u_1} {S : Type u_2} [ring R] [ordered_semiring S] (abv : absolute_value R S) (a b c : R) :

⇑abv (a - c) ≤ ⇑abv (a - b) + ⇑abv (b - c)

source

@[simp]

theorem absolute_value.map_sub_eq_zero_iff {R : Type u_1} {S : Type u_2} [ring R] [ordered_semiring S] (abv : absolute_value R S) (a b : R) :

⇑abv (a - b) = 0 ↔ a = b

source

@[protected, simp]

theorem absolute_value.map_one {R : Type u_1} {S : Type u_2} [semiring R] [ordered_ring S] (abv : absolute_value R S) [is_domain S] [nontrivial R] :

⇑abv 1 = 1

source

@[protected, instance]

def absolute_value.monoid_with_zero_hom_class {R : Type u_1} {S : Type u_2} [semiring R] [ordered_ring S] [is_domain S] [nontrivial R] :

monoid_with_zero_hom_class (absolute_value R S) R S

Equations

absolute_value.monoid_with_zero_hom_class = {coe := mul_hom_class.coe absolute_value.mul_hom_class, coe_injective' := _, map_mul := _, map_one := _, map_zero := _}

source

def absolute_value.to_monoid_with_zero_hom {R : Type u_1} {S : Type u_2} [semiring R] [ordered_ring S] (abv : absolute_value R S) [is_domain S] [nontrivial R] :

R →*₀ S

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

Equations

abv.to_monoid_with_zero_hom = ↑abv

source

@[simp]

theorem absolute_value.coe_to_monoid_with_zero_hom {R : Type u_1} {S : Type u_2} [semiring R] [ordered_ring S] (abv : absolute_value R S) [is_domain S] [nontrivial R] :

⇑(abv.to_monoid_with_zero_hom) = ⇑abv

source

def absolute_value.to_monoid_hom {R : Type u_1} {S : Type u_2} [semiring R] [ordered_ring S] (abv : absolute_value R S) [is_domain S] [nontrivial R] :

R →* S

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

Equations

abv.to_monoid_hom = ↑abv

source

@[simp]

theorem absolute_value.coe_to_monoid_hom {R : Type u_1} {S : Type u_2} [semiring R] [ordered_ring S] (abv : absolute_value R S) [is_domain S] [nontrivial R] :

⇑(abv.to_monoid_hom) = ⇑abv

source

@[protected, simp]

theorem absolute_value.map_pow {R : Type u_1} {S : Type u_2} [semiring R] [ordered_ring S] (abv : absolute_value R S) [is_domain S] [nontrivial R] (a : R) (n : ℕ) :

⇑abv (a ^ n) = ⇑abv a ^ n

source

@[protected]

theorem absolute_value.le_sub {R : Type u_1} {S : Type u_2} [ring R] [ordered_ring S] (abv : absolute_value R S) (a b : R) :

⇑abv a - ⇑abv b ≤ ⇑abv (a - b)

source

@[protected, simp]

theorem absolute_value.map_neg {R : Type u_1} {S : Type u_2} [ring R] [ordered_comm_ring S] (abv : absolute_value R S) [no_zero_divisors S] (a : R) :

⇑abv (-a) = ⇑abv a

source

@[protected]

theorem absolute_value.map_sub {R : Type u_1} {S : Type u_2} [ring R] [ordered_comm_ring S] (abv : absolute_value R S) [no_zero_divisors S] (a b : R) :

⇑abv (a - b) = ⇑abv (b - a)

source

@[protected, instance]

def absolute_value.mul_ring_norm_class {R : Type u_1} {S : Type u_2} [ring R] [ordered_comm_ring S] [nontrivial R] [is_domain S] :

mul_ring_norm_class (absolute_value R S) R S

Equations

absolute_value.mul_ring_norm_class = {coe := subadditive_hom_class.coe absolute_value.subadditive_hom_class, coe_injective' := _, map_add_le_add := _, map_zero := _, map_neg_eq_map := _, map_mul := _, map_one := _, eq_zero_of_map_eq_zero := _}

source

@[protected]

def absolute_value.abs {S : Type u_2} [linear_ordered_ring S] :

absolute_value S S

absolute_value.abs is abs as a bundled absolute_value.

Equations

absolute_value.abs = {to_mul_hom := {to_fun := has_abs.abs has_neg.to_has_abs, map_mul' := _}, nonneg' := _, eq_zero' := _, add_le' := _}

source

@[simp]

theorem absolute_value.abs_apply {S : Type u_2} [linear_ordered_ring S] (ᾰ : S) :

⇑absolute_value.abs ᾰ = |ᾰ|

source

@[simp]

theorem absolute_value.abs_to_mul_hom_apply {S : Type u_2} [linear_ordered_ring S] (ᾰ : S) :

⇑(absolute_value.abs.to_mul_hom) ᾰ = |ᾰ|

source

@[protected, instance]

def absolute_value.inhabited {S : Type u_2} [linear_ordered_ring S] :

inhabited (absolute_value S S)

Equations

absolute_value.inhabited = {default := absolute_value.abs _inst_2}

source

theorem absolute_value.abs_abv_sub_le_abv_sub {R : Type u_1} {S : Type u_2} [ring R] [linear_ordered_comm_ring S] (abv : absolute_value R S) (a b : R) :

|⇑abv a - ⇑abv b| ≤ ⇑abv (a - b)

source

@[class]

structure is_absolute_value {S : Type u_1} [ordered_semiring S] {R : Type u_2} [semiring R] (f : R → S) :

Prop

abv_nonneg : ∀ (x : R), 0 ≤ f x
abv_eq_zero : ∀ {x : R}, f x = 0 ↔ x = 0
abv_add : ∀ (x y : R), f (x + y) ≤ f x + f y
abv_mul : ∀ (x y : R), f (x * y) = f x * f y

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

See also the type absolute_value which represents a bundled version of absolute values.

Instances of this typeclass

source

@[protected, instance]

def absolute_value.is_absolute_value {S : Type u_1} [ordered_semiring S] {R : Type u_2} [semiring R] (abv : absolute_value R S) :

is_absolute_value ⇑abv

A bundled absolute value is an absolute value.

source

def is_absolute_value.to_absolute_value {S : Type u_1} [ordered_semiring S] {R : Type u_2} [semiring R] (abv : R → S) [is_absolute_value abv] :

absolute_value R S

Convert an unbundled is_absolute_value to a bundled absolute_value.

Equations

is_absolute_value.to_absolute_value abv = {to_mul_hom := {to_fun := abv, map_mul' := _}, nonneg' := _, eq_zero' := _, add_le' := _}

source

@[simp]

theorem is_absolute_value.to_absolute_value_to_mul_hom_apply {S : Type u_1} [ordered_semiring S] {R : Type u_2} [semiring R] (abv : R → S) [is_absolute_value abv] (ᾰ : R) :

⇑((is_absolute_value.to_absolute_value abv).to_mul_hom) ᾰ = abv ᾰ

source

@[simp]

theorem is_absolute_value.to_absolute_value_apply {S : Type u_1} [ordered_semiring S] {R : Type u_2} [semiring R] (abv : R → S) [is_absolute_value abv] (ᾰ : R) :

⇑(is_absolute_value.to_absolute_value abv) ᾰ = abv ᾰ

source

theorem is_absolute_value.abv_zero {S : Type u_1} [ordered_semiring S] {R : Type u_2} [semiring R] (abv : R → S) [is_absolute_value abv] :

abv 0 = 0

source

theorem is_absolute_value.abv_pos {S : Type u_1} [ordered_semiring S] {R : Type u_2} [semiring R] (abv : R → S) [is_absolute_value abv] {a : R} :

0 < abv a ↔ a ≠ 0

source

@[protected, instance]

def is_absolute_value.abs_is_absolute_value {S : Type u_1} [linear_ordered_ring S] :

is_absolute_value has_abs.abs

source

theorem is_absolute_value.abv_one {S : Type u_1} [ordered_ring S] {R : Type u_2} [semiring R] (abv : R → S) [is_absolute_value abv] [is_domain S] [nontrivial R] :

abv 1 = 1

source

def is_absolute_value.abv_hom {S : Type u_1} [ordered_ring S] {R : Type u_2} [semiring R] (abv : R → S) [is_absolute_value abv] [is_domain S] [nontrivial R] :

R →*₀ S

abv as a monoid_with_zero_hom.

Equations

is_absolute_value.abv_hom abv = (is_absolute_value.to_absolute_value abv).to_monoid_with_zero_hom

source

theorem is_absolute_value.abv_pow {S : Type u_1} [ordered_ring S] {R : Type u_2} [semiring R] [is_domain S] [nontrivial R] (abv : R → S) [is_absolute_value abv] (a : R) (n : ℕ) :

abv (a ^ n) = abv a ^ n

source

theorem is_absolute_value.abv_sub_le {S : Type u_1} [ordered_ring S] {R : Type u_2} [ring R] (abv : R → S) [is_absolute_value abv] (a b c : R) :

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

source

theorem is_absolute_value.sub_abv_le_abv_sub {S : Type u_1} [ordered_ring S] {R : Type u_2} [ring R] (abv : R → S) [is_absolute_value abv] (a b : R) :

abv a - abv b ≤ abv (a - b)

source

theorem is_absolute_value.abv_neg {S : Type u_1} [ordered_comm_ring S] {R : Type u_2} [ring R] (abv : R → S) [is_absolute_value abv] [no_zero_divisors S] (a : R) :

abv (-a) = abv a

source

theorem is_absolute_value.abv_sub {S : Type u_1} [ordered_comm_ring S] {R : Type u_2} [ring R] (abv : R → S) [is_absolute_value abv] [no_zero_divisors S] (a b : R) :

abv (a - b) = abv (b - a)

source

theorem is_absolute_value.abs_abv_sub_le_abv_sub {S : Type u_1} [linear_ordered_comm_ring S] {R : Type u_2} [ring R] (abv : R → S) [is_absolute_value abv] (a b : R) :

|abv a - abv b| ≤ abv (a - b)

source

theorem is_absolute_value.abv_one' {S : Type u_1} [linear_ordered_semifield S] {R : Type u_2} [semiring R] [nontrivial R] (abv : R → S) [is_absolute_value abv] :

abv 1 = 1

source

def is_absolute_value.abv_hom' {S : Type u_1} [linear_ordered_semifield S] {R : Type u_2} [semiring R] [nontrivial R] (abv : R → S) [is_absolute_value abv] :

R →*₀ S

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

Equations

is_absolute_value.abv_hom' abv = {to_fun := abv, map_zero' := _, map_one' := _, map_mul' := _}

source

theorem is_absolute_value.abv_inv {S : Type u_1} [linear_ordered_semifield S] {R : Type u_2} [division_semiring R] (abv : R → S) [is_absolute_value abv] (a : R) :

abv a⁻¹ = (abv a)⁻¹

source

theorem is_absolute_value.abv_div {S : Type u_1} [linear_ordered_semifield S] {R : Type u_2} [division_semiring R] (abv : R → S) [is_absolute_value abv] (a b : R) :

abv (a / b) = abv a / abv b

mathlib3 documentation

Absolute values #

Main definitions #