Documentation

Mathlib.Analysis.Seminorm

Seminorms #

This file defines seminorms.

A seminorm is a function to the reals which is positive-semidefinite, absolutely homogeneous, and subadditive. They are closely related to convex sets, and a topological vector space is locally convex if and only if its topology is induced by a family of seminorms.

Main declarations #

For a module over a normed ring:

References #

Tags #

seminorm, locally convex, LCTVS

structure Seminorm (๐•œ : Type u_13) (E : Type u_14) [SeminormedRing ๐•œ] [AddGroup E] [SMul ๐•œ E] extends AddGroupSeminorm :
Type u_14

A seminorm on a module over a normed ring is a function to the reals that is positive semidefinite, positive homogeneous, and subadditive.

  • toFun : E โ†’ โ„
  • map_zero' : self.toFun 0 = 0
  • add_le' : โˆ€ (r s : E), self.toFun (r + s) โ‰ค self.toFun r + self.toFun s
  • neg' : โˆ€ (r : E), self.toFun (-r) = self.toFun r
  • smul' : โˆ€ (a : ๐•œ) (x : E), self.toFun (a โ€ข x) = โ€–aโ€– * self.toFun x

    The seminorm of a scalar multiplication is the product of the absolute value of the scalar and the original seminorm.

Instances For
    theorem Seminorm.smul' {๐•œ : Type u_13} {E : Type u_14} [SeminormedRing ๐•œ] [AddGroup E] [SMul ๐•œ E] (self : Seminorm ๐•œ E) (a : ๐•œ) (x : E) :
    self.toFun (a โ€ข x) = โ€–aโ€– * self.toFun x

    The seminorm of a scalar multiplication is the product of the absolute value of the scalar and the original seminorm.

    class SeminormClass (F : Type u_13) (๐•œ : outParam (Type u_14)) (E : outParam (Type u_15)) [SeminormedRing ๐•œ] [AddGroup E] [SMul ๐•œ E] [FunLike F E โ„] extends AddGroupSeminormClass :

    SeminormClass F ๐•œ E states that F is a type of seminorms on the ๐•œ-module E.

    You should extend this class when you extend Seminorm.

    • map_add_le_add : โˆ€ (f : F) (a b : E), f (a + b) โ‰ค f a + f b
    • map_zero : โˆ€ (f : F), f 0 = 0
    • map_neg_eq_map : โˆ€ (f : F) (a : E), f (-a) = f a
    • map_smul_eq_mul : โˆ€ (f : F) (a : ๐•œ) (x : E), f (a โ€ข x) = โ€–aโ€– * f x

      The seminorm of a scalar multiplication is the product of the absolute value of the scalar and the original seminorm.

    Instances
      theorem SeminormClass.map_smul_eq_mul {F : Type u_13} {๐•œ : outParam (Type u_14)} {E : outParam (Type u_15)} :
      โˆ€ {inst : SeminormedRing ๐•œ} {inst_1 : AddGroup E} {inst_2 : SMul ๐•œ E} {inst_3 : FunLike F E โ„} [self : SeminormClass F ๐•œ E] (f : F) (a : ๐•œ) (x : E), f (a โ€ข x) = โ€–aโ€– * f x

      The seminorm of a scalar multiplication is the product of the absolute value of the scalar and the original seminorm.

      def Seminorm.of {๐•œ : Type u_3} {E : Type u_7} [SeminormedRing ๐•œ] [AddCommGroup E] [Module ๐•œ E] (f : E โ†’ โ„) (add_le : โˆ€ (x y : E), f (x + y) โ‰ค f x + f y) (smul : โˆ€ (a : ๐•œ) (x : E), f (a โ€ข x) = โ€–aโ€– * f x) :
      Seminorm ๐•œ E

      Alternative constructor for a Seminorm on an AddCommGroup E that is a module over a SeminormedRing ๐•œ.

      Equations
      • Seminorm.of f add_le smul = { toFun := f, map_zero' := โ‹ฏ, add_le' := add_le, neg' := โ‹ฏ, smul' := smul }
      Instances For
        def Seminorm.ofSMulLE {๐•œ : Type u_3} {E : Type u_7} [NormedField ๐•œ] [AddCommGroup E] [Module ๐•œ E] (f : E โ†’ โ„) (map_zero : f 0 = 0) (add_le : โˆ€ (x y : E), f (x + y) โ‰ค f x + f y) (smul_le : โˆ€ (r : ๐•œ) (x : E), f (r โ€ข x) โ‰ค โ€–rโ€– * f x) :
        Seminorm ๐•œ E

        Alternative constructor for a Seminorm over a normed field ๐•œ that only assumes f 0 = 0 and an inequality for the scalar multiplication.

        Equations
        Instances For
          instance Seminorm.instFunLike {๐•œ : Type u_3} {E : Type u_7} [SeminormedRing ๐•œ] [AddGroup E] [SMul ๐•œ E] :
          FunLike (Seminorm ๐•œ E) E โ„
          Equations
          • Seminorm.instFunLike = { coe := fun (f : Seminorm ๐•œ E) => f.toFun, coe_injective' := โ‹ฏ }
          instance Seminorm.instSeminormClass {๐•œ : Type u_3} {E : Type u_7} [SeminormedRing ๐•œ] [AddGroup E] [SMul ๐•œ E] :
          SeminormClass (Seminorm ๐•œ E) ๐•œ E
          Equations
          • โ‹ฏ = โ‹ฏ
          theorem Seminorm.ext_iff {๐•œ : Type u_3} {E : Type u_7} [SeminormedRing ๐•œ] [AddGroup E] [SMul ๐•œ E] {p : Seminorm ๐•œ E} {q : Seminorm ๐•œ E} :
          p = q โ†” โˆ€ (x : E), p x = q x
          theorem Seminorm.ext {๐•œ : Type u_3} {E : Type u_7} [SeminormedRing ๐•œ] [AddGroup E] [SMul ๐•œ E] {p : Seminorm ๐•œ E} {q : Seminorm ๐•œ E} (h : โˆ€ (x : E), p x = q x) :
          p = q
          instance Seminorm.instZero {๐•œ : Type u_3} {E : Type u_7} [SeminormedRing ๐•œ] [AddGroup E] [SMul ๐•œ E] :
          Zero (Seminorm ๐•œ E)
          Equations
          • Seminorm.instZero = { zero := let __src := Zero.zero; { toAddGroupSeminorm := __src, smul' := โ‹ฏ } }
          @[simp]
          theorem Seminorm.coe_zero {๐•œ : Type u_3} {E : Type u_7} [SeminormedRing ๐•œ] [AddGroup E] [SMul ๐•œ E] :
          โ‡‘0 = 0
          @[simp]
          theorem Seminorm.zero_apply {๐•œ : Type u_3} {E : Type u_7} [SeminormedRing ๐•œ] [AddGroup E] [SMul ๐•œ E] (x : E) :
          0 x = 0
          instance Seminorm.instInhabited {๐•œ : Type u_3} {E : Type u_7} [SeminormedRing ๐•œ] [AddGroup E] [SMul ๐•œ E] :
          Inhabited (Seminorm ๐•œ E)
          Equations
          • Seminorm.instInhabited = { default := 0 }
          instance Seminorm.instSMul {R : Type u_1} {๐•œ : Type u_3} {E : Type u_7} [SeminormedRing ๐•œ] [AddGroup E] [SMul ๐•œ E] [SMul R โ„] [SMul R NNReal] [IsScalarTower R NNReal โ„] :
          SMul R (Seminorm ๐•œ E)

          Any action on โ„ which factors through โ„โ‰ฅ0 applies to a seminorm.

          Equations
          • One or more equations did not get rendered due to their size.
          instance Seminorm.instIsScalarTowerOfReal {R : Type u_1} {R' : Type u_2} {๐•œ : Type u_3} {E : Type u_7} [SeminormedRing ๐•œ] [AddGroup E] [SMul ๐•œ 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' (Seminorm ๐•œ E)
          Equations
          • โ‹ฏ = โ‹ฏ
          theorem Seminorm.coe_smul {R : Type u_1} {๐•œ : Type u_3} {E : Type u_7} [SeminormedRing ๐•œ] [AddGroup E] [SMul ๐•œ E] [SMul R โ„] [SMul R NNReal] [IsScalarTower R NNReal โ„] (r : R) (p : Seminorm ๐•œ E) :
          โ‡‘(r โ€ข p) = r โ€ข โ‡‘p
          @[simp]
          theorem Seminorm.smul_apply {R : Type u_1} {๐•œ : Type u_3} {E : Type u_7} [SeminormedRing ๐•œ] [AddGroup E] [SMul ๐•œ E] [SMul R โ„] [SMul R NNReal] [IsScalarTower R NNReal โ„] (r : R) (p : Seminorm ๐•œ E) (x : E) :
          (r โ€ข p) x = r โ€ข p x
          instance Seminorm.instAdd {๐•œ : Type u_3} {E : Type u_7} [SeminormedRing ๐•œ] [AddGroup E] [SMul ๐•œ E] :
          Add (Seminorm ๐•œ E)
          Equations
          • One or more equations did not get rendered due to their size.
          theorem Seminorm.coe_add {๐•œ : Type u_3} {E : Type u_7} [SeminormedRing ๐•œ] [AddGroup E] [SMul ๐•œ E] (p : Seminorm ๐•œ E) (q : Seminorm ๐•œ E) :
          โ‡‘(p + q) = โ‡‘p + โ‡‘q
          @[simp]
          theorem Seminorm.add_apply {๐•œ : Type u_3} {E : Type u_7} [SeminormedRing ๐•œ] [AddGroup E] [SMul ๐•œ E] (p : Seminorm ๐•œ E) (q : Seminorm ๐•œ E) (x : E) :
          (p + q) x = p x + q x
          instance Seminorm.instAddMonoid {๐•œ : Type u_3} {E : Type u_7} [SeminormedRing ๐•œ] [AddGroup E] [SMul ๐•œ E] :
          AddMonoid (Seminorm ๐•œ E)
          Equations
          instance Seminorm.instOrderedCancelAddCommMonoid {๐•œ : Type u_3} {E : Type u_7} [SeminormedRing ๐•œ] [AddGroup E] [SMul ๐•œ E] :
          Equations
          instance Seminorm.instMulAction {R : Type u_1} {๐•œ : Type u_3} {E : Type u_7} [SeminormedRing ๐•œ] [AddGroup E] [SMul ๐•œ E] [Monoid R] [MulAction R โ„] [SMul R NNReal] [IsScalarTower R NNReal โ„] :
          MulAction R (Seminorm ๐•œ E)
          Equations
          @[simp]
          theorem Seminorm.coeFnAddMonoidHom_apply (๐•œ : Type u_3) (E : Type u_7) [SeminormedRing ๐•œ] [AddGroup E] [SMul ๐•œ E] :
          โˆ€ (a : Seminorm ๐•œ E) (a_1 : E), (Seminorm.coeFnAddMonoidHom ๐•œ E) a a_1 = a a_1
          def Seminorm.coeFnAddMonoidHom (๐•œ : Type u_3) (E : Type u_7) [SeminormedRing ๐•œ] [AddGroup E] [SMul ๐•œ E] :
          Seminorm ๐•œ E โ†’+ E โ†’ โ„

          coeFn as an AddMonoidHom. Helper definition for showing that Seminorm ๐•œ E is a module.

          Equations
          Instances For
            theorem Seminorm.coeFnAddMonoidHom_injective (๐•œ : Type u_3) (E : Type u_7) [SeminormedRing ๐•œ] [AddGroup E] [SMul ๐•œ E] :
            instance Seminorm.instDistribMulAction {R : Type u_1} {๐•œ : Type u_3} {E : Type u_7} [SeminormedRing ๐•œ] [AddGroup E] [SMul ๐•œ E] [Monoid R] [DistribMulAction R โ„] [SMul R NNReal] [IsScalarTower R NNReal โ„] :
            DistribMulAction R (Seminorm ๐•œ E)
            Equations
            instance Seminorm.instModule {R : Type u_1} {๐•œ : Type u_3} {E : Type u_7} [SeminormedRing ๐•œ] [AddGroup E] [SMul ๐•œ E] [Semiring R] [Module R โ„] [SMul R NNReal] [IsScalarTower R NNReal โ„] :
            Module R (Seminorm ๐•œ E)
            Equations
            instance Seminorm.instSup {๐•œ : Type u_3} {E : Type u_7} [SeminormedRing ๐•œ] [AddGroup E] [SMul ๐•œ E] :
            Sup (Seminorm ๐•œ E)
            Equations
            • One or more equations did not get rendered due to their size.
            @[simp]
            theorem Seminorm.coe_sup {๐•œ : Type u_3} {E : Type u_7} [SeminormedRing ๐•œ] [AddGroup E] [SMul ๐•œ E] (p : Seminorm ๐•œ E) (q : Seminorm ๐•œ E) :
            โ‡‘(p โŠ” q) = โ‡‘p โŠ” โ‡‘q
            theorem Seminorm.sup_apply {๐•œ : Type u_3} {E : Type u_7} [SeminormedRing ๐•œ] [AddGroup E] [SMul ๐•œ E] (p : Seminorm ๐•œ E) (q : Seminorm ๐•œ E) (x : E) :
            (p โŠ” q) x = p x โŠ” q x
            theorem Seminorm.smul_sup {R : Type u_1} {๐•œ : Type u_3} {E : Type u_7} [SeminormedRing ๐•œ] [AddGroup E] [SMul ๐•œ E] [SMul R โ„] [SMul R NNReal] [IsScalarTower R NNReal โ„] (r : R) (p : Seminorm ๐•œ E) (q : Seminorm ๐•œ E) :
            instance Seminorm.instPartialOrder {๐•œ : Type u_3} {E : Type u_7} [SeminormedRing ๐•œ] [AddGroup E] [SMul ๐•œ E] :
            PartialOrder (Seminorm ๐•œ E)
            Equations
            @[simp]
            theorem Seminorm.coe_le_coe {๐•œ : Type u_3} {E : Type u_7} [SeminormedRing ๐•œ] [AddGroup E] [SMul ๐•œ E] {p : Seminorm ๐•œ E} {q : Seminorm ๐•œ E} :
            โ‡‘p โ‰ค โ‡‘q โ†” p โ‰ค q
            @[simp]
            theorem Seminorm.coe_lt_coe {๐•œ : Type u_3} {E : Type u_7} [SeminormedRing ๐•œ] [AddGroup E] [SMul ๐•œ E] {p : Seminorm ๐•œ E} {q : Seminorm ๐•œ E} :
            โ‡‘p < โ‡‘q โ†” p < q
            theorem Seminorm.le_def {๐•œ : Type u_3} {E : Type u_7} [SeminormedRing ๐•œ] [AddGroup E] [SMul ๐•œ E] {p : Seminorm ๐•œ E} {q : Seminorm ๐•œ E} :
            p โ‰ค q โ†” โˆ€ (x : E), p x โ‰ค q x
            theorem Seminorm.lt_def {๐•œ : Type u_3} {E : Type u_7} [SeminormedRing ๐•œ] [AddGroup E] [SMul ๐•œ E] {p : Seminorm ๐•œ E} {q : Seminorm ๐•œ E} :
            p < q โ†” p โ‰ค q โˆง โˆƒ (x : E), p x < q x
            instance Seminorm.instSemilatticeSup {๐•œ : Type u_3} {E : Type u_7} [SeminormedRing ๐•œ] [AddGroup E] [SMul ๐•œ E] :
            SemilatticeSup (Seminorm ๐•œ E)
            Equations
            Equations
            def Seminorm.comp {๐•œ : Type u_3} {๐•œโ‚‚ : Type u_4} {E : Type u_7} {Eโ‚‚ : Type u_8} [SeminormedRing ๐•œ] [SeminormedRing ๐•œโ‚‚] {ฯƒโ‚โ‚‚ : ๐•œ โ†’+* ๐•œโ‚‚} [RingHomIsometric ฯƒโ‚โ‚‚] [AddCommGroup E] [AddCommGroup Eโ‚‚] [Module ๐•œ E] [Module ๐•œโ‚‚ Eโ‚‚] (p : Seminorm ๐•œโ‚‚ Eโ‚‚) (f : E โ†’โ‚›โ‚—[ฯƒโ‚โ‚‚] Eโ‚‚) :
            Seminorm ๐•œ E

            Composition of a seminorm with a linear map is a seminorm.

            Equations
            • p.comp f = { toFun := fun (x : E) => p (f x), map_zero' := โ‹ฏ, add_le' := โ‹ฏ, neg' := โ‹ฏ, smul' := โ‹ฏ }
            Instances For
              theorem Seminorm.coe_comp {๐•œ : Type u_3} {๐•œโ‚‚ : Type u_4} {E : Type u_7} {Eโ‚‚ : Type u_8} [SeminormedRing ๐•œ] [SeminormedRing ๐•œโ‚‚] {ฯƒโ‚โ‚‚ : ๐•œ โ†’+* ๐•œโ‚‚} [RingHomIsometric ฯƒโ‚โ‚‚] [AddCommGroup E] [AddCommGroup Eโ‚‚] [Module ๐•œ E] [Module ๐•œโ‚‚ Eโ‚‚] (p : Seminorm ๐•œโ‚‚ Eโ‚‚) (f : E โ†’โ‚›โ‚—[ฯƒโ‚โ‚‚] Eโ‚‚) :
              โ‡‘(p.comp f) = โ‡‘p โˆ˜ โ‡‘f
              @[simp]
              theorem Seminorm.comp_apply {๐•œ : Type u_3} {๐•œโ‚‚ : Type u_4} {E : Type u_7} {Eโ‚‚ : Type u_8} [SeminormedRing ๐•œ] [SeminormedRing ๐•œโ‚‚] {ฯƒโ‚โ‚‚ : ๐•œ โ†’+* ๐•œโ‚‚} [RingHomIsometric ฯƒโ‚โ‚‚] [AddCommGroup E] [AddCommGroup Eโ‚‚] [Module ๐•œ E] [Module ๐•œโ‚‚ Eโ‚‚] (p : Seminorm ๐•œโ‚‚ Eโ‚‚) (f : E โ†’โ‚›โ‚—[ฯƒโ‚โ‚‚] Eโ‚‚) (x : E) :
              (p.comp f) x = p (f x)
              @[simp]
              theorem Seminorm.comp_id {๐•œ : Type u_3} {E : Type u_7} [SeminormedRing ๐•œ] [AddCommGroup E] [Module ๐•œ E] (p : Seminorm ๐•œ E) :
              p.comp LinearMap.id = p
              @[simp]
              theorem Seminorm.comp_zero {๐•œ : Type u_3} {๐•œโ‚‚ : Type u_4} {E : Type u_7} {Eโ‚‚ : Type u_8} [SeminormedRing ๐•œ] [SeminormedRing ๐•œโ‚‚] {ฯƒโ‚โ‚‚ : ๐•œ โ†’+* ๐•œโ‚‚} [RingHomIsometric ฯƒโ‚โ‚‚] [AddCommGroup E] [AddCommGroup Eโ‚‚] [Module ๐•œ E] [Module ๐•œโ‚‚ Eโ‚‚] (p : Seminorm ๐•œโ‚‚ Eโ‚‚) :
              p.comp 0 = 0
              @[simp]
              theorem Seminorm.zero_comp {๐•œ : Type u_3} {๐•œโ‚‚ : Type u_4} {E : Type u_7} {Eโ‚‚ : Type u_8} [SeminormedRing ๐•œ] [SeminormedRing ๐•œโ‚‚] {ฯƒโ‚โ‚‚ : ๐•œ โ†’+* ๐•œโ‚‚} [RingHomIsometric ฯƒโ‚โ‚‚] [AddCommGroup E] [AddCommGroup Eโ‚‚] [Module ๐•œ E] [Module ๐•œโ‚‚ Eโ‚‚] (f : E โ†’โ‚›โ‚—[ฯƒโ‚โ‚‚] Eโ‚‚) :
              theorem Seminorm.comp_comp {๐•œ : Type u_3} {๐•œโ‚‚ : Type u_4} {๐•œโ‚ƒ : Type u_5} {E : Type u_7} {Eโ‚‚ : Type u_8} {Eโ‚ƒ : Type u_9} [SeminormedRing ๐•œ] [SeminormedRing ๐•œโ‚‚] [SeminormedRing ๐•œโ‚ƒ] {ฯƒโ‚โ‚‚ : ๐•œ โ†’+* ๐•œโ‚‚} [RingHomIsometric ฯƒโ‚โ‚‚] {ฯƒโ‚‚โ‚ƒ : ๐•œโ‚‚ โ†’+* ๐•œโ‚ƒ} [RingHomIsometric ฯƒโ‚‚โ‚ƒ] {ฯƒโ‚โ‚ƒ : ๐•œ โ†’+* ๐•œโ‚ƒ} [RingHomIsometric ฯƒโ‚โ‚ƒ] [AddCommGroup E] [AddCommGroup Eโ‚‚] [AddCommGroup Eโ‚ƒ] [Module ๐•œ E] [Module ๐•œโ‚‚ Eโ‚‚] [Module ๐•œโ‚ƒ Eโ‚ƒ] [RingHomCompTriple ฯƒโ‚โ‚‚ ฯƒโ‚‚โ‚ƒ ฯƒโ‚โ‚ƒ] (p : Seminorm ๐•œโ‚ƒ Eโ‚ƒ) (g : Eโ‚‚ โ†’โ‚›โ‚—[ฯƒโ‚‚โ‚ƒ] Eโ‚ƒ) (f : E โ†’โ‚›โ‚—[ฯƒโ‚โ‚‚] Eโ‚‚) :
              p.comp (g.comp f) = (p.comp g).comp f
              theorem Seminorm.add_comp {๐•œ : Type u_3} {๐•œโ‚‚ : Type u_4} {E : Type u_7} {Eโ‚‚ : Type u_8} [SeminormedRing ๐•œ] [SeminormedRing ๐•œโ‚‚] {ฯƒโ‚โ‚‚ : ๐•œ โ†’+* ๐•œโ‚‚} [RingHomIsometric ฯƒโ‚โ‚‚] [AddCommGroup E] [AddCommGroup Eโ‚‚] [Module ๐•œ E] [Module ๐•œโ‚‚ Eโ‚‚] (p : Seminorm ๐•œโ‚‚ Eโ‚‚) (q : Seminorm ๐•œโ‚‚ Eโ‚‚) (f : E โ†’โ‚›โ‚—[ฯƒโ‚โ‚‚] Eโ‚‚) :
              (p + q).comp f = p.comp f + q.comp f
              theorem Seminorm.comp_add_le {๐•œ : Type u_3} {๐•œโ‚‚ : Type u_4} {E : Type u_7} {Eโ‚‚ : Type u_8} [SeminormedRing ๐•œ] [SeminormedRing ๐•œโ‚‚] {ฯƒโ‚โ‚‚ : ๐•œ โ†’+* ๐•œโ‚‚} [RingHomIsometric ฯƒโ‚โ‚‚] [AddCommGroup E] [AddCommGroup Eโ‚‚] [Module ๐•œ E] [Module ๐•œโ‚‚ Eโ‚‚] (p : Seminorm ๐•œโ‚‚ Eโ‚‚) (f : E โ†’โ‚›โ‚—[ฯƒโ‚โ‚‚] Eโ‚‚) (g : E โ†’โ‚›โ‚—[ฯƒโ‚โ‚‚] Eโ‚‚) :
              p.comp (f + g) โ‰ค p.comp f + p.comp g
              theorem Seminorm.smul_comp {R : Type u_1} {๐•œ : Type u_3} {๐•œโ‚‚ : Type u_4} {E : Type u_7} {Eโ‚‚ : Type u_8} [SeminormedRing ๐•œ] [SeminormedRing ๐•œโ‚‚] {ฯƒโ‚โ‚‚ : ๐•œ โ†’+* ๐•œโ‚‚} [RingHomIsometric ฯƒโ‚โ‚‚] [AddCommGroup E] [AddCommGroup Eโ‚‚] [Module ๐•œ E] [Module ๐•œโ‚‚ Eโ‚‚] [SMul R โ„] [SMul R NNReal] [IsScalarTower R NNReal โ„] (p : Seminorm ๐•œโ‚‚ Eโ‚‚) (f : E โ†’โ‚›โ‚—[ฯƒโ‚โ‚‚] Eโ‚‚) (c : R) :
              (c โ€ข p).comp f = c โ€ข p.comp f
              theorem Seminorm.comp_mono {๐•œ : Type u_3} {๐•œโ‚‚ : Type u_4} {E : Type u_7} {Eโ‚‚ : Type u_8} [SeminormedRing ๐•œ] [SeminormedRing ๐•œโ‚‚] {ฯƒโ‚โ‚‚ : ๐•œ โ†’+* ๐•œโ‚‚} [RingHomIsometric ฯƒโ‚โ‚‚] [AddCommGroup E] [AddCommGroup Eโ‚‚] [Module ๐•œ E] [Module ๐•œโ‚‚ Eโ‚‚] {p : Seminorm ๐•œโ‚‚ Eโ‚‚} {q : Seminorm ๐•œโ‚‚ Eโ‚‚} (f : E โ†’โ‚›โ‚—[ฯƒโ‚โ‚‚] Eโ‚‚) (hp : p โ‰ค q) :
              p.comp f โ‰ค q.comp f
              @[simp]
              theorem Seminorm.pullback_apply {๐•œ : Type u_3} {๐•œโ‚‚ : Type u_4} {E : Type u_7} {Eโ‚‚ : Type u_8} [SeminormedRing ๐•œ] [SeminormedRing ๐•œโ‚‚] {ฯƒโ‚โ‚‚ : ๐•œ โ†’+* ๐•œโ‚‚} [RingHomIsometric ฯƒโ‚โ‚‚] [AddCommGroup E] [AddCommGroup Eโ‚‚] [Module ๐•œ E] [Module ๐•œโ‚‚ Eโ‚‚] (f : E โ†’โ‚›โ‚—[ฯƒโ‚โ‚‚] Eโ‚‚) (p : Seminorm ๐•œโ‚‚ Eโ‚‚) :
              (Seminorm.pullback f) p = p.comp f
              def Seminorm.pullback {๐•œ : Type u_3} {๐•œโ‚‚ : Type u_4} {E : Type u_7} {Eโ‚‚ : Type u_8} [SeminormedRing ๐•œ] [SeminormedRing ๐•œโ‚‚] {ฯƒโ‚โ‚‚ : ๐•œ โ†’+* ๐•œโ‚‚} [RingHomIsometric ฯƒโ‚โ‚‚] [AddCommGroup E] [AddCommGroup Eโ‚‚] [Module ๐•œ E] [Module ๐•œโ‚‚ Eโ‚‚] (f : E โ†’โ‚›โ‚—[ฯƒโ‚โ‚‚] Eโ‚‚) :
              Seminorm ๐•œโ‚‚ Eโ‚‚ โ†’+ Seminorm ๐•œ E

              The composition as an AddMonoidHom.

              Equations
              • Seminorm.pullback f = { toFun := fun (p : Seminorm ๐•œโ‚‚ Eโ‚‚) => p.comp f, map_zero' := โ‹ฏ, map_add' := โ‹ฏ }
              Instances For
                instance Seminorm.instOrderBot {๐•œ : Type u_3} {E : Type u_7} [SeminormedRing ๐•œ] [AddCommGroup E] [Module ๐•œ E] :
                OrderBot (Seminorm ๐•œ E)
                Equations
                @[simp]
                theorem Seminorm.coe_bot {๐•œ : Type u_3} {E : Type u_7} [SeminormedRing ๐•œ] [AddCommGroup E] [Module ๐•œ E] :
                โ‡‘โŠฅ = 0
                theorem Seminorm.bot_eq_zero {๐•œ : Type u_3} {E : Type u_7} [SeminormedRing ๐•œ] [AddCommGroup E] [Module ๐•œ E] :
                theorem Seminorm.smul_le_smul {๐•œ : Type u_3} {E : Type u_7} [SeminormedRing ๐•œ] [AddCommGroup E] [Module ๐•œ E] {p : Seminorm ๐•œ E} {q : Seminorm ๐•œ E} {a : NNReal} {b : NNReal} (hpq : p โ‰ค q) (hab : a โ‰ค b) :
                theorem Seminorm.finset_sup_apply {๐•œ : Type u_3} {E : Type u_7} {ฮน : Type u_12} [SeminormedRing ๐•œ] [AddCommGroup E] [Module ๐•œ E] (p : ฮน โ†’ Seminorm ๐•œ E) (s : Finset ฮน) (x : E) :
                (s.sup p) x = โ†‘(s.sup fun (i : ฮน) => โŸจ(p i) x, โ‹ฏโŸฉ)
                theorem Seminorm.exists_apply_eq_finset_sup {๐•œ : Type u_3} {E : Type u_7} {ฮน : Type u_12} [SeminormedRing ๐•œ] [AddCommGroup E] [Module ๐•œ E] (p : ฮน โ†’ Seminorm ๐•œ E) {s : Finset ฮน} (hs : s.Nonempty) (x : E) :
                โˆƒ i โˆˆ s, (s.sup p) x = (p i) x
                theorem Seminorm.zero_or_exists_apply_eq_finset_sup {๐•œ : Type u_3} {E : Type u_7} {ฮน : Type u_12} [SeminormedRing ๐•œ] [AddCommGroup E] [Module ๐•œ E] (p : ฮน โ†’ Seminorm ๐•œ E) (s : Finset ฮน) (x : E) :
                (s.sup p) x = 0 โˆจ โˆƒ i โˆˆ s, (s.sup p) x = (p i) x
                theorem Seminorm.finset_sup_smul {๐•œ : Type u_3} {E : Type u_7} {ฮน : Type u_12} [SeminormedRing ๐•œ] [AddCommGroup E] [Module ๐•œ E] (p : ฮน โ†’ Seminorm ๐•œ E) (s : Finset ฮน) (C : NNReal) :
                s.sup (C โ€ข p) = C โ€ข s.sup p
                theorem Seminorm.finset_sup_le_sum {๐•œ : Type u_3} {E : Type u_7} {ฮน : Type u_12} [SeminormedRing ๐•œ] [AddCommGroup E] [Module ๐•œ E] (p : ฮน โ†’ Seminorm ๐•œ E) (s : Finset ฮน) :
                s.sup p โ‰ค โˆ‘ i โˆˆ s, p i
                theorem Seminorm.finset_sup_apply_le {๐•œ : Type u_3} {E : Type u_7} {ฮน : Type u_12} [SeminormedRing ๐•œ] [AddCommGroup E] [Module ๐•œ E] {p : ฮน โ†’ Seminorm ๐•œ E} {s : Finset ฮน} {x : E} {a : โ„} (ha : 0 โ‰ค a) (h : โˆ€ i โˆˆ s, (p i) x โ‰ค a) :
                (s.sup p) x โ‰ค a
                theorem Seminorm.le_finset_sup_apply {๐•œ : Type u_3} {E : Type u_7} {ฮน : Type u_12} [SeminormedRing ๐•œ] [AddCommGroup E] [Module ๐•œ E] {p : ฮน โ†’ Seminorm ๐•œ E} {s : Finset ฮน} {x : E} {i : ฮน} (hi : i โˆˆ s) :
                (p i) x โ‰ค (s.sup p) x
                theorem Seminorm.finset_sup_apply_lt {๐•œ : Type u_3} {E : Type u_7} {ฮน : Type u_12} [SeminormedRing ๐•œ] [AddCommGroup E] [Module ๐•œ E] {p : ฮน โ†’ Seminorm ๐•œ E} {s : Finset ฮน} {x : E} {a : โ„} (ha : 0 < a) (h : โˆ€ i โˆˆ s, (p i) x < a) :
                (s.sup p) x < a
                theorem Seminorm.norm_sub_map_le_sub {๐•œ : Type u_3} {E : Type u_7} [SeminormedRing ๐•œ] [AddCommGroup E] [Module ๐•œ E] (p : Seminorm ๐•œ E) (x : E) (y : E) :
                โ€–p x - p yโ€– โ‰ค p (x - y)
                theorem Seminorm.comp_smul {๐•œ : Type u_3} {๐•œโ‚‚ : Type u_4} {E : Type u_7} {Eโ‚‚ : Type u_8} [SeminormedRing ๐•œ] [SeminormedCommRing ๐•œโ‚‚] {ฯƒโ‚โ‚‚ : ๐•œ โ†’+* ๐•œโ‚‚} [RingHomIsometric ฯƒโ‚โ‚‚] [AddCommGroup E] [AddCommGroup Eโ‚‚] [Module ๐•œ E] [Module ๐•œโ‚‚ Eโ‚‚] (p : Seminorm ๐•œโ‚‚ Eโ‚‚) (f : E โ†’โ‚›โ‚—[ฯƒโ‚โ‚‚] Eโ‚‚) (c : ๐•œโ‚‚) :
                p.comp (c โ€ข f) = โ€–cโ€–โ‚Š โ€ข p.comp f
                theorem Seminorm.comp_smul_apply {๐•œ : Type u_3} {๐•œโ‚‚ : Type u_4} {E : Type u_7} {Eโ‚‚ : Type u_8} [SeminormedRing ๐•œ] [SeminormedCommRing ๐•œโ‚‚] {ฯƒโ‚โ‚‚ : ๐•œ โ†’+* ๐•œโ‚‚} [RingHomIsometric ฯƒโ‚โ‚‚] [AddCommGroup E] [AddCommGroup Eโ‚‚] [Module ๐•œ E] [Module ๐•œโ‚‚ Eโ‚‚] (p : Seminorm ๐•œโ‚‚ Eโ‚‚) (f : E โ†’โ‚›โ‚—[ฯƒโ‚โ‚‚] Eโ‚‚) (c : ๐•œโ‚‚) (x : E) :
                (p.comp (c โ€ข f)) x = โ€–cโ€– * p (f x)
                theorem Seminorm.bddBelow_range_add {๐•œ : Type u_3} {E : Type u_7} [NormedField ๐•œ] [AddCommGroup E] [Module ๐•œ E] {p : Seminorm ๐•œ E} {q : Seminorm ๐•œ E} {x : E} :
                BddBelow (Set.range fun (u : E) => p u + q (x - u))

                Auxiliary lemma to show that the infimum of seminorms is well-defined.

                noncomputable instance Seminorm.instInf {๐•œ : Type u_3} {E : Type u_7} [NormedField ๐•œ] [AddCommGroup E] [Module ๐•œ E] :
                Inf (Seminorm ๐•œ E)
                Equations
                • One or more equations did not get rendered due to their size.
                @[simp]
                theorem Seminorm.inf_apply {๐•œ : Type u_3} {E : Type u_7} [NormedField ๐•œ] [AddCommGroup E] [Module ๐•œ E] (p : Seminorm ๐•œ E) (q : Seminorm ๐•œ E) (x : E) :
                (p โŠ“ q) x = โจ… (u : E), p u + q (x - u)
                noncomputable instance Seminorm.instLattice {๐•œ : Type u_3} {E : Type u_7} [NormedField ๐•œ] [AddCommGroup E] [Module ๐•œ E] :
                Lattice (Seminorm ๐•œ E)
                Equations
                • Seminorm.instLattice = Lattice.mk โ‹ฏ โ‹ฏ โ‹ฏ
                theorem Seminorm.smul_inf {R : Type u_1} {๐•œ : Type u_3} {E : Type u_7} [NormedField ๐•œ] [AddCommGroup E] [Module ๐•œ E] [SMul R โ„] [SMul R NNReal] [IsScalarTower R NNReal โ„] (r : R) (p : Seminorm ๐•œ E) (q : Seminorm ๐•œ E) :
                noncomputable instance Seminorm.instSupSet {๐•œ : Type u_3} {E : Type u_7} [NormedField ๐•œ] [AddCommGroup E] [Module ๐•œ E] :
                SupSet (Seminorm ๐•œ E)

                We define the supremum of an arbitrary subset of Seminorm ๐•œ E as follows:

                • if s is BddAbove as a set of functions E โ†’ โ„ (that is, if s is pointwise bounded above), we take the pointwise supremum of all elements of s, and we prove that it is indeed a seminorm.
                • otherwise, we take the zero seminorm โŠฅ.

                There are two things worth mentioning here:

                • First, it is not trivial at first that s being bounded above by a function implies being bounded above as a seminorm. We show this in Seminorm.bddAbove_iff by using that the Sup s as defined here is then a bounding seminorm for s. So it is important to make the case disjunction on BddAbove ((โ†‘) '' s : Set (E โ†’ โ„)) and not BddAbove s.
                • Since the pointwise Sup already gives 0 at points where a family of functions is not bounded above, one could hope that just using the pointwise Sup would work here, without the need for an additional case disjunction. As discussed on Zulip, this doesn't work because this can give a function which does not satisfy the seminorm axioms (typically sub-additivity).
                Equations
                • One or more equations did not get rendered due to their size.
                theorem Seminorm.coe_sSup_eq' {๐•œ : Type u_3} {E : Type u_7} [NormedField ๐•œ] [AddCommGroup E] [Module ๐•œ E] {s : Set (Seminorm ๐•œ E)} (hs : BddAbove (DFunLike.coe '' s)) :
                โ‡‘(sSup s) = โจ† (p : โ†‘s), โ‡‘โ†‘p
                theorem Seminorm.bddAbove_iff {๐•œ : Type u_3} {E : Type u_7} [NormedField ๐•œ] [AddCommGroup E] [Module ๐•œ E] {s : Set (Seminorm ๐•œ E)} :
                BddAbove s โ†” BddAbove (DFunLike.coe '' s)
                theorem Seminorm.bddAbove_range_iff {๐•œ : Type u_3} {E : Type u_7} [NormedField ๐•œ] [AddCommGroup E] [Module ๐•œ E] {ฮน : Sort u_13} {p : ฮน โ†’ Seminorm ๐•œ E} :
                BddAbove (Set.range p) โ†” โˆ€ (x : E), BddAbove (Set.range fun (i : ฮน) => (p i) x)
                theorem Seminorm.coe_sSup_eq {๐•œ : Type u_3} {E : Type u_7} [NormedField ๐•œ] [AddCommGroup E] [Module ๐•œ E] {s : Set (Seminorm ๐•œ E)} (hs : BddAbove s) :
                โ‡‘(sSup s) = โจ† (p : โ†‘s), โ‡‘โ†‘p
                theorem Seminorm.coe_iSup_eq {๐•œ : Type u_3} {E : Type u_7} [NormedField ๐•œ] [AddCommGroup E] [Module ๐•œ E] {ฮน : Sort u_13} {p : ฮน โ†’ Seminorm ๐•œ E} (hp : BddAbove (Set.range p)) :
                โ‡‘(โจ† (i : ฮน), p i) = โจ† (i : ฮน), โ‡‘(p i)
                theorem Seminorm.sSup_apply {๐•œ : Type u_3} {E : Type u_7} [NormedField ๐•œ] [AddCommGroup E] [Module ๐•œ E] {s : Set (Seminorm ๐•œ E)} (hp : BddAbove s) {x : E} :
                (sSup s) x = โจ† (p : โ†‘s), โ†‘p x
                theorem Seminorm.iSup_apply {๐•œ : Type u_3} {E : Type u_7} [NormedField ๐•œ] [AddCommGroup E] [Module ๐•œ E] {ฮน : Sort u_13} {p : ฮน โ†’ Seminorm ๐•œ E} (hp : BddAbove (Set.range p)) {x : E} :
                (โจ† (i : ฮน), p i) x = โจ† (i : ฮน), (p i) x
                theorem Seminorm.sSup_empty {๐•œ : Type u_3} {E : Type u_7} [NormedField ๐•œ] [AddCommGroup E] [Module ๐•œ E] :
                noncomputable instance Seminorm.instConditionallyCompleteLattice {๐•œ : Type u_3} {E : Type u_7} [NormedField ๐•œ] [AddCommGroup E] [Module ๐•œ E] :

                Seminorm ๐•œ E is a conditionally complete lattice.

                Note that, while inf, sup and sSup have good definitional properties (corresponding to the instances given here for Inf, Sup and SupSet respectively), sInf s is just defined as the supremum of the lower bounds of s, which is not really useful in practice. If you need to use sInf on seminorms, then you should probably provide a more workable definition first, but this is unlikely to happen so we keep the "bad" definition for now.

                Equations

                Seminorm ball #

                def Seminorm.ball {๐•œ : Type u_3} {E : Type u_7} [SeminormedRing ๐•œ] [AddCommGroup E] [SMul ๐•œ E] (p : Seminorm ๐•œ E) (x : E) (r : โ„) :
                Set E

                The ball of radius r at x with respect to seminorm p is the set of elements y with p (y - x) < r.

                Equations
                • p.ball x r = {y : E | p (y - x) < r}
                Instances For
                  def Seminorm.closedBall {๐•œ : Type u_3} {E : Type u_7} [SeminormedRing ๐•œ] [AddCommGroup E] [SMul ๐•œ E] (p : Seminorm ๐•œ E) (x : E) (r : โ„) :
                  Set E

                  The closed ball of radius r at x with respect to seminorm p is the set of elements y with p (y - x) โ‰ค r.

                  Equations
                  Instances For
                    @[simp]
                    theorem Seminorm.mem_ball {๐•œ : Type u_3} {E : Type u_7} [SeminormedRing ๐•œ] [AddCommGroup E] [SMul ๐•œ E] (p : Seminorm ๐•œ E) {x : E} {y : E} {r : โ„} :
                    y โˆˆ p.ball x r โ†” p (y - x) < r
                    @[simp]
                    theorem Seminorm.mem_closedBall {๐•œ : Type u_3} {E : Type u_7} [SeminormedRing ๐•œ] [AddCommGroup E] [SMul ๐•œ E] (p : Seminorm ๐•œ E) {x : E} {y : E} {r : โ„} :
                    y โˆˆ p.closedBall x r โ†” p (y - x) โ‰ค r
                    theorem Seminorm.mem_ball_self {๐•œ : Type u_3} {E : Type u_7} [SeminormedRing ๐•œ] [AddCommGroup E] [SMul ๐•œ E] (p : Seminorm ๐•œ E) {x : E} {r : โ„} (hr : 0 < r) :
                    x โˆˆ p.ball x r
                    theorem Seminorm.mem_closedBall_self {๐•œ : Type u_3} {E : Type u_7} [SeminormedRing ๐•œ] [AddCommGroup E] [SMul ๐•œ E] (p : Seminorm ๐•œ E) {x : E} {r : โ„} (hr : 0 โ‰ค r) :
                    x โˆˆ p.closedBall x r
                    theorem Seminorm.mem_ball_zero {๐•œ : Type u_3} {E : Type u_7} [SeminormedRing ๐•œ] [AddCommGroup E] [SMul ๐•œ E] (p : Seminorm ๐•œ E) {y : E} {r : โ„} :
                    y โˆˆ p.ball 0 r โ†” p y < r
                    theorem Seminorm.mem_closedBall_zero {๐•œ : Type u_3} {E : Type u_7} [SeminormedRing ๐•œ] [AddCommGroup E] [SMul ๐•œ E] (p : Seminorm ๐•œ E) {y : E} {r : โ„} :
                    y โˆˆ p.closedBall 0 r โ†” p y โ‰ค r
                    theorem Seminorm.ball_zero_eq {๐•œ : Type u_3} {E : Type u_7} [SeminormedRing ๐•œ] [AddCommGroup E] [SMul ๐•œ E] (p : Seminorm ๐•œ E) {r : โ„} :
                    p.ball 0 r = {y : E | p y < r}
                    theorem Seminorm.closedBall_zero_eq {๐•œ : Type u_3} {E : Type u_7} [SeminormedRing ๐•œ] [AddCommGroup E] [SMul ๐•œ E] (p : Seminorm ๐•œ E) {r : โ„} :
                    p.closedBall 0 r = {y : E | p y โ‰ค r}
                    theorem Seminorm.ball_subset_closedBall {๐•œ : Type u_3} {E : Type u_7} [SeminormedRing ๐•œ] [AddCommGroup E] [SMul ๐•œ E] (p : Seminorm ๐•œ E) (x : E) (r : โ„) :
                    p.ball x r โŠ† p.closedBall x r
                    theorem Seminorm.closedBall_eq_biInter_ball {๐•œ : Type u_3} {E : Type u_7} [SeminormedRing ๐•œ] [AddCommGroup E] [SMul ๐•œ E] (p : Seminorm ๐•œ E) (x : E) (r : โ„) :
                    p.closedBall x r = โ‹‚ (ฯ : โ„), โ‹‚ (_ : ฯ > r), p.ball x ฯ
                    @[simp]
                    theorem Seminorm.ball_zero' {๐•œ : Type u_3} {E : Type u_7} [SeminormedRing ๐•œ] [AddCommGroup E] [SMul ๐•œ E] {r : โ„} (x : E) (hr : 0 < r) :
                    Seminorm.ball 0 x r = Set.univ
                    @[simp]
                    theorem Seminorm.closedBall_zero' {๐•œ : Type u_3} {E : Type u_7} [SeminormedRing ๐•œ] [AddCommGroup E] [SMul ๐•œ E] {r : โ„} (x : E) (hr : 0 < r) :
                    Seminorm.closedBall 0 x r = Set.univ
                    theorem Seminorm.ball_smul {๐•œ : Type u_3} {E : Type u_7} [SeminormedRing ๐•œ] [AddCommGroup E] [SMul ๐•œ E] (p : Seminorm ๐•œ E) {c : NNReal} (hc : 0 < c) (r : โ„) (x : E) :
                    (c โ€ข p).ball x r = p.ball x (r / โ†‘c)
                    theorem Seminorm.closedBall_smul {๐•œ : Type u_3} {E : Type u_7} [SeminormedRing ๐•œ] [AddCommGroup E] [SMul ๐•œ E] (p : Seminorm ๐•œ E) {c : NNReal} (hc : 0 < c) (r : โ„) (x : E) :
                    (c โ€ข p).closedBall x r = p.closedBall x (r / โ†‘c)
                    theorem Seminorm.ball_sup {๐•œ : Type u_3} {E : Type u_7} [SeminormedRing ๐•œ] [AddCommGroup E] [SMul ๐•œ E] (p : Seminorm ๐•œ E) (q : Seminorm ๐•œ E) (e : E) (r : โ„) :
                    (p โŠ” q).ball e r = p.ball e r โˆฉ q.ball e r
                    theorem Seminorm.closedBall_sup {๐•œ : Type u_3} {E : Type u_7} [SeminormedRing ๐•œ] [AddCommGroup E] [SMul ๐•œ E] (p : Seminorm ๐•œ E) (q : Seminorm ๐•œ E) (e : E) (r : โ„) :
                    (p โŠ” q).closedBall e r = p.closedBall e r โˆฉ q.closedBall e r
                    theorem Seminorm.ball_finset_sup' {๐•œ : Type u_3} {E : Type u_7} {ฮน : Type u_12} [SeminormedRing ๐•œ] [AddCommGroup E] [SMul ๐•œ E] (p : ฮน โ†’ Seminorm ๐•œ E) (s : Finset ฮน) (H : s.Nonempty) (e : E) (r : โ„) :
                    (s.sup' H p).ball e r = s.inf' H fun (i : ฮน) => (p i).ball e r
                    theorem Seminorm.closedBall_finset_sup' {๐•œ : Type u_3} {E : Type u_7} {ฮน : Type u_12} [SeminormedRing ๐•œ] [AddCommGroup E] [SMul ๐•œ E] (p : ฮน โ†’ Seminorm ๐•œ E) (s : Finset ฮน) (H : s.Nonempty) (e : E) (r : โ„) :
                    (s.sup' H p).closedBall e r = s.inf' H fun (i : ฮน) => (p i).closedBall e r
                    theorem Seminorm.ball_mono {๐•œ : Type u_3} {E : Type u_7} [SeminormedRing ๐•œ] [AddCommGroup E] [SMul ๐•œ E] {x : E} {p : Seminorm ๐•œ E} {rโ‚ : โ„} {rโ‚‚ : โ„} (h : rโ‚ โ‰ค rโ‚‚) :
                    p.ball x rโ‚ โŠ† p.ball x rโ‚‚
                    theorem Seminorm.closedBall_mono {๐•œ : Type u_3} {E : Type u_7} [SeminormedRing ๐•œ] [AddCommGroup E] [SMul ๐•œ E] {x : E} {p : Seminorm ๐•œ E} {rโ‚ : โ„} {rโ‚‚ : โ„} (h : rโ‚ โ‰ค rโ‚‚) :
                    p.closedBall x rโ‚ โŠ† p.closedBall x rโ‚‚
                    theorem Seminorm.ball_antitone {๐•œ : Type u_3} {E : Type u_7} [SeminormedRing ๐•œ] [AddCommGroup E] [SMul ๐•œ E] {x : E} {r : โ„} {p : Seminorm ๐•œ E} {q : Seminorm ๐•œ E} (h : q โ‰ค p) :
                    p.ball x r โŠ† q.ball x r
                    theorem Seminorm.closedBall_antitone {๐•œ : Type u_3} {E : Type u_7} [SeminormedRing ๐•œ] [AddCommGroup E] [SMul ๐•œ E] {x : E} {r : โ„} {p : Seminorm ๐•œ E} {q : Seminorm ๐•œ E} (h : q โ‰ค p) :
                    p.closedBall x r โŠ† q.closedBall x r
                    theorem Seminorm.ball_add_ball_subset {๐•œ : Type u_3} {E : Type u_7} [SeminormedRing ๐•œ] [AddCommGroup E] [SMul ๐•œ E] (p : Seminorm ๐•œ E) (rโ‚ : โ„) (rโ‚‚ : โ„) (xโ‚ : E) (xโ‚‚ : E) :
                    p.ball xโ‚ rโ‚ + p.ball xโ‚‚ rโ‚‚ โŠ† p.ball (xโ‚ + xโ‚‚) (rโ‚ + rโ‚‚)
                    theorem Seminorm.closedBall_add_closedBall_subset {๐•œ : Type u_3} {E : Type u_7} [SeminormedRing ๐•œ] [AddCommGroup E] [SMul ๐•œ E] (p : Seminorm ๐•œ E) (rโ‚ : โ„) (rโ‚‚ : โ„) (xโ‚ : E) (xโ‚‚ : E) :
                    p.closedBall xโ‚ rโ‚ + p.closedBall xโ‚‚ rโ‚‚ โŠ† p.closedBall (xโ‚ + xโ‚‚) (rโ‚ + rโ‚‚)
                    theorem Seminorm.sub_mem_ball {๐•œ : Type u_3} {E : Type u_7} [SeminormedRing ๐•œ] [AddCommGroup E] [SMul ๐•œ E] (p : Seminorm ๐•œ E) (xโ‚ : E) (xโ‚‚ : E) (y : E) (r : โ„) :
                    xโ‚ - xโ‚‚ โˆˆ p.ball y r โ†” xโ‚ โˆˆ p.ball (xโ‚‚ + y) r
                    theorem Seminorm.vadd_ball {๐•œ : Type u_3} {E : Type u_7} [SeminormedRing ๐•œ] [AddCommGroup E] [SMul ๐•œ E] {x : E} {y : E} {r : โ„} (p : Seminorm ๐•œ E) :
                    x +แตฅ p.ball y r = p.ball (x +แตฅ y) r

                    The image of a ball under addition with a singleton is another ball.

                    theorem Seminorm.vadd_closedBall {๐•œ : Type u_3} {E : Type u_7} [SeminormedRing ๐•œ] [AddCommGroup E] [SMul ๐•œ E] {x : E} {y : E} {r : โ„} (p : Seminorm ๐•œ E) :
                    x +แตฅ p.closedBall y r = p.closedBall (x +แตฅ y) r

                    The image of a closed ball under addition with a singleton is another closed ball.

                    theorem Seminorm.ball_comp {๐•œ : Type u_3} {๐•œโ‚‚ : Type u_4} {E : Type u_7} {Eโ‚‚ : Type u_8} [SeminormedRing ๐•œ] [AddCommGroup E] [Module ๐•œ E] [SeminormedRing ๐•œโ‚‚] [AddCommGroup Eโ‚‚] [Module ๐•œโ‚‚ Eโ‚‚] {ฯƒโ‚โ‚‚ : ๐•œ โ†’+* ๐•œโ‚‚} [RingHomIsometric ฯƒโ‚โ‚‚] (p : Seminorm ๐•œโ‚‚ Eโ‚‚) (f : E โ†’โ‚›โ‚—[ฯƒโ‚โ‚‚] Eโ‚‚) (x : E) (r : โ„) :
                    (p.comp f).ball x r = โ‡‘f โปยน' p.ball (f x) r
                    theorem Seminorm.closedBall_comp {๐•œ : Type u_3} {๐•œโ‚‚ : Type u_4} {E : Type u_7} {Eโ‚‚ : Type u_8} [SeminormedRing ๐•œ] [AddCommGroup E] [Module ๐•œ E] [SeminormedRing ๐•œโ‚‚] [AddCommGroup Eโ‚‚] [Module ๐•œโ‚‚ Eโ‚‚] {ฯƒโ‚โ‚‚ : ๐•œ โ†’+* ๐•œโ‚‚} [RingHomIsometric ฯƒโ‚โ‚‚] (p : Seminorm ๐•œโ‚‚ Eโ‚‚) (f : E โ†’โ‚›โ‚—[ฯƒโ‚โ‚‚] Eโ‚‚) (x : E) (r : โ„) :
                    (p.comp f).closedBall x r = โ‡‘f โปยน' p.closedBall (f x) r
                    theorem Seminorm.preimage_metric_ball {๐•œ : Type u_3} {E : Type u_7} [SeminormedRing ๐•œ] [AddCommGroup E] [Module ๐•œ E] (p : Seminorm ๐•œ E) {r : โ„} :
                    โ‡‘p โปยน' Metric.ball 0 r = {x : E | p x < r}
                    theorem Seminorm.preimage_metric_closedBall {๐•œ : Type u_3} {E : Type u_7} [SeminormedRing ๐•œ] [AddCommGroup E] [Module ๐•œ E] (p : Seminorm ๐•œ E) {r : โ„} :
                    โ‡‘p โปยน' Metric.closedBall 0 r = {x : E | p x โ‰ค r}
                    theorem Seminorm.ball_zero_eq_preimage_ball {๐•œ : Type u_3} {E : Type u_7} [SeminormedRing ๐•œ] [AddCommGroup E] [Module ๐•œ E] (p : Seminorm ๐•œ E) {r : โ„} :
                    p.ball 0 r = โ‡‘p โปยน' Metric.ball 0 r
                    theorem Seminorm.closedBall_zero_eq_preimage_closedBall {๐•œ : Type u_3} {E : Type u_7} [SeminormedRing ๐•œ] [AddCommGroup E] [Module ๐•œ E] (p : Seminorm ๐•œ E) {r : โ„} :
                    p.closedBall 0 r = โ‡‘p โปยน' Metric.closedBall 0 r
                    @[simp]
                    theorem Seminorm.ball_bot {๐•œ : Type u_3} {E : Type u_7} [SeminormedRing ๐•œ] [AddCommGroup E] [Module ๐•œ E] {r : โ„} (x : E) (hr : 0 < r) :
                    โŠฅ.ball x r = Set.univ
                    @[simp]
                    theorem Seminorm.closedBall_bot {๐•œ : Type u_3} {E : Type u_7} [SeminormedRing ๐•œ] [AddCommGroup E] [Module ๐•œ E] {r : โ„} (x : E) (hr : 0 < r) :
                    โŠฅ.closedBall x r = Set.univ
                    theorem Seminorm.balanced_ball_zero {๐•œ : Type u_3} {E : Type u_7} [SeminormedRing ๐•œ] [AddCommGroup E] [Module ๐•œ E] (p : Seminorm ๐•œ E) (r : โ„) :
                    Balanced ๐•œ (p.ball 0 r)

                    Seminorm-balls at the origin are balanced.

                    theorem Seminorm.balanced_closedBall_zero {๐•œ : Type u_3} {E : Type u_7} [SeminormedRing ๐•œ] [AddCommGroup E] [Module ๐•œ E] (p : Seminorm ๐•œ E) (r : โ„) :
                    Balanced ๐•œ (p.closedBall 0 r)

                    Closed seminorm-balls at the origin are balanced.

                    theorem Seminorm.ball_finset_sup_eq_iInter {๐•œ : Type u_3} {E : Type u_7} {ฮน : Type u_12} [SeminormedRing ๐•œ] [AddCommGroup E] [Module ๐•œ E] (p : ฮน โ†’ Seminorm ๐•œ E) (s : Finset ฮน) (x : E) {r : โ„} (hr : 0 < r) :
                    (s.sup p).ball x r = โ‹‚ i โˆˆ s, (p i).ball x r
                    theorem Seminorm.closedBall_finset_sup_eq_iInter {๐•œ : Type u_3} {E : Type u_7} {ฮน : Type u_12} [SeminormedRing ๐•œ] [AddCommGroup E] [Module ๐•œ E] (p : ฮน โ†’ Seminorm ๐•œ E) (s : Finset ฮน) (x : E) {r : โ„} (hr : 0 โ‰ค r) :
                    (s.sup p).closedBall x r = โ‹‚ i โˆˆ s, (p i).closedBall x r
                    theorem Seminorm.ball_finset_sup {๐•œ : Type u_3} {E : Type u_7} {ฮน : Type u_12} [SeminormedRing ๐•œ] [AddCommGroup E] [Module ๐•œ E] (p : ฮน โ†’ Seminorm ๐•œ E) (s : Finset ฮน) (x : E) {r : โ„} (hr : 0 < r) :
                    (s.sup p).ball x r = s.inf fun (i : ฮน) => (p i).ball x r
                    theorem Seminorm.closedBall_finset_sup {๐•œ : Type u_3} {E : Type u_7} {ฮน : Type u_12} [SeminormedRing ๐•œ] [AddCommGroup E] [Module ๐•œ E] (p : ฮน โ†’ Seminorm ๐•œ E) (s : Finset ฮน) (x : E) {r : โ„} (hr : 0 โ‰ค r) :
                    (s.sup p).closedBall x r = s.inf fun (i : ฮน) => (p i).closedBall x r
                    @[simp]
                    theorem Seminorm.ball_eq_emptyset {๐•œ : Type u_3} {E : Type u_7} [SeminormedRing ๐•œ] [AddCommGroup E] [Module ๐•œ E] (p : Seminorm ๐•œ E) {x : E} {r : โ„} (hr : r โ‰ค 0) :
                    p.ball x r = โˆ…
                    @[simp]
                    theorem Seminorm.closedBall_eq_emptyset {๐•œ : Type u_3} {E : Type u_7} [SeminormedRing ๐•œ] [AddCommGroup E] [Module ๐•œ E] (p : Seminorm ๐•œ E) {x : E} {r : โ„} (hr : r < 0) :
                    p.closedBall x r = โˆ…
                    theorem Seminorm.closedBall_smul_ball {๐•œ : Type u_3} {E : Type u_7} [SeminormedRing ๐•œ] [AddCommGroup E] [Module ๐•œ E] (p : Seminorm ๐•œ E) {rโ‚ : โ„} (hrโ‚ : rโ‚ โ‰  0) (rโ‚‚ : โ„) :
                    Metric.closedBall 0 rโ‚ โ€ข p.ball 0 rโ‚‚ โŠ† p.ball 0 (rโ‚ * rโ‚‚)
                    theorem Seminorm.ball_smul_closedBall {๐•œ : Type u_3} {E : Type u_7} [SeminormedRing ๐•œ] [AddCommGroup E] [Module ๐•œ E] (p : Seminorm ๐•œ E) (rโ‚ : โ„) {rโ‚‚ : โ„} (hrโ‚‚ : rโ‚‚ โ‰  0) :
                    Metric.ball 0 rโ‚ โ€ข p.closedBall 0 rโ‚‚ โŠ† p.ball 0 (rโ‚ * rโ‚‚)
                    theorem Seminorm.ball_smul_ball {๐•œ : Type u_3} {E : Type u_7} [SeminormedRing ๐•œ] [AddCommGroup E] [Module ๐•œ E] (p : Seminorm ๐•œ E) (rโ‚ : โ„) (rโ‚‚ : โ„) :
                    Metric.ball 0 rโ‚ โ€ข p.ball 0 rโ‚‚ โŠ† p.ball 0 (rโ‚ * rโ‚‚)
                    theorem Seminorm.closedBall_smul_closedBall {๐•œ : Type u_3} {E : Type u_7} [SeminormedRing ๐•œ] [AddCommGroup E] [Module ๐•œ E] (p : Seminorm ๐•œ E) (rโ‚ : โ„) (rโ‚‚ : โ„) :
                    Metric.closedBall 0 rโ‚ โ€ข p.closedBall 0 rโ‚‚ โŠ† p.closedBall 0 (rโ‚ * rโ‚‚)
                    theorem Seminorm.neg_mem_ball_zero {๐•œ : Type u_3} {E : Type u_7} [SeminormedRing ๐•œ] [AddCommGroup E] [Module ๐•œ E] (p : Seminorm ๐•œ E) {r : โ„} {x : E} :
                    -x โˆˆ p.ball 0 r โ†” x โˆˆ p.ball 0 r
                    @[simp]
                    theorem Seminorm.neg_ball {๐•œ : Type u_3} {E : Type u_7} [SeminormedRing ๐•œ] [AddCommGroup E] [Module ๐•œ E] (p : Seminorm ๐•œ E) (r : โ„) (x : E) :
                    -p.ball x r = p.ball (-x) r
                    theorem Seminorm.closedBall_iSup {๐•œ : Type u_3} {E : Type u_7} [NormedField ๐•œ] [AddCommGroup E] [Module ๐•œ E] {ฮน : Sort u_13} {p : ฮน โ†’ Seminorm ๐•œ E} (hp : BddAbove (Set.range p)) (e : E) {r : โ„} (hr : 0 < r) :
                    (โจ† (i : ฮน), p i).closedBall e r = โ‹‚ (i : ฮน), (p i).closedBall e r
                    theorem Seminorm.ball_norm_mul_subset {๐•œ : Type u_3} {E : Type u_7} [NormedField ๐•œ] [AddCommGroup E] [Module ๐•œ E] {p : Seminorm ๐•œ E} {k : ๐•œ} {r : โ„} :
                    p.ball 0 (โ€–kโ€– * r) โŠ† k โ€ข p.ball 0 r
                    theorem Seminorm.smul_ball_zero {๐•œ : Type u_3} {E : Type u_7} [NormedField ๐•œ] [AddCommGroup E] [Module ๐•œ E] {p : Seminorm ๐•œ E} {k : ๐•œ} {r : โ„} (hk : k โ‰  0) :
                    k โ€ข p.ball 0 r = p.ball 0 (โ€–kโ€– * r)
                    theorem Seminorm.smul_closedBall_subset {๐•œ : Type u_3} {E : Type u_7} [NormedField ๐•œ] [AddCommGroup E] [Module ๐•œ E] {p : Seminorm ๐•œ E} {k : ๐•œ} {r : โ„} :
                    k โ€ข p.closedBall 0 r โŠ† p.closedBall 0 (โ€–kโ€– * r)
                    theorem Seminorm.smul_closedBall_zero {๐•œ : Type u_3} {E : Type u_7} [NormedField ๐•œ] [AddCommGroup E] [Module ๐•œ E] {p : Seminorm ๐•œ E} {k : ๐•œ} {r : โ„} (hk : 0 < โ€–kโ€–) :
                    k โ€ข p.closedBall 0 r = p.closedBall 0 (โ€–kโ€– * r)
                    theorem Seminorm.ball_zero_absorbs_ball_zero {๐•œ : Type u_3} {E : Type u_7} [NormedField ๐•œ] [AddCommGroup E] [Module ๐•œ E] (p : Seminorm ๐•œ E) {rโ‚ : โ„} {rโ‚‚ : โ„} (hrโ‚ : 0 < rโ‚) :
                    Absorbs ๐•œ (p.ball 0 rโ‚) (p.ball 0 rโ‚‚)
                    theorem Seminorm.absorbent_ball_zero {๐•œ : Type u_3} {E : Type u_7} [NormedField ๐•œ] [AddCommGroup E] [Module ๐•œ E] (p : Seminorm ๐•œ E) {r : โ„} (hr : 0 < r) :
                    Absorbent ๐•œ (p.ball 0 r)

                    Seminorm-balls at the origin are absorbent.

                    theorem Seminorm.absorbent_closedBall_zero {๐•œ : Type u_3} {E : Type u_7} [NormedField ๐•œ] [AddCommGroup E] [Module ๐•œ E] (p : Seminorm ๐•œ E) {r : โ„} (hr : 0 < r) :
                    Absorbent ๐•œ (p.closedBall 0 r)

                    Closed seminorm-balls at the origin are absorbent.

                    theorem Seminorm.absorbent_ball {๐•œ : Type u_3} {E : Type u_7} [NormedField ๐•œ] [AddCommGroup E] [Module ๐•œ E] (p : Seminorm ๐•œ E) {r : โ„} {x : E} (hpr : p x < r) :
                    Absorbent ๐•œ (p.ball x r)

                    Seminorm-balls containing the origin are absorbent.

                    theorem Seminorm.absorbent_closedBall {๐•œ : Type u_3} {E : Type u_7} [NormedField ๐•œ] [AddCommGroup E] [Module ๐•œ E] (p : Seminorm ๐•œ E) {r : โ„} {x : E} (hpr : p x < r) :
                    Absorbent ๐•œ (p.closedBall x r)

                    Seminorm-balls containing the origin are absorbent.

                    @[simp]
                    theorem Seminorm.smul_ball_preimage {๐•œ : Type u_3} {E : Type u_7} [NormedField ๐•œ] [AddCommGroup E] [Module ๐•œ E] (p : Seminorm ๐•œ E) (y : E) (r : โ„) (a : ๐•œ) (ha : a โ‰  0) :
                    (fun (x : E) => a โ€ข x) โปยน' p.ball y r = p.ball (aโปยน โ€ข y) (r / โ€–aโ€–)
                    theorem Seminorm.convexOn {๐•œ : Type u_3} {E : Type u_7} [NormedField ๐•œ] [AddCommGroup E] [NormedSpace โ„ ๐•œ] [Module ๐•œ E] [SMul โ„ E] [IsScalarTower โ„ ๐•œ E] (p : Seminorm ๐•œ E) :
                    ConvexOn โ„ Set.univ โ‡‘p

                    A seminorm is convex. Also see convexOn_norm.

                    theorem Seminorm.convex_ball {๐•œ : Type u_3} {E : Type u_7} [NormedField ๐•œ] [AddCommGroup E] [NormedSpace โ„ ๐•œ] [Module ๐•œ E] [Module โ„ E] [IsScalarTower โ„ ๐•œ E] (p : Seminorm ๐•œ E) (x : E) (r : โ„) :
                    Convex โ„ (p.ball x r)

                    Seminorm-balls are convex.

                    theorem Seminorm.convex_closedBall {๐•œ : Type u_3} {E : Type u_7} [NormedField ๐•œ] [AddCommGroup E] [NormedSpace โ„ ๐•œ] [Module ๐•œ E] [Module โ„ E] [IsScalarTower โ„ ๐•œ E] (p : Seminorm ๐•œ E) (x : E) (r : โ„) :
                    Convex โ„ (p.closedBall x r)

                    Closed seminorm-balls are convex.

                    def Seminorm.restrictScalars (๐•œ : Type u_3) {E : Type u_7} {๐•œ' : Type u_13} [NormedField ๐•œ] [SeminormedRing ๐•œ'] [NormedAlgebra ๐•œ ๐•œ'] [NormOneClass ๐•œ'] [AddCommGroup E] [Module ๐•œ' E] [SMul ๐•œ E] [IsScalarTower ๐•œ ๐•œ' E] (p : Seminorm ๐•œ' E) :
                    Seminorm ๐•œ E

                    Reinterpret a seminorm over a field ๐•œ' as a seminorm over a smaller field ๐•œ. This will typically be used with RCLike ๐•œ' and ๐•œ = โ„.

                    Equations
                    Instances For
                      @[simp]
                      theorem Seminorm.coe_restrictScalars (๐•œ : Type u_3) {E : Type u_7} {๐•œ' : Type u_13} [NormedField ๐•œ] [SeminormedRing ๐•œ'] [NormedAlgebra ๐•œ ๐•œ'] [NormOneClass ๐•œ'] [AddCommGroup E] [Module ๐•œ' E] [SMul ๐•œ E] [IsScalarTower ๐•œ ๐•œ' E] (p : Seminorm ๐•œ' E) :
                      โ‡‘(Seminorm.restrictScalars ๐•œ p) = โ‡‘p
                      @[simp]
                      theorem Seminorm.restrictScalars_ball (๐•œ : Type u_3) {E : Type u_7} {๐•œ' : Type u_13} [NormedField ๐•œ] [SeminormedRing ๐•œ'] [NormedAlgebra ๐•œ ๐•œ'] [NormOneClass ๐•œ'] [AddCommGroup E] [Module ๐•œ' E] [SMul ๐•œ E] [IsScalarTower ๐•œ ๐•œ' E] (p : Seminorm ๐•œ' E) :
                      (Seminorm.restrictScalars ๐•œ p).ball = p.ball
                      @[simp]
                      theorem Seminorm.restrictScalars_closedBall (๐•œ : Type u_3) {E : Type u_7} {๐•œ' : Type u_13} [NormedField ๐•œ] [SeminormedRing ๐•œ'] [NormedAlgebra ๐•œ ๐•œ'] [NormOneClass ๐•œ'] [AddCommGroup E] [Module ๐•œ' E] [SMul ๐•œ E] [IsScalarTower ๐•œ ๐•œ' E] (p : Seminorm ๐•œ' E) :
                      (Seminorm.restrictScalars ๐•œ p).closedBall = p.closedBall

                      Continuity criterions for seminorms #

                      theorem Seminorm.continuousAt_zero_of_forall' {๐• : Type u_6} {E : Type u_7} [SeminormedRing ๐•] [AddCommGroup E] [Module ๐• E] [TopologicalSpace E] {p : Seminorm ๐• E} (hp : โˆ€ r > 0, p.closedBall 0 r โˆˆ nhds 0) :
                      ContinuousAt (โ‡‘p) 0

                      A seminorm is continuous at 0 if p.closedBall 0 r โˆˆ ๐“ 0 for all r > 0. Over a NontriviallyNormedField it is actually enough to check that this is true for some r, see Seminorm.continuousAt_zero'.

                      theorem Seminorm.continuousAt_zero' {๐•œ : Type u_3} {E : Type u_7} [NontriviallyNormedField ๐•œ] [AddCommGroup E] [Module ๐•œ E] [TopologicalSpace E] [ContinuousConstSMul ๐•œ E] {p : Seminorm ๐•œ E} {r : โ„} (hp : p.closedBall 0 r โˆˆ nhds 0) :
                      ContinuousAt (โ‡‘p) 0
                      theorem Seminorm.continuousAt_zero_of_forall {๐• : Type u_6} {E : Type u_7} [SeminormedRing ๐•] [AddCommGroup E] [Module ๐• E] [TopologicalSpace E] {p : Seminorm ๐• E} (hp : โˆ€ r > 0, p.ball 0 r โˆˆ nhds 0) :
                      ContinuousAt (โ‡‘p) 0

                      A seminorm is continuous at 0 if p.ball 0 r โˆˆ ๐“ 0 for all r > 0. Over a NontriviallyNormedField it is actually enough to check that this is true for some r, see Seminorm.continuousAt_zero'.

                      theorem Seminorm.continuousAt_zero {๐•œ : Type u_3} {E : Type u_7} [NontriviallyNormedField ๐•œ] [AddCommGroup E] [Module ๐•œ E] [TopologicalSpace E] [ContinuousConstSMul ๐•œ E] {p : Seminorm ๐•œ E} {r : โ„} (hp : p.ball 0 r โˆˆ nhds 0) :
                      ContinuousAt (โ‡‘p) 0
                      theorem Seminorm.uniformContinuous_of_continuousAt_zero {๐• : Type u_6} {E : Type u_7} [SeminormedRing ๐•] [AddCommGroup E] [Module ๐• E] [UniformSpace E] [UniformAddGroup E] {p : Seminorm ๐• E} (hp : ContinuousAt (โ‡‘p) 0) :
                      theorem Seminorm.continuous_of_continuousAt_zero {๐• : Type u_6} {E : Type u_7} [SeminormedRing ๐•] [AddCommGroup E] [Module ๐• E] [TopologicalSpace E] [TopologicalAddGroup E] {p : Seminorm ๐• E} (hp : ContinuousAt (โ‡‘p) 0) :
                      Continuous โ‡‘p
                      theorem Seminorm.uniformContinuous_of_forall {๐• : Type u_6} {E : Type u_7} [SeminormedRing ๐•] [AddCommGroup E] [Module ๐• E] [UniformSpace E] [UniformAddGroup E] {p : Seminorm ๐• E} (hp : โˆ€ r > 0, p.ball 0 r โˆˆ nhds 0) :

                      A seminorm is uniformly continuous if p.ball 0 r โˆˆ ๐“ 0 for all r > 0. Over a NontriviallyNormedField it is actually enough to check that this is true for some r, see Seminorm.uniformContinuous.

                      theorem Seminorm.uniformContinuous {๐•œ : Type u_3} {E : Type u_7} [NontriviallyNormedField ๐•œ] [AddCommGroup E] [Module ๐•œ E] [UniformSpace E] [UniformAddGroup E] [ContinuousConstSMul ๐•œ E] {p : Seminorm ๐•œ E} {r : โ„} (hp : p.ball 0 r โˆˆ nhds 0) :
                      theorem Seminorm.uniformContinuous_of_forall' {๐• : Type u_6} {E : Type u_7} [SeminormedRing ๐•] [AddCommGroup E] [Module ๐• E] [UniformSpace E] [UniformAddGroup E] {p : Seminorm ๐• E} (hp : โˆ€ r > 0, p.closedBall 0 r โˆˆ nhds 0) :

                      A seminorm is uniformly continuous if p.closedBall 0 r โˆˆ ๐“ 0 for all r > 0. Over a NontriviallyNormedField it is actually enough to check that this is true for some r, see Seminorm.uniformContinuous'.

                      theorem Seminorm.uniformContinuous' {๐•œ : Type u_3} {E : Type u_7} [NontriviallyNormedField ๐•œ] [AddCommGroup E] [Module ๐•œ E] [UniformSpace E] [UniformAddGroup E] [ContinuousConstSMul ๐•œ E] {p : Seminorm ๐•œ E} {r : โ„} (hp : p.closedBall 0 r โˆˆ nhds 0) :
                      theorem Seminorm.continuous_of_forall {๐• : Type u_6} {E : Type u_7} [SeminormedRing ๐•] [AddCommGroup E] [Module ๐• E] [TopologicalSpace E] [TopologicalAddGroup E] {p : Seminorm ๐• E} (hp : โˆ€ r > 0, p.ball 0 r โˆˆ nhds 0) :
                      Continuous โ‡‘p

                      A seminorm is continuous if p.ball 0 r โˆˆ ๐“ 0 for all r > 0. Over a NontriviallyNormedField it is actually enough to check that this is true for some r, see Seminorm.continuous.

                      theorem Seminorm.continuous {๐•œ : Type u_3} {E : Type u_7} [NontriviallyNormedField ๐•œ] [AddCommGroup E] [Module ๐•œ E] [TopologicalSpace E] [TopologicalAddGroup E] [ContinuousConstSMul ๐•œ E] {p : Seminorm ๐•œ E} {r : โ„} (hp : p.ball 0 r โˆˆ nhds 0) :
                      Continuous โ‡‘p
                      theorem Seminorm.continuous_of_forall' {๐• : Type u_6} {E : Type u_7} [SeminormedRing ๐•] [AddCommGroup E] [Module ๐• E] [TopologicalSpace E] [TopologicalAddGroup E] {p : Seminorm ๐• E} (hp : โˆ€ r > 0, p.closedBall 0 r โˆˆ nhds 0) :
                      Continuous โ‡‘p

                      A seminorm is continuous if p.closedBall 0 r โˆˆ ๐“ 0 for all r > 0. Over a NontriviallyNormedField it is actually enough to check that this is true for some r, see Seminorm.continuous'.

                      theorem Seminorm.continuous' {๐•œ : Type u_3} {E : Type u_7} [NontriviallyNormedField ๐•œ] [AddCommGroup E] [Module ๐•œ E] [TopologicalSpace E] [TopologicalAddGroup E] [ContinuousConstSMul ๐•œ E] {p : Seminorm ๐•œ E} {r : โ„} (hp : p.closedBall 0 r โˆˆ nhds 0) :
                      Continuous โ‡‘p
                      theorem Seminorm.continuous_of_le {๐• : Type u_6} {E : Type u_7} [SeminormedRing ๐•] [AddCommGroup E] [Module ๐• E] [TopologicalSpace E] [TopologicalAddGroup E] {p : Seminorm ๐• E} {q : Seminorm ๐• E} (hq : Continuous โ‡‘q) (hpq : p โ‰ค q) :
                      Continuous โ‡‘p
                      theorem Seminorm.ball_mem_nhds {๐• : Type u_6} {E : Type u_7} [SeminormedRing ๐•] [AddCommGroup E] [Module ๐• E] [TopologicalSpace E] {p : Seminorm ๐• E} (hp : Continuous โ‡‘p) {r : โ„} (hr : 0 < r) :
                      p.ball 0 r โˆˆ nhds 0
                      theorem Seminorm.uniformSpace_eq_of_hasBasis {๐•œ : Type u_3} {E : Type u_7} [NontriviallyNormedField ๐•œ] [AddCommGroup E] [Module ๐•œ E] {ฮน : Sort u_13} [UniformSpace E] [UniformAddGroup E] [ContinuousConstSMul ๐•œ E] {p' : ฮน โ†’ Prop} {s : ฮน โ†’ Set E} (p : Seminorm ๐•œ E) (hb : (nhds 0).HasBasis p' s) (hโ‚ : โˆƒ (r : โ„), p.closedBall 0 r โˆˆ nhds 0) (hโ‚‚ : โˆ€ (i : ฮน), p' i โ†’ โˆƒ r > 0, p.ball 0 r โŠ† s i) :
                      instโœยฒ = PseudoMetricSpace.toUniformSpace
                      theorem Seminorm.uniformity_eq_of_hasBasis {๐•œ : Type u_3} {E : Type u_7} [NontriviallyNormedField ๐•œ] [AddCommGroup E] [Module ๐•œ E] {ฮน : Sort u_13} [UniformSpace E] [UniformAddGroup E] [ContinuousConstSMul ๐•œ E] {p' : ฮน โ†’ Prop} {s : ฮน โ†’ Set E} (p : Seminorm ๐•œ E) (hb : (nhds 0).HasBasis p' s) (hโ‚ : โˆƒ (r : โ„), p.closedBall 0 r โˆˆ nhds 0) (hโ‚‚ : โˆ€ (i : ฮน), p' i โ†’ โˆƒ r > 0, p.ball 0 r โŠ† s i) :
                      uniformity E = โจ… (r : โ„), โจ… (_ : r > 0), Filter.principal {x : E ร— E | p (x.1 - x.2) < r}
                      theorem Seminorm.rescale_to_shell_zpow {๐•œ : Type u_3} {E : Type u_7} [NormedField ๐•œ] [AddCommGroup E] [Module ๐•œ E] (p : Seminorm ๐•œ E) {c : ๐•œ} (hc : 1 < โ€–cโ€–) {ฮต : โ„} (ฮตpos : 0 < ฮต) {x : E} (hx : p x โ‰  0) :

                      Let p be a seminorm on a vector space over a NormedField. If there is a scalar c with โ€–cโ€–>1, then any x such that p x โ‰  0 can be moved by scalar multiplication to any p-shell of width โ€–cโ€–. Also recap information on the value of p on the rescaling element that shows up in applications.

                      theorem Seminorm.rescale_to_shell {๐•œ : Type u_3} {E : Type u_7} [NormedField ๐•œ] [AddCommGroup E] [Module ๐•œ E] (p : Seminorm ๐•œ E) {c : ๐•œ} (hc : 1 < โ€–cโ€–) {ฮต : โ„} (ฮตpos : 0 < ฮต) {x : E} (hx : p x โ‰  0) :

                      Let p be a seminorm on a vector space over a NormedField. If there is a scalar c with โ€–cโ€–>1, then any x such that p x โ‰  0 can be moved by scalar multiplication to any p-shell of width โ€–cโ€–. Also recap information on the value of p on the rescaling element that shows up in applications.

                      theorem Seminorm.bound_of_shell {๐•œ : Type u_3} {E : Type u_7} [NormedField ๐•œ] [AddCommGroup E] [Module ๐•œ E] (p : Seminorm ๐•œ E) (q : Seminorm ๐•œ E) {ฮต : โ„} {C : โ„} (ฮต_pos : 0 < ฮต) {c : ๐•œ} (hc : 1 < โ€–cโ€–) (hf : โˆ€ (x : E), ฮต / โ€–cโ€– โ‰ค p x โ†’ p x < ฮต โ†’ q x โ‰ค C * p x) {x : E} (hx : p x โ‰  0) :
                      q x โ‰ค C * p x

                      Let p and q be two seminorms on a vector space over a NontriviallyNormedField. If we have q x โ‰ค C * p x on some shell of the form {x | ฮต/โ€–cโ€– โ‰ค p x < ฮต} (where ฮต > 0 and โ€–cโ€– > 1), then we also have q x โ‰ค C * p x for all x such that p x โ‰  0.

                      theorem Seminorm.bound_of_shell_smul {๐•œ : Type u_3} {E : Type u_7} [NormedField ๐•œ] [AddCommGroup E] [Module ๐•œ E] (p : Seminorm ๐•œ E) (q : Seminorm ๐•œ E) {ฮต : โ„} {C : NNReal} (ฮต_pos : 0 < ฮต) {c : ๐•œ} (hc : 1 < โ€–cโ€–) (hf : โˆ€ (x : E), ฮต / โ€–cโ€– โ‰ค p x โ†’ p x < ฮต โ†’ q x โ‰ค (C โ€ข p) x) {x : E} (hx : p x โ‰  0) :
                      q x โ‰ค (C โ€ข p) x

                      A version of Seminorm.bound_of_shell expressed using pointwise scalar multiplication of seminorms.

                      theorem Seminorm.bound_of_shell_sup {๐•œ : Type u_3} {E : Type u_7} {ฮน : Type u_12} [NormedField ๐•œ] [AddCommGroup E] [Module ๐•œ E] (p : ฮน โ†’ Seminorm ๐•œ E) (s : Finset ฮน) (q : Seminorm ๐•œ E) {ฮต : โ„} {C : NNReal} (ฮต_pos : 0 < ฮต) {c : ๐•œ} (hc : 1 < โ€–cโ€–) (hf : โˆ€ (x : E), (โˆ€ i โˆˆ s, (p i) x < ฮต) โ†’ โˆ€ j โˆˆ s, ฮต / โ€–cโ€– โ‰ค (p j) x โ†’ q x โ‰ค (C โ€ข p j) x) {x : E} (hx : โˆƒ j โˆˆ s, (p j) x โ‰  0) :
                      q x โ‰ค (C โ€ข s.sup p) x
                      theorem Seminorm.bddAbove_of_absorbent {๐•œ : Type u_3} {E : Type u_7} [NontriviallyNormedField ๐•œ] [AddCommGroup E] [Module ๐•œ E] {ฮน : Sort u_13} {p : ฮน โ†’ Seminorm ๐•œ E} {s : Set E} (hs : Absorbent ๐•œ s) (h : โˆ€ x โˆˆ s, BddAbove (Set.range fun (x_1 : ฮน) => (p x_1) x)) :

                      Let p i be a family of seminorms on E. Let s be an absorbent set in ๐•œ. If all seminorms are uniformly bounded at every point of s, then they are bounded in the space of seminorms.

                      The norm as a seminorm #

                      def normSeminorm (๐•œ : Type u_3) (E : Type u_7) [NormedField ๐•œ] [SeminormedAddCommGroup E] [NormedSpace ๐•œ E] :
                      Seminorm ๐•œ E

                      The norm of a seminormed group as a seminorm.

                      Equations
                      Instances For
                        @[simp]
                        theorem coe_normSeminorm (๐•œ : Type u_3) (E : Type u_7) [NormedField ๐•œ] [SeminormedAddCommGroup E] [NormedSpace ๐•œ E] :
                        โ‡‘(normSeminorm ๐•œ E) = norm
                        @[simp]
                        theorem ball_normSeminorm (๐•œ : Type u_3) (E : Type u_7) [NormedField ๐•œ] [SeminormedAddCommGroup E] [NormedSpace ๐•œ E] :
                        (normSeminorm ๐•œ E).ball = Metric.ball
                        theorem absorbent_ball_zero {๐•œ : Type u_3} {E : Type u_7} [NormedField ๐•œ] [SeminormedAddCommGroup E] [NormedSpace ๐•œ E] {r : โ„} (hr : 0 < r) :
                        Absorbent ๐•œ (Metric.ball 0 r)

                        Balls at the origin are absorbent.

                        theorem absorbent_ball {๐•œ : Type u_3} {E : Type u_7} [NormedField ๐•œ] [SeminormedAddCommGroup E] [NormedSpace ๐•œ E] {r : โ„} {x : E} (hx : โ€–xโ€– < r) :
                        Absorbent ๐•œ (Metric.ball x r)

                        Balls containing the origin are absorbent.

                        theorem balanced_ball_zero {๐•œ : Type u_3} {E : Type u_7} [NormedField ๐•œ] [SeminormedAddCommGroup E] [NormedSpace ๐•œ E] {r : โ„} :
                        Balanced ๐•œ (Metric.ball 0 r)

                        Balls at the origin are balanced.

                        theorem rescale_to_shell_semi_normed_zpow {๐•œ : Type u_3} {E : Type u_7} [NormedField ๐•œ] [SeminormedAddCommGroup E] [NormedSpace ๐•œ E] {c : ๐•œ} (hc : 1 < โ€–cโ€–) {ฮต : โ„} (ฮตpos : 0 < ฮต) {x : E} (hx : โ€–xโ€– โ‰  0) :

                        If there is a scalar c with โ€–cโ€–>1, then any element with nonzero norm can be moved by scalar multiplication to any shell of width โ€–cโ€–. Also recap information on the norm of the rescaling element that shows up in applications.

                        theorem rescale_to_shell_semi_normed {๐•œ : Type u_3} {E : Type u_7} [NormedField ๐•œ] [SeminormedAddCommGroup E] [NormedSpace ๐•œ E] {c : ๐•œ} (hc : 1 < โ€–cโ€–) {ฮต : โ„} (ฮตpos : 0 < ฮต) {x : E} (hx : โ€–xโ€– โ‰  0) :

                        If there is a scalar c with โ€–cโ€–>1, then any element with nonzero norm can be moved by scalar multiplication to any shell of width โ€–cโ€–. Also recap information on the norm of the rescaling element that shows up in applications.

                        theorem rescale_to_shell_zpow {๐•œ : Type u_3} {F : Type u_10} [NormedField ๐•œ] [NormedAddCommGroup F] [NormedSpace ๐•œ F] {c : ๐•œ} (hc : 1 < โ€–cโ€–) {ฮต : โ„} (ฮตpos : 0 < ฮต) {x : F} (hx : x โ‰  0) :
                        theorem rescale_to_shell {๐•œ : Type u_3} {F : Type u_10} [NormedField ๐•œ] [NormedAddCommGroup F] [NormedSpace ๐•œ F] {c : ๐•œ} (hc : 1 < โ€–cโ€–) {ฮต : โ„} (ฮตpos : 0 < ฮต) {x : F} (hx : x โ‰  0) :

                        If there is a scalar c with โ€–cโ€–>1, then any element can be moved by scalar multiplication to any shell of width โ€–cโ€–. Also recap information on the norm of the rescaling element that shows up in applications.