Documentation

Mathlib.Analysis.Normed.Module.Basic

Normed spaces #

In this file we define (semi)normed spaces and algebras. We also prove some theorems about these definitions.

class NormedSpace (๐•œ : Type u_6) (E : Type u_7) [NormedField ๐•œ] [SeminormedAddCommGroup E] extends Module ๐•œ E :
Type (max u_6 u_7)

A normed space over a normed field is a vector space endowed with a norm which satisfies the equality โ€–c โ€ข xโ€– = โ€–cโ€– โ€–xโ€–. We require only โ€–c โ€ข xโ€– โ‰ค โ€–cโ€– โ€–xโ€– in the definition, then prove โ€–c โ€ข xโ€– = โ€–cโ€– โ€–xโ€– in norm_smul.

Note that since this requires SeminormedAddCommGroup and not NormedAddCommGroup, this typeclass can be used for "semi normed spaces" too, just as Module can be used for "semi modules".

Instances
    @[instance 100]
    instance NormedSpace.boundedSMul {๐•œ : Type u_1} {E : Type u_3} [NormedField ๐•œ] [SeminormedAddCommGroup E] [NormedSpace ๐•œ E] :
    BoundedSMul ๐•œ E
    instance NormedField.toNormedSpace {๐•œ : Type u_1} [NormedField ๐•œ] :
    NormedSpace ๐•œ ๐•œ
    Equations
    instance NormedField.to_boundedSMul {๐•œ : Type u_1} [NormedField ๐•œ] :
    BoundedSMul ๐•œ ๐•œ
    theorem norm_zsmul (๐•œ : Type u_1) {E : Type u_3} [NormedField ๐•œ] [SeminormedAddCommGroup E] [NormedSpace ๐•œ E] (n : โ„ค) (x : E) :
    theorem eventually_nhds_norm_smul_sub_lt {๐•œ : Type u_1} {E : Type u_3} [NormedField ๐•œ] [SeminormedAddCommGroup E] [NormedSpace ๐•œ E] (c : ๐•œ) (x : E) {ฮต : โ„} (h : 0 < ฮต) :
    โˆ€แถ  (y : E) in nhds x, โ€–c โ€ข (y - x)โ€– < ฮต
    theorem Filter.Tendsto.zero_smul_isBoundedUnder_le {๐•œ : Type u_1} {E : Type u_3} {ฮฑ : Type u_5} [NormedField ๐•œ] [SeminormedAddCommGroup E] [NormedSpace ๐•œ E] {f : ฮฑ โ†’ ๐•œ} {g : ฮฑ โ†’ E} {l : Filter ฮฑ} (hf : Filter.Tendsto f l (nhds 0)) (hg : Filter.IsBoundedUnder (fun (x1 x2 : โ„) => x1 โ‰ค x2) l (norm โˆ˜ g)) :
    Filter.Tendsto (fun (x : ฮฑ) => f x โ€ข g x) l (nhds 0)
    theorem Filter.IsBoundedUnder.smul_tendsto_zero {๐•œ : Type u_1} {E : Type u_3} {ฮฑ : Type u_5} [NormedField ๐•œ] [SeminormedAddCommGroup E] [NormedSpace ๐•œ E] {f : ฮฑ โ†’ ๐•œ} {g : ฮฑ โ†’ E} {l : Filter ฮฑ} (hf : Filter.IsBoundedUnder (fun (x1 x2 : โ„) => x1 โ‰ค x2) l (norm โˆ˜ f)) (hg : Filter.Tendsto g l (nhds 0)) :
    Filter.Tendsto (fun (x : ฮฑ) => f x โ€ข g x) l (nhds 0)
    instance ULift.normedSpace {๐•œ : Type u_1} {E : Type u_3} [NormedField ๐•œ] [SeminormedAddCommGroup E] [NormedSpace ๐•œ E] :
    Equations
    instance Prod.normedSpace {๐•œ : Type u_1} {E : Type u_3} {F : Type u_4} [NormedField ๐•œ] [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [NormedSpace ๐•œ E] [NormedSpace ๐•œ F] :
    NormedSpace ๐•œ (E ร— F)

    The product of two normed spaces is a normed space, with the sup norm.

    Equations
    instance Pi.normedSpace {๐•œ : Type u_1} [NormedField ๐•œ] {ฮน : Type u_6} {E : ฮน โ†’ Type u_7} [Fintype ฮน] [(i : ฮน) โ†’ SeminormedAddCommGroup (E i)] [(i : ฮน) โ†’ NormedSpace ๐•œ (E i)] :
    NormedSpace ๐•œ ((i : ฮน) โ†’ E i)

    The product of finitely many normed spaces is a normed space, with the sup norm.

    Equations
    instance SeparationQuotient.instNormedSpace {๐•œ : Type u_1} {E : Type u_3} [NormedField ๐•œ] [SeminormedAddCommGroup E] [NormedSpace ๐•œ E] :
    Equations
    instance MulOpposite.instNormedSpace {๐•œ : Type u_1} {E : Type u_3} [NormedField ๐•œ] [SeminormedAddCommGroup E] [NormedSpace ๐•œ E] :
    Equations
    instance Submodule.normedSpace {๐•œ : Type u_6} {R : Type u_7} [SMul ๐•œ R] [NormedField ๐•œ] [Ring R] {E : Type u_8} [SeminormedAddCommGroup E] [NormedSpace ๐•œ E] [Module R E] [IsScalarTower ๐•œ R E] (s : Submodule R E) :
    NormedSpace ๐•œ โ†ฅs

    A subspace of a normed space is also a normed space, with the restriction of the norm.

    Equations
    @[instance 75]
    instance SubmoduleClass.toNormedSpace {S : Type u_6} {๐•œ : Type u_7} {R : Type u_8} {E : Type u_9} [SMul ๐•œ R] [NormedField ๐•œ] [Ring R] [SeminormedAddCommGroup E] [NormedSpace ๐•œ E] [Module R E] [IsScalarTower ๐•œ R E] [SetLike S E] [AddSubgroupClass S E] [SMulMemClass S R E] (s : S) :
    NormedSpace ๐•œ โ†ฅs
    Equations
    @[reducible, inline]
    abbrev NormedSpace.induced {F : Type u_6} (๐•œ : Type u_7) (E : Type u_8) (G : Type u_9) [NormedField ๐•œ] [AddCommGroup E] [Module ๐•œ E] [SeminormedAddCommGroup G] [NormedSpace ๐•œ G] [FunLike F E G] [LinearMapClass F ๐•œ E G] (f : F) :
    NormedSpace ๐•œ E

    A linear map from a Module to a NormedSpace induces a NormedSpace structure on the domain, using the SeminormedAddCommGroup.induced norm.

    See note [reducible non-instances]

    Equations
    Instances For
      @[instance 100]
      instance NormedSpace.toModule' {๐•œ : Type u_1} {F : Type u_4} [NormedField ๐•œ] [NormedAddCommGroup F] [NormedSpace ๐•œ F] :
      Module ๐•œ F

      While this may appear identical to NormedSpace.toModule, it contains an implicit argument involving NormedAddCommGroup.toSeminormedAddCommGroup that typeclass inference has trouble inferring.

      Specifically, the following instance cannot be found without this NormedSpace.toModule':

      example
        (๐•œ ฮน : Type*) (E : ฮน โ†’ Type*)
        [NormedField ๐•œ] [ฮ  i, NormedAddCommGroup (E i)] [ฮ  i, NormedSpace ๐•œ (E i)] :
        ฮ  i, Module ๐•œ (E i) := by infer_instance
      

      This Zulip thread gives some more context.

      Equations
      • NormedSpace.toModule' = NormedSpace.toModule
      theorem NormedSpace.exists_lt_norm (๐•œ : Type u_1) (E : Type u_3) [NontriviallyNormedField ๐•œ] [NormedAddCommGroup E] [NormedSpace ๐•œ E] [Nontrivial E] (c : โ„) :
      โˆƒ (x : E), c < โ€–xโ€–

      If E is a nontrivial normed space over a nontrivially normed field ๐•œ, then E is unbounded: for any c : โ„, there exists a vector x : E with norm strictly greater than c.

      theorem NormedSpace.unbounded_univ (๐•œ : Type u_1) (E : Type u_3) [NontriviallyNormedField ๐•œ] [NormedAddCommGroup E] [NormedSpace ๐•œ E] [Nontrivial E] :
      theorem NormedSpace.cobounded_neBot (๐•œ : Type u_1) (E : Type u_3) [NontriviallyNormedField ๐•œ] [NormedAddCommGroup E] [NormedSpace ๐•œ E] [Nontrivial E] :
      @[instance 100]
      instance NontriviallyNormedField.cobounded_neBot (๐•œ : Type u_1) [NontriviallyNormedField ๐•œ] :
      (Bornology.cobounded ๐•œ).NeBot
      @[instance 80]
      instance NontriviallyNormedField.infinite (๐•œ : Type u_1) [NontriviallyNormedField ๐•œ] :
      Infinite ๐•œ
      theorem NormedSpace.noncompactSpace (๐•œ : Type u_1) (E : Type u_3) [NormedField ๐•œ] [Infinite ๐•œ] [NormedAddCommGroup E] [Nontrivial E] [NormedSpace ๐•œ E] :

      A normed vector space over an infinite normed field is a noncompact space. This cannot be an instance because in order to apply it, Lean would have to search for NormedSpace ๐•œ E with unknown ๐•œ. We register this as an instance in two cases: ๐•œ = E and ๐•œ = โ„.

      @[instance 100]
      instance NormedField.noncompactSpace (๐•œ : Type u_1) [NormedField ๐•œ] [Infinite ๐•œ] :
      NoncompactSpace ๐•œ
      class NormedAlgebra (๐•œ : Type u_6) (๐•œ' : Type u_7) [NormedField ๐•œ] [SeminormedRing ๐•œ'] extends Algebra ๐•œ ๐•œ' :
      Type (max u_6 u_7)

      A normed algebra ๐•œ' over ๐•œ is normed module that is also an algebra.

      See the implementation notes for Algebra for a discussion about non-unital algebras. Following the strategy there, a non-unital normed algebra can be written as:

      variable [NormedField ๐•œ] [NonUnitalSeminormedRing ๐•œ']
      variable [NormedSpace ๐•œ ๐•œ'] [SMulCommClass ๐•œ ๐•œ' ๐•œ'] [IsScalarTower ๐•œ ๐•œ' ๐•œ']
      
      • smul : ๐•œ โ†’ ๐•œ' โ†’ ๐•œ'
      • toFun : ๐•œ โ†’ ๐•œ'
      • map_one' : (โ†‘โ†‘Algebra.toRingHom).toFun 1 = 1
      • map_mul' (x y : ๐•œ) : (โ†‘โ†‘Algebra.toRingHom).toFun (x * y) = (โ†‘โ†‘Algebra.toRingHom).toFun x * (โ†‘โ†‘Algebra.toRingHom).toFun y
      • map_zero' : (โ†‘โ†‘Algebra.toRingHom).toFun 0 = 0
      • map_add' (x y : ๐•œ) : (โ†‘โ†‘Algebra.toRingHom).toFun (x + y) = (โ†‘โ†‘Algebra.toRingHom).toFun x + (โ†‘โ†‘Algebra.toRingHom).toFun y
      • commutes' (r : ๐•œ) (x : ๐•œ') : Algebra.toRingHom r * x = x * Algebra.toRingHom r
      • smul_def' (r : ๐•œ) (x : ๐•œ') : r โ€ข x = Algebra.toRingHom r * x
      • norm_smul_le (r : ๐•œ) (x : ๐•œ') : โ€–r โ€ข xโ€– โ‰ค โ€–rโ€– * โ€–xโ€–

        A normed algebra ๐•œ' over ๐•œ is normed module that is also an algebra.

        See the implementation notes for Algebra for a discussion about non-unital algebras. Following the strategy there, a non-unital normed algebra can be written as:

        variable [NormedField ๐•œ] [NonUnitalSeminormedRing ๐•œ']
        variable [NormedSpace ๐•œ ๐•œ'] [SMulCommClass ๐•œ ๐•œ' ๐•œ'] [IsScalarTower ๐•œ ๐•œ' ๐•œ']
        
      Instances
        @[instance 100]
        instance NormedAlgebra.toNormedSpace {๐•œ : Type u_1} (๐•œ' : Type u_2) [NormedField ๐•œ] [SeminormedRing ๐•œ'] [NormedAlgebra ๐•œ ๐•œ'] :
        NormedSpace ๐•œ ๐•œ'
        Equations
        @[instance 100]
        instance NormedAlgebra.toNormedSpace' {๐•œ : Type u_1} [NormedField ๐•œ] {๐•œ' : Type u_6} [NormedRing ๐•œ'] [NormedAlgebra ๐•œ ๐•œ'] :
        NormedSpace ๐•œ ๐•œ'

        While this may appear identical to NormedAlgebra.toNormedSpace, it contains an implicit argument involving NormedRing.toSeminormedRing that typeclass inference has trouble inferring.

        Specifically, the following instance cannot be found without this NormedSpace.toModule':

        example
          (๐•œ ฮน : Type*) (E : ฮน โ†’ Type*)
          [NormedField ๐•œ] [ฮ  i, NormedRing (E i)] [ฮ  i, NormedAlgebra ๐•œ (E i)] :
          ฮ  i, Module ๐•œ (E i) := by infer_instance
        

        See NormedSpace.toModule' for a similar situation.

        Equations
        • NormedAlgebra.toNormedSpace' = inferInstance
        theorem norm_algebraMap {๐•œ : Type u_1} (๐•œ' : Type u_2) [NormedField ๐•œ] [SeminormedRing ๐•œ'] [NormedAlgebra ๐•œ ๐•œ'] (x : ๐•œ) :
        theorem nnnorm_algebraMap {๐•œ : Type u_1} (๐•œ' : Type u_2) [NormedField ๐•œ] [SeminormedRing ๐•œ'] [NormedAlgebra ๐•œ ๐•œ'] (x : ๐•œ) :
        theorem dist_algebraMap {๐•œ : Type u_1} (๐•œ' : Type u_2) [NormedField ๐•œ] [SeminormedRing ๐•œ'] [NormedAlgebra ๐•œ ๐•œ'] (x y : ๐•œ) :
        dist ((algebraMap ๐•œ ๐•œ') x) ((algebraMap ๐•œ ๐•œ') y) = dist x y * โ€–1โ€–
        @[simp]
        theorem norm_algebraMap' {๐•œ : Type u_1} (๐•œ' : Type u_2) [NormedField ๐•œ] [SeminormedRing ๐•œ'] [NormedAlgebra ๐•œ ๐•œ'] [NormOneClass ๐•œ'] (x : ๐•œ) :
        โ€–(algebraMap ๐•œ ๐•œ') xโ€– = โ€–xโ€–

        This is a simpler version of norm_algebraMap when โ€–1โ€– = 1 in ๐•œ'.

        @[simp]
        theorem nnnorm_algebraMap' {๐•œ : Type u_1} (๐•œ' : Type u_2) [NormedField ๐•œ] [SeminormedRing ๐•œ'] [NormedAlgebra ๐•œ ๐•œ'] [NormOneClass ๐•œ'] (x : ๐•œ) :

        This is a simpler version of nnnorm_algebraMap when โ€–1โ€– = 1 in ๐•œ'.

        @[simp]
        theorem dist_algebraMap' {๐•œ : Type u_1} (๐•œ' : Type u_2) [NormedField ๐•œ] [SeminormedRing ๐•œ'] [NormedAlgebra ๐•œ ๐•œ'] [NormOneClass ๐•œ'] (x y : ๐•œ) :
        dist ((algebraMap ๐•œ ๐•œ') x) ((algebraMap ๐•œ ๐•œ') y) = dist x y

        This is a simpler version of dist_algebraMap when โ€–1โ€– = 1 in ๐•œ'.

        @[simp]
        theorem norm_algebraMap_nnreal (๐•œ' : Type u_2) [SeminormedRing ๐•œ'] [NormOneClass ๐•œ'] [NormedAlgebra โ„ ๐•œ'] (x : NNReal) :
        โ€–(algebraMap NNReal ๐•œ') xโ€– = โ†‘x
        @[simp]
        theorem nnnorm_algebraMap_nnreal (๐•œ' : Type u_2) [SeminormedRing ๐•œ'] [NormOneClass ๐•œ'] [NormedAlgebra โ„ ๐•œ'] (x : NNReal) :
        theorem algebraMap_isometry (๐•œ : Type u_1) (๐•œ' : Type u_2) [NormedField ๐•œ] [SeminormedRing ๐•œ'] [NormedAlgebra ๐•œ ๐•œ'] [NormOneClass ๐•œ'] :
        Isometry โ‡‘(algebraMap ๐•œ ๐•œ')

        In a normed algebra, the inclusion of the base field in the extended field is an isometry.

        instance NormedAlgebra.id (๐•œ : Type u_1) [NormedField ๐•œ] :
        NormedAlgebra ๐•œ ๐•œ
        Equations
        instance normedAlgebraRat {๐•œ : Type u_6} [NormedDivisionRing ๐•œ] [CharZero ๐•œ] [NormedAlgebra โ„ ๐•œ] :

        Any normed characteristic-zero division ring that is a normed algebra over the reals is also a normed algebra over the rationals.

        Phrased another way, if ๐•œ is a normed algebra over the reals, then AlgebraRat respects that norm.

        Equations
        instance PUnit.normedAlgebra (๐•œ : Type u_1) [NormedField ๐•œ] :
        Equations
        instance instNormedAlgebraULift (๐•œ : Type u_1) (๐•œ' : Type u_2) [NormedField ๐•œ] [SeminormedRing ๐•œ'] [NormedAlgebra ๐•œ ๐•œ'] :
        NormedAlgebra ๐•œ (ULift.{u_6, u_2} ๐•œ')
        Equations
        instance Prod.normedAlgebra (๐•œ : Type u_1) [NormedField ๐•œ] {E : Type u_6} {F : Type u_7} [SeminormedRing E] [SeminormedRing F] [NormedAlgebra ๐•œ E] [NormedAlgebra ๐•œ F] :
        NormedAlgebra ๐•œ (E ร— F)

        The product of two normed algebras is a normed algebra, with the sup norm.

        Equations
        instance Pi.normedAlgebra (๐•œ : Type u_1) [NormedField ๐•œ] {ฮน : Type u_6} {E : ฮน โ†’ Type u_7} [Fintype ฮน] [(i : ฮน) โ†’ SeminormedRing (E i)] [(i : ฮน) โ†’ NormedAlgebra ๐•œ (E i)] :
        NormedAlgebra ๐•œ ((i : ฮน) โ†’ E i)

        The product of finitely many normed algebras is a normed algebra, with the sup norm.

        Equations
        instance SeparationQuotient.instNormedAlgebra (๐•œ : Type u_1) {E : Type u_3} [NormedField ๐•œ] [SeminormedRing E] [NormedAlgebra ๐•œ E] :
        Equations
        instance MulOpposite.instNormedAlgebra (๐•œ : Type u_1) [NormedField ๐•œ] {E : Type u_6} [SeminormedRing E] [NormedAlgebra ๐•œ E] :
        Equations
        @[reducible, inline]
        abbrev NormedAlgebra.induced {F : Type u_6} (๐•œ : Type u_7) (R : Type u_8) (S : Type u_9) [NormedField ๐•œ] [Ring R] [Algebra ๐•œ R] [SeminormedRing S] [NormedAlgebra ๐•œ S] [FunLike F R S] [NonUnitalAlgHomClass F ๐•œ R S] (f : F) :
        NormedAlgebra ๐•œ R

        A non-unital algebra homomorphism from an Algebra to a NormedAlgebra induces a NormedAlgebra structure on the domain, using the SeminormedRing.induced norm.

        See note [reducible non-instances]

        Equations
        Instances For
          instance Subalgebra.toNormedAlgebra {๐•œ : Type u_6} {A : Type u_7} [SeminormedRing A] [NormedField ๐•œ] [NormedAlgebra ๐•œ A] (S : Subalgebra ๐•œ A) :
          NormedAlgebra ๐•œ โ†ฅS
          Equations
          @[instance 75]
          instance SubalgebraClass.toNormedAlgebra {S : Type u_6} {๐•œ : Type u_7} {E : Type u_8} [NormedField ๐•œ] [SeminormedRing E] [NormedAlgebra ๐•œ E] [SetLike S E] [SubringClass S E] [SMulMemClass S ๐•œ E] (s : S) :
          NormedAlgebra ๐•œ โ†ฅs
          Equations
          instance instSeminormedAddCommGroupRestrictScalars {๐•œ : Type u_1} {๐•œ' : Type u_2} {E : Type u_3} [I : SeminormedAddCommGroup E] :
          SeminormedAddCommGroup (RestrictScalars ๐•œ ๐•œ' E)
          Equations
          • instSeminormedAddCommGroupRestrictScalars = I
          instance instNormedAddCommGroupRestrictScalars {๐•œ : Type u_1} {๐•œ' : Type u_2} {E : Type u_3} [I : NormedAddCommGroup E] :
          NormedAddCommGroup (RestrictScalars ๐•œ ๐•œ' E)
          Equations
          • instNormedAddCommGroupRestrictScalars = I
          instance instNonUnitalSeminormedRingRestrictScalars {๐•œ : Type u_1} {๐•œ' : Type u_2} {E : Type u_3} [I : NonUnitalSeminormedRing E] :
          NonUnitalSeminormedRing (RestrictScalars ๐•œ ๐•œ' E)
          Equations
          • instNonUnitalSeminormedRingRestrictScalars = I
          instance instNonUnitalNormedRingRestrictScalars {๐•œ : Type u_1} {๐•œ' : Type u_2} {E : Type u_3} [I : NonUnitalNormedRing E] :
          NonUnitalNormedRing (RestrictScalars ๐•œ ๐•œ' E)
          Equations
          • instNonUnitalNormedRingRestrictScalars = I
          instance instSeminormedRingRestrictScalars {๐•œ : Type u_1} {๐•œ' : Type u_2} {E : Type u_3} [I : SeminormedRing E] :
          SeminormedRing (RestrictScalars ๐•œ ๐•œ' E)
          Equations
          • instSeminormedRingRestrictScalars = I
          instance instNormedRingRestrictScalars {๐•œ : Type u_1} {๐•œ' : Type u_2} {E : Type u_3} [I : NormedRing E] :
          NormedRing (RestrictScalars ๐•œ ๐•œ' E)
          Equations
          • instNormedRingRestrictScalars = I
          instance instNonUnitalSeminormedCommRingRestrictScalars {๐•œ : Type u_1} {๐•œ' : Type u_2} {E : Type u_3} [I : NonUnitalSeminormedCommRing E] :
          Equations
          • instNonUnitalSeminormedCommRingRestrictScalars = I
          instance instNonUnitalNormedCommRingRestrictScalars {๐•œ : Type u_1} {๐•œ' : Type u_2} {E : Type u_3} [I : NonUnitalNormedCommRing E] :
          NonUnitalNormedCommRing (RestrictScalars ๐•œ ๐•œ' E)
          Equations
          • instNonUnitalNormedCommRingRestrictScalars = I
          instance instSeminormedCommRingRestrictScalars {๐•œ : Type u_1} {๐•œ' : Type u_2} {E : Type u_3} [I : SeminormedCommRing E] :
          SeminormedCommRing (RestrictScalars ๐•œ ๐•œ' E)
          Equations
          • instSeminormedCommRingRestrictScalars = I
          instance instNormedCommRingRestrictScalars {๐•œ : Type u_1} {๐•œ' : Type u_2} {E : Type u_3} [I : NormedCommRing E] :
          NormedCommRing (RestrictScalars ๐•œ ๐•œ' E)
          Equations
          • instNormedCommRingRestrictScalars = I
          instance RestrictScalars.normedSpace (๐•œ : Type u_1) (๐•œ' : Type u_2) (E : Type u_3) [NormedField ๐•œ] [NormedField ๐•œ'] [NormedAlgebra ๐•œ ๐•œ'] [SeminormedAddCommGroup E] [NormedSpace ๐•œ' E] :
          NormedSpace ๐•œ (RestrictScalars ๐•œ ๐•œ' E)

          If E is a normed space over ๐•œ' and ๐•œ is a normed algebra over ๐•œ', then RestrictScalars.module is additionally a NormedSpace.

          Equations
          def Module.RestrictScalars.normedSpaceOrig {๐•œ : Type u_6} {๐•œ' : Type u_7} {E : Type u_8} [NormedField ๐•œ'] [SeminormedAddCommGroup E] [I : NormedSpace ๐•œ' E] :
          NormedSpace ๐•œ' (RestrictScalars ๐•œ ๐•œ' E)

          The action of the original normed_field on RestrictScalars ๐•œ ๐•œ' E. This is not an instance as it would be contrary to the purpose of RestrictScalars.

          Equations
          • Module.RestrictScalars.normedSpaceOrig = I
          Instances For
            @[reducible, inline]
            abbrev NormedSpace.restrictScalars (๐•œ : Type u_1) (๐•œ' : Type u_2) (E : Type u_3) [NormedField ๐•œ] [NormedField ๐•œ'] [NormedAlgebra ๐•œ ๐•œ'] [SeminormedAddCommGroup E] [NormedSpace ๐•œ' E] :
            NormedSpace ๐•œ E

            Warning: This declaration should be used judiciously. Please consider using IsScalarTower and/or RestrictScalars ๐•œ ๐•œ' E instead.

            This definition allows the RestrictScalars.normedSpace instance to be put directly on E rather on RestrictScalars ๐•œ ๐•œ' E. This would be a very bad instance; both because ๐•œ' cannot be inferred, and because it is likely to create instance diamonds.

            See Note [reducible non-instances].

            Equations
            Instances For
              instance RestrictScalars.normedAlgebra (๐•œ : Type u_1) (๐•œ' : Type u_2) (E : Type u_3) [NormedField ๐•œ] [NormedField ๐•œ'] [NormedAlgebra ๐•œ ๐•œ'] [SeminormedRing E] [NormedAlgebra ๐•œ' E] :
              NormedAlgebra ๐•œ (RestrictScalars ๐•œ ๐•œ' E)

              If E is a normed algebra over ๐•œ' and ๐•œ is a normed algebra over ๐•œ', then RestrictScalars.module is additionally a NormedAlgebra.

              Equations
              def Module.RestrictScalars.normedAlgebraOrig {๐•œ : Type u_6} {๐•œ' : Type u_7} {E : Type u_8} [NormedField ๐•œ'] [SeminormedRing E] [I : NormedAlgebra ๐•œ' E] :
              NormedAlgebra ๐•œ' (RestrictScalars ๐•œ ๐•œ' E)

              The action of the original normed_field on RestrictScalars ๐•œ ๐•œ' E. This is not an instance as it would be contrary to the purpose of RestrictScalars.

              Equations
              • Module.RestrictScalars.normedAlgebraOrig = I
              Instances For
                @[reducible, inline]
                abbrev NormedAlgebra.restrictScalars (๐•œ : Type u_1) (๐•œ' : Type u_2) (E : Type u_3) [NormedField ๐•œ] [NormedField ๐•œ'] [NormedAlgebra ๐•œ ๐•œ'] [SeminormedRing E] [NormedAlgebra ๐•œ' E] :
                NormedAlgebra ๐•œ E

                Warning: This declaration should be used judiciously. Please consider using IsScalarTower and/or RestrictScalars ๐•œ ๐•œ' E instead.

                This definition allows the RestrictScalars.normedAlgebra instance to be put directly on E rather on RestrictScalars ๐•œ ๐•œ' E. This would be a very bad instance; both because ๐•œ' cannot be inferred, and because it is likely to create instance diamonds.

                See Note [reducible non-instances].

                Equations
                Instances For

                  Structures for constructing new normed spaces #

                  This section contains tools meant for constructing new normed spaces. These allow one to easily construct all the relevant instances (distances measures, etc) while proving only a minimal set of axioms. Furthermore, tools are provided to add a norm structure to a type that already has a preexisting uniformity or bornology: in such cases, it is necessary to keep the preexisting instances, while ensuring that the norm induces the same uniformity/bornology.

                  structure SeminormedAddCommGroup.Core (๐•œ : Type u_6) (E : Type u_7) [NormedField ๐•œ] [AddCommGroup E] [Norm E] [Module ๐•œ E] :

                  A structure encapsulating minimal axioms needed to defined a seminormed vector space, as found in textbooks. This is meant to be used to easily define SeminormedAddCommGroup E instances from scratch on a type with no preexisting distance or topology.

                  Instances For
                    @[reducible, inline]
                    abbrev PseudoMetricSpace.ofSeminormedAddCommGroupCore {๐•œ : Type u_6} {E : Type u_7} [NormedField ๐•œ] [AddCommGroup E] [Norm E] [Module ๐•œ E] (core : SeminormedAddCommGroup.Core ๐•œ E) :

                    Produces a PseudoMetricSpace E instance from a SeminormedAddCommGroup.Core. Note that if this is used to define an instance on a type, it also provides a new uniformity and topology on the type. See note [reducible non-instances].

                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      @[reducible, inline]
                      abbrev PseudoEMetricSpace.ofSeminormedAddCommGroupCore {๐•œ : Type u_6} {E : Type u_7} [NormedField ๐•œ] [AddCommGroup E] [Norm E] [Module ๐•œ E] (core : SeminormedAddCommGroup.Core ๐•œ E) :

                      Produces a PseudoEMetricSpace E instance from a SeminormedAddCommGroup.Core. Note that if this is used to define an instance on a type, it also provides a new uniformity and topology on the type. See note [reducible non-instances].

                      Equations
                      Instances For
                        @[reducible, inline]
                        abbrev PseudoMetricSpace.ofSeminormedAddCommGroupCoreReplaceUniformity {๐•œ : Type u_6} {E : Type u_7} [NormedField ๐•œ] [AddCommGroup E] [Norm E] [Module ๐•œ E] [U : UniformSpace E] (core : SeminormedAddCommGroup.Core ๐•œ E) (H : uniformity E = uniformity E) :

                        Produces a PseudoEMetricSpace E instance from a SeminormedAddCommGroup.Core on a type that already has an existing uniform space structure. This requires a proof that the uniformity induced by the norm is equal to the preexisting uniformity. See note [reducible non-instances].

                        Equations
                        Instances For
                          @[reducible, inline]
                          abbrev PseudoMetricSpace.ofSeminormedAddCommGroupCoreReplaceAll {๐•œ : Type u_6} {E : Type u_7} [NormedField ๐•œ] [AddCommGroup E] [Norm E] [Module ๐•œ E] [U : UniformSpace E] [B : Bornology E] (core : SeminormedAddCommGroup.Core ๐•œ E) (HU : uniformity E = uniformity E) (HB : โˆ€ (s : Set E), Bornology.IsBounded s โ†” Bornology.IsBounded s) :

                          Produces a PseudoEMetricSpace E instance from a SeminormedAddCommGroup.Core on a type that already has a preexisting uniform space structure and a preexisting bornology. This requires proofs that the uniformity induced by the norm is equal to the preexisting uniformity, and likewise for the bornology. See note [reducible non-instances].

                          Equations
                          Instances For
                            @[reducible, inline]
                            abbrev SeminormedAddCommGroup.ofCore {๐•œ : Type u_6} {E : Type u_7} [NormedField ๐•œ] [AddCommGroup E] [Norm E] [Module ๐•œ E] (core : SeminormedAddCommGroup.Core ๐•œ E) :

                            Produces a SeminormedAddCommGroup E instance from a SeminormedAddCommGroup.Core. Note that if this is used to define an instance on a type, it also provides a new distance measure from the norm. it must therefore not be used on a type with a preexisting distance measure or topology. See note [reducible non-instances].

                            Equations
                            Instances For
                              @[reducible, inline]
                              abbrev SeminormedAddCommGroup.ofCoreReplaceUniformity {๐•œ : Type u_6} {E : Type u_7} [NormedField ๐•œ] [AddCommGroup E] [Norm E] [Module ๐•œ E] [U : UniformSpace E] (core : SeminormedAddCommGroup.Core ๐•œ E) (H : uniformity E = uniformity E) :

                              Produces a SeminormedAddCommGroup E instance from a SeminormedAddCommGroup.Core on a type that already has an existing uniform space structure. This requires a proof that the uniformity induced by the norm is equal to the preexisting uniformity. See note [reducible non-instances].

                              Equations
                              Instances For
                                @[reducible, inline]
                                abbrev SeminormedAddCommGroup.ofCoreReplaceAll {๐•œ : Type u_6} {E : Type u_7} [NormedField ๐•œ] [AddCommGroup E] [Norm E] [Module ๐•œ E] [U : UniformSpace E] [B : Bornology E] (core : SeminormedAddCommGroup.Core ๐•œ E) (HU : uniformity E = uniformity E) (HB : โˆ€ (s : Set E), Bornology.IsBounded s โ†” Bornology.IsBounded s) :

                                Produces a SeminormedAddCommGroup E instance from a SeminormedAddCommGroup.Core on a type that already has a preexisting uniform space structure and a preexisting bornology. This requires proofs that the uniformity induced by the norm is equal to the preexisting uniformity, and likewise for the bornology. See note [reducible non-instances].

                                Equations
                                Instances For
                                  structure NormedSpace.Core (๐•œ : Type u_6) (E : Type u_7) [NormedField ๐•œ] [AddCommGroup E] [Module ๐•œ E] [Norm E] extends SeminormedAddCommGroup.Core ๐•œ E :

                                  A structure encapsulating minimal axioms needed to defined a normed vector space, as found in textbooks. This is meant to be used to easily define NormedAddCommGroup E and NormedSpace E instances from scratch on a type with no preexisting distance or topology.

                                  Instances For
                                    @[reducible, inline]
                                    abbrev NormedAddCommGroup.ofCore {๐•œ : Type u_6} {E : Type u_7} [NormedField ๐•œ] [AddCommGroup E] [Module ๐•œ E] [Norm E] (core : NormedSpace.Core ๐•œ E) :

                                    Produces a NormedAddCommGroup E instance from a NormedSpace.Core. Note that if this is used to define an instance on a type, it also provides a new distance measure from the norm. it must therefore not be used on a type with a preexisting distance measure. See note [reducible non-instances].

                                    Equations
                                    Instances For
                                      @[reducible, inline]
                                      abbrev NormedAddCommGroup.ofCoreReplaceUniformity {๐•œ : Type u_6} {E : Type u_7} [NormedField ๐•œ] [AddCommGroup E] [Module ๐•œ E] [Norm E] [U : UniformSpace E] (core : NormedSpace.Core ๐•œ E) (H : uniformity E = uniformity E) :

                                      Produces a NormedAddCommGroup E instance from a NormedAddCommGroup.Core on a type that already has an existing uniform space structure. This requires a proof that the uniformity induced by the norm is equal to the preexisting uniformity. See note [reducible non-instances].

                                      Equations
                                      Instances For
                                        @[reducible, inline]
                                        abbrev NormedAddCommGroup.ofCoreReplaceAll {๐•œ : Type u_6} {E : Type u_7} [NormedField ๐•œ] [AddCommGroup E] [Module ๐•œ E] [Norm E] [U : UniformSpace E] [B : Bornology E] (core : NormedSpace.Core ๐•œ E) (HU : uniformity E = uniformity E) (HB : โˆ€ (s : Set E), Bornology.IsBounded s โ†” Bornology.IsBounded s) :

                                        Produces a NormedAddCommGroup E instance from a NormedAddCommGroup.Core on a type that already has a preexisting uniform space structure and a preexisting bornology. This requires proofs that the uniformity induced by the norm is equal to the preexisting uniformity, and likewise for the bornology. See note [reducible non-instances].

                                        Equations
                                        Instances For
                                          @[reducible, inline]
                                          abbrev NormedSpace.ofCore {๐•œ : Type u_8} {E : Type u_9} [NormedField ๐•œ] [SeminormedAddCommGroup E] [Module ๐•œ E] (core : NormedSpace.Core ๐•œ E) :
                                          NormedSpace ๐•œ E

                                          Produces a NormedSpace ๐•œ E instance from a NormedSpace.Core. This is meant to be used on types where the NormedAddCommGroup E instance has also been defined using core. See note [reducible non-instances].

                                          Equations
                                          Instances For