Documentation

Mathlib.Analysis.Normed.Ring.SeminormFromBounded

seminormFromBounded #

In this file, we prove BGR, Proposition 1.2.1/2 : given a nonzero additive group seminorm on a commutative ring R such that for some c : ℝ and every x y : R, the inequality f (x * y) ≤ c * f x * f y) is satisfied, we create a ring seminorm on R.

In the file comments, we will use the expression f is multiplicatively bounded to indicate that this condition holds.

Main Definitions #

Main Results #

References #

Tags #

seminormFromBounded, RingSeminorm, Nonarchimedean

def seminormFromBounded' {R : Type u_1} [CommRing R] (f : R) :
R

The real-valued function sending x ∈ R to the supremum of f(x*y)/f(y), where y runs over the elements of R.

Equations
Instances For
    theorem map_one_ne_zero {R : Type u_1} [CommRing R] {f : R} {c : } (f_ne_zero : f 0) (f_nonneg : 0 f) (f_mul : ∀ (x y : R), f (x * y) c * f x * f y) :
    f 1 0

    If f : R → ℝ is a nonzero, nonnegative, multiplicatively bounded function, then f 1 ≠ 0.

    theorem map_pow_ne_zero {R : Type u_1} [CommRing R] {f : R} {c : } (f_nonneg : 0 f) {x : R} (hx : IsUnit x) (hfx : f x 0) (n : ) (f_mul : ∀ (x y : R), f (x * y) c * f x * f y) :
    f (x ^ n) 0

    If f : R → ℝ is a nonnegative multiplicatively bounded function and x : R is a unit with f x ≠ 0, then for every n : ℕ, we have f (x ^ n) ≠ 0.

    theorem map_mul_zero_of_map_zero {R : Type u_1} [CommRing R] {f : R} {c : } (f_nonneg : 0 f) (f_mul : ∀ (x y : R), f (x * y) c * f x * f y) {x : R} (hx : f x = 0) (y : R) :
    f (x * y) = 0

    If f : R → ℝ is a nonnegative, multiplicatively bounded function, then given x y : R with f x = 0, we have f (x * y) = 0.

    theorem seminormFromBounded_zero {R : Type u_1} [CommRing R] {f : R} (f_zero : f 0 = 0) :

    seminormFromBounded' f preserves 0.

    theorem seminormFromBounded_aux {R : Type u_1} [CommRing R] {f : R} {c : } (f_nonneg : 0 f) (f_mul : ∀ (x y : R), f (x * y) c * f x * f y) (x : R) :
    0 c * f x
    theorem seminormFromBounded_bddAbove_range {R : Type u_1} [CommRing R] {f : R} {c : } (f_nonneg : 0 f) (f_mul : ∀ (x y : R), f (x * y) c * f x * f y) (x : R) :
    BddAbove (Set.range fun (y : R) => f (x * y) / f y)

    If f : R → ℝ is a nonnegative, multiplicatively bounded function, then for every x : R, the image of y ↦ f (x * y) / f y is bounded above.

    theorem seminormFromBounded_le {R : Type u_1} [CommRing R] {f : R} {c : } (f_nonneg : 0 f) (f_mul : ∀ (x y : R), f (x * y) c * f x * f y) (x : R) :

    If f : R → ℝ is a nonnegative, multiplicatively bounded function, then for every x : R, seminormFromBounded' f x is bounded above by some multiple of f x.

    theorem seminormFromBounded_ge {R : Type u_1} [CommRing R] {f : R} {c : } (f_nonneg : 0 f) (f_mul : ∀ (x y : R), f (x * y) c * f x * f y) (x : R) :

    If f : R → ℝ is a nonnegative, multiplicatively bounded function, then for every x : R, f x ≤ f 1 * seminormFromBounded' f x.

    theorem seminormFromBounded_nonneg {R : Type u_1} [CommRing R] {f : R} {c : } (f_nonneg : 0 f) (f_mul : ∀ (x y : R), f (x * y) c * f x * f y) :

    If f : R → ℝ is a nonnegative, multiplicatively bounded function, then seminormFromBounded' f is nonnegative.

    theorem seminormFromBounded_eq_zero_iff {R : Type u_1} [CommRing R] {f : R} {c : } (f_nonneg : 0 f) (f_mul : ∀ (x y : R), f (x * y) c * f x * f y) (x : R) :

    If f : R → ℝ is a nonnegative, multiplicatively bounded function, then seminormFromBounded' f x = 0 if and only if f x = 0.

    theorem seminormFromBounded_neg {R : Type u_1} [CommRing R] {f : R} (f_neg : ∀ (x : R), f (-x) = f x) (x : R) :

    If f is invariant under negation of x, then so is seminormFromBounded'.

    theorem seminormFromBounded_mul {R : Type u_1} [CommRing R] {f : R} {c : } (f_nonneg : 0 f) (f_mul : ∀ (x y : R), f (x * y) c * f x * f y) (x : R) (y : R) :

    If f : R → ℝ is a nonnegative, multiplicatively bounded function, then seminormFromBounded' f is submultiplicative.

    theorem seminormFromBounded_one {R : Type u_1} [CommRing R] {f : R} {c : } (f_ne_zero : f 0) (f_nonneg : 0 f) (f_mul : ∀ (x y : R), f (x * y) c * f x * f y) :

    If f : R → ℝ is a nonzero, nonnegative, multiplicatively bounded function, then seminormFromBounded' f 1 = 1.

    theorem seminormFromBounded_one_le {R : Type u_1} [CommRing R] {f : R} {c : } (f_nonneg : 0 f) (f_mul : ∀ (x y : R), f (x * y) c * f x * f y) :

    If f : R → ℝ is a nonnegative, multiplicatively bounded function, then seminormFromBounded' f 1 ≤ 1.

    theorem seminormFromBounded_add {R : Type u_1} [CommRing R] {f : R} {c : } (f_nonneg : 0 f) (f_mul : ∀ (x y : R), f (x * y) c * f x * f y) (f_add : ∀ (a b : R), f (a + b) f a + f b) (x : R) (y : R) :

    If f : R → ℝ is a nonnegative, multiplicatively bounded, subadditive function, then seminormFromBounded' f is subadditive.

    def seminormFromBounded {R : Type u_1} [CommRing R] {f : R} {c : } (f_zero : f 0 = 0) (f_nonneg : 0 f) (f_mul : ∀ (x y : R), f (x * y) c * f x * f y) (f_add : ∀ (a b : R), f (a + b) f a + f b) (f_neg : ∀ (x : R), f (-x) = f x) :

    seminormFromBounded' is a ring seminorm on R.

    Equations
    Instances For
      theorem seminormFromBounded_isNonarchimedean {R : Type u_1} [CommRing R] {f : R} {c : } (f_nonneg : 0 f) (f_mul : ∀ (x y : R), f (x * y) c * f x * f y) (hna : IsNonarchimedean f) :

      If f : R → ℝ is a nonnegative, multiplicatively bounded, nonarchimedean function, then seminormFromBounded' f is nonarchimedean.

      theorem seminormFromBounded_of_mul_apply {R : Type u_1} [CommRing R] {f : R} {c : } (f_nonneg : 0 f) (f_mul : ∀ (x y : R), f (x * y) c * f x * f y) {x : R} (hx : ∀ (y : R), f (x * y) = f x * f y) :

      If f : R → ℝ is a nonnegative, multiplicatively bounded function and x : R is multiplicative for f, then seminormFromBounded' f x = f x.

      theorem seminormFromBounded_of_mul_le {R : Type u_1} [CommRing R] {f : R} (f_nonneg : 0 f) {x : R} (hx : ∀ (y : R), f (x * y) f x * f y) (h_one : f 1 1) :

      If f : R → ℝ is a nonnegative function and x : R is submultiplicative for f, then seminormFromBounded' f x = f x.

      theorem seminormFromBounded_nonzero {R : Type u_1} [CommRing R] {f : R} {c : } (f_ne_zero : f 0) (f_nonneg : 0 f) (f_mul : ∀ (x y : R), f (x * y) c * f x * f y) :

      If f : R → ℝ is a nonzero, nonnegative, multiplicatively bounded function, then seminormFromBounded' f is nonzero.

      theorem seminormFromBounded_ker {R : Type u_1} [CommRing R] {f : R} {c : } (f_nonneg : 0 f) (f_mul : ∀ (x y : R), f (x * y) c * f x * f y) :

      If f : R → ℝ is a nonnegative, multiplicatively bounded function, then the kernel of seminormFromBounded' f equals the kernel of f.

      theorem seminormFromBounded_is_norm_iff {R : Type u_1} [CommRing R] {f : R} {c : } (f_zero : f 0 = 0) (f_nonneg : 0 f) (f_mul : ∀ (x y : R), f (x * y) c * f x * f y) (f_add : ∀ (a b : R), f (a + b) f a + f b) (f_neg : ∀ (x : R), f (-x) = f x) :
      (∀ (x : R), (seminormFromBounded f_zero f_nonneg f_mul f_add f_neg).toFun x = 0x = 0) f ⁻¹' {0} = {0}

      If f : R → ℝ is a nonnegative, multiplicatively bounded, subadditive function that preserves zero and negation, then seminormFromBounded' f is a norm if and only if f⁻¹' {0} = {0}.

      def normFromBounded {R : Type u_1} [CommRing R] {f : R} {c : } (f_zero : f 0 = 0) (f_nonneg : 0 f) (f_mul : ∀ (x y : R), f (x * y) c * f x * f y) (f_add : ∀ (a b : R), f (a + b) f a + f b) (f_neg : ∀ (x : R), f (-x) = f x) (f_ker : f ⁻¹' {0} = {0}) :

      seminormFromBounded' f as a RingNorm on R, provided that f is nonnegative, multiplicatively bounded and subadditive, that it preserves 0 and negation, and that f has trivial kernel.

      Equations
      Instances For
        theorem seminormFromBounded_of_mul_is_mul {R : Type u_1} [CommRing R] {f : R} {c : } (f_nonneg : 0 f) (f_mul : ∀ (x y : R), f (x * y) c * f x * f y) {x : R} (hx : ∀ (y : R), f (x * y) = f x * f y) (y : R) :

        If f : R → ℝ is a nonnegative, multiplicatively bounded function and x : R is multiplicative for f, then x is multiplicative for seminormFromBounded' f.