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_1) (S : Type u_2) [inst : Semiring R] [inst : OrderedSemiring S] extends MulHom :

Type (maxu_1u_2)

The absolute value is nonnegative
nonneg' : ∀ (x : R), 0 ≤ MulHom.toFun toMulHom x
The absolute value is positive definitive
eq_zero' : ∀ (x : R), MulHom.toFun toMulHom x = 0 ↔ x = 0
The absolute value satisfies the triangle inequality
add_le' : ∀ (x y : R), MulHom.toFun toMulHom (x + y) ≤ MulHom.toFun toMulHom x + MulHom.toFun toMulHom y

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.

Instances For

source

ink

instance AbsoluteValue.zeroHomClass {R : Type u_1} {S : Type u_2} [inst : Semiring R] [inst : OrderedSemiring S] :

ZeroHomClass (AbsoluteValue R S) R S

Equations

AbsoluteValue.zeroHomClass = ZeroHomClass.mk (_ : ∀ (f : AbsoluteValue R S), MulHom.toFun f.toMulHom 0 = 0)

source

ink

instance AbsoluteValue.mulHomClass {R : Type u_1} {S : Type u_2} [inst : Semiring R] [inst : OrderedSemiring S] :

MulHomClass (AbsoluteValue R S) R S

Equations

One or more equations did not get rendered due to their size.

source

ink

instance AbsoluteValue.nonnegHomClass {R : Type u_1} {S : Type u_2} [inst : Semiring R] [inst : OrderedSemiring S] :

NonnegHomClass (AbsoluteValue R S) R S

Equations

AbsoluteValue.nonnegHomClass = let src := AbsoluteValue.zeroHomClass; NonnegHomClass.mk (_ : ∀ (f : AbsoluteValue R S) (x : R), 0 ≤ MulHom.toFun f.toMulHom x)

source

ink

instance AbsoluteValue.subadditiveHomClass {R : Type u_1} {S : Type u_2} [inst : Semiring R] [inst : OrderedSemiring S] :

SubadditiveHomClass (AbsoluteValue R S) R S

Equations

One or more equations did not get rendered due to their size.

source

ink

@[simp]

theorem AbsoluteValue.coe_mk {R : Type u_1} {S : Type u_2} [inst : Semiring R] [inst : OrderedSemiring S] (f : R →ₙ* S) {h₁ : ∀ (x : R), 0 ≤ MulHom.toFun f x} {h₂ : ∀ (x : R), MulHom.toFun f x = 0 ↔ x = 0} {h₃ : ∀ (x y : R), MulHom.toFun f (x + y) ≤ MulHom.toFun f x + MulHom.toFun f y} :

