Documentation

Mathlib.Analysis.Normed.Ring.Seminorm

Seminorms and norms on rings #

This file defines seminorms and norms on rings. These definitions are useful when one needs to consider multiple (semi)norms on a given ring.

Main declarations #

For a ring R:

Notes #

The corresponding hom classes are defined in Mathlib.Analysis.Order.Hom.Basic to be used by absolute values.

References #

Tags #

ring_seminorm, ring_norm

structure RingSeminorm (R : Type u_4) [NonUnitalNonAssocRing R] extends AddGroupSeminorm :
Type u_4

A seminorm on a ring R is a function f : R → ℝ that preserves zero, takes nonnegative values, is subadditive and submultiplicative and such that f (-x) = f x for all x ∈ R.

  • toFun : R
  • map_zero' : self.toFun 0 = 0
  • add_le' : ∀ (r s : R), self.toFun (r + s) self.toFun r + self.toFun s
  • neg' : ∀ (r : R), self.toFun (-r) = self.toFun r
  • mul_le' : ∀ (x y : R), self.toFun (x * y) self.toFun x * self.toFun y

    The property of a RingSeminorm that for all x and y in the ring, the norm of x * y is less than the norm of x times the norm of y.

Instances For
    theorem RingSeminorm.mul_le' {R : Type u_4} [NonUnitalNonAssocRing R] (self : RingSeminorm R) (x : R) (y : R) :
    self.toFun (x * y) self.toFun x * self.toFun y

    The property of a RingSeminorm that for all x and y in the ring, the norm of x * y is less than the norm of x times the norm of y.

    structure RingNorm (R : Type u_4) [NonUnitalNonAssocRing R] extends RingSeminorm :
    Type u_4

    A function f : R → ℝ is a norm on a (nonunital) ring if it is a seminorm and f x = 0 implies x = 0.

    • toFun : R
    • map_zero' : self.toFun 0 = 0
    • add_le' : ∀ (r s : R), self.toFun (r + s) self.toFun r + self.toFun s
    • neg' : ∀ (r : R), self.toFun (-r) = self.toFun r
    • mul_le' : ∀ (x y : R), self.toFun (x * y) self.toFun x * self.toFun y
    • eq_zero_of_map_eq_zero' : ∀ (x : R), self.toFun x = 0x = 0

      If the image under the seminorm is zero, then the argument is zero.

    Instances For
      structure MulRingSeminorm (R : Type u_4) [NonAssocRing R] extends AddGroupSeminorm :
      Type u_4

      A multiplicative seminorm on a ring R is a function f : R → ℝ that preserves zero and multiplication, takes nonnegative values, is subadditive and such that f (-x) = f x for all x.

      • toFun : R
      • map_zero' : self.toFun 0 = 0
      • add_le' : ∀ (r s : R), self.toFun (r + s) self.toFun r + self.toFun s
      • neg' : ∀ (r : R), self.toFun (-r) = self.toFun r
      • map_one' : self.toFun 1 = 1

        The proposition that the function preserves 1

      • map_mul' : ∀ (x y : R), self.toFun (x * y) = self.toFun x * self.toFun y

        The proposition that the function preserves multiplication

      Instances For
        structure MulRingNorm (R : Type u_4) [NonAssocRing R] extends MulRingSeminorm :
        Type u_4

        A multiplicative norm on a ring R is a multiplicative ring seminorm such that f x = 0 implies x = 0.

        • toFun : R
        • map_zero' : self.toFun 0 = 0
        • add_le' : ∀ (r s : R), self.toFun (r + s) self.toFun r + self.toFun s
        • neg' : ∀ (r : R), self.toFun (-r) = self.toFun r
        • map_one' : self.toFun 1 = 1
        • map_mul' : ∀ (x y : R), self.toFun (x * y) = self.toFun x * self.toFun y
        • eq_zero_of_map_eq_zero' : ∀ (x : R), self.toFun x = 0x = 0

          If the image under the seminorm is zero, then the argument is zero.

        Instances For
          Equations
          • RingSeminorm.funLike = { coe := fun (f : RingSeminorm R) => f.toFun, coe_injective' := }
          @[simp]
          theorem RingSeminorm.toFun_eq_coe {R : Type u_2} [NonUnitalRing R] (p : RingSeminorm R) :
          p.toAddGroupSeminorm = p
          theorem RingSeminorm.ext_iff {R : Type u_2} [NonUnitalRing R] {p : RingSeminorm R} {q : RingSeminorm R} :
          p = q ∀ (x : R), p x = q x
          theorem RingSeminorm.ext {R : Type u_2} [NonUnitalRing R] {p : RingSeminorm R} {q : RingSeminorm R} :
          (∀ (x : R), p x = q x)p = q
          Equations
          • RingSeminorm.instZero = { zero := let __src := Zero.zero; { toAddGroupSeminorm := __src, mul_le' := } }
          theorem RingSeminorm.eq_zero_iff {R : Type u_2} [NonUnitalRing R] {p : RingSeminorm R} :
          p = 0 ∀ (x : R), p x = 0
          theorem RingSeminorm.ne_zero_iff {R : Type u_2} [NonUnitalRing R] {p : RingSeminorm R} :
          p 0 ∃ (x : R), p x 0
          Equations
          • RingSeminorm.instInhabited = { default := 0 }

          The trivial seminorm on a ring R is the RingSeminorm taking value 0 at 0 and 1 at every other element.

          Equations
          • RingSeminorm.instOneOfDecidableEq = { one := let __src := 1; { toAddGroupSeminorm := __src, mul_le' := } }
          @[simp]
          theorem RingSeminorm.apply_one {R : Type u_2} [NonUnitalRing R] [DecidableEq R] (x : R) :
          1 x = if x = 0 then 0 else 1
          theorem RingSeminorm.seminorm_one_eq_one_iff_ne_zero {R : Type u_2} [Ring R] (p : RingSeminorm R) (hp : p 1 1) :
          p 1 = 1 p 0
          theorem map_pow_le_pow {F : Type u_4} {α : Type u_5} [Ring α] [FunLike F α ] [RingSeminormClass F α ] (f : F) (a : α) {n : } :
          n 0f (a ^ n) f a ^ n

          If f is a ring seminorm on a, then ∀ {n : ℕ}, n ≠ 0 → f (a ^ n) ≤ f a ^ n.

          theorem map_pow_le_pow' {F : Type u_4} {α : Type u_5} [Ring α] [FunLike F α ] [RingSeminormClass F α ] {f : F} (hf1 : f 1 1) (a : α) (n : ) :
          f (a ^ n) f a ^ n

          If f is a ring seminorm on a with f 1 ≤ 1, then ∀ (n : ℕ), f (a ^ n) ≤ f a ^ n.

          The norm of a NonUnitalSeminormedRing as a RingSeminorm.

          Equations
          • normRingSeminorm R = { toFun := norm, map_zero' := , add_le' := , neg' := , mul_le' := }
          Instances For
            instance RingNorm.funLike {R : Type u_2} [NonUnitalRing R] :
            Equations
            • RingNorm.funLike = { coe := fun (f : RingNorm R) => f.toFun, coe_injective' := }
            Equations
            • =
            theorem RingNorm.toFun_eq_coe {R : Type u_2} [NonUnitalRing R] (p : RingNorm R) :
            p.toFun = p
            theorem RingNorm.ext_iff {R : Type u_2} [NonUnitalRing R] {p : RingNorm R} {q : RingNorm R} :
            p = q ∀ (x : R), p x = q x
            theorem RingNorm.ext {R : Type u_2} [NonUnitalRing R] {p : RingNorm R} {q : RingNorm R} :
            (∀ (x : R), p x = q x)p = q

            The trivial norm on a ring R is the RingNorm taking value 0 at 0 and 1 at every other element.

            Equations
            @[simp]
            theorem RingNorm.apply_one (R : Type u_2) [NonUnitalRing R] [DecidableEq R] (x : R) :
            1 x = if x = 0 then 0 else 1
            Equations
            • MulRingSeminorm.funLike = { coe := fun (f : MulRingSeminorm R) => f.toFun, coe_injective' := }
            @[simp]
            theorem MulRingSeminorm.toFun_eq_coe {R : Type u_2} [NonAssocRing R] (p : MulRingSeminorm R) :
            p.toAddGroupSeminorm = p
            theorem MulRingSeminorm.ext_iff {R : Type u_2} [NonAssocRing R] {p : MulRingSeminorm R} {q : MulRingSeminorm R} :
            p = q ∀ (x : R), p x = q x
            theorem MulRingSeminorm.ext {R : Type u_2} [NonAssocRing R] {p : MulRingSeminorm R} {q : MulRingSeminorm R} :
            (∀ (x : R), p x = q x)p = q

            The trivial seminorm on a ring R is the MulRingSeminorm taking value 0 at 0 and 1 at every other element.

            Equations
            • MulRingSeminorm.instOne = { one := let __src := 1; { toAddGroupSeminorm := __src, map_one' := , map_mul' := } }
            @[simp]
            theorem MulRingSeminorm.apply_one {R : Type u_2} [NonAssocRing R] [DecidableEq R] [NoZeroDivisors R] [Nontrivial R] (x : R) :
            1 x = if x = 0 then 0 else 1
            Equations
            • MulRingSeminorm.instInhabited = { default := 1 }
            Equations
            • MulRingNorm.funLike = { coe := fun (f : MulRingNorm R) => f.toFun, coe_injective' := }
            theorem MulRingNorm.toFun_eq_coe {R : Type u_2} [NonAssocRing R] (p : MulRingNorm R) :
            p.toFun = p
            theorem MulRingNorm.ext_iff {R : Type u_2} [NonAssocRing R] {p : MulRingNorm R} {q : MulRingNorm R} :
            p = q ∀ (x : R), p x = q x
            theorem MulRingNorm.ext {R : Type u_2} [NonAssocRing R] {p : MulRingNorm R} {q : MulRingNorm R} :
            (∀ (x : R), p x = q x)p = q

            The trivial norm on a ring R is the MulRingNorm taking value 0 at 0 and 1 at every other element.

            Equations
            • MulRingNorm.instOne R = { one := let __src := 1; let __src_1 := 1; { toMulRingSeminorm := __src, eq_zero_of_map_eq_zero' := } }
            @[simp]
            theorem MulRingNorm.apply_one (R : Type u_2) [NonAssocRing R] [DecidableEq R] [NoZeroDivisors R] [Nontrivial R] (x : R) :
            1 x = if x = 0 then 0 else 1
            def MulRingNorm.equiv {R : Type u_4} [Ring R] (f : MulRingNorm R) (g : MulRingNorm R) :

            Two multiplicative ring norms f, g on R are equivalent if there exists a positive constant c such that for all x ∈ R, (f x)^c = g x.

            Equations
            • f.equiv g = ∃ (c : ), 0 < c (fun (x : R) => f x ^ c) = g
            Instances For
              theorem MulRingNorm.equiv_refl {R : Type u_4} [Ring R] (f : MulRingNorm R) :
              f.equiv f

              Equivalence of multiplicative ring norms is reflexive.

              theorem MulRingNorm.equiv_symm {R : Type u_4} [Ring R] {f : MulRingNorm R} {g : MulRingNorm R} (hfg : f.equiv g) :
              g.equiv f

              Equivalence of multiplicative ring norms is symmetric.

              theorem MulRingNorm.equiv_trans {R : Type u_4} [Ring R] {f : MulRingNorm R} {g : MulRingNorm R} {k : MulRingNorm R} (hfg : f.equiv g) (hgk : g.equiv k) :
              f.equiv k

              Equivalence of multiplicative ring norms is transitive.

              def RingSeminorm.toRingNorm {K : Type u_4} [Field K] (f : RingSeminorm K) (hnt : f 0) :

              A nonzero ring seminorm on a field K is a ring norm.

              Equations
              • f.toRingNorm hnt = { toRingSeminorm := f, eq_zero_of_map_eq_zero' := }
              Instances For
                @[simp]
                theorem normRingNorm_toFun (R : Type u_4) [NonUnitalNormedRing R] :
                ∀ (a : R), (normRingNorm R).toFun a = a

                The norm of a NonUnitalNormedRing as a RingNorm.

                Equations
                Instances For
                  theorem MulRingNorm_nat_le_nat {R : Type u_4} [Ring R] (n : ) (f : MulRingNorm R) :
                  f n n

                  A multiplicative ring norm satisfies f n ≤ n for every n : ℕ.

                  theorem MulRingNorm.apply_natAbs_eq {R : Type u_4} [Ring R] (x : ) (f : MulRingNorm R) :
                  f x.natAbs = f x

                  A multiplicative norm composed with the absolute value on integers equals the norm itself.

                  The seminorm on a SeminormedRing, as a RingSeminorm.

                  Equations
                  Instances For
                    @[simp]
                    theorem NormedRing.toRingNorm_toFun (R : Type u_4) [NormedRing R] :
                    ∀ (a : R), (NormedRing.toRingNorm R).toFun a = a

                    The norm on a NormedRing, as a RingNorm.

                    Equations
                    • NormedRing.toRingNorm R = { toFun := norm, map_zero' := , add_le' := , neg' := , mul_le' := , eq_zero_of_map_eq_zero' := }
                    Instances For
                      @[simp]

                      The norm on a NormedField, as a MulRingNorm.

                      Equations
                      • NormedField.toMulRingNorm R = { toFun := norm, map_zero' := , add_le' := , neg' := , map_one' := , map_mul' := , eq_zero_of_map_eq_zero' := }
                      Instances For