Group seminorms #

This file defines norms and seminorms in a group. A group seminorm is a function to the reals which is positive-semidefinite and subadditive. A norm further only maps zero to zero.

Main declarations #

AddGroupSeminorm: A function f from an additive group G to the reals that preserves zero, takes nonnegative values, is subadditive and such that f (-x) = f x for all x.
NonarchAddGroupSeminorm: A function f from an additive group G to the reals that preserves zero, takes nonnegative values, is nonarchimedean and such that f (-x) = f x for all x.
GroupSeminorm: A function f from a group G to the reals that sends one to zero, takes nonnegative values, is submultiplicative and such that f x⁻¹ = f x for all x.
AddGroupNorm: A seminorm f such that f x = 0 → x = 0 for all x.
NonarchAddGroupNorm: A nonarchimedean seminorm f such that f x = 0 → x = 0 for all x.
GroupNorm: A seminorm f such that f x = 0 → x = 1 for all x.

Notes #

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

We do not define NonarchAddGroupSeminorm as an extension of AddGroupSeminorm to avoid having a superfluous add_le' field in the resulting structure. The same applies to NonarchAddGroupNorm.

References #

[H. H. Schaefer, Topological Vector Spaces][schaefer1966]

Tags #

norm, seminorm

source

structure AddGroupSeminorm (G : Type u_6) [AddGroup G] :

Type u_6

A seminorm on an additive group G is a function f : G → ℝ that preserves zero, is subadditive and such that f (-x) = f x for all x.

toFun : G → ℝ
The bare function of an AddGroupSeminorm.
map_zero' : self.toFun 0 = 0
The image of zero is zero.
add_le' (r s : G) : self.toFun (r + s) ≤ self.toFun r + self.toFun s
The seminorm is subadditive.
neg' (r : G) : self.toFun (-r) = self.toFun r
The seminorm is invariant under negation.

Instances For

source

structure GroupSeminorm (G : Type u_6) [Group G] :

Type u_6

A seminorm on a group G is a function f : G → ℝ that sends one to zero, is submultiplicative and such that f x⁻¹ = f x for all x.

toFun : G → ℝ
The bare function of a GroupSeminorm.
map_one' : self.toFun 1 = 0
The image of one is zero.
mul_le' (x y : G) : self.toFun (x * y) ≤ self.toFun x + self.toFun y
The seminorm applied to a product is dominated by the sum of the seminorm applied to the factors.
inv' (x : G) : self.toFun x⁻¹ = self.toFun x
The seminorm is invariant under inversion.

Instances For

source

structure NonarchAddGroupSeminorm (G : Type u_6) [AddGroup G] extends ZeroHom G ℝ :

Type u_6

A nonarchimedean seminorm on an additive group G is a function f : G → ℝ that preserves zero, is nonarchimedean and such that f (-x) = f x for all x.

toFun : G → ℝ
map_zero' : self.toFun 0 = 0
add_le_max' (r s : G) : self.toFun (r + s) ≤ max (self.toFun r) (self.toFun s)
The seminorm applied to a sum is dominated by the maximum of the function applied to the addends.
neg' (r : G) : self.toFun (-r) = self.toFun r
The seminorm is invariant under negation.

Instances For

NOTE: We do not define NonarchAddGroupSeminorm as an extension of AddGroupSeminorm to avoid having a superfluous add_le' field in the resulting structure. The same applies to NonarchAddGroupNorm below.

source

structure AddGroupNorm (G : Type u_6) [AddGroup G] extends AddGroupSeminorm G :

Type u_6

A norm on an additive group G is a function f : G → ℝ that preserves zero, is subadditive and such that f (-x) = f x and f x = 0 → x = 0 for all x.

toFun : G → ℝ
map_zero' : self.toFun 0 = 0
add_le' (r s : G) : self.toFun (r + s) ≤ self.toFun r + self.toFun s
neg' (r : G) : self.toFun (-r) = self.toFun r
eq_zero_of_map_eq_zero' (x : G) : self.toFun x = 0 → x = 0
If the image under the seminorm is zero, then the argument is zero.

Instances For

source

structure GroupNorm (G : Type u_6) [Group G] extends GroupSeminorm G :

Type u_6

A seminorm on a group G is a function f : G → ℝ that sends one to zero, is submultiplicative and such that f x⁻¹ = f x and f x = 0 → x = 1 for all x.

toFun : G → ℝ
map_one' : self.toFun 1 = 0
mul_le' (x y : G) : self.toFun (x * y) ≤ self.toFun x + self.toFun y
inv' (x : G) : self.toFun x⁻¹ = self.toFun x
eq_one_of_map_eq_zero' (x : G) : self.toFun x = 0 → x = 1
If the image under the norm is zero, then the argument is one.

Instances For

source

structure NonarchAddGroupNorm (G : Type u_6) [AddGroup G] extends NonarchAddGroupSeminorm G :

Type u_6

A nonarchimedean norm on an additive group G is a function f : G → ℝ that preserves zero, is nonarchimedean and such that f (-x) = f x and f x = 0 → x = 0 for all x.

toFun : G → ℝ
map_zero' : self.toFun 0 = 0
add_le_max' (r s : G) : self.toFun (r + s) ≤ max (self.toFun r) (self.toFun s)
neg' (r : G) : self.toFun (-r) = self.toFun r
eq_zero_of_map_eq_zero' (x : G) : self.toFun x = 0 → x = 0
If the image under the norm is zero, then the argument is zero.

Instances For

source

class NonarchAddGroupSeminormClass (F : Type u_6) (α : outParam (Type u_7)) [AddGroup α] [FunLike F α ℝ] extends NonarchimedeanHomClass F α ℝ :

Prop

NonarchAddGroupSeminormClass F α states that F is a type of nonarchimedean seminorms on the additive group α.

You should extend this class when you extend NonarchAddGroupSeminorm.

map_add_le_max (f : F) (a b : α) : f (a + b) ≤ max (f a) (f b)
map_zero (f : F) : f 0 = 0
The image of zero is zero.
map_neg_eq_map' (f : F) (a : α) : f (-a) = f a
The seminorm is invariant under negation.

Instances

source

class NonarchAddGroupNormClass (F : Type u_6) (α : outParam (Type u_7)) [AddGroup α] [FunLike F α ℝ] extends NonarchAddGroupSeminormClass F α :

Prop

NonarchAddGroupNormClass F α states that F is a type of nonarchimedean norms on the additive group α.

You should extend this class when you extend NonarchAddGroupNorm.

map_add_le_max (f : F) (a b : α) : f (a + b) ≤ max (f a) (f b)
map_zero (f : F) : f 0 = 0
map_neg_eq_map' (f : F) (a : α) : f (-a) = f a
eq_zero_of_map_eq_zero (f : F) {a : α} : f a = 0 → a = 0
If the image under the norm is zero, then the argument is zero.