Documentation

Mathlib.Analysis.Normed.Module.Completion

Normed space structure on the completion of a normed space #

If E is a normed space over 𝕜, then so is UniformSpace.Completion E. In this file we provide necessary instances and define UniformSpace.Completion.toComplₗᵢ - coercion E → UniformSpace.Completion E as a bundled linear isometry.

We also show that if A is a normed algebra over 𝕜, then so is UniformSpace.Completion A.

TODO: Generalise the results here from the concrete completion to any AbstractCompletion.

source
instance UniformSpace.Completion.instNormedSpace (𝕜 : Type u_1) (E : Type u_2) [NormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] :
NormedSpace 𝕜 (UniformSpace.Completion E)
Equations
source
def UniformSpace.Completion.toComplₗᵢ {𝕜 : Type u_1} {E : Type u_2} [Semiring 𝕜] [SeminormedAddCommGroup E] [Module 𝕜 E] [UniformContinuousConstSMul 𝕜 E] :
E →ₗᵢ[𝕜] UniformSpace.Completion E

Embedding of a normed space to its completion as a linear isometry.

Equations
  • UniformSpace.Completion.toComplₗᵢ = { toFun := ↑E, map_add' := ⋯, map_smul' := ⋯, norm_map' := ⋯ }
Instances For
    source
    @[simp]
    theorem UniformSpace.Completion.coe_toComplₗᵢ {𝕜 : Type u_1} {E : Type u_2} [Semiring 𝕜] [SeminormedAddCommGroup E] [Module 𝕜 E] [UniformContinuousConstSMul 𝕜 E] :
    ⇑UniformSpace.Completion.toComplₗᵢ = ↑E
    source
    def UniformSpace.Completion.toComplL {𝕜 : Type u_1} {E : Type u_2} [Semiring 𝕜] [SeminormedAddCommGroup E] [Module 𝕜 E] [UniformContinuousConstSMul 𝕜 E] :
    E →L[𝕜] UniformSpace.Completion E

    Embedding of a normed space to its completion as a continuous linear map.

    Equations
    • UniformSpace.Completion.toComplL = UniformSpace.Completion.toComplₗᵢ.toContinuousLinearMap
    Instances For
      source
      @[simp]
      theorem UniformSpace.Completion.coe_toComplL {𝕜 : Type u_1} {E : Type u_2} [Semiring 𝕜] [SeminormedAddCommGroup E] [Module 𝕜 E] [UniformContinuousConstSMul 𝕜 E] :
      ⇑UniformSpace.Completion.toComplL = ↑E
      source
      @[simp]
      theorem UniformSpace.Completion.norm_toComplL {𝕜 : Type u_3} {E : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [Nontrivial E] :
      ‖UniformSpace.Completion.toComplL‖ = 1
      source
      instance UniformSpace.Completion.instNormedRing (A : Type u_3) [SeminormedRing A] :
      NormedRing (UniformSpace.Completion A)
      Equations
      source
      instance UniformSpace.Completion.instNormedCommRing (A : Type u_3) [SeminormedCommRing A] :
      NormedCommRing (UniformSpace.Completion A)
      Equations
      source
      instance UniformSpace.Completion.instNormedAlgebra (𝕜 : Type u_1) (A : Type u_3) [NormedField 𝕜] [SeminormedCommRing A] [NormedAlgebra 𝕜 A] :
      NormedAlgebra 𝕜 (UniformSpace.Completion A)
      Equations
      source
      instance UniformSpace.Completion.instNormedFieldOfCompletableTopField (A : Type u_3) [NormedField A] [CompletableTopField A] :
      NormedField (UniformSpace.Completion A)
      Equations