# mathlib3documentation

analysis.normed.group.seminorm

# Group seminorms #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 #

• `add_group_seminorm`: 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`.
• `nonarch_add_group_seminorm`: 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`.
• `group_seminorm`: 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`.
• `add_group_norm`: A seminorm `f` such that `f x = 0 → x = 0` for all `x`.
• `nonarch_add_group_norm`: A nonarchimedean seminorm `f` such that `f x = 0 → x = 0` for all `x`.
• `group_norm`: 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 `nonarch_add_group_seminorm` as an extension of `add_group_seminorm` to avoid having a superfluous `add_le'` field in the resulting structure. The same applies to `nonarch_add_group_norm`.

## Tags #

norm, seminorm

@[nolint]
Type u_7

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 `add_group_seminorm`
structure group_seminorm (G : Type u_7) [group G] :
Type u_7

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 `group_seminorm`
Type u_7

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 `nonarch_add_group_seminorm`

NOTE: We do not define `nonarch_add_group_seminorm` as an extension of `add_group_seminorm` to avoid having a superfluous `add_le'` field in the resulting structure. The same applies to `nonarch_add_group_norm` below.

Type u_7

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 `add_group_norm`
@[nolint]
@[nolint]
def group_norm.to_group_seminorm {G : Type u_7} [group G] (self : group_norm G) :
structure group_norm (G : Type u_7) [group G] :
Type u_7

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 `group_norm`
Type u_7

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 `nonarch_add_group_norm`
@[class]
structure nonarch_add_group_seminorm_class (F : Type u_7) (α : out_param (Type u_8)) [add_group α] :
Type (max u_7 u_8)

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

You should extend this class when you extend `nonarch_add_group_seminorm`.

Instances of this typeclass
Instances of other typeclasses for `nonarch_add_group_seminorm_class`
@[instance]
@[class]
structure nonarch_add_group_norm_class (F : Type u_7) (α : out_param (Type u_8)) [add_group α] :
Type (max u_7 u_8)

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

You should extend this class when you extend `nonarch_add_group_norm`.

Instances of this typeclass
Instances of other typeclasses for `nonarch_add_group_norm_class`
@[instance]
theorem map_sub_le_max {E : Type u_4} {F : Type u_5} [add_group E] (f : F) (x y : E) :
f (x - y) linear_order.max (f x) (f y)

### Seminorms #

