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

Instances For
    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.

    Instances For
      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.

      Instances For
        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 = 0x = 0

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

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

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

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

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

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

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

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

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

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

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

              NonarchAddGroupSeminormClass F α states that F is a type of nonarchimedean seminorms on the additive group α.

              You should extend this class when you extend NonarchAddGroupSeminorm.

              • map_add_le_max : ∀ (f : F) (a b : α), f (a + b) max (f a) (f b)
              • map_zero : ∀ (f : F), f 0 = 0

                The image of zero is zero.

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

                The seminorm is invariant under negation.

              Instances
                theorem NonarchAddGroupSeminormClass.map_zero {F : Type u_7} {α : outParam (Type u_8)} [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.

                NonarchAddGroupNormClass F α states that F is a type of nonarchimedean norms on the additive group α.

                You should extend this class when you extend NonarchAddGroupNorm.

                • map_add_le_max : ∀ (f : F) (a b : α), f (a + b) max (f a) (f b)
                • map_zero : ∀ (f : F), f 0 = 0
                • map_neg_eq_map' : ∀ (f : F) (a : α), f (-a) = f a
                • eq_zero_of_map_eq_zero : ∀ (f : F) {a : α}, f a = 0a = 0

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

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

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

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

                  Seminorms #

                  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
                  Equations
                  • GroupSeminorm.funLike = { coe := fun (f : GroupSeminorm E) => f.toFun, coe_injective' := }

                  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
                  Equations
                  Equations
                  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
                  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)
                  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
                  Equations
                  • AddGroupSeminorm.instInhabited = { default := 0 }
                  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
                  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] :
                  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
                  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] :
                  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
                  Equations
                  Equations
                  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) :

                  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' := }
                  Instances For
                    def GroupSeminorm.comp {E : Type u_4} {F : Type u_5} [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' := }
                    Instances For
                      @[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) :
                      @[simp]
                      theorem GroupSeminorm.zero_comp {E : Type u_4} {F : Type u_5} [Group E] [Group F] (f : F →* E) :
                      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] :
                      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] :
                      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] :
                      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] :
                      Equations
                      • GroupSeminorm.instLattice = let __src := GroupSeminorm.semilatticeSup; Lattice.mk
                      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

                      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' ] :
                      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
                      Equations

                      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
                      Equations
                      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
                      Equations
                      • NonarchAddGroupSeminorm.instInhabited = { default := 0 }
                      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
                      Equations
                      instance GroupSeminorm.toOne {E : Type u_4} [Group E] [DecidableEq 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 ] :

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

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

                      Norms #

                      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] :
                      Equations
                      • GroupNorm.funLike = { coe := fun (f : GroupNorm E) => f.toFun, coe_injective' := }
                      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
                      Equations
                      Equations
                      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] :
                      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] :
                      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] :
                      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] :
                      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
                      Equations
                      Equations
                      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
                      Equations
                      • AddGroupNorm.instInhabited = { default := 1 }
                      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] :
                      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
                      Equations
                      • GroupNorm.instInhabited = { default := 1 }
                      Equations
                      • NonarchAddGroupNorm.funLike = { coe := fun (f : NonarchAddGroupNorm E) => f.toFun, coe_injective' := }
                      noncomputable instance NonarchAddGroupNorm.instCoeFunForallReal {E : Type u_4} [AddGroup 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
                      Equations
                      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
                      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
                      Equations
                      Equations
                      • NonarchAddGroupNorm.instOneOfDecidableEq = { one := let __src := 1; { toNonarchAddGroupSeminorm := __src, eq_zero_of_map_eq_zero' := } }
                      @[simp]
                      theorem NonarchAddGroupNorm.apply_one {E : Type u_4} [AddGroup E] [DecidableEq E] (x : E) :
                      1 x = if x = 0 then 0 else 1
                      Equations
                      • NonarchAddGroupNorm.instInhabitedOfDecidableEq = { default := 1 }