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) [Semiring R] [Semiring S] [PartialOrder S] extends R →ₙ* S : 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 inequality.

• toFun : R → S
• 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

@[implicit_reducible]

instance AbsoluteValue.funLike {R : Type u_5} {S : Type u_6} [Semiring R] [Semiring S] [PartialOrder S] : FunLike (AbsoluteValue R S) R S

instance AbsoluteValue.zeroHomClass {R : Type u_5} {S : Type u_6} [Semiring R] [Semiring S] [PartialOrder S] : ZeroHomClass (AbsoluteValue R S) R S

instance AbsoluteValue.mulHomClass {R : Type u_5} {S : Type u_6} [Semiring R] [Semiring S] [PartialOrder S] : MulHomClass (AbsoluteValue R S) R S

instance AbsoluteValue.nonnegHomClass {R : Type u_5} {S : Type u_6} [Semiring R] [Semiring S] [PartialOrder S] : NonnegHomClass (AbsoluteValue R S) R S

instance AbsoluteValue.subadditiveHomClass {R : Type u_5} {S : Type u_6} [Semiring R] [Semiring S] [PartialOrder S] : SubadditiveHomClass (AbsoluteValue R S) R S

@[simp]

theorem AbsoluteValue.coe_mk {R : Type u_5} {S : Type u_6} [Semiring R] [Semiring S] [PartialOrder S] (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} [Semiring R] [Semiring S] [PartialOrder S] ⦃f g : AbsoluteValue R S⦄ : (∀ (x : R), f x = g x) → f = g

theorem AbsoluteValue.ext_iff {R : Type u_5} {S : Type u_6} [Semiring R] [Semiring S] [PartialOrder S] {f g : AbsoluteValue R S} : f = g ↔ ∀ (x : R), f x = g x

def AbsoluteValue.Simps.apply {R : Type u_5} {S : Type u_6} [Semiring R] [Semiring S] [PartialOrder S] (f : AbsoluteValue R S) : R → S

See Note [custom simps projection].

@[simp]

theorem AbsoluteValue.coe_toMulHom {R : Type u_5} {S : Type u_6} [Semiring R] [Semiring S] [PartialOrder S] (abv : AbsoluteValue R S) : ⇑abv.toMulHom = ⇑abv

theorem AbsoluteValue.nonneg {R : Type u_5} {S : Type u_6} [Semiring R] [Semiring S] [PartialOrder S] (abv : AbsoluteValue R S) (x : R) : 0 ≤ abv x

@[simp]

theorem AbsoluteValue.eq_zero {R : Type u_5} {S : Type u_6} [Semiring R] [Semiring S] [PartialOrder S] (abv : AbsoluteValue R S) {x : R} : abv x = 0 ↔ x = 0

theorem AbsoluteValue.add_le {R : Type u_5} {S : Type u_6} [Semiring R] [Semiring S] [PartialOrder S] (abv : AbsoluteValue R S) (x y : R) : abv (x + y) ≤ abv x + abv y

theorem AbsoluteValue.listSum_le {R : Type u_5} {S : Type u_6} [Semiring R] [Semiring S] [PartialOrder S] (abv : AbsoluteValue R S) [AddLeftMono S] (l : List R) : abv l.sum ≤ (List.map (⇑abv) l).sum

The triangle inequality for an AbsoluteValue applied to a list.

@[simp]

theorem AbsoluteValue.map_mul {R : Type u_5} {S : Type u_6} [Semiring R] [Semiring S] [PartialOrder S] (abv : AbsoluteValue R S) (x y : R) : abv (x * y) = abv x * abv y

theorem AbsoluteValue.ne_zero_iff {R : Type u_5} {S : Type u_6} [Semiring R] [Semiring S] [PartialOrder S] (abv : AbsoluteValue R S) {x : R} : abv x ≠ 0 ↔ x ≠ 0

theorem AbsoluteValue.ne_zero {R : Type u_5} {S : Type u_6} [Semiring R] [Semiring S] [PartialOrder S] (abv : AbsoluteValue R S) {x : R} : x ≠ 0 → abv x ≠ 0

Alias of the reverse direction of AbsoluteValue.ne_zero_iff.

@[simp]

