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) [AddGroup 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.

• 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

  The seminorm is subadditive.

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

  The seminorm is invariant under negation.

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

The image of zero is zero.

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

The seminorm is subadditive.

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

The seminorm is invariant under negation.

structure GroupSeminorm (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.

• 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.

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

The image of one is zero.

theorem GroupSeminorm.mul_le' {G : Type u_7} [Group G] (self : GroupSeminorm G) (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} [Group G] (self : GroupSeminorm G) (x : G) : self.toFun x⁻¹ = self.toFun x

The seminorm is invariant under inversion.

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

theorem NonarchAddGroupSeminorm.add_le_max' {G : Type u_7} [AddGroup G] (self : NonarchAddGroupSeminorm G) (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} [AddGroup G] (self : NonarchAddGroupSeminorm G) (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) [AddGroup G] extends AddGroupSeminorm : 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 = 0 → x = 0

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

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

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

structure GroupNorm (G : Type u_7) [Group G] extends GroupSeminorm : 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 = 0 → x = 1

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

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

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

structure NonarchAddGroupNorm (G : Type u_7) [AddGroup G] extends NonarchAddGroupSeminorm : 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 = 0 → x = 0

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

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

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

class NonarchAddGroupSeminormClass (F : Type u_7) (α : outParam (Type u_8)) [AddGroup α] [FunLike F α ℝ] extends NonarchimedeanHomClass : Prop

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.

theorem NonarchAddGroupSeminormClass.map_zero {F : Type u_7} {α : outParam (Type u_8)} [AddGroup α] [FunLike F α ℝ] [self : NonarchAddGroupSeminormClass F α] (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)} [AddGroup α] [FunLike F α ℝ] [self : NonarchAddGroupSeminormClass F α] (f : F) (a : α) : f (-a) = f a

The seminorm is invariant under negation.

class NonarchAddGroupNormClass (F : Type u_7) (α : outParam (Type u_8)) [AddGroup α] [FunLike F α ℝ] extends NonarchAddGroupSeminormClass : Prop

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 = 0 → a = 0

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

theorem NonarchAddGroupNormClass.eq_zero_of_map_eq_zero {F : Type u_7} {α : outParam (Type u_8)} [AddGroup α] [FunLike F α ℝ] [self : NonarchAddGroupNormClass F α] (f : F) {a : α} : f a = 0 → a = 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} [AddGroup E] [FunLike F E ℝ] [NonarchAddGroupSeminormClass F E] (f : F) (x : E) (y : E) : f (x - y) ≤ max (f x) (f y)

@[instance 100]

instance NonarchAddGroupSeminormClass.toAddGroupSeminormClass {E : Type u_4} {F : Type u_5} [FunLike F E ℝ] [AddGroup E] [NonarchAddGroupSeminormClass F E] : AddGroupSeminormClass F E ℝ

Equations

• ⋯ = ⋯

@[instance 100]

instance NonarchAddGroupNormClass.toAddGroupNormClass {E : Type u_4} {F : Type u_5} [FunLike F E ℝ] [AddGroup E] [NonarchAddGroupNormClass F E] : AddGroupNormClass F E ℝ

Equations

• ⋯ = ⋯

Seminorms

instance AddGroupSeminorm.funLike {E : Type u_4} [AddGroup E] : FunLike (AddGroupSeminorm E) E ℝ

Equations

• AddGroupSeminorm.funLike = { coe := fun (f : AddGroupSeminorm E) => f.toFun, coe_injective' := ⋯ }

theorem AddGroupSeminorm.funLike.proof_1 {E : Type u_1} [AddGroup E] (f : AddGroupSeminorm E) (g : AddGroupSeminorm E) (h : (fun (f : AddGroupSeminorm E) => f.toFun) f = (fun (f : AddGroupSeminorm E) => f.toFun) g) : f = g

instance GroupSeminorm.funLike {E : Type u_4} [Group E] : FunLike (GroupSeminorm E) E ℝ

Equations

• GroupSeminorm.funLike = { coe := fun (f : GroupSeminorm E) => f.toFun, coe_injective' := ⋯ }

instance AddGroupSeminorm.addGroupSeminormClass {E : Type u_4} [AddGroup E] : AddGroupSeminormClass (AddGroupSeminorm E) E ℝ

Equations

• ⋯ = ⋯

instance GroupSeminorm.groupSeminormClass {E : Type u_4} [Group E] : GroupSeminormClass (GroupSeminorm E) E ℝ

Equations

• ⋯ = ⋯

instance AddGroupSeminorm.instCoeFunForallReal {E : Type u_4} [AddGroup E] : CoeFun (AddGroupSeminorm E) fun (x : AddGroupSeminorm E) => 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} [Group E] : CoeFun (GroupSeminorm E) fun (x : GroupSeminorm E) => 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} [AddGroup E] {p : AddGroupSeminorm E} : p.toFun = ⇑p

@[simp]

theorem GroupSeminorm.toFun_eq_coe {E : Type u_4} [Group E] {p : GroupSeminorm E} : p.toFun = ⇑p

theorem AddGroupSeminorm.ext {E : Type u_4} [AddGroup E] {p : AddGroupSeminorm E} {q : AddGroupSeminorm E} : (∀ (x : E), p x = q x) → p = q

theorem GroupSeminorm.ext {E : Type u_4} [Group E] {p : GroupSeminorm E} {q : GroupSeminorm E} : (∀ (x : E), p x = q x) → p = q

instance AddGroupSeminorm.instPartialOrder {E : Type u_4} [AddGroup E] : PartialOrder (AddGroupSeminorm E)

Equations

• AddGroupSeminorm.instPartialOrder = PartialOrder.lift (fun (f : AddGroupSeminorm E) => ⇑f) ⋯

theorem AddGroupSeminorm.instPartialOrder.proof_1 {E : Type u_1} [AddGroup E] : Function.Injective fun (f : AddGroupSeminorm E) => ⇑f

instance GroupSeminorm.instPartialOrder {E : Type u_4} [Group E] : PartialOrder (GroupSeminorm E)

Equations

• GroupSeminorm.instPartialOrder = PartialOrder.lift (fun (f : GroupSeminorm E) => ⇑f) ⋯

