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_6) [AddGroup G] : Type u_6

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.

structure GroupSeminorm (G : Type u_6) [Group G] : Type u_6

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.

structure NonarchAddGroupSeminorm (G : Type u_6) [AddGroup G] extends ZeroHom G ℝ : Type u_6

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) ≤ 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.

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_6) [AddGroup G] extends AddGroupSeminorm G : Type u_6

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.

structure GroupNorm (G : Type u_6) [Group G] extends GroupSeminorm G : Type u_6

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.

structure NonarchAddGroupNorm (G : Type u_6) [AddGroup G] extends NonarchAddGroupSeminorm G : Type u_6

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) ≤ 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.

class NonarchAddGroupSeminormClass (F : Type u_6) (α : outParam (Type u_7)) [AddGroup α] [FunLike F α ℝ] extends NonarchimedeanHomClass F α ℝ : 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) ≤ 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.

class NonarchAddGroupNormClass (F : Type u_6) (α : outParam (Type u_7)) [AddGroup α] [FunLike F α ℝ] extends NonarchAddGroupSeminormClass F α : 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) ≤ 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 map_sub_le_max {E : Type u_3} {F : Type u_4} [AddGroup E] [FunLike F E ℝ] [NonarchAddGroupSeminormClass F E] (f : F) (x y : E) : f (x - y) ≤ f x ⊔ f y

@[instance 100]

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

Equations

• ⋯ = ⋯

@[instance 100]

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

Equations

• ⋯ = ⋯

Seminorms

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

Equations

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

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

Equations

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

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

@[simp]

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

@[simp]

theorem AddGroupSeminorm.toFun_eq_coe {E : Type u_3} [AddGroup E] {p : AddGroupSeminorm E} : p.toFun = ⇑p

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

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

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

Equations

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

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

Equations

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

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

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

Equations

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

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

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

Equations

• GroupSeminorm.instInhabited = { default := 0 }

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

Equations

• AddGroupSeminorm.instInhabited = { default := 0 }