theorem AbsoluteValue.pos_iff {R : Type u_5} {S : Type u_6} [Semiring R] [Semiring S] [PartialOrder S] (abv : AbsoluteValue R S) {x : R} : 0 < abv x ↔ x ≠ 0

theorem AbsoluteValue.pos {R : Type u_5} {S : Type u_6} [Semiring R] [Semiring S] [PartialOrder S] (abv : AbsoluteValue R S) {x : R} : x ≠ 0 → 0 < abv x

Alias of the reverse direction of AbsoluteValue.pos_iff.

@[simp]

theorem AbsoluteValue.nonpos_iff {R : Type u_5} {S : Type u_6} [Semiring R] [Semiring S] [PartialOrder S] (abv : AbsoluteValue R S) {x : R} : abv x ≤ 0 ↔ x = 0

theorem AbsoluteValue.map_one_of_isLeftRegular {R : Type u_5} {S : Type u_6} [Semiring R] [Semiring S] [PartialOrder S] (abv : AbsoluteValue R S) (h : IsLeftRegular (abv 1)) : abv 1 = 1

@[simp]

theorem AbsoluteValue.map_zero {R : Type u_5} {S : Type u_6} [Semiring R] [Semiring S] [PartialOrder S] (abv : AbsoluteValue R S) : abv 0 = 0

theorem AbsoluteValue.sub_le {R : Type u_5} {S : Type u_6} [Ring R] [Semiring S] [PartialOrder S] (abv : AbsoluteValue R S) (a b 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] [Semiring S] [PartialOrder S] (abv : AbsoluteValue R S) (a b : R) : abv (a - b) = 0 ↔ a = b

@[simp]

theorem AbsoluteValue.map_one {R : Type u_5} {S : Type u_6} [Semiring R] [Semiring S] [PartialOrder S] (abv : AbsoluteValue R S) [IsDomain S] [Nontrivial R] : abv 1 = 1

instance AbsoluteValue.monoidWithZeroHomClass {R : Type u_5} {S : Type u_6} [Semiring R] [Semiring S] [PartialOrder S] [IsDomain S] [Nontrivial R] : MonoidWithZeroHomClass (AbsoluteValue R S) R S

def AbsoluteValue.toMonoidWithZeroHom {R : Type u_5} {S : Type u_6} [Semiring R] [Semiring S] [PartialOrder S] (abv : AbsoluteValue R S) [IsDomain S] [Nontrivial R] : R →*₀ S

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

@[simp]

theorem AbsoluteValue.coe_toMonoidWithZeroHom {R : Type u_5} {S : Type u_6} [Semiring R] [Semiring S] [PartialOrder S] (abv : AbsoluteValue R S) [IsDomain S] [Nontrivial R] : ⇑abv.toMonoidWithZeroHom = ⇑abv

def AbsoluteValue.toMonoidHom {R : Type u_5} {S : Type u_6} [Semiring R] [Semiring S] [PartialOrder S] (abv : AbsoluteValue R S) [IsDomain S] [Nontrivial R] : R →* S

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

@[simp]

theorem AbsoluteValue.coe_toMonoidHom {R : Type u_5} {S : Type u_6} [Semiring R] [Semiring S] [PartialOrder S] (abv : AbsoluteValue R S) [IsDomain S] [Nontrivial R] : ⇑abv.toMonoidHom = ⇑abv

@[simp]

theorem AbsoluteValue.map_pow {R : Type u_5} {S : Type u_6} [Semiring R] [Semiring S] [PartialOrder S] (abv : AbsoluteValue R S) [IsDomain S] [Nontrivial R] (a : R) (n : ℕ) : abv (a ^ n) = abv a ^ n

theorem AbsoluteValue.apply_nat_le_self {R : Type u_5} {S : Type u_6} [Semiring R] [Semiring S] [PartialOrder S] (abv : AbsoluteValue R S) [IsDomain S] [IsOrderedRing S] (n : ℕ) : abv ↑n ≤ ↑n

An absolute value satisfies f (n : R) ≤ n for every n : ℕ.

theorem AbsoluteValue.le_sub {R : Type u_5} {S : Type u_6} [Ring R] [Ring S] [PartialOrder S] [IsOrderedRing S] (abv : AbsoluteValue R S) (a b : R) : abv a - abv b ≤ abv (a - b)

