Documentation

Mathlib.Algebra.Order.AbsoluteValue

Absolute values #

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

Main definitions #

structure AbsoluteValue (R : Type u_1) (S : Type u_2) [inst : Semiring R] [inst : OrderedSemiring S] extends MulHom :
Type (maxu_1u_2)

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
    instance AbsoluteValue.zeroHomClass {R : Type u_1} {S : Type u_2} [inst : Semiring R] [inst : OrderedSemiring S] :
    Equations
    instance AbsoluteValue.mulHomClass {R : Type u_1} {S : Type u_2} [inst : Semiring R] [inst : OrderedSemiring S] :
    Equations
    • One or more equations did not get rendered due to their size.
    instance AbsoluteValue.nonnegHomClass {R : Type u_1} {S : Type u_2} [inst : Semiring R] [inst : OrderedSemiring S] :
    Equations
    instance AbsoluteValue.subadditiveHomClass {R : Type u_1} {S : Type u_2} [inst : Semiring R] [inst : OrderedSemiring S] :
    Equations
    • One or more equations did not get rendered due to their size.
    @[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
    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
    def AbsoluteValue.Simps.apply {R : Type u_1} {S : Type u_2} [inst : Semiring R] [inst : OrderedSemiring S] (f : AbsoluteValue R S) :
    RS

    See Note [custom simps projection].

    Equations
    @[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
    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
    @[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
    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
    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
    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
    @[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
    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
    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
    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)
    @[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
    @[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
    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] :

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

    Equations
    @[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] :
    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
    @[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] :
    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)
    @[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
    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)
    @[simp]
    theorem AbsoluteValue.abs_apply {S : Type u_1} [inst : LinearOrderedRing S] :
    ∀ (a : S), AbsoluteValue.abs a = abs a

    AbsoluteValue.abs is abs as a bundled AbsoluteValue.

    Equations
    • One or more equations did not get rendered due to their size.
    Equations
    • AbsoluteValue.instInhabitedAbsoluteValueToSemiringToStrictOrderedSemiringToLinearOrderedSemiringToOrderedSemiring = { default := AbsoluteValue.abs }
    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)
    class IsAbsoluteValue {S : Type u_1} [inst : OrderedSemiring S] {R : Type u_2} [inst : Semiring R] (f : RS) :
    • 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
      theorem IsAbsoluteValue.abv_nonneg {S : Type u_1} [inst : OrderedSemiring S] {R : Type u_2} [inst : Semiring R] (abv : RS) [inst : IsAbsoluteValue abv] (x : R) :
      0 abv x
      theorem IsAbsoluteValue.abv_eq_zero {S : Type u_1} [inst : OrderedSemiring S] {R : Type u_2} [inst : Semiring R] (abv : RS) [inst : IsAbsoluteValue abv] {x : R} :
      abv x = 0 x = 0
      theorem IsAbsoluteValue.abv_add {S : Type u_1} [inst : OrderedSemiring S] {R : Type u_2} [inst : Semiring R] (abv : RS) [inst : IsAbsoluteValue abv] (x : R) (y : R) :
      abv (x + y) abv x + abv y
      theorem IsAbsoluteValue.abv_mul {S : Type u_1} [inst : OrderedSemiring S] {R : Type u_2} [inst : Semiring R] (abv : RS) [inst : IsAbsoluteValue abv] (x : R) (y : R) :
      abv (x * y) = abv x * abv y
      instance AbsoluteValue.isAbsoluteValue {S : Type u_1} [inst : OrderedSemiring S] {R : Type u_2} [inst : Semiring R] (abv : AbsoluteValue R S) :

      A bundled absolute value is an absolute value.

      Equations
      @[simp]
      theorem IsAbsoluteValue.toAbsoluteValue_apply {S : Type u_1} [inst : OrderedSemiring S] {R : Type u_2} [inst : Semiring R] (abv : RS) [inst : IsAbsoluteValue abv] :
      ∀ (a : R), ↑(IsAbsoluteValue.toAbsoluteValue abv) a = abv a
      def IsAbsoluteValue.toAbsoluteValue {S : Type u_1} [inst : OrderedSemiring S] {R : Type u_2} [inst : Semiring R] (abv : RS) [inst : IsAbsoluteValue abv] :

      Convert an unbundled IsAbsoluteValue to a bundled AbsoluteValue.

      Equations
      • One or more equations did not get rendered due to their size.
      theorem IsAbsoluteValue.abv_zero {S : Type u_1} [inst : OrderedSemiring S] {R : Type u_2} [inst : Semiring R] (abv : RS) [inst : IsAbsoluteValue abv] :
      abv 0 = 0
      theorem IsAbsoluteValue.abv_pos {S : Type u_1} [inst : OrderedSemiring S] {R : Type u_2} [inst : Semiring R] (abv : RS) [inst : IsAbsoluteValue abv] {a : R} :
      0 < abv a a 0
      theorem IsAbsoluteValue.abv_one {S : Type u_2} [inst : OrderedRing S] {R : Type u_1} [inst : Semiring R] (abv : RS) [inst : IsAbsoluteValue abv] [inst : IsDomain S] [inst : Nontrivial R] :
      abv 1 = 1
      def IsAbsoluteValue.abvHom {S : Type u_1} [inst : OrderedRing S] {R : Type u_2} [inst : Semiring R] (abv : RS) [inst : IsAbsoluteValue abv] [inst : IsDomain S] [inst : Nontrivial R] :

      abv as a MonoidWithZeroHom.

      Equations
      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 : RS) [inst : IsAbsoluteValue abv] (a : R) (n : ) :
      abv (a ^ n) = abv a ^ n
      theorem IsAbsoluteValue.abv_sub_le {S : Type u_1} [inst : OrderedRing S] {R : Type u_2} [inst : Ring R] (abv : RS) [inst : IsAbsoluteValue abv] (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_1} [inst : OrderedRing S] {R : Type u_2} [inst : Ring R] (abv : RS) [inst : IsAbsoluteValue abv] (a : R) (b : R) :
      abv a - abv b abv (a - b)
      theorem IsAbsoluteValue.abv_neg {S : Type u_1} [inst : OrderedCommRing S] {R : Type u_2} [inst : Ring R] (abv : RS) [inst : IsAbsoluteValue abv] [inst : NoZeroDivisors S] (a : R) :
      abv (-a) = abv a
      theorem IsAbsoluteValue.abv_sub {S : Type u_1} [inst : OrderedCommRing S] {R : Type u_2} [inst : Ring R] (abv : RS) [inst : IsAbsoluteValue abv] [inst : NoZeroDivisors S] (a : R) (b : R) :
      abv (a - b) = abv (b - a)
      theorem IsAbsoluteValue.abs_abv_sub_le_abv_sub {S : Type u_1} [inst : LinearOrderedCommRing S] {R : Type u_2} [inst : Ring R] (abv : RS) [inst : IsAbsoluteValue abv] (a : R) (b : R) :
      abs (abv a - abv b) abv (a - b)
      theorem IsAbsoluteValue.abv_one' {S : Type u_1} [inst : LinearOrderedSemifield S] {R : Type u_2} [inst : Semiring R] [inst : Nontrivial R] (abv : RS) [inst : IsAbsoluteValue abv] :
      abv 1 = 1
      def IsAbsoluteValue.abvHom' {S : Type u_1} [inst : LinearOrderedSemifield S] {R : Type u_2} [inst : Semiring R] [inst : Nontrivial R] (abv : RS) [inst : IsAbsoluteValue abv] :

      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) }
      theorem IsAbsoluteValue.abv_inv {S : Type u_1} [inst : LinearOrderedSemifield S] {R : Type u_2} [inst : DivisionSemiring R] (abv : RS) [inst : IsAbsoluteValue abv] (a : R) :
      abv a⁻¹ = (abv a)⁻¹
      theorem IsAbsoluteValue.abv_div {S : Type u_1} [inst : LinearOrderedSemifield S] {R : Type u_2} [inst : DivisionSemiring R] (abv : RS) [inst : IsAbsoluteValue abv] (a : R) (b : R) :
      abv (a / b) = abv a / abv b