Documentation

Mathlib.Analysis.Normed.Group.Seminorm

Group seminorms #

This file defines norms and seminorms in a group. A group seminorm is a function to the reals which is positive-semidefinite and subadditive. A norm further only maps zero to zero.

Main declarations #

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 #

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.

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.

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.

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

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.

Instances
    class NonarchAddGroupNormClass (F : Type u_6) (α : outParam (Type u_7)) [AddGroup α] [FunLike F α ] extends NonarchAddGroupSeminormClass F α :

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

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

    Instances
      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

      Seminorms #

      Equations
      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
      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
      Equations
      Equations
      @[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.instAdd {E : Type u_3} [Group E] :
      Equations
      Equations
      @[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] :
      Equations
      Equations
      @[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
      def GroupSeminorm.comp {E : Type u_3} {F : Type u_4} [Group E] [Group F] (p : GroupSeminorm E) (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' := }
      def AddGroupSeminorm.comp {E : Type u_3} {F : Type u_4} [AddGroup E] [AddGroup F] (p : AddGroupSeminorm E) (f : F →+ E) :

      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) :
      @[simp]
      @[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) :
      comp 0 f = 0
      @[simp]
      theorem AddGroupSeminorm.zero_comp {E : Type u_3} {F : Type u_4} [AddGroup E] [AddGroup F] (f : F →+ E) :
      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] :
      Equations
      noncomputable instance AddGroupSeminorm.instMin {E : Type u_3} [AddCommGroup E] :
      Equations
      @[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] :
      Equations
      noncomputable instance AddGroupSeminorm.instLattice {E : Type u_3} [AddCommGroup E] :
      Equations
      Equations
      @[simp]
      theorem AddGroupSeminorm.apply_one {E : Type u_3} [AddGroup E] [DecidableEq E] (x : E) :
      1 x = if x = 0 then 0 else 1

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

      Equations
      @[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
      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
      Equations
      theorem NonarchAddGroupSeminorm.ext {E : Type u_3} [AddGroup E] {p q : NonarchAddGroupSeminorm E} :
      (∀ (x : E), p x = q x)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
      Equations
      @[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
      Equations
      @[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
      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] :
      Equations
      @[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 ] :

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

      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
      Equations
      @[simp]
      theorem NonarchAddGroupSeminorm.apply_one {E : Type u_3} [AddGroup E] [DecidableEq E] (x : E) :
      1 x = if x = 0 then 0 else 1

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

      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] :
      Equations
      Equations
      @[simp]
      theorem GroupNorm.toGroupSeminorm_eq_coe {E : Type u_3} [Group E] {p : GroupNorm E} :
      p.toGroupSeminorm = 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
      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] :
      Equations
      instance AddGroupNorm.instAdd {E : Type u_3} [AddGroup 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] :
      Equations
      instance AddGroupNorm.instMax {E : Type u_3} [AddGroup 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
      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
      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] :
      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
      Equations
      Equations
      theorem NonarchAddGroupNorm.ext {E : Type u_3} [AddGroup E] {p q : NonarchAddGroupNorm E} :
      (∀ (x : E), p x = q x)p = q
      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
      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
      Equations
      @[simp]
      theorem NonarchAddGroupNorm.apply_one {E : Type u_3} [AddGroup E] [DecidableEq E] (x : E) :
      1 x = if x = 0 then 0 else 1