theorem AbsoluteValue.map_neg {R : Type u_3} {S : Type u_4} [CommRing S] [PartialOrder S] [IsOrderedRing S] [Ring R] (abv : AbsoluteValue R S) [NoZeroDivisors S] (a : R) : abv (-a) = abv a

theorem AbsoluteValue.map_sub {R : Type u_3} {S : Type u_4} [CommRing S] [PartialOrder S] [IsOrderedRing S] [Ring R] (abv : AbsoluteValue R S) [NoZeroDivisors S] (a b : R) : abv (a - b) = abv (b - a)

theorem AbsoluteValue.le_add {R : Type u_3} {S : Type u_4} [CommRing S] [PartialOrder S] [IsOrderedRing S] [Ring R] (abv : AbsoluteValue R S) [NoZeroDivisors S] (a 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} [CommRing S] [PartialOrder S] [IsOrderedRing S] [Ring R] (abv : AbsoluteValue R S) [NoZeroDivisors S] (a b : R) : abv (a - b) ≤ abv a + abv b

Bound abv (a - b) from above

instance AbsoluteValue.addGroupSeminormClass {R : Type u_3} {S : Type u_4} [CommRing S] [PartialOrder S] [IsOrderedRing S] [Ring R] [NoZeroDivisors S] : AddGroupSeminormClass (AbsoluteValue R S) R S

instance AbsoluteValue.instMulRingNormClassOfNontrivialOfIsDomain {R : Type u_3} {S : Type u_4} [CommRing S] [PartialOrder S] [IsOrderedRing S] [Ring R] [NoZeroDivisors S] [Nontrivial R] [IsDomain S] : MulRingNormClass (AbsoluteValue R S) R S

theorem AbsoluteValue.apply_natAbs_eq {R : Type u_3} {S : Type u_4} [CommRing S] [PartialOrder S] [IsOrderedRing S] [Ring R] (abv : AbsoluteValue R S) [NoZeroDivisors S] (x : ℤ) : abv ↑x.natAbs = abv ↑x

theorem AbsoluteValue.eq_on_nat_iff_eq_on_int {R : Type u_3} {S : Type u_4} [CommRing S] [PartialOrder S] [IsOrderedRing S] [Ring R] [NoZeroDivisors S] {f g : AbsoluteValue R S} : (∀ (n : ℕ), f ↑n = g ↑n) ↔ ∀ (n : ℤ), f ↑n = g ↑n

Values of an absolute value coincide on the image of ℕ in R if and only if they coincide on the image of ℤ in R.

def AbsoluteValue.abs {S : Type u_6} [Ring S] [LinearOrder S] [IsStrictOrderedRing S] : AbsoluteValue S S

AbsoluteValue.abs is abs as a bundled AbsoluteValue.

@[simp]

theorem AbsoluteValue.abs_apply {S : Type u_6} [Ring S] [LinearOrder S] [IsStrictOrderedRing S] (a : S) : AbsoluteValue.abs a = |a|

@[implicit_reducible]

instance AbsoluteValue.instInhabited {S : Type u_6} [Ring S] [LinearOrder S] [IsStrictOrderedRing S] : Inhabited (AbsoluteValue S S)

theorem AbsoluteValue.abs_abv_sub_le_abv_sub {R : Type u_5} {S : Type u_6} [Ring R] [CommRing S] [LinearOrder S] [IsStrictOrderedRing S] (abv : AbsoluteValue R S) (a b : R) : |abv a - abv b| ≤ abv (a - b)

def AbsoluteValue.trivial {R : Type u_5} [Semiring R] [DecidablePred fun (x : R) => x = 0] [NoZeroDivisors R] {S : Type u_6} [Semiring S] [PartialOrder S] [IsOrderedRing S] [Nontrivial S] : AbsoluteValue R S

The trivial absolute value takes the value 1 on all nonzero elements.

@[simp]

theorem AbsoluteValue.trivial_apply {R : Type u_5} [Semiring R] [DecidablePred fun (x : R) => x = 0] [NoZeroDivisors R] {S : Type u_6} [Semiring S] [PartialOrder S] [IsOrderedRing S] [Nontrivial S] {x : R} (hx : x ≠ 0) : AbsoluteValue.trivial x = 1

def AbsoluteValue.IsNontrivial {R : Type u_5} [Semiring R] {S : Type u_6} [Semiring S] [PartialOrder S] (v : AbsoluteValue R S) : Prop

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.

