# mathlibdocumentation

analysis.normed.group.seminorm

# 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 #

• 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.
• 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.
• group_norm: A seminorm f such that f x = 0 → x = 1 for all x.

## 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 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
@[class]
structure add_group_seminorm_class (F : Type u_7) (α : out_param (Type u_8)) [add_group α] :
Type (max u_7 u_8)
• coe : F Π (a : α), (λ (_x : α), ) a
• coe_injective' :
• map_add_le_add : (f : F) (a b : α), f (a + b) f a + f b
• map_zero : (f : F), f 0 = 0
• map_neg_eq_map : (f : F) (a : α), f (-a) = f a

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

You should extend this class when you extend add_group_seminorm.

Instances of this typeclass
Instances of other typeclasses for add_group_seminorm_class
@[instance]
def add_group_seminorm_class.to_subadditive_hom_class (F : Type u_7) (α : out_param (Type u_8)) [add_group α] [self : α] :
@[instance]
def group_seminorm_class.to_mul_le_add_hom_class (F : Type u_7) (α : out_param (Type u_8)) [group α] [self : α] :
@[class]
structure group_seminorm_class (F : Type u_7) (α : out_param (Type u_8)) [group α] :
Type (max u_7 u_8)
• coe : F Π (a : α), (λ (_x : α), ) a
• coe_injective' :
• map_mul_le_add : (f : F) (a b : α), f (a * b) f a + f b
• map_one_eq_zero : (f : F), f 1 = 0
• map_inv_eq_map : (f : F) (a : α), f a⁻¹ = f a

group_seminorm_class F α states that F is a type of seminorms on the group α.

You should extend this class when you extend group_seminorm.

Instances of this typeclass
Instances of other typeclasses for group_seminorm_class
• group_seminorm_class.has_sizeof_inst
@[instance]
def add_group_norm_class.to_add_group_seminorm_class (F : Type u_7) (α : out_param (Type u_8)) [add_group α] [self : α] :
@[class]
structure add_group_norm_class (F : Type u_7) (α : out_param (Type u_8)) [add_group α] :
Type (max u_7 u_8)
• coe : F Π (a : α), (λ (_x : α), ) a
• coe_injective' :
• map_add_le_add : (f : F) (a b : α), f (a + b) 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

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

You should extend this class when you extend add_group_norm.

Instances of this typeclass
Instances of other typeclasses for add_group_norm_class
@[class]
structure group_norm_class (F : Type u_7) (α : out_param (Type u_8)) [group α] :
Type (max u_7 u_8)
• coe : F Π (a : α), (λ (_x : α), ) a
• coe_injective' :
• map_mul_le_add : (f : F) (a b : α), f (a * b) f a + f b
• map_one_eq_zero : (f : F), f 1 = 0
• map_inv_eq_map : (f : F) (a : α), f a⁻¹ = f a
• eq_one_of_map_eq_zero : (f : F) {a : α}, f a = 0 a = 1

group_norm_class F α states that F is a type of norms on the group α.

You should extend this class when you extend group_norm.

Instances of this typeclass
Instances of other typeclasses for group_norm_class
• group_norm_class.has_sizeof_inst
@[instance]
def group_norm_class.to_group_seminorm_class (F : Type u_7) (α : out_param (Type u_8)) [group α] [self : α] :
@[instance]
theorem map_div_le_add {E : Type u_4} {F : Type u_5} [group E] [ E] (f : F) (x y : E) :
f (x / y) f x + f y
theorem map_sub_le_add {E : Type u_4} {F : Type u_5} [add_group E] (f : F) (x y : E) :
f (x - y) f x + f y
theorem map_sub_rev {E : Type u_4} {F : Type u_5} [add_group E] (f : F) (x y : E) :
f (x - y) = f (y - x)
theorem map_div_rev {E : Type u_4} {F : Type u_5} [group E] [ E] (f : F) (x y : E) :
f (x / y) = f (y / x)
theorem le_map_add_map_sub' {E : Type u_4} {F : Type u_5} [add_group E] (f : F) (x y : E) :
f x f y + f (y - x)
theorem le_map_add_map_div' {E : Type u_4} {F : Type u_5} [group E] [ E] (f : F) (x y : E) :
f x f y + f (y / x)
theorem abs_sub_map_le_div {E : Type u_4} {F : Type u_5} [group E] [ E] (f : F) (x y : E) :
|f x - f y| f (x / y)
theorem abs_sub_map_le_sub {E : Type u_4} {F : Type u_5} [add_group E] (f : F) (x y : E) :
|f x - f y| f (x - y)
@[protected, instance]
def group_seminorm_class.to_nonneg_hom_class {E : Type u_4} {F : Type u_5} [group E] [ E] :
Equations
theorem map_pos_of_ne_zero {E : Type u_4} {F : Type u_5} [add_group E] [ E] (f : F) {x : E} (hx : x 0) :
0 < f x
theorem map_pos_of_ne_one {E : Type u_4} {F : Type u_5} [group E] [ E] (f : F) {x : E} (hx : x 1) :
0 < f x
@[simp]
theorem map_eq_zero_iff_eq_one {E : Type u_4} {F : Type u_5} [group E] [ E] (f : F) {x : E} :
f x = 0 x = 1
@[simp]
theorem map_eq_zero_iff_eq_zero {E : Type u_4} {F : Type u_5} [add_group E] [ E] (f : F) {x : E} :
f x = 0 x = 0
theorem map_ne_zero_iff_ne_one {E : Type u_4} {F : Type u_5} [group E] [ E] (f : F) {x : E} :
f x 0 x 1
theorem map_ne_zero_iff_ne_zero {E : Type u_4} {F : Type u_5} [add_group E] [ E] (f : F) {x : E} :
f x 0 x 0

### 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]
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]
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]
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]
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]
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]
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]
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

### 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]
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]
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]
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