theorem AddGroupSeminorm.le_def {E : Type u_4} [AddGroup E] {p : AddGroupSeminorm E} {q : AddGroupSeminorm E} : p ≤ q ↔ ⇑p ≤ ⇑q

theorem GroupSeminorm.le_def {E : Type u_4} [Group E] {p : GroupSeminorm E} {q : GroupSeminorm E} : p ≤ q ↔ ⇑p ≤ ⇑q

theorem AddGroupSeminorm.lt_def {E : Type u_4} [AddGroup E] {p : AddGroupSeminorm E} {q : AddGroupSeminorm E} : p < q ↔ ⇑p < ⇑q

theorem GroupSeminorm.lt_def {E : Type u_4} [Group E] {p : GroupSeminorm E} {q : GroupSeminorm E} : p < q ↔ ⇑p < ⇑q

@[simp]

theorem AddGroupSeminorm.coe_le_coe {E : Type u_4} [AddGroup E] {p : AddGroupSeminorm E} {q : AddGroupSeminorm E} : ⇑p ≤ ⇑q ↔ p ≤ q

@[simp]

theorem GroupSeminorm.coe_le_coe {E : Type u_4} [Group E] {p : GroupSeminorm E} {q : GroupSeminorm E} : ⇑p ≤ ⇑q ↔ p ≤ q

@[simp]

theorem AddGroupSeminorm.coe_lt_coe {E : Type u_4} [AddGroup E] {p : AddGroupSeminorm E} {q : AddGroupSeminorm E} : ⇑p < ⇑q ↔ p < q

@[simp]

theorem GroupSeminorm.coe_lt_coe {E : Type u_4} [Group E] {p : GroupSeminorm E} {q : GroupSeminorm E} : ⇑p < ⇑q ↔ p < q

theorem AddGroupSeminorm.instZeroAddGroupSeminorm.proof_1 {E : Type u_1} [AddGroup E] : 0 0 = 0

instance AddGroupSeminorm.instZeroAddGroupSeminorm {E : Type u_4} [AddGroup E] : Zero (AddGroupSeminorm E)

Equations

