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 #
Tags #
norm, seminorm
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.
The seminorm is subadditive.
The seminorm is invariant under negation.
Instances For
The image of zero is zero.
The seminorm is subadditive.
The seminorm is invariant under negation.
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.
The seminorm applied to a product is dominated by the sum of the seminorm applied to the factors.
The seminorm is invariant under inversion.
Instances For
The image of one is zero.
The seminorm applied to a product is dominated by the sum of the seminorm applied to the factors.
The seminorm is invariant under inversion.
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
The seminorm applied to a sum is dominated by the maximum of the function applied to the addends.
The seminorm is invariant under negation.
Instances For
The seminorm applied to a sum is dominated by the maximum of the function applied to the addends.
The seminorm is invariant under negation.
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.
If the image under the seminorm is zero, then the argument is zero.
If the image under the norm is zero, then the argument is zero.
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_zero : ∀ (f : F), f 0 = 0
The image of zero is zero.
The seminorm is invariant under negation.
Instances
The image of zero 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
.
- map_zero : ∀ (f : F), f 0 = 0
If the image under the norm is zero, then the argument is zero.
Instances
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Seminorms #
Equations
- AddGroupSeminorm.funLike = { coe := fun (f : AddGroupSeminorm E) => f.toFun, coe_injective' := ⋯ }
Equations
- GroupSeminorm.funLike = { coe := fun (f : GroupSeminorm E) => f.toFun, coe_injective' := ⋯ }
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Helper instance for when there's too many metavariables to apply
DFunLike.hasCoeToFun
.
Equations
- AddGroupSeminorm.instCoeFunForallReal = { coe := DFunLike.coe }
Helper instance for when there's too many metavariables to apply DFunLike.hasCoeToFun
.
Equations
- GroupSeminorm.instCoeFunForallReal = { coe := DFunLike.coe }
Equations
- AddGroupSeminorm.instPartialOrder = PartialOrder.lift (fun (f : AddGroupSeminorm E) => ⇑f) ⋯
Equations
- GroupSeminorm.instPartialOrder = PartialOrder.lift (fun (f : GroupSeminorm E) => ⇑f) ⋯
Equations
- AddGroupSeminorm.instZeroAddGroupSeminorm = { zero := { toFun := 0, map_zero' := ⋯, add_le' := ⋯, neg' := ⋯ } }
Equations
- GroupSeminorm.instZeroGroupSeminorm = { zero := { toFun := 0, map_one' := ⋯, mul_le' := ⋯, inv' := ⋯ } }
Equations
- AddGroupSeminorm.instInhabited = { default := 0 }
Equations
- GroupSeminorm.instInhabited = { default := 0 }
Equations
- AddGroupSeminorm.instAdd = { add := fun (p q : AddGroupSeminorm E) => { toFun := fun (x : E) => p x + q x, map_zero' := ⋯, add_le' := ⋯, neg' := ⋯ } }
Equations
- GroupSeminorm.instAdd = { add := fun (p q : GroupSeminorm E) => { toFun := fun (x : E) => p x + q x, map_one' := ⋯, mul_le' := ⋯, inv' := ⋯ } }
Equations
- AddGroupSeminorm.instSup = { sup := fun (p q : AddGroupSeminorm E) => { toFun := ⇑p ⊔ ⇑q, map_zero' := ⋯, add_le' := ⋯, neg' := ⋯ } }
Equations
- GroupSeminorm.instSup = { sup := fun (p q : GroupSeminorm E) => { toFun := ⇑p ⊔ ⇑q, map_one' := ⋯, mul_le' := ⋯, inv' := ⋯ } }
Equations
- AddGroupSeminorm.semilatticeSup = Function.Injective.semilatticeSup (fun (f : AddGroupSeminorm E) => ⇑f) ⋯ ⋯
Equations
- GroupSeminorm.semilatticeSup = Function.Injective.semilatticeSup (fun (f : GroupSeminorm E) => ⇑f) ⋯ ⋯
Composition of an additive group seminorm with an additive monoid homomorphism as an additive group seminorm.
Equations
- p.comp f = { toFun := fun (x : F) => p (f x), map_zero' := ⋯, add_le' := ⋯, neg' := ⋯ }
Instances For
Composition of a group seminorm with a monoid homomorphism as a group seminorm.
Equations
- p.comp f = { toFun := fun (x : F) => p (f x), map_one' := ⋯, mul_le' := ⋯, inv' := ⋯ }
Instances For
Equations
- AddGroupSeminorm.instInf = { inf := fun (p q : AddGroupSeminorm E) => { toFun := fun (x : E) => ⨅ (y : E), p y + q (x - y), map_zero' := ⋯, add_le' := ⋯, neg' := ⋯ } }
Equations
- GroupSeminorm.instInf = { inf := fun (p q : GroupSeminorm E) => { toFun := fun (x : E) => ⨅ (y : E), p y + q (x / y), map_one' := ⋯, mul_le' := ⋯, inv' := ⋯ } }
Equations
- AddGroupSeminorm.instLattice = Lattice.mk ⋯ ⋯ ⋯
Equations
- GroupSeminorm.instLattice = Lattice.mk ⋯ ⋯ ⋯
Any action on ℝ
which factors through ℝ≥0
applies to an AddGroupSeminorm
.
Equations
- AddGroupSeminorm.toSMul = { smul := fun (r : R) (p : AddGroupSeminorm E) => { toFun := fun (x : E) => r • p x, map_zero' := ⋯, add_le' := ⋯, neg' := ⋯ } }
Equations
- ⋯ = ⋯
Equations
- NonarchAddGroupSeminorm.funLike = { coe := fun (f : NonarchAddGroupSeminorm E) => f.toFun, coe_injective' := ⋯ }
Equations
- ⋯ = ⋯
Helper instance for when there's too many metavariables to apply DFunLike.hasCoeToFun
.
Equations
- NonarchAddGroupSeminorm.instCoeFunForallReal = { coe := DFunLike.coe }
Equations
- NonarchAddGroupSeminorm.instPartialOrder = PartialOrder.lift (fun (f : NonarchAddGroupSeminorm E) => ⇑f) ⋯
Equations
- NonarchAddGroupSeminorm.instZero = { zero := { toFun := 0, map_zero' := ⋯, add_le_max' := ⋯, neg' := ⋯ } }
Equations
- NonarchAddGroupSeminorm.instInhabited = { default := 0 }
Equations
- NonarchAddGroupSeminorm.instSup = { sup := fun (p q : NonarchAddGroupSeminorm E) => { toFun := ⇑p ⊔ ⇑q, map_zero' := ⋯, add_le_max' := ⋯, neg' := ⋯ } }
Equations
- NonarchAddGroupSeminorm.instSemilatticeSup = Function.Injective.semilatticeSup (fun (f : NonarchAddGroupSeminorm E) => ⇑f) ⋯ ⋯
Any action on ℝ
which factors through ℝ≥0
applies to an AddGroupSeminorm
.
Equations
- GroupSeminorm.instSMul = { smul := fun (r : R) (p : GroupSeminorm E) => { toFun := fun (x : E) => r • p x, map_one' := ⋯, mul_le' := ⋯, inv' := ⋯ } }
Equations
- ⋯ = ⋯
Any action on ℝ
which factors through ℝ≥0
applies to a NonarchAddGroupSeminorm
.
Equations
- NonarchAddGroupSeminorm.instSMul = { smul := fun (r : R) (p : NonarchAddGroupSeminorm E) => { toFun := fun (x : E) => r • p x, map_zero' := ⋯, add_le_max' := ⋯, neg' := ⋯ } }
Equations
- ⋯ = ⋯
Norms #
Equations
- AddGroupNorm.funLike = { coe := fun (f : AddGroupNorm E) => f.toFun, coe_injective' := ⋯ }
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Helper instance for when there's too many metavariables to apply
DFunLike.hasCoeToFun
directly.
Equations
- AddGroupNorm.instCoeFunForallReal = DFunLike.hasCoeToFun
Helper instance for when there's too many metavariables to apply DFunLike.hasCoeToFun
directly.
Equations
- GroupNorm.instCoeFunForallReal = DFunLike.hasCoeToFun
Equations
- AddGroupNorm.instPartialOrder = PartialOrder.lift (fun (f : AddGroupNorm E) => ⇑f) ⋯
Equations
- GroupNorm.instPartialOrder = PartialOrder.lift (fun (f : GroupNorm E) => ⇑f) ⋯
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- AddGroupNorm.instSemilatticeSup = Function.Injective.semilatticeSup (fun (f : AddGroupNorm E) => ⇑f) ⋯ ⋯
Equations
- GroupNorm.instSemilatticeSup = Function.Injective.semilatticeSup (fun (f : GroupNorm E) => ⇑f) ⋯ ⋯
Equations
- AddGroupNorm.instOne = { one := let __src := 1; { toAddGroupSeminorm := __src, eq_zero_of_map_eq_zero' := ⋯ } }
Equations
- AddGroupNorm.instInhabited = { default := 1 }
Equations
- AddGroupNorm.toOne = { one := let __src := 1; { toAddGroupSeminorm := __src, eq_zero_of_map_eq_zero' := ⋯ } }
Equations
- GroupNorm.toOne = { one := let __src := 1; { toGroupSeminorm := __src, eq_one_of_map_eq_zero' := ⋯ } }
Equations
- GroupNorm.instInhabited = { default := 1 }
Equations
- NonarchAddGroupNorm.funLike = { coe := fun (f : NonarchAddGroupNorm E) => f.toFun, coe_injective' := ⋯ }
Equations
- ⋯ = ⋯
Helper instance for when there's too many metavariables to apply DFunLike.hasCoeToFun
.
Equations
- NonarchAddGroupNorm.instCoeFunForallReal = DFunLike.hasCoeToFun
Equations
- NonarchAddGroupNorm.instPartialOrder = PartialOrder.lift (fun (f : NonarchAddGroupNorm E) => ⇑f) ⋯
Equations
- One or more equations did not get rendered due to their size.
Equations
- NonarchAddGroupNorm.instSemilatticeSup = Function.Injective.semilatticeSup (fun (f : NonarchAddGroupNorm E) => ⇑f) ⋯ ⋯
Equations
- NonarchAddGroupNorm.instOneOfDecidableEq = { one := let __src := 1; { toNonarchAddGroupSeminorm := __src, eq_zero_of_map_eq_zero' := ⋯ } }
Equations
- NonarchAddGroupNorm.instInhabitedOfDecidableEq = { default := 1 }