@[protected, instance]
Equations
@[protected, instance]
(λ (_x : , E )

Helper instance for when there's too many metavariables to apply `fun_like.has_coe_to_fun`.

Equations
@[protected, instance]
def group_seminorm.has_coe_to_fun {E : Type u_4} [group E] :
(λ (_x : , E )

Helper instance for when there's too many metavariables to apply `fun_like.has_coe_to_fun`.

Equations
@[simp]
@[simp]
theorem group_seminorm.to_fun_eq_coe {E : Type u_4} [group E] {p : group_seminorm E} :
@[ext]
theorem group_seminorm.ext {E : Type u_4} [group E] {p q : group_seminorm E} :
( (x : E), p x = q x) p = q
@[ext]
( (x : E), p x = q x) p = q
@[protected, instance]
Equations
@[protected, instance]
def group_seminorm.partial_order {E : Type u_4} [group E] :
Equations
theorem group_seminorm.le_def {E : Type u_4} [group E] {p q : group_seminorm E} :
p q p q
p q p q
p < q p < q
theorem group_seminorm.lt_def {E : Type u_4} [group E] {p q : group_seminorm E} :
p < q p < q
@[simp, norm_cast]
theorem group_seminorm.coe_le_coe {E : Type u_4} [group E] {p q : group_seminorm E} :
p q p q
@[simp]
p q p q
@[simp, norm_cast]
theorem group_seminorm.coe_lt_coe {E : Type u_4} [group E] {p q : group_seminorm E} :
p < q p < q
@[simp]
p < q p < q
@[protected, instance]
Equations
@[protected, instance]
def group_seminorm.has_zero {E : Type u_4} [group E] :
Equations
@[simp]
0 = 0
@[simp, norm_cast]
theorem group_seminorm.coe_zero {E : Type u_4} [group E] :
0 = 0
@[simp]
theorem add_group_seminorm.zero_apply {E : Type u_4} [add_group E] (x : E) :
0 x = 0
@[simp]
theorem group_seminorm.zero_apply {E : Type u_4} [group E] (x : E) :
0 x = 0
@[protected, instance]
def group_seminorm.inhabited {E : Type u_4} [group E] :
Equations
@[protected, instance]
Equations
@[protected, instance]
def group_seminorm.has_add {E : Type u_4} [group E] :
Equations
@[protected, instance]
Equations
@[simp]
(p + q) = p + q
@[simp]
theorem group_seminorm.coe_add {E : Type u_4} [group E] (p q : group_seminorm E) :
(p + q) = p + q
@[simp]
(p + q) x = p x + q x
@[simp]
theorem group_seminorm.add_apply {E : Type u_4} [group E] (p q : group_seminorm E) (x : E) :
(p + q) x = p x + q x
@[protected, instance]
def group_seminorm.has_sup {E : Type u_4} [group E] :
Equations
@[protected, instance]
Equations
@[simp]
(p q) = p q
@[simp, norm_cast]
theorem group_seminorm.coe_sup {E : Type u_4} [group E] (p q : group_seminorm E) :
(p q) = p q
@[simp]
theorem add_group_seminorm.sup_apply {E : Type u_4} [add_group E] (p q : add_group_seminorm E) (x : E) :
(p q) x = p x q x
@[simp]
theorem group_seminorm.sup_apply {E : Type u_4} [group E] (p q : group_seminorm E) (x : E) :
(p q) x = p x q x
@[protected, instance]
Equations
@[protected, instance]
Equations
def add_group_seminorm.comp {E : Type u_4} {F : Type u_5} [add_group E] [add_group F] (p : add_group_seminorm E) (f : F →+ E) :

Equations
def group_seminorm.comp {E : Type u_4} {F : Type u_5} [group E] [group F] (p : group_seminorm E) (f : F →* E) :

Composition of a group seminorm with a monoid homomorphism as a group seminorm.

Equations
@[simp]
theorem add_group_seminorm.coe_comp {E : Type u_4} {F : Type u_5} [add_group E] [add_group F] (p : add_group_seminorm E) (f : F →+ E) :
(p.comp f) = p f
@[simp]
theorem group_seminorm.coe_comp {E : Type u_4} {F : Type u_5} [group E] [group F] (p : group_seminorm E) (f : F →* E) :
(p.comp f) = p f
@[simp]
theorem add_group_seminorm.comp_apply {E : Type u_4} {F : Type u_5} [add_group E] [add_group F] (p : add_group_seminorm E) (f : F →+ E) (x : F) :
(p.comp f) x = p (f x)
@[simp]
theorem group_seminorm.comp_apply {E : Type u_4} {F : Type u_5} [group E] [group F] (p : group_seminorm E) (f : F →* E) (x : F) :
(p.comp f) x = p (f x)
@[simp]
p.comp = p
@[simp]
theorem group_seminorm.comp_id {E : Type u_4} [group E] (p : group_seminorm E) :
p.comp = p
@[simp]
p.comp 0 = 0
@[simp]
theorem group_seminorm.comp_zero {E : Type u_4} {F : Type u_5} [group E] [group F] (p : group_seminorm E) :
p.comp 1 = 0
@[simp]
theorem group_seminorm.zero_comp {E : Type u_4} {F : Type u_5} [group E] [group F] (f : F →* E) :
0.comp f = 0
@[simp]
theorem add_group_seminorm.zero_comp {E : Type u_4} {F : Type u_5} [add_group E] [add_group F] (f : F →+ E) :
0.comp f = 0
theorem group_seminorm.comp_assoc {E : Type u_4} {F : Type u_5} {G : Type u_6} [group E] [group F] [group G] (p : group_seminorm E) (g : F →* E) (f : G →* F) :
p.comp (g.comp f) = (p.comp g).comp f
theorem add_group_seminorm.comp_assoc {E : Type u_4} {F : Type u_5} {G : Type u_6} [add_group E] [add_group F] [add_group G] (p : add_group_seminorm E) (g : F →+ E) (f : G →+ F) :
p.comp (g.comp f) = (p.comp g).comp f
(p + q).comp f = p.comp f + q.comp f
theorem group_seminorm.add_comp {E : Type u_4} {F : Type u_5} [group E] [group F] (p q : group_seminorm E) (f : F →* E) :
(p + q).comp f = p.comp f + q.comp f
theorem group_seminorm.comp_mono {E : Type u_4} {F : Type u_5} [group E] [group F] {p q : group_seminorm E} (f : F →* E) (hp : p q) :
p.comp f q.comp f
theorem add_group_seminorm.comp_mono {E : Type u_4} {F : Type u_5} [add_group E] [add_group F] {p q : add_group_seminorm E} (f : F →+ E) (hp : p q) :
p.comp f q.comp f
theorem group_seminorm.comp_mul_le {E : Type u_4} {F : Type u_5} [comm_group E] [comm_group F] (p : group_seminorm E) (f g : F →* E) :
p.comp (f * g) p.comp f + p.comp g
theorem add_group_seminorm.comp_add_le {E : Type u_4} {F : Type u_5} (p : add_group_seminorm E) (f g : F →+ E) :
p.comp (f + g) p.comp f + p.comp g
theorem group_seminorm.mul_bdd_below_range_add {E : Type u_4} [comm_group E] {p q : group_seminorm E} {x : E} :
bdd_below (set.range (λ (y : E), p y + q (x / y)))
bdd_below (set.range (λ (y : E), p y + q (x - y)))
@[protected, instance]
noncomputable def add_group_seminorm.has_inf {E : Type u_4}  :
Equations
@[protected, instance]
noncomputable def group_seminorm.has_inf {E : Type u_4} [comm_group E] :
Equations
@[simp]
theorem group_seminorm.inf_apply {E : Type u_4} [comm_group E] (p q : group_seminorm E) (x : E) :
(p q) x = (y : E), p y + q (x / y)
@[simp]
theorem add_group_seminorm.inf_apply {E : Type u_4} (p q : add_group_seminorm E) (x : E) :
(p q) x = (y : E), p y + q (x - y)
@[protected, instance]
noncomputable def group_seminorm.lattice {E : Type u_4} [comm_group E] :
Equations
@[protected, instance]
noncomputable def add_group_seminorm.lattice {E : Type u_4}  :
Equations
@[protected, instance]
Equations
@[simp]
theorem add_group_seminorm.apply_one {E : Type u_4} [add_group E] [decidable_eq E] (x : E) :
1 x = ite (x = 0) 0 1
@[protected, instance]
def add_group_seminorm.has_smul {R : Type u_2} {E : Type u_4} [add_group E] [ ] [ nnreal]  :

Any action on `ℝ` which factors through `ℝ≥0` applies to an `add_group_seminorm`.

Equations
@[simp, norm_cast]
theorem add_group_seminorm.coe_smul {R : Type u_2} {E : Type u_4} [add_group E] [ ] [ nnreal] (r : R) (p : add_group_seminorm E) :
(r p) = r p
@[simp]
theorem add_group_seminorm.smul_apply {R : Type u_2} {E : Type u_4} [add_group E] [ ] [ nnreal] (r : R) (p : add_group_seminorm E) (x : E) :
(r p) x = r p x
@[protected, instance]
def add_group_seminorm.is_scalar_tower {R : Type u_2} {R' : Type u_3} {E : Type u_4} [add_group E] [ ] [ nnreal] [has_smul R' ] [has_smul R' nnreal] [ ] [ R'] [ R' ] :
R'
theorem add_group_seminorm.smul_sup {R : Type u_2} {E : Type u_4} [add_group E] [ ] [ nnreal] (r : R) (p q : add_group_seminorm E) :
r (p q) = r p r q
@[protected, instance]
(λ (_x : , E )

Helper instance for when there's too many metavariables to apply `fun_like.has_coe_to_fun`.

Equations
@[ext]
( (x : E), p x = q x) p = q
@[protected, instance]
Equations
@[simp, norm_cast]
@[simp, norm_cast]
@[protected, instance]
Equations
@[simp, norm_cast]
@[simp]
theorem nonarch_add_group_seminorm.zero_apply {E : Type u_4} [add_group E] (x : E) :
0 x = 0
@[protected, instance]
Equations
@[protected, instance]
Equations
@[simp, norm_cast]
@[simp]
theorem nonarch_add_group_seminorm.sup_apply {E : Type u_4} [add_group E] (p q : nonarch_add_group_seminorm E) (x : E) :
(p q) x = p x q x
@[protected, instance]
Equations
bdd_below (set.range (λ (y : E), p y + q (x - y)))
@[protected, instance]
def group_seminorm.has_one {E : Type u_4} [group E] [decidable_eq E] :
Equations
@[simp]
theorem group_seminorm.apply_one {E : Type u_4} [group E] [decidable_eq E] (x : E) :
1 x = ite (x = 1) 0 1
@[protected, instance]
def group_seminorm.has_smul {R : Type u_2} {E : Type u_4} [group E] [ ] [ nnreal]  :

Any action on `ℝ` which factors through `ℝ≥0` applies to an `add_group_seminorm`.

Equations
@[protected, instance]
def group_seminorm.is_scalar_tower {R : Type u_2} {R' : Type u_3} {E : Type u_4} [group E] [ ] [ nnreal] [has_smul R' ] [has_smul R' nnreal] [ ] [ R'] [ R' ] :
R'
@[simp, norm_cast]
theorem group_seminorm.coe_smul {R : Type u_2} {E : Type u_4} [group E] [ ] [ nnreal] (r : R) (p : group_seminorm E) :
(r p) = r p
@[simp]
theorem group_seminorm.smul_apply {R : Type u_2} {E : Type u_4} [group E] [ ] [ nnreal] (r : R) (p : group_seminorm E) (x : E) :
(r p) x = r p x
theorem group_seminorm.smul_sup {R : Type u_2} {E : Type u_4} [group E] [ ] [ nnreal] (r : R) (p q : group_seminorm E) :
r (p q) = r p r q
@[protected, instance]
Equations
@[simp]
theorem nonarch_add_group_seminorm.apply_one {E : Type u_4} [add_group E] [decidable_eq E] (x : E) :
1 x = ite (x = 0) 0 1
@[protected, instance]
def nonarch_add_group_seminorm.has_smul {R : Type u_2} {E : Type u_4} [add_group E] [ ] [ nnreal]  :

Any action on `ℝ` which factors through `ℝ≥0` applies to a `nonarch_add_group_seminorm`.

Equations
@[protected, instance]
def nonarch_add_group_seminorm.is_scalar_tower {R : Type u_2} {R' : Type u_3} {E : Type u_4} [add_group E] [ ] [ nnreal] [has_smul R' ] [has_smul R' nnreal] [ ] [ R'] [ R' ] :
@[simp, norm_cast]
theorem nonarch_add_group_seminorm.coe_smul {R : Type u_2} {E : Type u_4} [add_group E] [ ] [ nnreal] (r : R)  :
(r p) = r p
@[simp]
theorem nonarch_add_group_seminorm.smul_apply {R : Type u_2} {E : Type u_4} [add_group E] [ ] [ nnreal] (r : R) (x : E) :
(r p) x = r p x
theorem nonarch_add_group_seminorm.smul_sup {R : Type u_2} {E : Type u_4} [add_group E] [ ] [ nnreal] (r : R) (p q : nonarch_add_group_seminorm E) :
r (p q) = r p r q

### Norms #

@[protected, instance]
def group_norm.group_norm_class {E : Type u_4} [group E] :
Equations
@[protected, instance]
def group_norm.has_coe_to_fun {E : Type u_4} [group E] :
(λ (_x : , E )

Helper instance for when there's too many metavariables to apply `fun_like.has_coe_to_fun` directly.

Equations
@[protected, instance]
(λ (_x : , E )

Helper instance for when there's too many metavariables to apply `fun_like.has_coe_to_fun` directly.

Equations
@[simp]
theorem group_norm.to_fun_eq_coe {E : Type u_4} [group E] {p : group_norm E} :
@[simp]
@[ext]
( (x : E), p x = q x) p = q
@[ext]
theorem group_norm.ext {E : Type u_4} [group E] {p q : group_norm E} :
( (x : E), p x = q x) p = q
@[protected, instance]
Equations
@[protected, instance]
def group_norm.partial_order {E : Type u_4} [group E] :
Equations
theorem group_norm.le_def {E : Type u_4} [group E] {p q : group_norm E} :
p q p q
p q p q
theorem group_norm.lt_def {E : Type u_4} [group E] {p q : group_norm E} :
p < q p < q
p < q p < q
@[simp, norm_cast]
theorem group_norm.coe_le_coe {E : Type u_4} [group E] {p q : group_norm E} :
p q p q
@[simp]
p q p q
@[simp, norm_cast]
theorem group_norm.coe_lt_coe {E : Type u_4} [group E] {p q : group_norm E} :
p < q p < q
@[simp]
p < q p < q
@[protected, instance]
def group_norm.has_add {E : Type u_4} [group E] :
Equations
@[protected, instance]
Equations
@[simp]
(p + q) = p + q
@[simp]
theorem group_norm.coe_add {E : Type u_4} [group E] (p q : group_norm E) :
(p + q) = p + q
@[simp]
theorem group_norm.add_apply {E : Type u_4} [group E] (p q : group_norm E) (x : E) :
(p + q) x = p x + q x
@[simp]
(p + q) x = p x + q x
@[protected, instance]
Equations
@[protected, instance]
def group_norm.has_sup {E : Type u_4} [group E] :
Equations
@[simp, norm_cast]
theorem group_norm.coe_sup {E : Type u_4} [group E] (p q : group_norm E) :
(p q) = p q
@[simp]
(p q) = p q
@[simp]
theorem add_group_norm.sup_apply {E : Type u_4} [add_group E] (p q : add_group_norm E) (x : E) :
(p q) x = p x q x
@[simp]
theorem group_norm.sup_apply {E : Type u_4} [group E] (p q : group_norm E) (x : E) :
(p q) x = p x q x
@[protected, instance]
Equations
@[protected, instance]
def group_norm.semilattice_sup {E : Type u_4} [group E] :
Equations
@[protected, instance]
Equations
@[simp]
theorem add_group_norm.apply_one {E : Type u_4} [add_group E] [decidable_eq E] (x : E) :
1 x = ite (x = 0) 0 1
@[protected, instance]
Equations
@[protected, instance]
def group_norm.has_one {E : Type u_4} [group E] [decidable_eq E] :
Equations
@[simp]
theorem group_norm.apply_one {E : Type u_4} [group E] [decidable_eq E] (x : E) :
1 x = ite (x = 1) 0 1
@[protected, instance]
def group_norm.inhabited {E : Type u_4} [group E] [decidable_eq E] :
Equations
@[protected, instance]
(λ (_x : , E )

Helper instance for when there's too many metavariables to apply `fun_like.has_coe_to_fun`.

Equations
@[ext]
( (x : E), p x = q x) p = q
@[protected, instance]
Equations
@[simp, norm_cast]
@[simp, norm_cast]
@[protected, instance]
Equations
@[simp, norm_cast]
@[simp]
theorem nonarch_add_group_norm.sup_apply {E : Type u_4} [add_group E] (p q : nonarch_add_group_norm E) (x : E) :
(p q) x = p x q x
@[protected, instance]