• AddGroupSeminorm.instZeroAddGroupSeminorm = { zero := { toFun := 0, map_zero' := ⋯, add_le' := ⋯, neg' := ⋯ } }

theorem AddGroupSeminorm.instZeroAddGroupSeminorm.proof_3 {E : Type u_1} [AddGroup E] : ∀ (x : E), 0 (-x) = 0 (-x)

theorem AddGroupSeminorm.instZeroAddGroupSeminorm.proof_2 {E : Type u_1} [AddGroup E] : ∀ (x x_1 : E), 0 (x + x_1) ≤ 0 + 0 (x + x_1)

instance GroupSeminorm.instZeroGroupSeminorm {E : Type u_4} [Group E] : Zero (GroupSeminorm E)

Equations

• GroupSeminorm.instZeroGroupSeminorm = { zero := { toFun := 0, map_one' := ⋯, mul_le' := ⋯, inv' := ⋯ } }

@[simp]

theorem AddGroupSeminorm.coe_zero {E : Type u_4} [AddGroup E] : ⇑0 = 0

@[simp]

theorem GroupSeminorm.coe_zero {E : Type u_4} [Group E] : ⇑0 = 0

@[simp]

theorem AddGroupSeminorm.zero_apply {E : Type u_4} [AddGroup E] (x : E) : 0 x = 0

@[simp]

theorem GroupSeminorm.zero_apply {E : Type u_4} [Group E] (x : E) : 0 x = 0

instance AddGroupSeminorm.instInhabited {E : Type u_4} [AddGroup E] : Inhabited (AddGroupSeminorm E)

Equations

• AddGroupSeminorm.instInhabited = { default := 0 }

instance GroupSeminorm.instInhabited {E : Type u_4} [Group E] : Inhabited (GroupSeminorm E)

Equations

• GroupSeminorm.instInhabited = { default := 0 }

theorem AddGroupSeminorm.instAdd.proof_1 {E : Type u_1} [AddGroup E] (p : AddGroupSeminorm E) (q : AddGroupSeminorm E) : (fun (x : E) => p x + q x) 0 = 0

theorem AddGroupSeminorm.instAdd.proof_2 {E : Type u_1} [AddGroup E] (p : AddGroupSeminorm E) (q : AddGroupSeminorm E) : ∀ (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

instance AddGroupSeminorm.instAdd {E : Type u_4} [AddGroup E] : Add (AddGroupSeminorm E)

Equations

• AddGroupSeminorm.instAdd = { add := fun (p q : AddGroupSeminorm E) => { toFun := fun (x : E) => p x + q x, map_zero' := ⋯, add_le' := ⋯, neg' := ⋯ } }

theorem AddGroupSeminorm.instAdd.proof_3 {E : Type u_1} [AddGroup E] (p : AddGroupSeminorm E) (q : AddGroupSeminorm E) (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} [Group E] : Add (GroupSeminorm E)

Equations

• GroupSeminorm.instAdd = { add := fun (p q : GroupSeminorm E) => { toFun := fun (x : E) => p x + q x, map_one' := ⋯, mul_le' := ⋯, inv' := ⋯ } }

@[simp]

theorem AddGroupSeminorm.coe_add {E : Type u_4} [AddGroup E] (p : AddGroupSeminorm E) (q : AddGroupSeminorm E) : ⇑(p + q) = ⇑p + ⇑q

@[simp]

theorem GroupSeminorm.coe_add {E : Type u_4} [Group E] (p : GroupSeminorm E) (q : GroupSeminorm E) : ⇑(p + q) = ⇑p + ⇑q

@[simp]

theorem AddGroupSeminorm.add_apply {E : Type u_4} [AddGroup E] (p : AddGroupSeminorm E) (q : AddGroupSeminorm E) (x : E) : (p + q) x = p x + q x

@[simp]

theorem GroupSeminorm.add_apply {E : Type u_4} [Group E] (p : GroupSeminorm E) (q : GroupSeminorm E) (x : E) : (p + q) x = p x + q x

theorem AddGroupSeminorm.instSup.proof_1 {E : Type u_1} [AddGroup E] (p : AddGroupSeminorm E) (q : AddGroupSeminorm E) : (⇑p ⊔ ⇑q) 0 = 0

theorem AddGroupSeminorm.instSup.proof_3 {E : Type u_1} [AddGroup E] (p : AddGroupSeminorm E) (q : AddGroupSeminorm E) (x : E) : (⇑p ⊔ ⇑q) (-x) = (⇑p ⊔ ⇑q) x

instance AddGroupSeminorm.instSup {E : Type u_4} [AddGroup E] : Sup (AddGroupSeminorm E)

Equations

• AddGroupSeminorm.instSup = { sup := fun (p q : AddGroupSeminorm E) => { toFun := ⇑p ⊔ ⇑q, map_zero' := ⋯, add_le' := ⋯, neg' := ⋯ } }

theorem AddGroupSeminorm.instSup.proof_2 {E : Type u_1} [AddGroup E] (p : AddGroupSeminorm E) (q : AddGroupSeminorm E) (x : E) (y : E) : p (x + y) ⊔ q (x + y) ≤ (⇑p ⊔ ⇑q) x + (⇑p ⊔ ⇑q) y

instance GroupSeminorm.instSup {E : Type u_4} [Group E] : Sup (GroupSeminorm E)

Equations

• GroupSeminorm.instSup = { sup := fun (p q : GroupSeminorm E) => { toFun := ⇑p ⊔ ⇑q, map_one' := ⋯, mul_le' := ⋯, inv' := ⋯ } }

@[simp]

theorem AddGroupSeminorm.coe_sup {E : Type u_4} [AddGroup E] (p : AddGroupSeminorm E) (q : AddGroupSeminorm E) : ⇑(p ⊔ q) = ⇑p ⊔ ⇑q

@[simp]

theorem GroupSeminorm.coe_sup {E : Type u_4} [Group E] (p : GroupSeminorm E) (q : GroupSeminorm E) : ⇑(p ⊔ q) = ⇑p ⊔ ⇑q

@[simp]

theorem AddGroupSeminorm.sup_apply {E : Type u_4} [AddGroup E] (p : AddGroupSeminorm E) (q : AddGroupSeminorm E) (x : E) : (p ⊔ q) x = p x ⊔ q x

@[simp]

theorem GroupSeminorm.sup_apply {E : Type u_4} [Group E] (p : GroupSeminorm E) (q : GroupSeminorm E) (x : E) : (p ⊔ q) x = p x ⊔ q x

theorem AddGroupSeminorm.semilatticeSup.proof_1 {E : Type u_1} [AddGroup E] : Function.Injective fun (f : AddGroupSeminorm E) => ⇑f

instance AddGroupSeminorm.semilatticeSup {E : Type u_4} [AddGroup E] : SemilatticeSup (AddGroupSeminorm E)

Equations

• AddGroupSeminorm.semilatticeSup = Function.Injective.semilatticeSup (fun (f : AddGroupSeminorm E) => ⇑f) ⋯ ⋯

instance GroupSeminorm.semilatticeSup {E : Type u_4} [Group E] : SemilatticeSup (GroupSeminorm E)

Equations

• GroupSeminorm.semilatticeSup = Function.Injective.semilatticeSup (fun (f : GroupSeminorm E) => ⇑f) ⋯ ⋯

theorem AddGroupSeminorm.comp.proof_1 {E : Type u_1} {F : Type u_2} [AddGroup E] [AddGroup F] (p : AddGroupSeminorm E) (f : F →+ E) : (fun (x : F) => p (f x)) 0 = 0

theorem AddGroupSeminorm.comp.proof_3 {E : Type u_1} {F : Type u_2} [AddGroup E] [AddGroup F] (p : AddGroupSeminorm E) (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} [AddGroup E] [AddGroup F] (p : AddGroupSeminorm E) (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} [AddGroup E] [AddGroup F] (p : AddGroupSeminorm E) (f : F →+ E) : AddGroupSeminorm 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' := ⋯ }

def GroupSeminorm.comp {E : Type u_4} {F : Type u_5} [Group E] [Group F] (p : GroupSeminorm E) (f : F →* E) : GroupSeminorm F

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' := ⋯ }

@[simp]

theorem AddGroupSeminorm.coe_comp {E : Type u_4} {F : Type u_5} [AddGroup E] [AddGroup F] (p : AddGroupSeminorm E) (f : F →+ E) : ⇑(p.comp f) = ⇑p ∘ ⇑f

@[simp]

theorem GroupSeminorm.coe_comp {E : Type u_4} {F : Type u_5} [Group E] [Group F] (p : GroupSeminorm E) (f : F →* E) : ⇑(p.comp f) = ⇑p ∘ ⇑f

@[simp]

theorem AddGroupSeminorm.comp_apply {E : Type u_4} {F : Type u_5} [AddGroup E] [AddGroup F] (p : AddGroupSeminorm E) (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} [Group E] [Group F] (p : GroupSeminorm E) (f : F →* E) (x : F) : (p.comp f) x = p (f x)

@[simp]

theorem AddGroupSeminorm.comp_id {E : Type u_4} [AddGroup E] (p : AddGroupSeminorm E) : p.comp (AddMonoidHom.id E) = p

@[simp]

theorem GroupSeminorm.comp_id {E : Type u_4} [Group E] (p : GroupSeminorm E) : p.comp (MonoidHom.id E) = p

@[simp]

theorem AddGroupSeminorm.comp_zero {E : Type u_4} {F : Type u_5} [AddGroup E] [AddGroup F] (p : AddGroupSeminorm E) : p.comp 0 = 0

@[simp]

theorem GroupSeminorm.comp_zero {E : Type u_4} {F : Type u_5} [Group E] [Group F] (p : GroupSeminorm E) : p.comp 1 = 0

@[simp]

theorem AddGroupSeminorm.zero_comp {E : Type u_4} {F : Type u_5} [AddGroup E] [AddGroup F] (f : F →+ E) : AddGroupSeminorm.comp 0 f = 0

@[simp]

theorem GroupSeminorm.zero_comp {E : Type u_4} {F : Type u_5} [Group E] [Group F] (f : F →* E) : GroupSeminorm.comp 0 f = 0

theorem AddGroupSeminorm.comp_assoc {E : Type u_4} {F : Type u_5} {G : Type u_6} [AddGroup E] [AddGroup F] [AddGroup G] (p : AddGroupSeminorm E) (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} [Group E] [Group F] [Group G] (p : GroupSeminorm E) (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} [AddGroup E] [AddGroup F] (p : AddGroupSeminorm E) (q : AddGroupSeminorm E) (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} [Group E] [Group F] (p : GroupSeminorm E) (q : GroupSeminorm E) (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} [AddGroup E] [AddGroup F] {p : AddGroupSeminorm E} {q : AddGroupSeminorm E} (f : F →+ E) (hp : p ≤ q) : p.comp f ≤ q.comp f

theorem GroupSeminorm.comp_mono {E : Type u_4} {F : Type u_5} [Group E] [Group F] {p : GroupSeminorm E} {q : GroupSeminorm E} (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} [AddCommGroup E] [AddCommGroup F] (p : AddGroupSeminorm E) (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} [CommGroup E] [CommGroup F] (p : GroupSeminorm E) (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} [AddCommGroup E] {p : AddGroupSeminorm E} {q : AddGroupSeminorm E} {x : E} : BddBelow (Set.range fun (y : E) => p y + q (x - y))

theorem GroupSeminorm.mul_bddBelow_range_add {E : Type u_4} [CommGroup E] {p : GroupSeminorm E} {q : GroupSeminorm E} {x : E} : BddBelow (Set.range fun (y : E) => p y + q (x / y))

theorem AddGroupSeminorm.instInf.proof_2 {E : Type u_1} [AddCommGroup E] (p : AddGroupSeminorm E) (q : AddGroupSeminorm E) (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} [AddCommGroup E] (p : AddGroupSeminorm E) (q : AddGroupSeminorm E) (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} [AddCommGroup E] (p : AddGroupSeminorm E) (q : AddGroupSeminorm E) : ⨅ (i : E), p i + q (0 - i) = 0

noncomputable instance AddGroupSeminorm.instInf {E : Type u_4} [AddCommGroup E] : Inf (AddGroupSeminorm E)

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' := ⋯ } }

noncomputable instance GroupSeminorm.instInf {E : Type u_4} [CommGroup E] : Inf (GroupSeminorm E)

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' := ⋯ } }

@[simp]

theorem AddGroupSeminorm.inf_apply {E : Type u_4} [AddCommGroup E] (p : AddGroupSeminorm E) (q : AddGroupSeminorm E) (x : E) : (p ⊓ q) x = ⨅ (y : E), p y + q (x - y)

@[simp]

theorem GroupSeminorm.inf_apply {E : Type u_4} [CommGroup E] (p : GroupSeminorm E) (q : GroupSeminorm E) (x : E) : (p ⊓ q) x = ⨅ (y : E), p y + q (x / y)

theorem AddGroupSeminorm.instLattice.proof_3 {E : Type u_1} [AddCommGroup E] (a : AddGroupSeminorm E) (b : AddGroupSeminorm E) (c : AddGroupSeminorm E) (hb : a ≤ b) (hc : a ≤ c) (x : E) : (fun (f : AddGroupSeminorm E) => ⇑f) a x ≤ ⨅ (y : E), b y + c (x - y)

theorem AddGroupSeminorm.instLattice.proof_2 {E : Type u_1} [AddCommGroup E] (p : AddGroupSeminorm E) (q : AddGroupSeminorm E) (x : E) : ⨅ (y : E), p y + q (x - y) ≤ (fun (f : AddGroupSeminorm E) => ⇑f) q x

noncomputable instance AddGroupSeminorm.instLattice {E : Type u_4} [AddCommGroup E] : Lattice (AddGroupSeminorm E)

Equations

• AddGroupSeminorm.instLattice = let __src := AddGroupSeminorm.semilatticeSup; Lattice.mk ⋯ ⋯ ⋯

theorem AddGroupSeminorm.instLattice.proof_1 {E : Type u_1} [AddCommGroup E] (p : AddGroupSeminorm E) (q : AddGroupSeminorm E) (x : E) : ⨅ (y : E), p y + q (x - y) ≤ (fun (f : AddGroupSeminorm E) => ⇑f) p x

noncomputable instance GroupSeminorm.instLattice {E : Type u_4} [CommGroup E] : Lattice (GroupSeminorm E)

Equations

• GroupSeminorm.instLattice = let __src := GroupSeminorm.semilatticeSup; Lattice.mk ⋯ ⋯ ⋯

instance AddGroupSeminorm.toOne {E : Type u_4} [AddGroup E] [DecidableEq E] : One (AddGroupSeminorm E)

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} [AddGroup E] [DecidableEq E] (x : E) : 1 x = if x = 0 then 0 else 1

instance AddGroupSeminorm.toSMul {R : Type u_2} {E : Type u_4} [AddGroup E] [SMul R ℝ] [SMul R NNReal] [IsScalarTower R NNReal ℝ] : SMul R (AddGroupSeminorm E)

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' := ⋯ } }

@[simp]

theorem AddGroupSeminorm.coe_smul {R : Type u_2} {E : Type u_4} [AddGroup E] [SMul R ℝ] [SMul R NNReal] [IsScalarTower R NNReal ℝ] (r : R) (p : AddGroupSeminorm E) : ⇑(r • p) = r • ⇑p

@[simp]

theorem AddGroupSeminorm.smul_apply {R : Type u_2} {E : Type u_4} [AddGroup E] [SMul R ℝ] [SMul R NNReal] [IsScalarTower R NNReal ℝ] (r : R) (p : AddGroupSeminorm E) (x : E) : (r • p) x = r • p x

instance AddGroupSeminorm.isScalarTower {R : Type u_2} {R' : Type u_3} {E : Type u_4} [AddGroup E] [SMul R ℝ] [SMul R NNReal] [IsScalarTower R NNReal ℝ] [SMul R' ℝ] [SMul R' NNReal] [IsScalarTower R' NNReal ℝ] [SMul R R'] [IsScalarTower R R' ℝ] : IsScalarTower R R' (AddGroupSeminorm E)

Equations

• ⋯ = ⋯

theorem AddGroupSeminorm.smul_sup {R : Type u_2} {E : Type u_4} [AddGroup E] [SMul R ℝ] [SMul R NNReal] [IsScalarTower R NNReal ℝ] (r : R) (p : AddGroupSeminorm E) (q : AddGroupSeminorm E) : r • (p ⊔ q) = r • p ⊔ r • q

instance NonarchAddGroupSeminorm.funLike {E : Type u_4} [AddGroup E] : FunLike (NonarchAddGroupSeminorm E) E ℝ

Equations

• NonarchAddGroupSeminorm.funLike = { coe := fun (f : NonarchAddGroupSeminorm E) => f.toFun, coe_injective' := ⋯ }

instance NonarchAddGroupSeminorm.nonarchAddGroupSeminormClass {E : Type u_4} [AddGroup E] : NonarchAddGroupSeminormClass (NonarchAddGroupSeminorm E) E

Equations

• ⋯ = ⋯

instance NonarchAddGroupSeminorm.instCoeFunForallReal {E : Type u_4} [AddGroup E] : CoeFun (NonarchAddGroupSeminorm E) fun (x : NonarchAddGroupSeminorm E) => 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} [AddGroup E] {p : NonarchAddGroupSeminorm E} : ⇑p.toZeroHom = ⇑p

theorem NonarchAddGroupSeminorm.ext {E : Type u_4} [AddGroup E] {p : NonarchAddGroupSeminorm E} {q : NonarchAddGroupSeminorm E} : (∀ (x : E), p x = q x) → p = q

noncomputable instance NonarchAddGroupSeminorm.instPartialOrder {E : Type u_4} [AddGroup E] : PartialOrder (NonarchAddGroupSeminorm E)

Equations

• NonarchAddGroupSeminorm.instPartialOrder = PartialOrder.lift (fun (f : NonarchAddGroupSeminorm E) => ⇑f) ⋯

theorem NonarchAddGroupSeminorm.le_def {E : Type u_4} [AddGroup E] {p : NonarchAddGroupSeminorm E} {q : NonarchAddGroupSeminorm E} : p ≤ q ↔ ⇑p ≤ ⇑q

theorem NonarchAddGroupSeminorm.lt_def {E : Type u_4} [AddGroup E] {p : NonarchAddGroupSeminorm E} {q : NonarchAddGroupSeminorm E} : p < q ↔ ⇑p < ⇑q

@[simp]

theorem NonarchAddGroupSeminorm.coe_le_coe {E : Type u_4} [AddGroup E] {p : NonarchAddGroupSeminorm E} {q : NonarchAddGroupSeminorm E} : ⇑p ≤ ⇑q ↔ p ≤ q

@[simp]

theorem NonarchAddGroupSeminorm.coe_lt_coe {E : Type u_4} [AddGroup E] {p : NonarchAddGroupSeminorm E} {q : NonarchAddGroupSeminorm E} : ⇑p < ⇑q ↔ p < q

instance NonarchAddGroupSeminorm.instZero {E : Type u_4} [AddGroup E] : Zero (NonarchAddGroupSeminorm E)

Equations

• NonarchAddGroupSeminorm.instZero = { zero := { toFun := 0, map_zero' := ⋯, add_le_max' := ⋯, neg' := ⋯ } }

@[simp]

theorem NonarchAddGroupSeminorm.coe_zero {E : Type u_4} [AddGroup E] : ⇑0 = 0

@[simp]

theorem NonarchAddGroupSeminorm.zero_apply {E : Type u_4} [AddGroup E] (x : E) : 0 x = 0

instance NonarchAddGroupSeminorm.instInhabited {E : Type u_4} [AddGroup E] : Inhabited (NonarchAddGroupSeminorm E)

Equations

• NonarchAddGroupSeminorm.instInhabited = { default := 0 }

instance NonarchAddGroupSeminorm.instSup {E : Type u_4} [AddGroup E] : Sup (NonarchAddGroupSeminorm E)

Equations

• NonarchAddGroupSeminorm.instSup = { sup := fun (p q : NonarchAddGroupSeminorm E) => { toFun := ⇑p ⊔ ⇑q, map_zero' := ⋯, add_le_max' := ⋯, neg' := ⋯ } }

@[simp]

theorem NonarchAddGroupSeminorm.coe_sup {E : Type u_4} [AddGroup E] (p : NonarchAddGroupSeminorm E) (q : NonarchAddGroupSeminorm E) : ⇑(p ⊔ q) = ⇑p ⊔ ⇑q

@[simp]

theorem NonarchAddGroupSeminorm.sup_apply {E : Type u_4} [AddGroup E] (p : NonarchAddGroupSeminorm E) (q : NonarchAddGroupSeminorm E) (x : E) : (p ⊔ q) x = p x ⊔ q x

noncomputable instance NonarchAddGroupSeminorm.instSemilatticeSup {E : Type u_4} [AddGroup E] : SemilatticeSup (NonarchAddGroupSeminorm E)

Equations

• NonarchAddGroupSeminorm.instSemilatticeSup = Function.Injective.semilatticeSup (fun (f : NonarchAddGroupSeminorm E) => ⇑f) ⋯ ⋯

theorem NonarchAddGroupSeminorm.add_bddBelow_range_add {E : Type u_4} [AddCommGroup E] {p : NonarchAddGroupSeminorm E} {q : NonarchAddGroupSeminorm E} {x : E} : BddBelow (Set.range fun (y : E) => p y + q (x - y))

instance GroupSeminorm.toOne {E : Type u_4} [Group E] [DecidableEq E] : One (GroupSeminorm E)

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} [Group E] [DecidableEq E] (x : E) : 1 x = if x = 1 then 0 else 1

instance GroupSeminorm.instSMul {R : Type u_2} {E : Type u_4} [Group E] [SMul R ℝ] [SMul R NNReal] [IsScalarTower R NNReal ℝ] : SMul R (GroupSeminorm E)

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' := ⋯ } }

instance GroupSeminorm.instIsScalarTowerOfReal {R : Type u_2} {R' : Type u_3} {E : Type u_4} [Group E] [SMul R ℝ] [SMul R NNReal] [IsScalarTower R NNReal ℝ] [SMul R' ℝ] [SMul R' NNReal] [IsScalarTower R' NNReal ℝ] [SMul R R'] [IsScalarTower R R' ℝ] : IsScalarTower R R' (GroupSeminorm E)

Equations

• ⋯ = ⋯

@[simp]

theorem GroupSeminorm.coe_smul {R : Type u_2} {E : Type u_4} [Group E] [SMul R ℝ] [SMul R NNReal] [IsScalarTower R NNReal ℝ] (r : R) (p : GroupSeminorm E) : ⇑(r • p) = r • ⇑p

@[simp]

theorem GroupSeminorm.smul_apply {R : Type u_2} {E : Type u_4} [Group E] [SMul R ℝ] [SMul R NNReal] [IsScalarTower R NNReal ℝ] (r : R) (p : GroupSeminorm E) (x : E) : (r • p) x = r • p x

theorem GroupSeminorm.smul_sup {R : Type u_2} {E : Type u_4} [Group E] [SMul R ℝ] [SMul R NNReal] [IsScalarTower R NNReal ℝ] (r : R) (p : GroupSeminorm E) (q : GroupSeminorm E) : r • (p ⊔ q) = r • p ⊔ r • q

instance NonarchAddGroupSeminorm.instOneOfDecidableEq {E : Type u_4} [AddGroup E] [DecidableEq E] : One (NonarchAddGroupSeminorm E)

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} [AddGroup E] [DecidableEq E] (x : E) : 1 x = if x = 0 then 0 else 1

instance NonarchAddGroupSeminorm.instSMul {R : Type u_2} {E : Type u_4} [AddGroup E] [SMul R ℝ] [SMul R NNReal] [IsScalarTower R NNReal ℝ] : SMul R (NonarchAddGroupSeminorm E)

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' := ⋯ } }

instance NonarchAddGroupSeminorm.instIsScalarTowerOfReal {R : Type u_2} {R' : Type u_3} {E : Type u_4} [AddGroup E] [SMul R ℝ] [SMul R NNReal] [IsScalarTower R NNReal ℝ] [SMul R' ℝ] [SMul R' NNReal] [IsScalarTower R' NNReal ℝ] [SMul R R'] [IsScalarTower R R' ℝ] : IsScalarTower R R' (NonarchAddGroupSeminorm E)

Equations

• ⋯ = ⋯

@[simp]

theorem NonarchAddGroupSeminorm.coe_smul {R : Type u_2} {E : Type u_4} [AddGroup E] [SMul R ℝ] [SMul R NNReal] [IsScalarTower R NNReal ℝ] (r : R) (p : NonarchAddGroupSeminorm E) : ⇑(r • p) = r • ⇑p

@[simp]

theorem NonarchAddGroupSeminorm.smul_apply {R : Type u_2} {E : Type u_4} [AddGroup E] [SMul R ℝ] [SMul R NNReal] [IsScalarTower R NNReal ℝ] (r : R) (p : NonarchAddGroupSeminorm E) (x : E) : (r • p) x = r • p x

theorem NonarchAddGroupSeminorm.smul_sup {R : Type u_2} {E : Type u_4} [AddGroup E] [SMul R ℝ] [SMul R NNReal] [IsScalarTower R NNReal ℝ] (r : R) (p : NonarchAddGroupSeminorm E) (q : NonarchAddGroupSeminorm E) : r • (p ⊔ q) = r • p ⊔ r • q

Norms

instance AddGroupNorm.funLike {E : Type u_4} [AddGroup E] : FunLike (AddGroupNorm E) E ℝ

Equations

• AddGroupNorm.funLike = { coe := fun (f : AddGroupNorm E) => f.toFun, coe_injective' := ⋯ }

theorem AddGroupNorm.funLike.proof_1 {E : Type u_1} [AddGroup E] (f : AddGroupNorm E) (g : AddGroupNorm E) (h : (fun (f : AddGroupNorm E) => f.toFun) f = (fun (f : AddGroupNorm E) => f.toFun) g) : f = g

instance GroupNorm.funLike {E : Type u_4} [Group E] : FunLike (GroupNorm E) E ℝ

Equations

• GroupNorm.funLike = { coe := fun (f : GroupNorm E) => f.toFun, coe_injective' := ⋯ }

instance AddGroupNorm.addGroupNormClass {E : Type u_4} [AddGroup E] : AddGroupNormClass (AddGroupNorm E) E ℝ

Equations

• ⋯ = ⋯

instance GroupNorm.groupNormClass {E : Type u_4} [Group E] : GroupNormClass (GroupNorm E) E ℝ

Equations

• ⋯ = ⋯

instance AddGroupNorm.instCoeFunForallReal {E : Type u_4} [AddGroup E] : CoeFun (AddGroupNorm E) fun (x : AddGroupNorm E) => E → ℝ

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

Equations

• AddGroupNorm.instCoeFunForallReal = DFunLike.hasCoeToFun

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

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

Equations

• GroupNorm.instCoeFunForallReal = DFunLike.hasCoeToFun

@[simp]

theorem AddGroupNorm.toAddGroupSeminorm_eq_coe {E : Type u_4} [AddGroup E] {p : AddGroupNorm E} : ⇑p.toAddGroupSeminorm = ⇑p

@[simp]

theorem GroupNorm.toGroupSeminorm_eq_coe {E : Type u_4} [Group E] {p : GroupNorm E} : ⇑p.toGroupSeminorm = ⇑p

theorem AddGroupNorm.ext {E : Type u_4} [AddGroup E] {p : AddGroupNorm E} {q : AddGroupNorm E} : (∀ (x : E), p x = q x) → p = q

theorem GroupNorm.ext {E : Type u_4} [Group E] {p : GroupNorm E} {q : GroupNorm E} : (∀ (x : E), p x = q x) → p = q

theorem AddGroupNorm.instPartialOrder.proof_1 {E : Type u_1} [AddGroup E] : Function.Injective fun (f : AddGroupNorm E) => ⇑f

instance AddGroupNorm.instPartialOrder {E : Type u_4} [AddGroup E] : PartialOrder (AddGroupNorm E)

Equations

• AddGroupNorm.instPartialOrder = PartialOrder.lift (fun (f : AddGroupNorm E) => ⇑f) ⋯

instance GroupNorm.instPartialOrder {E : Type u_4} [Group E] : PartialOrder (GroupNorm E)

Equations

• GroupNorm.instPartialOrder = PartialOrder.lift (fun (f : GroupNorm E) => ⇑f) ⋯

theorem AddGroupNorm.le_def {E : Type u_4} [AddGroup E] {p : AddGroupNorm E} {q : AddGroupNorm E} : p ≤ q ↔ ⇑p ≤ ⇑q

theorem GroupNorm.le_def {E : Type u_4} [Group E] {p : GroupNorm E} {q : GroupNorm E} : p ≤ q ↔ ⇑p ≤ ⇑q

theorem AddGroupNorm.lt_def {E : Type u_4} [AddGroup E] {p : AddGroupNorm E} {q : AddGroupNorm E} : p < q ↔ ⇑p < ⇑q

theorem GroupNorm.lt_def {E : Type u_4} [Group E] {p : GroupNorm E} {q : GroupNorm E} : p < q ↔ ⇑p < ⇑q

@[simp]

theorem AddGroupNorm.coe_le_coe {E : Type u_4} [AddGroup E] {p : AddGroupNorm E} {q : AddGroupNorm E} : ⇑p ≤ ⇑q ↔ p ≤ q

@[simp]

theorem GroupNorm.coe_le_coe {E : Type u_4} [Group E] {p : GroupNorm E} {q : GroupNorm E} : ⇑p ≤ ⇑q ↔ p ≤ q

@[simp]

theorem AddGroupNorm.coe_lt_coe {E : Type u_4} [AddGroup E] {p : AddGroupNorm E} {q : AddGroupNorm E} : ⇑p < ⇑q ↔ p < q

@[simp]

theorem GroupNorm.coe_lt_coe {E : Type u_4} [Group E] {p : GroupNorm E} {q : GroupNorm E} : ⇑p < ⇑q ↔ p < q

instance AddGroupNorm.instAdd {E : Type u_4} [AddGroup E] : Add (AddGroupNorm E)

Equations

• One or more equations did not get rendered due to their size.

theorem AddGroupNorm.instAdd.proof_1 {E : Type u_1} [AddGroup E] (p : AddGroupNorm E) (q : AddGroupNorm E) (_x : E) (hx : (p.toAddGroupSeminorm + q.toAddGroupSeminorm).toFun _x = 0) : _x = 0

instance GroupNorm.instAdd {E : Type u_4} [Group E] : Add (GroupNorm E)

Equations

• GroupNorm.instAdd = { add := fun (p q : GroupNorm E) => let __src := p.toGroupSeminorm + q.toGroupSeminorm; { toGroupSeminorm := __src, eq_one_of_map_eq_zero' := ⋯ } }

@[simp]

theorem AddGroupNorm.coe_add {E : Type u_4} [AddGroup E] (p : AddGroupNorm E) (q : AddGroupNorm E) : ⇑(p + q) = ⇑p + ⇑q

@[simp]

theorem GroupNorm.coe_add {E : Type u_4} [Group E] (p : GroupNorm E) (q : GroupNorm E) : ⇑(p + q) = ⇑p + ⇑q

@[simp]

theorem AddGroupNorm.add_apply {E : Type u_4} [AddGroup E] (p : AddGroupNorm E) (q : AddGroupNorm E) (x : E) : (p + q) x = p x + q x

@[simp]

theorem GroupNorm.add_apply {E : Type u_4} [Group E] (p : GroupNorm E) (q : GroupNorm E) (x : E) : (p + q) x = p x + q x

instance AddGroupNorm.instSup {E : Type u_4} [AddGroup E] : Sup (AddGroupNorm E)

Equations

• One or more equations did not get rendered due to their size.

theorem AddGroupNorm.instSup.proof_1 {E : Type u_1} [AddGroup E] (p : AddGroupNorm E) (q : AddGroupNorm E) (_x : E) (hx : (p.toAddGroupSeminorm ⊔ q.toAddGroupSeminorm).toFun _x = 0) : _x = 0

instance GroupNorm.instSup {E : Type u_4} [Group E] : Sup (GroupNorm E)

Equations

• GroupNorm.instSup = { sup := fun (p q : GroupNorm E) => let __src := p.toGroupSeminorm ⊔ q.toGroupSeminorm; { toGroupSeminorm := __src, eq_one_of_map_eq_zero' := ⋯ } }

@[simp]

theorem AddGroupNorm.coe_sup {E : Type u_4} [AddGroup E] (p : AddGroupNorm E) (q : AddGroupNorm E) : ⇑(p ⊔ q) = ⇑p ⊔ ⇑q

@[simp]

theorem GroupNorm.coe_sup {E : Type u_4} [Group E] (p : GroupNorm E) (q : GroupNorm E) : ⇑(p ⊔ q) = ⇑p ⊔ ⇑q

@[simp]

theorem AddGroupNorm.sup_apply {E : Type u_4} [AddGroup E] (p : AddGroupNorm E) (q : AddGroupNorm E) (x : E) : (p ⊔ q) x = p x ⊔ q x

@[simp]

theorem GroupNorm.sup_apply {E : Type u_4} [Group E] (p : GroupNorm E) (q : GroupNorm E) (x : E) : (p ⊔ q) x = p x ⊔ q x

theorem AddGroupNorm.instSemilatticeSup.proof_1 {E : Type u_1} [AddGroup E] : Function.Injective fun (f : AddGroupNorm E) => ⇑f

instance AddGroupNorm.instSemilatticeSup {E : Type u_4} [AddGroup E] : SemilatticeSup (AddGroupNorm E)

Equations

• AddGroupNorm.instSemilatticeSup = Function.Injective.semilatticeSup (fun (f : AddGroupNorm E) => ⇑f) ⋯ ⋯

instance GroupNorm.instSemilatticeSup {E : Type u_4} [Group E] : SemilatticeSup (GroupNorm E)

Equations

• GroupNorm.instSemilatticeSup = Function.Injective.semilatticeSup (fun (f : GroupNorm E) => ⇑f) ⋯ ⋯

instance AddGroupNorm.instOne {E : Type u_4} [AddGroup E] [DecidableEq E] : One (AddGroupNorm E)

Equations

• AddGroupNorm.instOne = { one := let __src := 1; { toAddGroupSeminorm := __src, eq_zero_of_map_eq_zero' := ⋯ } }

@[simp]

theorem AddGroupNorm.apply_one {E : Type u_4} [AddGroup E] [DecidableEq E] (x : E) : 1 x = if x = 0 then 0 else 1

instance AddGroupNorm.instInhabited {E : Type u_4} [AddGroup E] [DecidableEq E] : Inhabited (AddGroupNorm E)

Equations

• AddGroupNorm.instInhabited = { default := 1 }

instance AddGroupNorm.toOne {E : Type u_4} [AddGroup E] [DecidableEq E] : One (AddGroupNorm E)

Equations

• AddGroupNorm.toOne = { one := let __src := 1; { toAddGroupSeminorm := __src, eq_zero_of_map_eq_zero' := ⋯ } }

instance GroupNorm.toOne {E : Type u_4} [Group E] [DecidableEq E] : One (GroupNorm E)

Equations

• GroupNorm.toOne = { one := let __src := 1; { toGroupSeminorm := __src, eq_one_of_map_eq_zero' := ⋯ } }

@[simp]

theorem GroupNorm.apply_one {E : Type u_4} [Group E] [DecidableEq E] (x : E) : 1 x = if x = 1 then 0 else 1

instance GroupNorm.instInhabited {E : Type u_4} [Group E] [DecidableEq E] : Inhabited (GroupNorm E)

Equations

• GroupNorm.instInhabited = { default := 1 }

instance NonarchAddGroupNorm.funLike {E : Type u_4} [AddGroup E] : FunLike (NonarchAddGroupNorm E) E ℝ

Equations

• NonarchAddGroupNorm.funLike = { coe := fun (f : NonarchAddGroupNorm E) => f.toFun, coe_injective' := ⋯ }

instance NonarchAddGroupNorm.nonarchAddGroupNormClass {E : Type u_4} [AddGroup E] : NonarchAddGroupNormClass (NonarchAddGroupNorm E) E

Equations

• ⋯ = ⋯

noncomputable instance NonarchAddGroupNorm.instCoeFunForallReal {E : Type u_4} [AddGroup E] : CoeFun (NonarchAddGroupNorm E) fun (x : NonarchAddGroupNorm E) => E → ℝ

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

Equations

• NonarchAddGroupNorm.instCoeFunForallReal = DFunLike.hasCoeToFun

@[simp]

theorem NonarchAddGroupNorm.toNonarchAddGroupSeminorm_eq_coe {E : Type u_4} [AddGroup E] {p : NonarchAddGroupNorm E} : ⇑p.toNonarchAddGroupSeminorm = ⇑p

theorem NonarchAddGroupNorm.ext {E : Type u_4} [AddGroup E] {p : NonarchAddGroupNorm E} {q : NonarchAddGroupNorm E} : (∀ (x : E), p x = q x) → p = q

noncomputable instance NonarchAddGroupNorm.instPartialOrder {E : Type u_4} [AddGroup E] : PartialOrder (NonarchAddGroupNorm E)

Equations

• NonarchAddGroupNorm.instPartialOrder = PartialOrder.lift (fun (f : NonarchAddGroupNorm E) => ⇑f) ⋯

theorem NonarchAddGroupNorm.le_def {E : Type u_4} [AddGroup E] {p : NonarchAddGroupNorm E} {q : NonarchAddGroupNorm E} : p ≤ q ↔ ⇑p ≤ ⇑q

theorem NonarchAddGroupNorm.lt_def {E : Type u_4} [AddGroup E] {p : NonarchAddGroupNorm E} {q : NonarchAddGroupNorm E} : p < q ↔ ⇑p < ⇑q

@[simp]

theorem NonarchAddGroupNorm.coe_le_coe {E : Type u_4} [AddGroup E] {p : NonarchAddGroupNorm E} {q : NonarchAddGroupNorm E} : ⇑p ≤ ⇑q ↔ p ≤ q

@[simp]

theorem NonarchAddGroupNorm.coe_lt_coe {E : Type u_4} [AddGroup E] {p : NonarchAddGroupNorm E} {q : NonarchAddGroupNorm E} : ⇑p < ⇑q ↔ p < q

instance NonarchAddGroupNorm.instSup {E : Type u_4} [AddGroup E] : Sup (NonarchAddGroupNorm E)

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem NonarchAddGroupNorm.coe_sup {E : Type u_4} [AddGroup E] (p : NonarchAddGroupNorm E) (q : NonarchAddGroupNorm E) : ⇑(p ⊔ q) = ⇑p ⊔ ⇑q

@[simp]

theorem NonarchAddGroupNorm.sup_apply {E : Type u_4} [AddGroup E] (p : NonarchAddGroupNorm E) (q : NonarchAddGroupNorm E) (x : E) : (p ⊔ q) x = p x ⊔ q x

noncomputable instance NonarchAddGroupNorm.instSemilatticeSup {E : Type u_4} [AddGroup E] : SemilatticeSup (NonarchAddGroupNorm E)

Equations

• NonarchAddGroupNorm.instSemilatticeSup = Function.Injective.semilatticeSup (fun (f : NonarchAddGroupNorm E) => ⇑f) ⋯ ⋯

instance NonarchAddGroupNorm.instOneOfDecidableEq {E : Type u_4} [AddGroup E] [DecidableEq E] : One (NonarchAddGroupNorm E)

Equations

• NonarchAddGroupNorm.instOneOfDecidableEq = { one := let __src := 1; { toNonarchAddGroupSeminorm := __src, eq_zero_of_map_eq_zero' := ⋯ } }

@[simp]

theorem NonarchAddGroupNorm.apply_one {E : Type u_4} [AddGroup E] [DecidableEq E] (x : E) : 1 x = if x = 0 then 0 else 1

instance NonarchAddGroupNorm.instInhabitedOfDecidableEq {E : Type u_4} [AddGroup E] [DecidableEq E] : Inhabited (NonarchAddGroupNorm E)

Equations

• NonarchAddGroupNorm.instInhabitedOfDecidableEq = { default := 1 }