↑{ toMulHom := f, nonneg' := h₁, eq_zero' := h₂, add_le' := h₃ } = ↑f

source

ink

theorem AbsoluteValue.ext {R : Type u_1} {S : Type u_2} [inst : Semiring R] [inst : OrderedSemiring S] ⦃f : AbsoluteValue R S⦄ ⦃g : AbsoluteValue R S⦄ :

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

source

ink

def AbsoluteValue.Simps.apply {R : Type u_1} {S : Type u_2} [inst : Semiring R] [inst : OrderedSemiring S] (f : AbsoluteValue R S) :

R → S

See Note [custom simps projection].

Equations

AbsoluteValue.Simps.apply f = ↑f

source

ink

@[simp]

theorem AbsoluteValue.coe_toMulHom {R : Type u_1} {S : Type u_2} [inst : Semiring R] [inst : OrderedSemiring S] (abv : AbsoluteValue R S) :

abv.toMulHom = ↑abv

source

ink

theorem AbsoluteValue.nonneg {R : Type u_2} {S : Type u_1} [inst : Semiring R] [inst : OrderedSemiring S] (abv : AbsoluteValue R S) (x : R) :

0 ≤ ↑abv x

source

ink

@[simp]

theorem AbsoluteValue.eq_zero {R : Type u_2} {S : Type u_1} [inst : Semiring R] [inst : OrderedSemiring S] (abv : AbsoluteValue R S) {x : R} :

↑abv x = 0 ↔ x = 0

source

ink

theorem AbsoluteValue.add_le {R : Type u_2} {S : Type u_1} [inst : Semiring R] [inst : OrderedSemiring S] (abv : AbsoluteValue R S) (x : R) (y : R) :

↑abv (x + y) ≤ ↑abv x + ↑abv y

source

ink

theorem AbsoluteValue.ne_zero_iff {R : Type u_2} {S : Type u_1} [inst : Semiring R] [inst : OrderedSemiring S] (abv : AbsoluteValue R S) {x : R} :

↑abv x ≠ 0 ↔ x ≠ 0

source

ink

theorem AbsoluteValue.pos {R : Type u_1} {S : Type u_2} [inst : Semiring R] [inst : OrderedSemiring S] (abv : AbsoluteValue R S) {x : R} (hx : x ≠ 0) :

0 < ↑abv x

source

ink

@[simp]

theorem AbsoluteValue.pos_iff {R : Type u_2} {S : Type u_1} [inst : Semiring R] [inst : OrderedSemiring S] (abv : AbsoluteValue R S) {x : R} :

0 < ↑abv x ↔ x ≠ 0

source

ink

theorem AbsoluteValue.ne_zero {R : Type u_1} {S : Type u_2} [inst : Semiring R] [inst : OrderedSemiring S] (abv : AbsoluteValue R S) {x : R} (hx : x ≠ 0) :

↑abv x ≠ 0

source

ink

theorem AbsoluteValue.map_one_of_isLeftRegular {R : Type u_2} {S : Type u_1} [inst : Semiring R] [inst : OrderedSemiring S] (abv : AbsoluteValue R S) (h : IsLeftRegular (↑abv 1)) :

↑abv 1 = 1

source

ink

theorem AbsoluteValue.sub_le {R : Type u_2} {S : Type u_1} [inst : Ring R] [inst : OrderedSemiring S] (abv : AbsoluteValue R S) (a : R) (b : R) (c : R) :

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

source

ink

@[simp]

theorem AbsoluteValue.map_sub_eq_zero_iff {R : Type u_2} {S : Type u_1} [inst : Ring R] [inst : OrderedSemiring S] (abv : AbsoluteValue R S) (a : R) (b : R) :

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

source

ink

@[simp]

theorem AbsoluteValue.map_one {R : Type u_2} {S : Type u_1} [inst : Semiring R] [inst : OrderedRing S] (abv : AbsoluteValue R S) [inst : IsDomain S] [inst : Nontrivial R] :

↑abv 1 = 1

source

ink

instance AbsoluteValue.instMonoidWithZeroHomClassAbsoluteValueToOrderedSemiringToMulZeroOneClassToNonAssocSemiringToMulZeroOneClassToNonAssocSemiringToNonAssocRingToRing {R : Type u_1} {S : Type u_2} [inst : Semiring R] [inst : OrderedRing S] [inst : IsDomain S] [inst : Nontrivial R] :

MonoidWithZeroHomClass (AbsoluteValue R S) R S

Equations

One or more equations did not get rendered due to their size.

source

ink

def AbsoluteValue.toMonoidWithZeroHom {R : Type u_1} {S : Type u_2} [inst : Semiring R] [inst : OrderedRing S] (abv : AbsoluteValue R S) [inst : IsDomain S] [inst : Nontrivial R] :

R →*₀ S

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

Equations

AbsoluteValue.toMonoidWithZeroHom abv = ↑abv

source

ink

@[simp]

theorem AbsoluteValue.coe_toMonoidWithZeroHom {R : Type u_1} {S : Type u_2} [inst : Semiring R] [inst : OrderedRing S] (abv : AbsoluteValue R S) [inst : IsDomain S] [inst : Nontrivial R] :

↑(AbsoluteValue.toMonoidWithZeroHom abv) = ↑abv

source

ink

def AbsoluteValue.toMonoidHom {R : Type u_1} {S : Type u_2} [inst : Semiring R] [inst : OrderedRing S] (abv : AbsoluteValue R S) [inst : IsDomain S] [inst : Nontrivial R] :

R →* S

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

Equations

AbsoluteValue.toMonoidHom abv = ↑abv

source

ink

@[simp]

theorem AbsoluteValue.coe_toMonoidHom {R : Type u_1} {S : Type u_2} [inst : Semiring R] [inst : OrderedRing S] (abv : AbsoluteValue R S) [inst : IsDomain S] [inst : Nontrivial R] :

↑(AbsoluteValue.toMonoidHom abv) = ↑abv

source

ink

theorem AbsoluteValue.le_sub {R : Type u_2} {S : Type u_1} [inst : Ring R] [inst : OrderedRing S] (abv : AbsoluteValue R S) (a : R) (b : R) :

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

source

ink

@[simp]

theorem AbsoluteValue.map_neg {R : Type u_2} {S : Type u_1} [inst : Ring R] [inst : OrderedCommRing S] (abv : AbsoluteValue R S) [inst : NoZeroDivisors S] (a : R) :

↑abv (-a) = ↑abv a

source

ink

theorem AbsoluteValue.map_sub {R : Type u_2} {S : Type u_1} [inst : Ring R] [inst : OrderedCommRing S] (abv : AbsoluteValue R S) [inst : NoZeroDivisors S] (a : R) (b : R) :

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

source

ink

@[simp]

theorem AbsoluteValue.abs_apply {S : Type u_1} [inst : LinearOrderedRing S] :

∀ (a : S), ↑AbsoluteValue.abs a = abs a

source

ink

def AbsoluteValue.abs {S : Type u_1} [inst : LinearOrderedRing S] :

AbsoluteValue S S

AbsoluteValue.abs is abs as a bundled AbsoluteValue.

Equations

One or more equations did not get rendered due to their size.

source

ink

instance AbsoluteValue.instInhabitedAbsoluteValueToSemiringToStrictOrderedSemiringToLinearOrderedSemiringToOrderedSemiring {S : Type u_1} [inst : LinearOrderedRing S] :

Inhabited (AbsoluteValue S S)

Equations

AbsoluteValue.instInhabitedAbsoluteValueToSemiringToStrictOrderedSemiringToLinearOrderedSemiringToOrderedSemiring = { default := AbsoluteValue.abs }

source

ink

theorem AbsoluteValue.abs_abv_sub_le_abv_sub {R : Type u_2} {S : Type u_1} [inst : Ring R] [inst : LinearOrderedCommRing S] (abv : AbsoluteValue R S) (a : R) (b : R) :

abs (↑abv a - ↑abv b) ≤ ↑abv (a - b)

source

ink

class IsAbsoluteValue {S : Type u_1} [inst : OrderedSemiring S] {R : Type u_2} [inst : Semiring R] (f : R → S) :

Prop

The absolute value is nonnegative
abv_nonneg' : ∀ (x : R), 0 ≤ f x
The absolute value is positive definitive
abv_eq_zero' : ∀ {x : R}, f x = 0 ↔ x = 0
The absolute value satisfies the triangle inequality
abv_add' : ∀ (x y : R), f (x + y) ≤ f x + f y
The absolute value is multiplicative
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 AbsoluteValue which represents a bundled version of absolute values.

Instances

source

ink

theorem IsAbsoluteValue.abv_nonneg {S : Type u_1} [inst : OrderedSemiring S] {R : Type u_2} [inst : Semiring R] (abv : R → S) [inst : IsAbsoluteValue abv] (x : R) :

0 ≤ abv x

source

ink

theorem IsAbsoluteValue.abv_eq_zero {S : Type u_1} [inst : OrderedSemiring S] {R : Type u_2} [inst : Semiring R] (abv : R → S) [inst : IsAbsoluteValue abv] {x : R} :

abv x = 0 ↔ x = 0

source

ink

theorem IsAbsoluteValue.abv_add {S : Type u_1} [inst : OrderedSemiring S] {R : Type u_2} [inst : Semiring R] (abv : R → S) [inst : IsAbsoluteValue abv] (x : R) (y : R) :

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

source

ink

theorem IsAbsoluteValue.abv_mul {S : Type u_1} [inst : OrderedSemiring S] {R : Type u_2} [inst : Semiring R] (abv : R → S) [inst : IsAbsoluteValue abv] (x : R) (y : R) :

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

source

ink

instance AbsoluteValue.isAbsoluteValue {S : Type u_1} [inst : OrderedSemiring S] {R : Type u_2} [inst : Semiring R] (abv : AbsoluteValue R S) :

IsAbsoluteValue ↑abv

A bundled absolute value is an absolute value.

Equations

@AbsoluteValue.isAbsoluteValue = @AbsoluteValue.isAbsoluteValue.proof_1

source

ink

@[simp]

theorem IsAbsoluteValue.toAbsoluteValue_apply {S : Type u_1} [inst : OrderedSemiring S] {R : Type u_2} [inst : Semiring R] (abv : R → S) [inst : IsAbsoluteValue abv] :

∀ (a : R), ↑(IsAbsoluteValue.toAbsoluteValue abv) a = abv a

source

ink

def IsAbsoluteValue.toAbsoluteValue {S : Type u_1} [inst : OrderedSemiring S] {R : Type u_2} [inst : Semiring R] (abv : R → S) [inst : IsAbsoluteValue abv] :

AbsoluteValue R S

Convert an unbundled IsAbsoluteValue to a bundled AbsoluteValue.

Equations

One or more equations did not get rendered due to their size.

source

ink

theorem IsAbsoluteValue.abv_zero {S : Type u_1} [inst : OrderedSemiring S] {R : Type u_2} [inst : Semiring R] (abv : R → S) [inst : IsAbsoluteValue abv] :

abv 0 = 0

source

ink

theorem IsAbsoluteValue.abv_pos {S : Type u_1} [inst : OrderedSemiring S] {R : Type u_2} [inst : Semiring R] (abv : R → S) [inst : IsAbsoluteValue abv] {a : R} :

0 < abv a ↔ a ≠ 0

source

ink

instance IsAbsoluteValue.abs_isAbsoluteValue {S : Type u_1} [inst : LinearOrderedRing S] :

IsAbsoluteValue abs

Equations

@IsAbsoluteValue.abs_isAbsoluteValue = @IsAbsoluteValue.abs_isAbsoluteValue.proof_1

source

ink

theorem IsAbsoluteValue.abv_one {S : Type u_2} [inst : OrderedRing S] {R : Type u_1} [inst : Semiring R] (abv : R → S) [inst : IsAbsoluteValue abv] [inst : IsDomain S] [inst : Nontrivial R] :

abv 1 = 1

source

ink

def IsAbsoluteValue.abvHom {S : Type u_1} [inst : OrderedRing S] {R : Type u_2} [inst : Semiring R] (abv : R → S) [inst : IsAbsoluteValue abv] [inst : IsDomain S] [inst : Nontrivial R] :

R →*₀ S

abv as a MonoidWithZeroHom.

Equations

IsAbsoluteValue.abvHom abv = AbsoluteValue.toMonoidWithZeroHom (IsAbsoluteValue.toAbsoluteValue abv)

source

ink

theorem IsAbsoluteValue.abv_pow {S : Type u_2} [inst : OrderedRing S] {R : Type u_1} [inst : Semiring R] [inst : IsDomain S] [inst : Nontrivial R] (abv : R → S) [inst : IsAbsoluteValue abv] (a : R) (n : ℕ) :

abv (a ^ n) = abv a ^ n

source

ink

theorem IsAbsoluteValue.abv_sub_le {S : Type u_1} [inst : OrderedRing S] {R : Type u_2} [inst : Ring R] (abv : R → S) [inst : IsAbsoluteValue abv] (a : R) (b : R) (c : R) :

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

source

ink

theorem IsAbsoluteValue.sub_abv_le_abv_sub {S : Type u_1} [inst : OrderedRing S] {R : Type u_2} [inst : Ring R] (abv : R → S) [inst : IsAbsoluteValue abv] (a : R) (b : R) :

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

source

ink

theorem IsAbsoluteValue.abv_neg {S : Type u_1} [inst : OrderedCommRing S] {R : Type u_2} [inst : Ring R] (abv : R → S) [inst : IsAbsoluteValue abv] [inst : NoZeroDivisors S] (a : R) :

abv (-a) = abv a

source

ink

theorem IsAbsoluteValue.abv_sub {S : Type u_1} [inst : OrderedCommRing S] {R : Type u_2} [inst : Ring R] (abv : R → S) [inst : IsAbsoluteValue abv] [inst : NoZeroDivisors S] (a : R) (b : R) :

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

source

ink

theorem IsAbsoluteValue.abs_abv_sub_le_abv_sub {S : Type u_1} [inst : LinearOrderedCommRing S] {R : Type u_2} [inst : Ring R] (abv : R → S) [inst : IsAbsoluteValue abv] (a : R) (b : R) :

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

source

ink

theorem IsAbsoluteValue.abv_one' {S : Type u_1} [inst : LinearOrderedSemifield S] {R : Type u_2} [inst : Semiring R] [inst : Nontrivial R] (abv : R → S) [inst : IsAbsoluteValue abv] :

abv 1 = 1

source

ink

def IsAbsoluteValue.abvHom' {S : Type u_1} [inst : LinearOrderedSemifield S] {R : Type u_2} [inst : Semiring R] [inst : Nontrivial R] (abv : R → S) [inst : IsAbsoluteValue abv] :

R →*₀ S

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

Equations

IsAbsoluteValue.abvHom' abv = { toZeroHom := { toFun := abv, map_zero' := (_ : abv 0 = 0) }, map_one' := (_ : abv 1 = 1), map_mul' := (_ : ∀ (x y : R), abv (x * y) = abv x * abv y) }

source

ink

theorem IsAbsoluteValue.abv_inv {S : Type u_1} [inst : LinearOrderedSemifield S] {R : Type u_2} [inst : DivisionSemiring R] (abv : R → S) [inst : IsAbsoluteValue abv] (a : R) :

abv a⁻¹ = (abv a)⁻¹

source

ink

theorem IsAbsoluteValue.abv_div {S : Type u_1} [inst : LinearOrderedSemifield S] {R : Type u_2} [inst : DivisionSemiring R] (abv : R → S) [inst : IsAbsoluteValue abv] (a : R) (b : R) :

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