Documentation

Mathlib.Algebra.Order.AbsoluteValue.Basic

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] [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 : 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] [Semiring S] [PartialOrder S] :
    Equations
      @[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) :
      RS

      See Note [custom simps projection].

      Equations
        Instances For
          @[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 0abv 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 00 < abv x

          Alias of the reverse direction of AbsoluteValue.pos_iff.

          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

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

          Equations
            Instances For
              @[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.

              Equations
                Instances For
                  @[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)
                  @[simp]
                  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

                  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.

                  AbsoluteValue.abs is abs as a bundled AbsoluteValue.

                  Equations
                    Instances For
                      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] :

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

                      Equations
                        Instances For
                          @[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) :
                          def AbsoluteValue.IsNontrivial {R : Type u_5} [Semiring R] {S : Type u_6} [Semiring S] [PartialOrder S] (v : AbsoluteValue R S) :

                          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.

                          Equations
                            Instances For
                              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 0v 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 : 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} [Semiring S] [PartialOrder 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
                                  Instances For
                                    theorem IsAbsoluteValue.abv_eq_zero {S : Type u_5} [Semiring S] [PartialOrder 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} [Semiring S] [PartialOrder S] {R : Type u_6} [Semiring R] (abv : RS) [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 : RS) [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) :

                                    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 : RS) [IsAbsoluteValue abv] :

                                    Convert an unbundled IsAbsoluteValue to a bundled AbsoluteValue.

                                    Equations
                                      Instances For
                                        @[simp]
                                        theorem IsAbsoluteValue.toAbsoluteValue_apply {S : Type u_5} [Semiring S] [PartialOrder S] {R : Type u_6} [Semiring R] (abv : RS) [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 : RS) [IsAbsoluteValue abv] :
                                        abv 0 = 0
                                        theorem IsAbsoluteValue.abv_pos {S : Type u_5} [Semiring S] [PartialOrder 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} [Ring S] [PartialOrder S] {R : Type u_6} [Semiring R] (abv : RS) [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 : RS) [IsAbsoluteValue abv] [IsDomain S] [Nontrivial R] :

                                        abv as a MonoidWithZeroHom.

                                        Equations
                                          Instances For
                                            theorem IsAbsoluteValue.abv_pow {S : Type u_5} [Ring S] [PartialOrder 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} [Ring S] [PartialOrder S] {R : Type u_6} [Ring R] (abv : RS) [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 : RS) [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 : RS) [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 : RS) [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 : RS) [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 : RS) [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 : 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} [Semifield S] [LinearOrder 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} [Semifield S] [LinearOrder S] {R : Type u_6} [DivisionSemiring R] (abv : RS) [IsAbsoluteValue abv] (a b : R) :
                                                abv (a / b) = abv a / abv b