theorem AbsoluteValue.isNontrivial_iff_ne_trivial {R : Type u_5} [Semiring R] {S : Type u_6} [Semiring S] [PartialOrder S] [IsOrderedRing S] [DecidablePred fun (x : R) => x = 0] [NoZeroDivisors R] [Nontrivial S] (v : AbsoluteValue R S) : v.IsNontrivial ↔ v ≠ AbsoluteValue.trivial

theorem AbsoluteValue.not_isNontrivial_iff {R : Type u_5} [Semiring R] {S : Type u_6} [Semiring S] [PartialOrder S] (v : AbsoluteValue R S) : ¬v.IsNontrivial ↔ ∀ (x : R), x ≠ 0 → v x = 1

@[simp]

theorem AbsoluteValue.not_isNontrivial_apply {R : Type u_5} [Semiring R] {S : Type u_6} [Semiring S] [PartialOrder S] {v : AbsoluteValue R S} (hv : ¬v.IsNontrivial) {x : R} (hx : x ≠ 0) : v x = 1

theorem AbsoluteValue.IsNontrivial.exists_abv_gt_one {R : Type u_3} {S : Type u_4} [Field R] [Semifield S] [LinearOrder S] [IsStrictOrderedRing S] [ExistsAddOfLE S] {v : AbsoluteValue R S} (h : v.IsNontrivial) : ∃ (x : R), 1 < v x

theorem AbsoluteValue.IsNontrivial.exists_abv_lt_one {R : Type u_3} {S : Type u_4} [Field R] [Semifield S] [LinearOrder S] [IsStrictOrderedRing S] [ExistsAddOfLE S] {v : AbsoluteValue R S} (h : v.IsNontrivial) : ∃ (x : R), x ≠ 0 ∧ v x < 1

class IsAbsoluteValue {S : Type u_5} [Semiring S] [PartialOrder S] {R : Type u_6} [Semiring R] (f : R → S) : Prop

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

theorem IsAbsoluteValue.abv_nonneg {S : Type u_5} [Semiring S] [PartialOrder S] {R : Type u_6} [Semiring R] (abv : R → S) [IsAbsoluteValue abv] (x : R) : 0 ≤ abv x

def IsAbsoluteValue.Mathlib.Meta.Positivity.evalAbv : Mathlib.Meta.Positivity.PositivityExt

The positivity extension which identifies expressions of the form abv a. For performance reasons, we only attempt to apply this when abv is a variable. If it is an explicit function, e.g. |_| or ‖_‖, another extension should apply.

theorem IsAbsoluteValue.abv_eq_zero {S : Type u_5} [Semiring S] [PartialOrder S] {R : Type u_6} [Semiring R] (abv : R → S) [IsAbsoluteValue abv] {x : R} : abv x = 0 ↔ x = 0

theorem IsAbsoluteValue.abv_add {S : Type u_5} [Semiring S] [PartialOrder S] {R : Type u_6} [Semiring R] (abv : R → S) [IsAbsoluteValue abv] (x y : R) : abv (x + y) ≤ abv x + abv y

theorem IsAbsoluteValue.abv_mul {S : Type u_5} [Semiring S] [PartialOrder S] {R : Type u_6} [Semiring R] (abv : R → S) [IsAbsoluteValue abv] (x y : R) : abv (x * y) = abv x * abv y

instance AbsoluteValue.isAbsoluteValue {S : Type u_5} [Semiring S] [PartialOrder S] {R : Type u_6} [Semiring R] (abv : AbsoluteValue R S) : IsAbsoluteValue ⇑abv

A bundled absolute value is an absolute value.

def IsAbsoluteValue.toAbsoluteValue {S : Type u_5} [Semiring S] [PartialOrder S] {R : Type u_6} [Semiring R] (abv : R → S) [IsAbsoluteValue abv] : AbsoluteValue R S

Convert an unbundled IsAbsoluteValue to a bundled AbsoluteValue.

@[simp]

theorem IsAbsoluteValue.toAbsoluteValue_apply {S : Type u_5} [Semiring S] [PartialOrder S] {R : Type u_6} [Semiring R] (abv : R → S) [IsAbsoluteValue abv] (a✝ : R) : (toAbsoluteValue abv) a✝ = abv a✝

