mathlib documentation

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 #

References #

Tags #

norm, seminorm

@[nolint]
structure add_group_seminorm (G : Type u_7) [add_group G] :
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
structure add_group_norm (G : Type u_7) [add_group G] :
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]
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)

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
  • add_group_seminorm_class.has_sizeof_inst
@[class]
structure group_seminorm_class (F : Type u_7) (α : out_param (Type u_8)) [group α] :
Type (max u_7 u_8)

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

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
  • add_group_norm_class.has_sizeof_inst
@[class]
structure group_norm_class (F : Type u_7) (α : out_param (Type u_8)) [group α] :
Type (max u_7 u_8)

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]
theorem map_div_le_add {E : Type u_4} {F : Type u_5} [group E] [group_seminorm_class F 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] [add_group_seminorm_class F 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] [add_group_seminorm_class F 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] [group_seminorm_class F 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] [add_group_seminorm_class F 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] [group_seminorm_class F 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] [group_seminorm_class F 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] [add_group_seminorm_class F E] (f : F) (x y : E) :
|f x - f y| f (x - y)
theorem map_pos_of_ne_zero {E : Type u_4} {F : Type u_5} [add_group E] [add_group_norm_class F 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] [group_norm_class F 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] [group_norm_class F 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] [add_group_norm_class F 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] [group_norm_class F 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] [add_group_norm_class F E] (f : F) {x : E} :
f x 0 x 0

Seminorms #

@[protected, instance]

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

Equations
@[protected, instance]

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]
theorem add_group_seminorm.ext {E : Type u_4} [add_group E] {p q : add_group_seminorm E} :
( (x : E), p x = q x) p = q
@[protected, instance]
Equations
@[protected, instance]
Equations
theorem group_seminorm.le_def {E : Type u_4} [group E] {p q : group_seminorm E} :
p q p q
theorem add_group_seminorm.le_def {E : Type u_4} [add_group E] {p q : add_group_seminorm E} :
p q p q
theorem add_group_seminorm.lt_def {E : Type u_4} [add_group E] {p q : add_group_seminorm E} :
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]
theorem add_group_seminorm.coe_le_coe {E : Type u_4} [add_group E] {p q : add_group_seminorm E} :
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]
theorem add_group_seminorm.coe_lt_coe {E : Type u_4} [add_group E] {p q : add_group_seminorm E} :
p < q p < q
@[protected, instance]
Equations
@[protected, instance]
Equations
@[simp]
theorem add_group_seminorm.coe_zero {E : Type u_4} [add_group E] :
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]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[simp]
theorem add_group_seminorm.coe_add {E : Type u_4} [add_group E] (p q : add_group_seminorm E) :
(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]
theorem add_group_seminorm.add_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.add_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
@[simp]
theorem add_group_seminorm.coe_sup {E : Type u_4} [add_group E] (p q : add_group_seminorm E) :
(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
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) :

Composition of an additive group seminorm with an additive monoid homomorphism as an additive group seminorm.

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]
@[simp]
theorem group_seminorm.comp_id {E : Type u_4} [group E] (p : group_seminorm E) :
@[simp]
theorem add_group_seminorm.comp_zero {E : Type u_4} {F : Type u_5} [add_group E] [add_group F] (p : add_group_seminorm E) :
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
theorem add_group_seminorm.add_comp {E : Type u_4} {F : Type u_5} [add_group E] [add_group F] (p q : add_group_seminorm E) (f : F →+ E) :
(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} [add_comm_group E] [add_comm_group F] (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)))
theorem add_group_seminorm.add_bdd_below_range_add {E : Type u_4} [add_comm_group E] {p q : add_group_seminorm E} {x : E} :
bdd_below (set.range (λ (y : E), p y + q (x - y)))
@[protected, instance]
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} [add_comm_group E] (p q : add_group_seminorm E) (x : E) :
(p q) x = (y : E), p y + q (x - y)
@[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]

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] [has_smul R ] [has_smul R nnreal] [is_scalar_tower R 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] [has_smul R ] [has_smul R nnreal] [is_scalar_tower R nnreal ] (r : R) (p : add_group_seminorm E) (x : E) :
(r p) x = r p x
theorem add_group_seminorm.smul_sup {R : Type u_2} {E : Type u_4} [add_group E] [has_smul R ] [has_smul R nnreal] [is_scalar_tower R nnreal ] (r : R) (p q : add_group_seminorm E) :
r (p q) = r p r q
@[protected, instance]
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]

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

Equations
@[protected, instance]
@[simp]
theorem group_seminorm.coe_smul {R : Type u_2} {E : Type u_4} [group E] [has_smul R ] [has_smul R nnreal] [is_scalar_tower R 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] [has_smul R ] [has_smul R nnreal] [is_scalar_tower R 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] [has_smul R ] [has_smul R nnreal] [is_scalar_tower R nnreal ] (r : R) (p q : group_seminorm E) :
r (p q) = r p r q

Norms #

@[protected, instance]
def group_norm.has_coe_to_fun {E : Type u_4} [group E] :

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

Equations
@[protected, instance]

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]
theorem add_group_norm.to_fun_eq_coe {E : Type u_4} [add_group E] {p : add_group_norm E} :
@[ext]
theorem add_group_norm.ext {E : Type u_4} [add_group E] {p q : add_group_norm E} :
( (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]
Equations
theorem group_norm.le_def {E : Type u_4} [group E] {p q : group_norm E} :
p q p q
theorem add_group_norm.le_def {E : Type u_4} [add_group E] {p q : add_group_norm E} :
p q p q
theorem group_norm.lt_def {E : Type u_4} [group E] {p q : group_norm E} :
p < q p < q
theorem add_group_norm.lt_def {E : Type u_4} [add_group E] {p q : add_group_norm E} :
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]
theorem add_group_norm.coe_le_coe {E : Type u_4} [add_group E] {p q : add_group_norm E} :
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]
theorem add_group_norm.coe_lt_coe {E : Type u_4} [add_group E] {p q : add_group_norm E} :
p < q p < q
@[protected, instance]
def group_norm.has_add {E : Type u_4} [group E] :
Equations
@[simp]
theorem add_group_norm.coe_add {E : Type u_4} [add_group E] (p q : add_group_norm E) :
(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]
theorem add_group_norm.add_apply {E : Type u_4} [add_group E] (p q : add_group_norm E) (x : E) :
(p + q) x = p x + q x
@[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]
theorem add_group_norm.coe_sup {E : Type u_4} [add_group E] (p q : add_group_norm E) :
(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]
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]
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]
Equations