# 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 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.
• NonarchAddGroupSeminorm: 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.
• GroupSeminorm: 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.
• AddGroupNorm: A seminorm f such that f x = 0 → x = 0 for all x.
• NonarchAddGroupNorm: A nonarchimedean seminorm f such that f x = 0 → x = 0 for all x.
• GroupNorm: 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 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

structure AddGroupSeminorm (G : Type u_7) [] :
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.

• toFun : G

The bare function of an AddGroupSeminorm.

• map_zero' : self.toFun 0 = 0

The image of zero is zero.

• add_le' : ∀ (r s : G), self.toFun (r + s) self.toFun r + self.toFun s

• neg' : ∀ (r : G), self.toFun (-r) = self.toFun r

The seminorm is invariant under negation.

Instances For
theorem AddGroupSeminorm.map_zero' {G : Type u_7} [] (self : ) :
self.toFun 0 = 0

The image of zero is zero.

theorem AddGroupSeminorm.add_le' {G : Type u_7} [] (self : ) (r : G) (s : G) :
self.toFun (r + s) self.toFun r + self.toFun s

theorem AddGroupSeminorm.neg' {G : Type u_7} [] (self : ) (r : G) :
self.toFun (-r) = self.toFun r

The seminorm is invariant under negation.

structure GroupSeminorm (G : Type u_7) [] :
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.

• toFun : G

The bare function of a GroupSeminorm.

• map_one' : self.toFun 1 = 0

The image of one is zero.

• mul_le' : ∀ (x y : G), self.toFun (x * y) self.toFun x + self.toFun y

The seminorm applied to a product is dominated by the sum of the seminorm applied to the factors.

• inv' : ∀ (x : G), self.toFun x⁻¹ = self.toFun x

The seminorm is invariant under inversion.

Instances For
theorem GroupSeminorm.map_one' {G : Type u_7} [] (self : ) :
self.toFun 1 = 0

The image of one is zero.

theorem GroupSeminorm.mul_le' {G : Type u_7} [] (self : ) (x : G) (y : G) :
self.toFun (x * y) self.toFun x + self.toFun y

The seminorm applied to a product is dominated by the sum of the seminorm applied to the factors.

theorem GroupSeminorm.inv' {G : Type u_7} [] (self : ) (x : G) :
self.toFun x⁻¹ = self.toFun x

The seminorm is invariant under inversion.

structure NonarchAddGroupSeminorm (G : Type u_7) [] extends :
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.

• toFun : G
• map_zero' : self.toFun 0 = 0
• add_le_max' : ∀ (r s : G), self.toFun (r + s) max (self.toFun r) (self.toFun s)

The seminorm applied to a sum is dominated by the maximum of the function applied to the addends.

• neg' : ∀ (r : G), self.toFun (-r) = self.toFun r

The seminorm is invariant under negation.

Instances For
theorem NonarchAddGroupSeminorm.add_le_max' {G : Type u_7} [] (self : ) (r : G) (s : G) :
self.toFun (r + s) max (self.toFun r) (self.toFun s)

The seminorm applied to a sum is dominated by the maximum of the function applied to the addends.

theorem NonarchAddGroupSeminorm.neg' {G : Type u_7} [] (self : ) (r : G) :
self.toFun (-r) = self.toFun r

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.

structure AddGroupNorm (G : Type u_7) [] extends :
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.

• toFun : G
• map_zero' : self.toFun 0 = 0
• add_le' : ∀ (r s : G), self.toFun (r + s) self.toFun r + self.toFun s
• neg' : ∀ (r : G), self.toFun (-r) = self.toFun r
• eq_zero_of_map_eq_zero' : ∀ (x : G), self.toFun x = 0x = 0

If the image under the seminorm is zero, then the argument is zero.

Instances For
theorem AddGroupNorm.eq_zero_of_map_eq_zero' {G : Type u_7} [] (self : ) (x : G) :
self.toFun x = 0x = 0

If the image under the seminorm is zero, then the argument is zero.

structure GroupNorm (G : Type u_7) [] extends :
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.

• toFun : G
• map_one' : self.toFun 1 = 0
• mul_le' : ∀ (x y : G), self.toFun (x * y) self.toFun x + self.toFun y
• inv' : ∀ (x : G), self.toFun x⁻¹ = self.toFun x
• eq_one_of_map_eq_zero' : ∀ (x : G), self.toFun x = 0x = 1

If the image under the norm is zero, then the argument is one.

Instances For
theorem GroupNorm.eq_one_of_map_eq_zero' {G : Type u_7} [] (self : ) (x : G) :
self.toFun x = 0x = 1

If the image under the norm is zero, then the argument is one.

structure NonarchAddGroupNorm (G : Type u_7) [] extends :
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.