instance GroupSeminorm.instAdd {E : Type u_3} [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' := ⋯ } }

instance AddGroupSeminorm.instAdd {E : Type u_3} [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' := ⋯ } }

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

instance GroupSeminorm.instMax {E : Type u_3} [Group E] : Max (GroupSeminorm E)

Equations

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

instance AddGroupSeminorm.instMax {E : Type u_3} [AddGroup E] : Max (AddGroupSeminorm E)

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

Equations

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

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

Equations

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

def GroupSeminorm.comp {E : Type u_3} {F : Type u_4} [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' := ⋯ }

def AddGroupSeminorm.comp {E : Type u_3} {F : Type u_4} [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' := ⋯ }

@[simp]

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

@[simp]

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

@[simp]

theorem GroupSeminorm.comp_apply {E : Type u_3} {F : Type u_4} [Group E] [Group F] (p : GroupSeminorm E) (f : F →* E) (x : F) : (p.comp f) x = p (f x)

@[simp]

theorem AddGroupSeminorm.comp_apply {E : Type u_3} {F : Type u_4} [AddGroup E] [AddGroup F] (p : AddGroupSeminorm E) (f : F →+ E) (x : F) : (p.comp f) x = p (f x)

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

theorem GroupSeminorm.comp_assoc {E : Type u_3} {F : Type u_4} {G : Type u_5} [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.comp_assoc {E : Type u_3} {F : Type u_4} {G : Type u_5} [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.add_comp {E : Type u_3} {F : Type u_4} [Group E] [Group F] (p q : GroupSeminorm E) (f : F →* E) : (p + q).comp f = p.comp f + q.comp f

theorem AddGroupSeminorm.add_comp {E : Type u_3} {F : Type u_4} [AddGroup E] [AddGroup F] (p q : AddGroupSeminorm E) (f : F →+ E) : (p + q).comp f = p.comp f + q.comp f

theorem GroupSeminorm.comp_mono {E : Type u_3} {F : Type u_4} [Group E] [Group F] {p q : GroupSeminorm E} (f : F →* E) (hp : p ≤ q) : p.comp f ≤ q.comp f

theorem AddGroupSeminorm.comp_mono {E : Type u_3} {F : Type u_4} [AddGroup E] [AddGroup F] {p q : AddGroupSeminorm E} (f : F →+ E) (hp : p ≤ q) : p.comp f ≤ q.comp f

theorem GroupSeminorm.comp_mul_le {E : Type u_3} {F : Type u_4} [CommGroup E] [CommGroup F] (p : GroupSeminorm E) (f g : F →* E) : p.comp (f * g) ≤ p.comp f + p.comp g

theorem AddGroupSeminorm.comp_add_le {E : Type u_3} {F : Type u_4} [AddCommGroup E] [AddCommGroup F] (p : AddGroupSeminorm E) (f g : F →+ E) : p.comp (f + g) ≤ p.comp f + p.comp g

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

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

noncomputable instance GroupSeminorm.instMin {E : Type u_3} [CommGroup E] : Min (GroupSeminorm E)

Equations

• GroupSeminorm.instMin = { min := fun (p q : GroupSeminorm E) => { toFun := fun (x : E) => ⨅ (y : E), p y + q (x / y), map_one' := ⋯, mul_le' := ⋯, inv' := ⋯ } }

noncomputable instance AddGroupSeminorm.instMin {E : Type u_3} [AddCommGroup E] : Min (AddGroupSeminorm E)

Equations

• AddGroupSeminorm.instMin = { min := fun (p q : AddGroupSeminorm E) => { toFun := fun (x : E) => ⨅ (y : E), p y + q (x - y), map_zero' := ⋯, add_le' := ⋯, neg' := ⋯ } }

@[simp]

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

@[simp]

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

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

Equations

• GroupSeminorm.instLattice = Lattice.mk (fun (x1 x2 : GroupSeminorm E) => x1 ⊓ x2) ⋯ ⋯ ⋯

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

Equations

• AddGroupSeminorm.instLattice = Lattice.mk (fun (x1 x2 : AddGroupSeminorm E) => x1 ⊓ x2) ⋯ ⋯ ⋯

instance AddGroupSeminorm.toOne {E : Type u_3} [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_3} [AddGroup E] [DecidableEq E] (x : E) : 1 x = if x = 0 then 0 else 1

instance AddGroupSeminorm.toSMul {R : Type u_1} {E : Type u_3} [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_1} {E : Type u_3} [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_1} {E : Type u_3} [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_1} {R' : Type u_2} {E : Type u_3} [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_1} {E : Type u_3} [AddGroup E] [SMul R ℝ] [SMul R NNReal] [IsScalarTower R NNReal ℝ] (r : R) (p q : AddGroupSeminorm E) : r • (p ⊔ q) = r • p ⊔ r • q

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

Equations

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

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

Equations

• ⋯ = ⋯

@[simp]

theorem NonarchAddGroupSeminorm.toZeroHom_eq_coe {E : Type u_3} [AddGroup E] {p : NonarchAddGroupSeminorm E} : ⇑p.toZeroHom = ⇑p

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

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

Equations

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

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

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

@[simp]

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

@[simp]

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

instance NonarchAddGroupSeminorm.instZero {E : Type u_3} [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_3} [AddGroup E] : ⇑0 = 0

@[simp]

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

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

Equations

• NonarchAddGroupSeminorm.instInhabited = { default := 0 }

instance NonarchAddGroupSeminorm.instMax {E : Type u_3} [AddGroup E] : Max (NonarchAddGroupSeminorm E)

Equations

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

@[simp]

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

@[simp]

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

noncomputable instance NonarchAddGroupSeminorm.instSemilatticeSup {E : Type u_3} [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_3} [AddCommGroup E] {p q : NonarchAddGroupSeminorm E} {x : E} : BddBelow (Set.range fun (y : E) => p y + q (x - y))

instance GroupSeminorm.toOne {E : Type u_3} [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_3} [Group E] [DecidableEq E] (x : E) : 1 x = if x = 1 then 0 else 1

instance GroupSeminorm.instSMul {R : Type u_1} {E : Type u_3} [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_1} {R' : Type u_2} {E : Type u_3} [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_1} {E : Type u_3} [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_1} {E : Type u_3} [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_1} {E : Type u_3} [Group E] [SMul R ℝ] [SMul R NNReal] [IsScalarTower R NNReal ℝ] (r : R) (p q : GroupSeminorm E) : r • (p ⊔ q) = r • p ⊔ r • q

instance NonarchAddGroupSeminorm.instOneOfDecidableEq {E : Type u_3} [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_3} [AddGroup E] [DecidableEq E] (x : E) : 1 x = if x = 0 then 0 else 1

instance NonarchAddGroupSeminorm.instSMul {R : Type u_1} {E : Type u_3} [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_1} {R' : Type u_2} {E : Type u_3} [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_1} {E : Type u_3} [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_1} {E : Type u_3} [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_1} {E : Type u_3} [AddGroup E] [SMul R ℝ] [SMul R NNReal] [IsScalarTower R NNReal ℝ] (r : R) (p q : NonarchAddGroupSeminorm E) : r • (p ⊔ q) = r • p ⊔ r • q

Norms

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

Equations

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

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

Equations

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

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

@[simp]

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

@[simp]

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

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

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

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

Equations

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

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

Equations

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

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

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

instance GroupNorm.instAdd {E : Type u_3} [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' := ⋯ } }

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

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

instance GroupNorm.instMax {E : Type u_3} [Group E] : Max (GroupNorm E)

Equations

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

instance AddGroupNorm.instMax {E : Type u_3} [AddGroup E] : Max (AddGroupNorm E)

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

Equations

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

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

Equations

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

instance AddGroupNorm.instOne {E : Type u_3} [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_3} [AddGroup E] [DecidableEq E] (x : E) : 1 x = if x = 0 then 0 else 1

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

Equations

• AddGroupNorm.instInhabited = { default := 1 }

instance AddGroupNorm.toOne {E : Type u_3} [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_3} [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_3} [Group E] [DecidableEq E] (x : E) : 1 x = if x = 1 then 0 else 1

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

Equations

• GroupNorm.instInhabited = { default := 1 }

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

Equations

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

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

Equations

• ⋯ = ⋯

@[simp]

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

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

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

Equations

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

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

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

@[simp]

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

@[simp]

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

instance NonarchAddGroupNorm.instMax {E : Type u_3} [AddGroup E] : Max (NonarchAddGroupNorm E)

Equations

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

@[simp]

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

@[simp]

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

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

Equations

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

instance NonarchAddGroupNorm.instOneOfDecidableEq {E : Type u_3} [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_3} [AddGroup E] [DecidableEq E] (x : E) : 1 x = if x = 0 then 0 else 1

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

Equations

• NonarchAddGroupNorm.instInhabitedOfDecidableEq = { default := 1 }