theorem IsAbsoluteValue.abv_zero {S : Type u_5} [Semiring S] [PartialOrder S] {R : Type u_6} [Semiring R] (abv : R → S) [IsAbsoluteValue abv] : abv 0 = 0

theorem IsAbsoluteValue.abv_pos {S : Type u_5} [Semiring S] [PartialOrder S] {R : Type u_6} [Semiring R] (abv : R → S) [IsAbsoluteValue abv] {a : R} : 0 < abv a ↔ a ≠ 0

instance IsAbsoluteValue.abs_isAbsoluteValue {S : Type u_5} [Ring S] [LinearOrder S] [IsStrictOrderedRing S] : IsAbsoluteValue abs

theorem IsAbsoluteValue.abv_one {S : Type u_5} [Ring S] [PartialOrder S] {R : Type u_6} [Semiring R] (abv : R → S) [IsAbsoluteValue abv] [IsDomain S] [Nontrivial R] : abv 1 = 1

def IsAbsoluteValue.abvHom {S : Type u_5} [Ring S] [PartialOrder S] {R : Type u_6} [Semiring R] (abv : R → S) [IsAbsoluteValue abv] [IsDomain S] [Nontrivial R] : R →*₀ S

abv as a MonoidWithZeroHom.

theorem IsAbsoluteValue.abv_pow {S : Type u_5} [Ring S] [PartialOrder S] {R : Type u_6} [Semiring R] [IsDomain S] [Nontrivial R] (abv : R → S) [IsAbsoluteValue abv] (a : R) (n : ℕ) : abv (a ^ n) = abv a ^ n

theorem IsAbsoluteValue.abv_sub_le {S : Type u_5} [Ring S] [PartialOrder S] {R : Type u_6} [Ring R] (abv : R → S) [IsAbsoluteValue abv] (a b c : R) : abv (a - c) ≤ abv (a - b) + abv (b - c)

theorem IsAbsoluteValue.sub_abv_le_abv_sub {S : Type u_5} [Ring S] [PartialOrder S] {R : Type u_6} [Ring R] (abv : R → S) [IsAbsoluteValue abv] [IsOrderedRing S] (a b : R) : abv a - abv b ≤ abv (a - b)

theorem IsAbsoluteValue.abv_neg {R : Type u_3} {S : Type u_4} [CommRing S] [PartialOrder S] [IsOrderedRing S] [NoZeroDivisors S] [Ring R] (abv : R → S) [IsAbsoluteValue abv] (a : R) : abv (-a) = abv a

theorem IsAbsoluteValue.abv_sub {R : Type u_3} {S : Type u_4} [CommRing S] [PartialOrder S] [IsOrderedRing S] [NoZeroDivisors S] [Ring R] (abv : R → S) [IsAbsoluteValue abv] (a b : R) : abv (a - b) = abv (b - a)

theorem IsAbsoluteValue.abs_abv_sub_le_abv_sub {S : Type u_5} [CommRing S] [LinearOrder S] [IsStrictOrderedRing S] {R : Type u_6} [Ring R] (abv : R → S) [IsAbsoluteValue abv] (a b : R) : |abv a - abv b| ≤ abv (a - b)

theorem IsAbsoluteValue.abv_one' {S : Type u_5} [Semiring S] [PartialOrder S] [IsCancelMulZero S] {R : Type u_6} [Semiring R] [Nontrivial R] (abv : R → S) [IsAbsoluteValue abv] : abv 1 = 1

def IsAbsoluteValue.abvHom' {S : Type u_5} [Semiring S] [PartialOrder S] [IsCancelMulZero S] {R : Type u_6} [Semiring R] [Nontrivial R] (abv : R → S) [IsAbsoluteValue abv] : R →*₀ S

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

theorem IsAbsoluteValue.abv_inv {S : Type u_5} [Semifield S] [LinearOrder S] {R : Type u_6} [DivisionSemiring R] (abv : R → S) [IsAbsoluteValue abv] (a : R) : abv a⁻¹ = (abv a)⁻¹

theorem IsAbsoluteValue.abv_div {S : Type u_5} [Semifield S] [LinearOrder S] {R : Type u_6} [DivisionSemiring R] (abv : R → S) [IsAbsoluteValue abv] (a b : R) : abv (a / b) = abv a / abv b