• toFun : G
• map_zero' : self.toFun 0 = 0
• add_le_max' : ∀ (r s : G), self.toFun (r + s) max (self.toFun r) (self.toFun s)
• neg' : ∀ (r : G), self.toFun (-r) = self.toFun r
• eq_zero_of_map_eq_zero' : ∀ (x : G), self.toFun x = 0x = 0

If the image under the norm is zero, then the argument is zero.

Instances For
theorem NonarchAddGroupNorm.eq_zero_of_map_eq_zero' {G : Type u_7} [] (self : ) (x : G) :
self.toFun x = 0x = 0

If the image under the norm is zero, then the argument is zero.

class NonarchAddGroupSeminormClass (F : Type u_7) (α : outParam (Type u_8)) [] [FunLike F α ] extends :

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_add_le_max : ∀ (f : F) (a b : α), f (a + b) max (f a) (f b)
• map_zero : ∀ (f : F), f 0 = 0

The image of zero is zero.

• map_neg_eq_map' : ∀ (f : F) (a : α), f (-a) = f a

The seminorm is invariant under negation.

Instances
theorem NonarchAddGroupSeminormClass.map_zero {F : Type u_7} {α : outParam (Type u_8)} [] [FunLike F α ] [self : ] (f : F) :
f 0 = 0

The image of zero is zero.

theorem NonarchAddGroupSeminormClass.map_neg_eq_map' {F : Type u_7} {α : outParam (Type u_8)} [] [FunLike F α ] [self : ] (f : F) (a : α) :
f (-a) = f a

The seminorm is invariant under negation.

