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 functionf
from an additive groupG
to the reals that preserves zero, takes nonnegative values, is subadditive and such thatf (-x) = f x
for allx
.NonarchAddGroupSeminorm
: A functionf
from an additive groupG
to the reals that preserves zero, takes nonnegative values, is nonarchimedean and such thatf (-x) = f x
for allx
.GroupSeminorm
: A functionf
from a groupG
to the reals that sends one to zero, takes nonnegative values, is submultiplicative and such thatf x⁻¹ = f x
for allx
.AddGroupNorm
: A seminormf
such thatf x = 0 → x = 0
for allx
.NonarchAddGroupNorm
: A nonarchimedean seminormf
such thatf x = 0 → x = 0
for allx
.GroupNorm
: A seminormf
such thatf x = 0 → x = 1
for allx
.
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
- toFun : G → ℝ
The bare function of an
AddGroupSeminorm
. - map_zero' : AddGroupSeminorm.toFun s 0 = 0
The image of zero is zero.
- add_le' : ∀ (r s_1 : G), AddGroupSeminorm.toFun s (r + s_1) ≤ AddGroupSeminorm.toFun s r + AddGroupSeminorm.toFun s s_1
The seminorm is subadditive.
- neg' : ∀ (r : G), AddGroupSeminorm.toFun s (-r) = AddGroupSeminorm.toFun s r
The seminorm is invariant under negation.
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
.
Instances For
- toFun : G → ℝ
The bare function of a
GroupSeminorm
. - map_one' : GroupSeminorm.toFun s 1 = 0
The image of one is zero.
- mul_le' : ∀ (x y : G), GroupSeminorm.toFun s (x * y) ≤ GroupSeminorm.toFun s x + GroupSeminorm.toFun s y
The seminorm applied to a product is dominated by the sum of the seminorm applied to the factors.
- inv' : ∀ (x : G), GroupSeminorm.toFun s x⁻¹ = GroupSeminorm.toFun s x
The seminorm is invariant under inversion.
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
.
Instances For
- toFun : G → ℝ
- map_zero' : ZeroHom.toFun s.toZeroHom 0 = 0
- add_le_max' : ∀ (r s_1 : G), ZeroHom.toFun s.toZeroHom (r + s_1) ≤ max (ZeroHom.toFun s.toZeroHom r) (ZeroHom.toFun s.toZeroHom s_1)
The seminorm applied to a sum is dominated by the maximum of the function applied to the addends.
- neg' : ∀ (r : G), ZeroHom.toFun s.toZeroHom (-r) = ZeroHom.toFun s.toZeroHom r
The seminorm is invariant under negation.
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
.
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.
- toFun : G → ℝ
- map_zero' : AddGroupSeminorm.toFun s.toAddGroupSeminorm 0 = 0
- add_le' : ∀ (r s_1 : G), AddGroupSeminorm.toFun s.toAddGroupSeminorm (r + s_1) ≤ AddGroupSeminorm.toFun s.toAddGroupSeminorm r + AddGroupSeminorm.toFun s.toAddGroupSeminorm s_1
- neg' : ∀ (r : G), AddGroupSeminorm.toFun s.toAddGroupSeminorm (-r) = AddGroupSeminorm.toFun s.toAddGroupSeminorm r
- eq_zero_of_map_eq_zero' : ∀ (x : G), AddGroupSeminorm.toFun s.toAddGroupSeminorm x = 0 → x = 0
If the image under the seminorm is zero, then the argument is zero.
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
.
Instances For
- toFun : G → ℝ
- map_one' : GroupSeminorm.toFun s.toGroupSeminorm 1 = 0
- mul_le' : ∀ (x y : G), GroupSeminorm.toFun s.toGroupSeminorm (x * y) ≤ GroupSeminorm.toFun s.toGroupSeminorm x + GroupSeminorm.toFun s.toGroupSeminorm y
- inv' : ∀ (x : G), GroupSeminorm.toFun s.toGroupSeminorm x⁻¹ = GroupSeminorm.toFun s.toGroupSeminorm x
- eq_one_of_map_eq_zero' : ∀ (x : G), GroupSeminorm.toFun s.toGroupSeminorm x = 0 → x = 1
If the image under the norm is zero, then the argument is one.
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
.
Instances For
- toFun : G → ℝ
- map_zero' : ZeroHom.toFun s.toZeroHom 0 = 0
- add_le_max' : ∀ (r s_1 : G), ZeroHom.toFun s.toZeroHom (r + s_1) ≤ max (ZeroHom.toFun s.toZeroHom r) (ZeroHom.toFun s.toZeroHom s_1)
- neg' : ∀ (r : G), ZeroHom.toFun s.toZeroHom (-r) = ZeroHom.toFun s.toZeroHom r
- eq_zero_of_map_eq_zero' : ∀ (x : G), ZeroHom.toFun s.toZeroHom x = 0 → x = 0
If the image under the norm is zero, then the argument is zero.
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
.
Instances For
- coe : F → α → ℝ
- coe_injective' : Function.Injective FunLike.coe
- map_zero : ∀ (f : F), ↑f 0 = 0
The image of zero is zero.
The seminorm is invariant under negation.
NonarchAddGroupSeminormClass F α
states that F
is a type of nonarchimedean seminorms on
the additive group α
.
You should extend this class when you extend NonarchAddGroupSeminorm
.
Instances
- coe : F → α → ℝ
- coe_injective' : Function.Injective FunLike.coe
- map_zero : ∀ (f : F), ↑f 0 = 0
If the image under the norm is zero, then the argument is zero.
NonarchAddGroupNormClass F α
states that F
is a type of nonarchimedean norms on the
additive group α
.
You should extend this class when you extend NonarchAddGroupNorm
.
Instances
Seminorms #
Helper instance for when there's too many metavariables to apply
FunLike.hasCoeToFun
.
Helper instance for when there's too many metavariables to apply FunLike.hasCoeToFun
.
Composition of an additive group seminorm with an additive monoid homomorphism as an additive group seminorm.
Instances For
Composition of a group seminorm with a monoid homomorphism as a group seminorm.
Instances For
Any action on ℝ
which factors through ℝ≥0
applies to an AddGroupSeminorm
.
Helper instance for when there's too many metavariables to apply FunLike.hasCoeToFun
.
Any action on ℝ
which factors through ℝ≥0
applies to an AddGroupSeminorm
.
Any action on ℝ
which factors through ℝ≥0
applies to a NonarchAddGroupSeminorm
.
Norms #
Helper instance for when there's too many metavariables to apply
FunLike.hasCoeToFun
directly.
Helper instance for when there's too many metavariables to apply FunLike.hasCoeToFun
directly.
Helper instance for when there's too many metavariables to apply FunLike.hasCoeToFun
.