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_5) (S : Type u_6) [Semiring R] [OrderedSemiring S] extends MulHom :
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
    instance AbsoluteValue.funLike {R : Type u_5} {S : Type u_6} [Semiring R] [OrderedSemiring S] :
    Equations
    • AbsoluteValue.funLike = { coe := fun (f : AbsoluteValue R S) => f.toFun, coe_injective' := }
    Equations
    • =
    instance AbsoluteValue.mulHomClass {R : Type u_5} {S : Type u_6} [Semiring R] [OrderedSemiring S] :
    Equations
    • =
    Equations
    • =
    Equations
    • =
    @[simp]
    theorem AbsoluteValue.coe_mk {R : Type u_5} {S : Type u_6} [Semiring R] [OrderedSemiring 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] [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_5} {S : Type u_6} [Semiring R] [OrderedSemiring S] (f : AbsoluteValue R S) :
    RS

    See Note [custom simps projection].

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

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

      Equations
      • AbsoluteValue.instCoeFunAbsoluteValueForAll = DFunLike.hasCoeToFun
      @[simp]
      theorem AbsoluteValue.coe_toMulHom {R : Type u_5} {S : Type u_6} [Semiring R] [OrderedSemiring S] (abv : AbsoluteValue R S) :
      abv.toMulHom = abv
      theorem AbsoluteValue.nonneg {R : Type u_5} {S : Type u_6} [Semiring R] [OrderedSemiring 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] [OrderedSemiring 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] [OrderedSemiring S] (abv : AbsoluteValue R S) (x : R) (y : R) :
      abv (x + y) abv x + abv y
      theorem AbsoluteValue.map_mul {R : Type u_5} {S : Type u_6} [Semiring R] [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_5} {S : Type u_6} [Semiring R] [OrderedSemiring S] (abv : AbsoluteValue R S) {x : R} :
      abv x 0 x 0
      theorem AbsoluteValue.pos {R : Type u_5} {S : Type u_6} [Semiring R] [OrderedSemiring S] (abv : AbsoluteValue R S) {x : R} (hx : x 0) :
      0 < abv x
      @[simp]
      theorem AbsoluteValue.pos_iff {R : Type u_5} {S : Type u_6} [Semiring R] [OrderedSemiring S] (abv : AbsoluteValue R S) {x : R} :
      0 < abv x x 0
      theorem AbsoluteValue.ne_zero {R : Type u_5} {S : Type u_6} [Semiring R] [OrderedSemiring S] (abv : AbsoluteValue R S) {x : R} (hx : x 0) :
      abv x 0
      theorem AbsoluteValue.map_one_of_isLeftRegular {R : Type u_5} {S : Type u_6} [Semiring R] [OrderedSemiring S] (abv : AbsoluteValue R S) (h : IsLeftRegular (abv 1)) :
      abv 1 = 1
      theorem AbsoluteValue.map_zero {R : Type u_5} {S : Type u_6} [Semiring R] [OrderedSemiring S] (abv : AbsoluteValue R S) :
      abv 0 = 0
      theorem AbsoluteValue.sub_le {R : Type u_5} {S : Type u_6} [Ring R] [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_5} {S : Type u_6} [Ring R] [OrderedSemiring S] (abv : AbsoluteValue R S) (a : R) (b : R) :
      abv (a - b) = 0 a = b
      theorem AbsoluteValue.map_one {R : Type u_5} {S : Type u_6} [Semiring R] [OrderedRing S] (abv : AbsoluteValue R S) [IsDomain S] [Nontrivial R] :
      abv 1 = 1

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

      Equations
      Instances For
        @[simp]
        def AbsoluteValue.toMonoidHom {R : Type u_5} {S : Type u_6} [Semiring R] [OrderedRing 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.

        Equations
        Instances For
          @[simp]
          theorem AbsoluteValue.coe_toMonoidHom {R : Type u_5} {S : Type u_6} [Semiring R] [OrderedRing S] (abv : AbsoluteValue R S) [IsDomain S] [Nontrivial R] :
          theorem AbsoluteValue.map_pow {R : Type u_5} {S : Type u_6} [Semiring R] [OrderedRing S] (abv : AbsoluteValue R S) [IsDomain S] [Nontrivial R] (a : R) (n : ) :
          abv (a ^ n) = abv a ^ n
          theorem AbsoluteValue.le_sub {R : Type u_5} {S : Type u_6} [Ring R] [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_3} {S : Type u_4} [OrderedCommRing 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} [OrderedCommRing S] [Ring R] (abv : AbsoluteValue R S) [NoZeroDivisors S] (a : R) (b : R) :
          abv (a - b) = abv (b - a)
          theorem AbsoluteValue.le_add {R : Type u_3} {S : Type u_4} [OrderedCommRing S] [Ring R] (abv : AbsoluteValue R S) [NoZeroDivisors S] (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} [OrderedCommRing S] [Ring R] (abv : AbsoluteValue R S) [NoZeroDivisors S] (a : R) (b : R) :
          abv (a - b) abv a + abv b

          Bound abv (a - b) from above

          @[simp]
          theorem AbsoluteValue.abs_apply {S : Type u_6} [LinearOrderedRing S] (a : S) :
          AbsoluteValue.abs a = |a|
          @[simp]
          theorem AbsoluteValue.abs_toFun {S : Type u_6} [LinearOrderedRing S] (a : S) :
          AbsoluteValue.abs a = |a|

          AbsoluteValue.abs is abs as a bundled AbsoluteValue.

          Equations
          • AbsoluteValue.abs = { toMulHom := { toFun := abs, map_mul' := }, nonneg' := , eq_zero' := , add_le' := }
          Instances For
            Equations
            • AbsoluteValue.instInhabitedAbsoluteValueToSemiringToStrictOrderedSemiringToLinearOrderedSemiringToOrderedSemiring = { default := AbsoluteValue.abs }
            theorem AbsoluteValue.abs_abv_sub_le_abv_sub {R : Type u_5} {S : Type u_6} [Ring R] [LinearOrderedCommRing S] (abv : AbsoluteValue R S) (a : R) (b : R) :
            |abv a - abv b| abv (a - b)
            class IsAbsoluteValue {S : Type u_5} [OrderedSemiring S] {R : Type u_6} [Semiring R] (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} [OrderedSemiring S] {R : Type u_6} [Semiring R] (abv : RS) [IsAbsoluteValue abv] (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} [OrderedSemiring S] {R : Type u_6} [Semiring R] (abv : RS) [IsAbsoluteValue abv] {x : R} :
                abv x = 0 x = 0
                theorem IsAbsoluteValue.abv_add {S : Type u_5} [OrderedSemiring S] {R : Type u_6} [Semiring R] (abv : RS) [IsAbsoluteValue abv] (x : R) (y : R) :
                abv (x + y) abv x + abv y
                theorem IsAbsoluteValue.abv_mul {S : Type u_5} [OrderedSemiring S] {R : Type u_6} [Semiring R] (abv : RS) [IsAbsoluteValue abv] (x : R) (y : R) :
                abv (x * y) = abv x * abv y
                instance AbsoluteValue.isAbsoluteValue {S : Type u_5} [OrderedSemiring S] {R : Type u_6} [Semiring R] (abv : AbsoluteValue R S) :

                A bundled absolute value is an absolute value.

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

                Convert an unbundled IsAbsoluteValue to a bundled AbsoluteValue.

                Equations
                Instances For
                  theorem IsAbsoluteValue.abv_zero {S : Type u_5} [OrderedSemiring S] {R : Type u_6} [Semiring R] (abv : RS) [IsAbsoluteValue abv] :
                  abv 0 = 0
                  theorem IsAbsoluteValue.abv_pos {S : Type u_5} [OrderedSemiring S] {R : Type u_6} [Semiring R] (abv : RS) [IsAbsoluteValue abv] {a : R} :
                  0 < abv a a 0
                  theorem IsAbsoluteValue.abv_one {S : Type u_5} [OrderedRing S] {R : Type u_6} [Semiring R] (abv : RS) [IsAbsoluteValue abv] [IsDomain S] [Nontrivial R] :
                  abv 1 = 1
                  theorem IsAbsoluteValue.abv_pow {S : Type u_5} [OrderedRing S] {R : Type u_6} [Semiring R] [IsDomain S] [Nontrivial R] (abv : RS) [IsAbsoluteValue abv] (a : R) (n : ) :
                  abv (a ^ n) = abv a ^ n
                  theorem IsAbsoluteValue.abv_sub_le {S : Type u_5} [OrderedRing S] {R : Type u_6} [Ring R] (abv : RS) [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_5} [OrderedRing S] {R : Type u_6} [Ring R] (abv : RS) [IsAbsoluteValue abv] (a : R) (b : R) :
                  abv a - abv b abv (a - b)
                  theorem IsAbsoluteValue.abv_neg {R : Type u_3} {S : Type u_4} [OrderedCommRing S] [NoZeroDivisors S] [Ring R] (abv : RS) [IsAbsoluteValue abv] (a : R) :
                  abv (-a) = abv a
                  theorem IsAbsoluteValue.abv_sub {R : Type u_3} {S : Type u_4} [OrderedCommRing S] [NoZeroDivisors S] [Ring R] (abv : RS) [IsAbsoluteValue abv] (a : R) (b : R) :
                  abv (a - b) = abv (b - a)
                  theorem IsAbsoluteValue.abs_abv_sub_le_abv_sub {S : Type u_5} [LinearOrderedCommRing S] {R : Type u_6} [Ring R] (abv : RS) [IsAbsoluteValue abv] (a : R) (b : R) :
                  |abv a - abv b| abv (a - b)
                  theorem IsAbsoluteValue.abv_one' {S : Type u_5} [LinearOrderedSemifield S] {R : Type u_6} [Semiring R] [Nontrivial R] (abv : RS) [IsAbsoluteValue abv] :
                  abv 1 = 1
                  def IsAbsoluteValue.abvHom' {S : Type u_5} [LinearOrderedSemifield S] {R : Type u_6} [Semiring R] [Nontrivial R] (abv : RS) [IsAbsoluteValue abv] :

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

                  Equations
                  Instances For
                    theorem IsAbsoluteValue.abv_inv {S : Type u_5} [LinearOrderedSemifield S] {R : Type u_6} [DivisionSemiring R] (abv : RS) [IsAbsoluteValue abv] (a : R) :
                    abv a⁻¹ = (abv a)⁻¹
                    theorem IsAbsoluteValue.abv_div {S : Type u_5} [LinearOrderedSemifield S] {R : Type u_6} [DivisionSemiring R] (abv : RS) [IsAbsoluteValue abv] (a : R) (b : R) :
                    abv (a / b) = abv a / abv b