class NonarchAddGroupNormClass (F : Type u_7) (α : outParam (Type u_8)) [] [FunLike F α ] extends :

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_add_le_max : ∀ (f : F) (a b : α), f (a + b) max (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 = 0a = 0

If the image under the norm is zero, then the argument is zero.

Instances
theorem NonarchAddGroupNormClass.eq_zero_of_map_eq_zero {F : Type u_7} {α : outParam (Type u_8)} [] [FunLike F α ] [self : ] (f : F) {a : α} :
f a = 0a = 0

If the image under the norm is zero, then the argument is zero.

theorem map_sub_le_max {E : Type u_4} {F : Type u_5} [] [FunLike F E ] (f : F) (x : E) (y : E) :
f (x - y) max (f x) (f y)
@[instance 100]
Equations
• =
@[instance 100]
instance NonarchAddGroupNormClass.toAddGroupNormClass {E : Type u_4} {F : Type u_5} [FunLike F E ] [] [] :
Equations
• =

### Seminorms #

instance AddGroupSeminorm.funLike {E : Type u_4} [] :
Equations
• AddGroupSeminorm.funLike = { coe := fun (f : ) => f.toFun, coe_injective' := }
theorem AddGroupSeminorm.funLike.proof_1 {E : Type u_1} [] (f : ) (g : ) (h : (fun (f : ) => f.toFun) f = (fun (f : ) => f.toFun) g) :
f = g
instance GroupSeminorm.funLike {E : Type u_4} [] :
Equations
• GroupSeminorm.funLike = { coe := fun (f : ) => f.toFun, coe_injective' := }
Equations
• =
instance GroupSeminorm.groupSeminormClass {E : Type u_4} [] :
Equations
• =
instance AddGroupSeminorm.instCoeFunForallReal {E : Type u_4} [] :
CoeFun () fun (x : ) => E

Helper instance for when there's too many metavariables to apply DFunLike.hasCoeToFun.

Equations
• AddGroupSeminorm.instCoeFunForallReal = { coe := DFunLike.coe }
instance GroupSeminorm.instCoeFunForallReal {E : Type u_4} [] :
CoeFun () fun (x : ) => E

Helper instance for when there's too many metavariables to apply DFunLike.hasCoeToFun.

Equations
• GroupSeminorm.instCoeFunForallReal = { coe := DFunLike.coe }
@[simp]
theorem AddGroupSeminorm.toFun_eq_coe {E : Type u_4} [] {p : } :
p.toFun = p
@[simp]
theorem GroupSeminorm.toFun_eq_coe {E : Type u_4} [] {p : } :
p.toFun = p
theorem AddGroupSeminorm.ext {E : Type u_4} [] {p : } {q : } :
(∀ (x : E), p x = q x)p = q
theorem GroupSeminorm.ext {E : Type u_4} [] {p : } {q : } :
(∀ (x : E), p x = q x)p = q
instance AddGroupSeminorm.instPartialOrder {E : Type u_4} [] :
Equations
instance GroupSeminorm.instPartialOrder {E : Type u_4} [] :
Equations
theorem AddGroupSeminorm.le_def {E : Type u_4} [] {p : } {q : } :
p q p q
theorem GroupSeminorm.le_def {E : Type u_4} [] {p : } {q : } :
p q p q
theorem AddGroupSeminorm.lt_def {E : Type u_4} [] {p : } {q : } :
p < q p < q
theorem GroupSeminorm.lt_def {E : Type u_4} [] {p : } {q : } :
p < q p < q
@[simp]
theorem AddGroupSeminorm.coe_le_coe {E : Type u_4} [] {p : } {q : } :
p q p q
@[simp]
theorem GroupSeminorm.coe_le_coe {E : Type u_4} [] {p : } {q : } :
p q p q
@[simp]
theorem AddGroupSeminorm.coe_lt_coe {E : Type u_4} [] {p : } {q : } :
p < q p < q
@[simp]
theorem GroupSeminorm.coe_lt_coe {E : Type u_4} [] {p : } {q : } :
p < q p < q
Equations
• AddGroupSeminorm.instZeroAddGroupSeminorm = { zero := { toFun := 0, map_zero' := , add_le' := , neg' := } }
∀ (x : E), 0 (-x) = 0 (-x)
∀ (x x_1 : E), 0 (x + x_1) 0 + 0 (x + x_1)
Equations
• GroupSeminorm.instZeroGroupSeminorm = { zero := { toFun := 0, map_one' := , mul_le' := , inv' := } }
@[simp]
theorem AddGroupSeminorm.coe_zero {E : Type u_4} [] :
0 = 0
@[simp]
theorem GroupSeminorm.coe_zero {E : Type u_4} [] :
0 = 0
@[simp]
theorem AddGroupSeminorm.zero_apply {E : Type u_4} [] (x : E) :
0 x = 0
@[simp]
theorem GroupSeminorm.zero_apply {E : Type u_4} [] (x : E) :
0 x = 0
instance AddGroupSeminorm.instInhabited {E : Type u_4} [] :
Equations
• AddGroupSeminorm.instInhabited = { default := 0 }
instance GroupSeminorm.instInhabited {E : Type u_4} [] :
Equations
• GroupSeminorm.instInhabited = { default := 0 }
theorem AddGroupSeminorm.instAdd.proof_1 {E : Type u_1} [] (p : ) (q : ) :
(fun (x : E) => p x + q x) 0 = 0
theorem AddGroupSeminorm.instAdd.proof_2 {E : Type u_1} [] (p : ) (q : ) :
∀ (x x_1 : E), p (x + x_1) + q (x + x_1) (fun (x : E) => p x + q x) x + (fun (x : E) => p x + q x) x_1
Equations
• AddGroupSeminorm.instAdd = { add := fun (p q : ) => { toFun := fun (x : E) => p x + q x, map_zero' := , add_le' := , neg' := } }
theorem AddGroupSeminorm.instAdd.proof_3 {E : Type u_1} [] (p : ) (q : ) (x : E) :
(fun (x : E) => p x + q x) (-x) = (fun (x : E) => p x + q x) x
instance GroupSeminorm.instAdd {E : Type u_4} [] :
Equations
• GroupSeminorm.instAdd = { add := fun (p q : ) => { toFun := fun (x : E) => p x + q x, map_one' := , mul_le' := , inv' := } }
@[simp]
theorem AddGroupSeminorm.coe_add {E : Type u_4} [] (p : ) (q : ) :
(p + q) = p + q
@[simp]
theorem GroupSeminorm.coe_add {E : Type u_4} [] (p : ) (q : ) :
(p + q) = p + q
@[simp]
theorem AddGroupSeminorm.add_apply {E : Type u_4} [] (p : ) (q : ) (x : E) :
(p + q) x = p x + q x
@[simp]
theorem GroupSeminorm.add_apply {E : Type u_4} [] (p : ) (q : ) (x : E) :
(p + q) x = p x + q x
theorem AddGroupSeminorm.instSup.proof_1 {E : Type u_1} [] (p : ) (q : ) :
(p q) 0 = 0
theorem AddGroupSeminorm.instSup.proof_3 {E : Type u_1} [] (p : ) (q : ) (x : E) :
(p q) (-x) = (p q) x
instance AddGroupSeminorm.instSup {E : Type u_4} [] :
Equations
• AddGroupSeminorm.instSup = { sup := fun (p q : ) => { toFun := p q, map_zero' := , add_le' := , neg' := } }
theorem AddGroupSeminorm.instSup.proof_2 {E : Type u_1} [] (p : ) (q : ) (x : E) (y : E) :
p (x + y) q (x + y) (p q) x + (p q) y
instance GroupSeminorm.instSup {E : Type u_4} [] :
Sup ()
Equations
• GroupSeminorm.instSup = { sup := fun (p q : ) => { toFun := p q, map_one' := , mul_le' := , inv' := } }
@[simp]
theorem AddGroupSeminorm.coe_sup {E : Type u_4} [] (p : ) (q : ) :
(p q) = p q
@[simp]
theorem GroupSeminorm.coe_sup {E : Type u_4} [] (p : ) (q : ) :
(p q) = p q
@[simp]
theorem AddGroupSeminorm.sup_apply {E : Type u_4} [] (p : ) (q : ) (x : E) :
(p q) x = p x q x
@[simp]
theorem GroupSeminorm.sup_apply {E : Type u_4} [] (p : ) (q : ) (x : E) :
(p q) x = p x q x
instance AddGroupSeminorm.semilatticeSup {E : Type u_4} [] :
Equations
instance GroupSeminorm.semilatticeSup {E : Type u_4} [] :
Equations
theorem AddGroupSeminorm.comp.proof_1 {E : Type u_1} {F : Type u_2} [] [] (p : ) (f : F →+ E) :
(fun (x : F) => p (f x)) 0 = 0
theorem AddGroupSeminorm.comp.proof_3 {E : Type u_1} {F : Type u_2} [] [] (p : ) (f : F →+ E) (x : F) :
(fun (x : F) => p (f x)) (-x) = (fun (x : F) => p (f x)) x
theorem AddGroupSeminorm.comp.proof_2 {E : Type u_1} {F : Type u_2} [] [] (p : ) (f : F →+ E) :
∀ (x x_1 : F), p (f (x + x_1)) (fun (x : F) => p (f x)) x + (fun (x : F) => p (f x)) x_1
def AddGroupSeminorm.comp {E : Type u_4} {F : Type u_5} [] [] (p : ) (f : F →+ E) :

Equations
• p.comp f = { toFun := fun (x : F) => p (f x), map_zero' := , add_le' := , neg' := }
Instances For
def GroupSeminorm.comp {E : Type u_4} {F : Type u_5} [] [] (p : ) (f : F →* E) :

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
@[simp]
theorem AddGroupSeminorm.coe_comp {E : Type u_4} {F : Type u_5} [] [] (p : ) (f : F →+ E) :
(p.comp f) = p f
@[simp]
theorem GroupSeminorm.coe_comp {E : Type u_4} {F : Type u_5} [] [] (p : ) (f : F →* E) :
(p.comp f) = p f
@[simp]
theorem AddGroupSeminorm.comp_apply {E : Type u_4} {F : Type u_5} [] [] (p : ) (f : F →+ E) (x : F) :
(p.comp f) x = p (f x)
@[simp]
theorem GroupSeminorm.comp_apply {E : Type u_4} {F : Type u_5} [] [] (p : ) (f : F →* E) (x : F) :
(p.comp f) x = p (f x)
@[simp]
theorem AddGroupSeminorm.comp_id {E : Type u_4} [] (p : ) :
p.comp () = p
@[simp]
theorem GroupSeminorm.comp_id {E : Type u_4} [] (p : ) :
p.comp () = p
@[simp]
theorem AddGroupSeminorm.comp_zero {E : Type u_4} {F : Type u_5} [] [] (p : ) :
p.comp 0 = 0
@[simp]
theorem GroupSeminorm.comp_zero {E : Type u_4} {F : Type u_5} [] [] (p : ) :
p.comp 1 = 0
@[simp]
theorem AddGroupSeminorm.zero_comp {E : Type u_4} {F : Type u_5} [] [] (f : F →+ E) :
@[simp]
theorem GroupSeminorm.zero_comp {E : Type u_4} {F : Type u_5} [] [] (f : F →* E) :
= 0
theorem AddGroupSeminorm.comp_assoc {E : Type u_4} {F : Type u_5} {G : Type u_6} [] [] [] (p : ) (g : F →+ E) (f : G →+ F) :
p.comp (g.comp f) = (p.comp g).comp f
theorem GroupSeminorm.comp_assoc {E : Type u_4} {F : Type u_5} {G : Type u_6} [] [] [] (p : ) (g : F →* E) (f : G →* F) :
p.comp (g.comp f) = (p.comp g).comp f
theorem AddGroupSeminorm.add_comp {E : Type u_4} {F : Type u_5} [] [] (p : ) (q : ) (f : F →+ E) :
(p + q).comp f = p.comp f + q.comp f
theorem GroupSeminorm.add_comp {E : Type u_4} {F : Type u_5} [] [] (p : ) (q : ) (f : F →* E) :
(p + q).comp f = p.comp f + q.comp f
theorem AddGroupSeminorm.comp_mono {E : Type u_4} {F : Type u_5} [] [] {p : } {q : } (f : F →+ E) (hp : p q) :
p.comp f q.comp f
theorem GroupSeminorm.comp_mono {E : Type u_4} {F : Type u_5} [] [] {p : } {q : } (f : F →* E) (hp : p q) :
p.comp f q.comp f
theorem AddGroupSeminorm.comp_add_le {E : Type u_4} {F : Type u_5} [] [] (p : ) (f : F →+ E) (g : F →+ E) :
p.comp (f + g) p.comp f + p.comp g
theorem GroupSeminorm.comp_mul_le {E : Type u_4} {F : Type u_5} [] [] (p : ) (f : F →* E) (g : F →* E) :
p.comp (f * g) p.comp f + p.comp g
theorem AddGroupSeminorm.add_bddBelow_range_add {E : Type u_4} [] {p : } {q : } {x : E} :
BddBelow (Set.range fun (y : E) => p y + q (x - y))
theorem GroupSeminorm.mul_bddBelow_range_add {E : Type u_4} [] {p : } {q : } {x : E} :
BddBelow (Set.range fun (y : E) => p y + q (x / y))
theorem AddGroupSeminorm.instInf.proof_2 {E : Type u_1} [] (p : ) (q : ) (x : E) (y : E) :
(fun (x : E) => ⨅ (y : E), p y + q (x - y)) (x + y) (⨅ (y : E), p y + q (x - y)) + ⨅ (y_1 : E), p y_1 + q (y - y_1)
theorem AddGroupSeminorm.instInf.proof_3 {E : Type u_1} [] (p : ) (q : ) (x : E) :
⨅ (y : E), p y + q (-x - y) = (fun (x : E) => ⨅ (y : E), p y + q (x - y)) x
theorem AddGroupSeminorm.instInf.proof_1 {E : Type u_1} [] (p : ) (q : ) :
⨅ (i : E), p i + q (0 - i) = 0
noncomputable instance AddGroupSeminorm.instInf {E : Type u_4} [] :
Equations
• AddGroupSeminorm.instInf = { inf := fun (p q : ) => { toFun := fun (x : E) => ⨅ (y : E), p y + q (x - y), map_zero' := , add_le' := , neg' := } }
noncomputable instance GroupSeminorm.instInf {E : Type u_4} [] :
Inf ()
Equations
• GroupSeminorm.instInf = { inf := fun (p q : ) => { toFun := fun (x : E) => ⨅ (y : E), p y + q (x / y), map_one' := , mul_le' := , inv' := } }
@[simp]
theorem AddGroupSeminorm.inf_apply {E : Type u_4} [] (p : ) (q : ) (x : E) :
(p q) x = ⨅ (y : E), p y + q (x - y)
@[simp]
theorem GroupSeminorm.inf_apply {E : Type u_4} [] (p : ) (q : ) (x : E) :
(p q) x = ⨅ (y : E), p y + q (x / y)
theorem AddGroupSeminorm.instLattice.proof_3 {E : Type u_1} [] (a : ) (b : ) (c : ) (hb : a b) (hc : a c) (x : E) :
(fun (f : ) => f) a x ⨅ (y : E), b y + c (x - y)
theorem AddGroupSeminorm.instLattice.proof_2 {E : Type u_1} [] (p : ) (q : ) (x : E) :
⨅ (y : E), p y + q (x - y) (fun (f : ) => f) q x
noncomputable instance AddGroupSeminorm.instLattice {E : Type u_4} [] :
Equations
theorem AddGroupSeminorm.instLattice.proof_1 {E : Type u_1} [] (p : ) (q : ) (x : E) :
⨅ (y : E), p y + q (x - y) (fun (f : ) => f) p x
noncomputable instance GroupSeminorm.instLattice {E : Type u_4} [] :
Equations
• GroupSeminorm.instLattice = let __src := GroupSeminorm.semilatticeSup; Lattice.mk
instance AddGroupSeminorm.toOne {E : Type u_4} [] [] :
Equations
• AddGroupSeminorm.toOne = { one := { toFun := fun (x : E) => if x = 0 then 0 else 1, map_zero' := , add_le' := , neg' := } }
@[simp]
theorem AddGroupSeminorm.apply_one {E : Type u_4} [] [] (x : E) :
1 x = if x = 0 then 0 else 1
instance AddGroupSeminorm.toSMul {R : Type u_2} {E : Type u_4} [] [] [] [] :
SMul R ()

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

Equations
• AddGroupSeminorm.toSMul = { smul := fun (r : R) (p : ) => { toFun := fun (x : E) => r p x, map_zero' := , add_le' := , neg' := } }
@[simp]
theorem AddGroupSeminorm.coe_smul {R : Type u_2} {E : Type u_4} [] [] [] [] (r : R) (p : ) :
(r p) = r p
@[simp]
theorem AddGroupSeminorm.smul_apply {R : Type u_2} {E : Type u_4} [] [] [] [] (r : R) (p : ) (x : E) :
(r p) x = r p x
instance AddGroupSeminorm.isScalarTower {R : Type u_2} {R' : Type u_3} {E : Type u_4} [] [] [] [] [SMul R' ] [] [] [SMul R R'] [] :
Equations
• =
theorem AddGroupSeminorm.smul_sup {R : Type u_2} {E : Type u_4} [] [] [] [] (r : R) (p : ) (q : ) :
r (p q) = r p r q
instance NonarchAddGroupSeminorm.funLike {E : Type u_4} [] :
Equations
• NonarchAddGroupSeminorm.funLike = { coe := fun (f : ) => f.toFun, coe_injective' := }
Equations
• =
instance NonarchAddGroupSeminorm.instCoeFunForallReal {E : Type u_4} [] :
CoeFun fun (x : ) => E

Helper instance for when there's too many metavariables to apply DFunLike.hasCoeToFun.

Equations
• NonarchAddGroupSeminorm.instCoeFunForallReal = { coe := DFunLike.coe }
@[simp]
theorem NonarchAddGroupSeminorm.toZeroHom_eq_coe {E : Type u_4} [] {p : } :
p.toZeroHom = p
theorem NonarchAddGroupSeminorm.ext {E : Type u_4} [] {p : } {q : } :
(∀ (x : E), p x = q x)p = q
noncomputable instance NonarchAddGroupSeminorm.instPartialOrder {E : Type u_4} [] :
Equations
theorem NonarchAddGroupSeminorm.le_def {E : Type u_4} [] {p : } {q : } :
p q p q
theorem NonarchAddGroupSeminorm.lt_def {E : Type u_4} [] {p : } {q : } :
p < q p < q
@[simp]
theorem NonarchAddGroupSeminorm.coe_le_coe {E : Type u_4} [] {p : } {q : } :
p q p q
@[simp]
theorem NonarchAddGroupSeminorm.coe_lt_coe {E : Type u_4} [] {p : } {q : } :
p < q p < q
instance NonarchAddGroupSeminorm.instZero {E : Type u_4} [] :
Equations
• NonarchAddGroupSeminorm.instZero = { zero := { toFun := 0, map_zero' := , add_le_max' := , neg' := } }
@[simp]
theorem NonarchAddGroupSeminorm.coe_zero {E : Type u_4} [] :
0 = 0
@[simp]
theorem NonarchAddGroupSeminorm.zero_apply {E : Type u_4} [] (x : E) :
0 x = 0
Equations
• NonarchAddGroupSeminorm.instInhabited = { default := 0 }
instance NonarchAddGroupSeminorm.instSup {E : Type u_4} [] :
Equations
• NonarchAddGroupSeminorm.instSup = { sup := fun (p q : ) => { toFun := p q, map_zero' := , add_le_max' := , neg' := } }
@[simp]
theorem NonarchAddGroupSeminorm.coe_sup {E : Type u_4} [] (p : ) (q : ) :
(p q) = p q
@[simp]
theorem NonarchAddGroupSeminorm.sup_apply {E : Type u_4} [] (p : ) (q : ) (x : E) :
(p q) x = p x q x
noncomputable instance NonarchAddGroupSeminorm.instSemilatticeSup {E : Type u_4} [] :
Equations
theorem NonarchAddGroupSeminorm.add_bddBelow_range_add {E : Type u_4} [] {p : } {q : } {x : E} :
BddBelow (Set.range fun (y : E) => p y + q (x - y))
instance GroupSeminorm.toOne {E : Type u_4} [] [] :
One ()
Equations
• GroupSeminorm.toOne = { one := { toFun := fun (x : E) => if x = 1 then 0 else 1, map_one' := , mul_le' := , inv' := } }
@[simp]
theorem GroupSeminorm.apply_one {E : Type u_4} [] [] (x : E) :
1 x = if x = 1 then 0 else 1
instance GroupSeminorm.instSMul {R : Type u_2} {E : Type u_4} [] [] [] [] :
SMul R ()

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

Equations
• GroupSeminorm.instSMul = { smul := fun (r : R) (p : ) => { toFun := fun (x : E) => r p x, map_one' := , mul_le' := , inv' := } }
instance GroupSeminorm.instIsScalarTowerOfReal {R : Type u_2} {R' : Type u_3} {E : Type u_4} [] [] [] [] [SMul R' ] [] [] [SMul R R'] [] :
Equations
• =
@[simp]
theorem GroupSeminorm.coe_smul {R : Type u_2} {E : Type u_4} [] [] [] [] (r : R) (p : ) :
(r p) = r p
@[simp]
theorem GroupSeminorm.smul_apply {R : Type u_2} {E : Type u_4} [] [] [] [] (r : R) (p : ) (x : E) :
(r p) x = r p x
theorem GroupSeminorm.smul_sup {R : Type u_2} {E : Type u_4} [] [] [] [] (r : R) (p : ) (q : ) :
r (p q) = r p r q
Equations
• NonarchAddGroupSeminorm.instOneOfDecidableEq = { one := { toFun := fun (x : E) => if x = 0 then 0 else 1, map_zero' := , add_le_max' := , neg' := } }
@[simp]
theorem NonarchAddGroupSeminorm.apply_one {E : Type u_4} [] [] (x : E) :
1 x = if x = 0 then 0 else 1
instance NonarchAddGroupSeminorm.instSMul {R : Type u_2} {E : Type u_4} [] [] [] [] :

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

Equations
• NonarchAddGroupSeminorm.instSMul = { smul := fun (r : R) (p : ) => { toFun := fun (x : E) => r p x, map_zero' := , add_le_max' := , neg' := } }
instance NonarchAddGroupSeminorm.instIsScalarTowerOfReal {R : Type u_2} {R' : Type u_3} {E : Type u_4} [] [] [] [] [SMul R' ] [] [] [SMul R R'] [] :
Equations
• =
@[simp]
theorem NonarchAddGroupSeminorm.coe_smul {R : Type u_2} {E : Type u_4} [] [] [] [] (r : R) (p : ) :
(r p) = r p
@[simp]
theorem NonarchAddGroupSeminorm.smul_apply {R : Type u_2} {E : Type u_4} [] [] [] [] (r : R) (p : ) (x : E) :
(r p) x = r p x
theorem NonarchAddGroupSeminorm.smul_sup {R : Type u_2} {E : Type u_4} [] [] [] [] (r : R) (p : ) (q : ) :
r (p q) = r p r q

### Norms #

instance AddGroupNorm.funLike {E : Type u_4} [] :
Equations
• AddGroupNorm.funLike = { coe := fun (f : ) => f.toFun, coe_injective' := }
theorem AddGroupNorm.funLike.proof_1 {E : Type u_1} [] (f : ) (g : ) (h : (fun (f : ) => f.toFun) f = (fun (f : ) => f.toFun) g) :
f = g
instance GroupNorm.funLike {E : Type u_4} [] :
Equations
• GroupNorm.funLike = { coe := fun (f : ) => f.toFun, coe_injective' := }
Equations
• =
instance GroupNorm.groupNormClass {E : Type u_4} [] :
Equations
• =
instance AddGroupNorm.instCoeFunForallReal {E : Type u_4} [] :
CoeFun () fun (x : ) => E

Helper instance for when there's too many metavariables to apply DFunLike.hasCoeToFun directly.

Equations
instance GroupNorm.instCoeFunForallReal {E : Type u_4} [] :
CoeFun () fun (x : ) => E

Helper instance for when there's too many metavariables to apply DFunLike.hasCoeToFun directly.

Equations
• GroupNorm.instCoeFunForallReal = DFunLike.hasCoeToFun
@[simp]
@[simp]
theorem GroupNorm.toGroupSeminorm_eq_coe {E : Type u_4} [] {p : } :
p.toGroupSeminorm = p
theorem AddGroupNorm.ext {E : Type u_4} [] {p : } {q : } :
(∀ (x : E), p x = q x)p = q
theorem GroupNorm.ext {E : Type u_4} [] {p : } {q : } :
(∀ (x : E), p x = q x)p = q
instance AddGroupNorm.instPartialOrder {E : Type u_4} [] :
Equations
instance GroupNorm.instPartialOrder {E : Type u_4} [] :
Equations
theorem AddGroupNorm.le_def {E : Type u_4} [] {p : } {q : } :
p q p q
theorem GroupNorm.le_def {E : Type u_4} [] {p : } {q : } :
p q p q
theorem AddGroupNorm.lt_def {E : Type u_4} [] {p : } {q : } :
p < q p < q
theorem GroupNorm.lt_def {E : Type u_4} [] {p : } {q : } :
p < q p < q
@[simp]
theorem AddGroupNorm.coe_le_coe {E : Type u_4} [] {p : } {q : } :
p q p q
@[simp]
theorem GroupNorm.coe_le_coe {E : Type u_4} [] {p : } {q : } :
p q p q
@[simp]
theorem AddGroupNorm.coe_lt_coe {E : Type u_4} [] {p : } {q : } :
p < q p < q
@[simp]
theorem GroupNorm.coe_lt_coe {E : Type u_4} [] {p : } {q : } :
p < q p < q
Equations
• One or more equations did not get rendered due to their size.
theorem AddGroupNorm.instAdd.proof_1 {E : Type u_1} [] (p : ) (q : ) (_x : E) (hx : (p.toAddGroupSeminorm + q.toAddGroupSeminorm).toFun _x = 0) :
_x = 0
instance GroupNorm.instAdd {E : Type u_4} [] :
Equations
• GroupNorm.instAdd = { add := fun (p q : ) => let __src := p.toGroupSeminorm + q.toGroupSeminorm; { toGroupSeminorm := __src, eq_one_of_map_eq_zero' := } }
@[simp]
theorem AddGroupNorm.coe_add {E : Type u_4} [] (p : ) (q : ) :
(p + q) = p + q
@[simp]
theorem GroupNorm.coe_add {E : Type u_4} [] (p : ) (q : ) :
(p + q) = p + q
@[simp]
theorem AddGroupNorm.add_apply {E : Type u_4} [] (p : ) (q : ) (x : E) :
(p + q) x = p x + q x
@[simp]
theorem GroupNorm.add_apply {E : Type u_4} [] (p : ) (q : ) (x : E) :
(p + q) x = p x + q x
instance AddGroupNorm.instSup {E : Type u_4} [] :
Sup ()
Equations
• One or more equations did not get rendered due to their size.
theorem AddGroupNorm.instSup.proof_1 {E : Type u_1} [] (p : ) (q : ) (_x : E) (hx : (p.toAddGroupSeminorm q.toAddGroupSeminorm).toFun _x = 0) :
_x = 0
instance GroupNorm.instSup {E : Type u_4} [] :
Sup ()
Equations
• GroupNorm.instSup = { sup := fun (p q : ) => let __src := p.toGroupSeminorm q.toGroupSeminorm; { toGroupSeminorm := __src, eq_one_of_map_eq_zero' := } }
@[simp]
theorem AddGroupNorm.coe_sup {E : Type u_4} [] (p : ) (q : ) :
(p q) = p q
@[simp]
theorem GroupNorm.coe_sup {E : Type u_4} [] (p : ) (q : ) :
(p q) = p q
@[simp]
theorem AddGroupNorm.sup_apply {E : Type u_4} [] (p : ) (q : ) (x : E) :
(p q) x = p x q x
@[simp]
theorem GroupNorm.sup_apply {E : Type u_4} [] (p : ) (q : ) (x : E) :
(p q) x = p x q x
instance AddGroupNorm.instSemilatticeSup {E : Type u_4} [] :
Equations
instance GroupNorm.instSemilatticeSup {E : Type u_4} [] :
Equations
instance AddGroupNorm.instOne {E : Type u_4} [] [] :
One ()
Equations
• AddGroupNorm.instOne = { one := let __src := 1; { toAddGroupSeminorm := __src, eq_zero_of_map_eq_zero' := } }
@[simp]
theorem AddGroupNorm.apply_one {E : Type u_4} [] [] (x : E) :
1 x = if x = 0 then 0 else 1
instance AddGroupNorm.instInhabited {E : Type u_4} [] [] :
Equations
• AddGroupNorm.instInhabited = { default := 1 }
instance AddGroupNorm.toOne {E : Type u_4} [] [] :
One ()
Equations
• AddGroupNorm.toOne = { one := let __src := 1; { toAddGroupSeminorm := __src, eq_zero_of_map_eq_zero' := } }
instance GroupNorm.toOne {E : Type u_4} [] [] :
One ()
Equations
• GroupNorm.toOne = { one := let __src := 1; { toGroupSeminorm := __src, eq_one_of_map_eq_zero' := } }
@[simp]
theorem GroupNorm.apply_one {E : Type u_4} [] [] (x : E) :
1 x = if x = 1 then 0 else 1
instance GroupNorm.instInhabited {E : Type u_4} [] [] :
Equations
• GroupNorm.instInhabited = { default := 1 }
instance NonarchAddGroupNorm.funLike {E : Type u_4} [] :
Equations
• NonarchAddGroupNorm.funLike = { coe := fun (f : ) => f.toFun, coe_injective' := }
Equations
• =
noncomputable instance NonarchAddGroupNorm.instCoeFunForallReal {E : Type u_4} [] :
CoeFun fun (x : ) => E

Helper instance for when there's too many metavariables to apply DFunLike.hasCoeToFun.

Equations
@[simp]
theorem NonarchAddGroupNorm.ext {E : Type u_4} [] {p : } {q : } :
(∀ (x : E), p x = q x)p = q
noncomputable instance NonarchAddGroupNorm.instPartialOrder {E : Type u_4} [] :
Equations
theorem NonarchAddGroupNorm.le_def {E : Type u_4} [] {p : } {q : } :
p q p q
theorem NonarchAddGroupNorm.lt_def {E : Type u_4} [] {p : } {q : } :
p < q p < q
@[simp]
theorem NonarchAddGroupNorm.coe_le_coe {E : Type u_4} [] {p : } {q : } :
p q p q
@[simp]
theorem NonarchAddGroupNorm.coe_lt_coe {E : Type u_4} [] {p : } {q : } :
p < q p < q
instance NonarchAddGroupNorm.instSup {E : Type u_4} [] :
Equations
• One or more equations did not get rendered due to their size.
@[simp]
theorem NonarchAddGroupNorm.coe_sup {E : Type u_4} [] (p : ) (q : ) :
(p q) = p q
@[simp]
theorem NonarchAddGroupNorm.sup_apply {E : Type u_4} [] (p : ) (q : ) (x : E) :
(p q) x = p x q x
noncomputable instance NonarchAddGroupNorm.instSemilatticeSup {E : Type u_4} [] :
Equations
Equations
• NonarchAddGroupNorm.instOneOfDecidableEq = { one := let __src := 1; { toNonarchAddGroupSeminorm := __src, eq_zero_of_map_eq_zero' := } }
@[simp]
theorem NonarchAddGroupNorm.apply_one {E : Type u_4} [] [] (x : E) :
1 x = if x = 0 then 0 else 1
Equations
• NonarchAddGroupNorm.instInhabitedOfDecidableEq = { default := 1 }