Documentation

Mathlib.Analysis.Normed.Ring.SeminormFromConst

SeminormFromConst #

In this file, we prove [BGR, Proposition 1.3.2/2][bosch-guntzer-remmert] : starting from a power-multiplicative seminorm on a commutative ring R and a nonzero c : R, we create a new power-multiplicative seminorm for which c is multiplicative.

Main Definitions #

Main Results #

References #

Tags #

SeminormFromConst, Seminorm, Nonarchimedean

def seminormFromConst_seq {R : Type u_1} [CommRing R] (c : R) (f : RingSeminorm R) (x : R) :

For a ring seminorm f on R and c ∈ R, the sequence given by (f (x * c^n))/((f c)^n).

Equations
Instances For
    theorem seminormFromConst_seq_def {R : Type u_1} [CommRing R] (c : R) (f : RingSeminorm R) (x : R) :
    seminormFromConst_seq c f x = fun (n : ) => f (x * c ^ n) / f c ^ n
    theorem seminormFromConst_seq_nonneg {R : Type u_1} [CommRing R] (c : R) (f : RingSeminorm R) (x : R) :

    The terms in the sequence seminormFromConst_seq c f x are nonnegative.

    theorem seminormFromConst_bddBelow {R : Type u_1} [CommRing R] (c : R) (f : RingSeminorm R) (x : R) :

    The image of seminormFromConst_seq c f x is bounded below by zero.

    theorem seminormFromConst_seq_zero {R : Type u_1} [CommRing R] (c : R) {f : RingSeminorm R} (hf : f 0 = 0) :

    seminormFromConst_seq c f 0 is the constant sequence zero.

    theorem seminormFromConst_seq_one {R : Type u_1} [CommRing R] {c : R} {f : RingSeminorm R} (hc : f c 0) (hpm : IsPowMul f) (n : ) (hn : 1 n) :

    If 1 ≤ n, then seminormFromConst_seq c f 1 n = 1.

    theorem seminormFromConst_seq_antitone {R : Type u_1} [CommRing R] {c : R} {f : RingSeminorm R} (hf1 : f 1 1) (hc : f c 0) (hpm : IsPowMul f) (x : R) :

    seminormFromConst_seq c f x is antitone.

    def seminormFromConst' {R : Type u_1} [CommRing R] {c : R} {f : RingSeminorm R} (hf1 : f 1 1) (hc : f c 0) (hpm : IsPowMul f) (x : R) :

    The real-valued function sending x ∈ R to the limit of (f (x * c^n))/((f c)^n).

    Equations
    Instances For
      theorem seminormFromConst_isLimit {R : Type u_1} [CommRing R] {c : R} {f : RingSeminorm R} (hf1 : f 1 1) (hc : f c 0) (hpm : IsPowMul f) (x : R) :
      Filter.Tendsto (seminormFromConst_seq c f x) Filter.atTop (nhds (seminormFromConst' hf1 hc hpm x))

      We prove that seminormFromConst' hf1 hc hpm x is the limit of the sequence seminormFromConst_seq c f x as n tends to infinity.

      theorem seminormFromConst_one {R : Type u_1} [CommRing R] {c : R} {f : RingSeminorm R} (hf1 : f 1 1) (hc : f c 0) (hpm : IsPowMul f) :
      seminormFromConst' hf1 hc hpm 1 = 1

      seminormFromConst' hf1 hc hpm 1 = 1.

      def seminormFromConst {R : Type u_1} [CommRing R] {c : R} {f : RingSeminorm R} (hf1 : f 1 1) (hc : f c 0) (hpm : IsPowMul f) :

      The function seminormFromConst is a RingSeminorm on R.

      Equations
      Instances For
        theorem seminormFromConst_def {R : Type u_1} [CommRing R] {c : R} {f : RingSeminorm R} (hf1 : f 1 1) (hc : f c 0) (hpm : IsPowMul f) (x : R) :
        (seminormFromConst hf1 hc hpm) x = seminormFromConst' hf1 hc hpm x
        theorem seminormFromConst_one_le {R : Type u_1} [CommRing R] {c : R} {f : RingSeminorm R} (hf1 : f 1 1) (hc : f c 0) (hpm : IsPowMul f) :
        seminormFromConst' hf1 hc hpm 1 1

        seminormFromConst' hf1 hc hpm 1 ≤ 1.

        theorem seminormFromConst_isNonarchimedean {R : Type u_1} [CommRing R] {c : R} {f : RingSeminorm R} (hf1 : f 1 1) (hc : f c 0) (hpm : IsPowMul f) (hna : IsNonarchimedean f) :

        The function seminormFromConst' hf1 hc hpm is nonarchimedean.

        theorem seminormFromConst_isPowMul {R : Type u_1} [CommRing R] {c : R} {f : RingSeminorm R} (hf1 : f 1 1) (hc : f c 0) (hpm : IsPowMul f) :

        The function seminormFromConst' hf1 hc hpm is power-multiplicative.

        theorem seminormFromConst_le_seminorm {R : Type u_1} [CommRing R] {c : R} {f : RingSeminorm R} (hf1 : f 1 1) (hc : f c 0) (hpm : IsPowMul f) (x : R) :
        seminormFromConst' hf1 hc hpm x f x

        The function seminormFromConst' hf1 hc hpm is bounded above by x.

        theorem seminormFromConst_apply_of_isMul {R : Type u_1} [CommRing R] {c : R} {f : RingSeminorm R} (hf1 : f 1 1) (hc : f c 0) (hpm : IsPowMul f) {x : R} (hx : ∀ (y : R), f (x * y) = f x * f y) :
        seminormFromConst' hf1 hc hpm x = f x

        If x : R is multiplicative for f, then seminormFromConst' hf1 hc hpm x = f x.

        theorem seminormFromConst_isMul_of_isMul {R : Type u_1} [CommRing R] {c : R} {f : RingSeminorm R} (hf1 : f 1 1) (hc : f c 0) (hpm : IsPowMul f) {x : R} (hx : ∀ (y : R), f (x * y) = f x * f y) (y : R) :
        seminormFromConst' hf1 hc hpm (x * y) = seminormFromConst' hf1 hc hpm x * seminormFromConst' hf1 hc hpm y

        If x : R is multiplicative for f, then it is multiplicative for seminormFromConst' hf1 hc hpm.

        theorem seminormFromConst_apply_c {R : Type u_1} [CommRing R] {c : R} {f : RingSeminorm R} (hf1 : f 1 1) (hc : f c 0) (hpm : IsPowMul f) :
        seminormFromConst' hf1 hc hpm c = f c

        seminormFromConst' hf1 hc hpm c = f c.

        theorem seminormFromConst_const_mul {R : Type u_1} [CommRing R] {c : R} {f : RingSeminorm R} (hf1 : f 1 1) (hc : f c 0) (hpm : IsPowMul f) (x : R) :
        seminormFromConst' hf1 hc hpm (c * x) = seminormFromConst' hf1 hc hpm c * seminormFromConst' hf1 hc hpm x

        For every x : R, seminormFromConst' hf1 hc hpm (c * x) equals the product seminormFromConst' hf1 hc hpm c * SeminormFromConst' hf1 hc hpm x.

        def normFromConst {K : Type u_1} [Field K] {k : K} {g : RingSeminorm K} (hg1 : g 1 1) (hg_k : g k 0) (hg_pm : IsPowMul g) :

        If K is a field, the function seminormFromConst is a RingNorm on K.

        Equations
        Instances For
          theorem seminormFromConstRingNormOfField_def {K : Type u_1} [Field K] {k : K} {g : RingSeminorm K} (hg1 : g 1 1) (hg_k : g k 0) (hg_pm : IsPowMul g) (x : K) :
          (normFromConst hg1 hg_k hg_pm) x = seminormFromConst' hg1 hg_k hg_pm x