Documentation

Mathlib.Analysis.NormedSpace.ContinuousLinearMap

Constructions of continuous linear maps between (semi-)normed spaces #

A fundamental fact about (semi-)linear maps between normed spaces over sensible fields is that continuity and boundedness are equivalent conditions. That is, for normed spaces E, F, a LinearMap f : E →ₛₗ[σ] F is the coercion of some ContinuousLinearMap f' : E →SL[σ] F, if and only if there exists a bound C such that for all x, ‖f x‖ ≤ C * ‖x‖.

We prove one direction in this file: LinearMap.mkContinuous, boundedness implies continuity. The other direction, ContinuousLinearMap.bound, is deferred to a later file, where the strong operator topology on E →SL[σ] F is available, because it is natural to use ContinuousLinearMap.bound to define a norm ⨆ x, ‖f x‖ / ‖x‖ on E →SL[σ] F and to show that this is compatible with the strong operator topology.

This file also contains several corollaries of LinearMap.mkContinuous: other "easy" constructions of continuous linear maps between normed spaces.

This file is meant to be lightweight (it is imported by much of the analysis library); think twice before adding imports!

General constructions #

def LinearMap.mkContinuous {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_3} {F : Type u_4} [Ring 𝕜] [Ring 𝕜₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [Module 𝕜 E] [Module 𝕜₂ F] {σ : 𝕜 →+* 𝕜₂} (f : E →ₛₗ[σ] F) (C : ) (h : ∀ (x : E), f x C * x) :
E →SL[σ] F

Construct a continuous linear map from a linear map and a bound on this linear map. The fact that the norm of the continuous linear map is then controlled is given in LinearMap.mkContinuous_norm_le.

Equations
Instances For
    def LinearMap.mkContinuousOfExistsBound {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_3} {F : Type u_4} [Ring 𝕜] [Ring 𝕜₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [Module 𝕜 E] [Module 𝕜₂ F] {σ : 𝕜 →+* 𝕜₂} (f : E →ₛₗ[σ] F) (h : C, ∀ (x : E), f x C * x) :
    E →SL[σ] F

    Construct a continuous linear map from a linear map and the existence of a bound on this linear map. If you have an explicit bound, use LinearMap.mkContinuous instead, as a norm estimate will follow automatically in LinearMap.mkContinuous_norm_le.

    Equations
    Instances For
      theorem continuous_of_linear_of_boundₛₗ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_3} {F : Type u_4} [Ring 𝕜] [Ring 𝕜₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [Module 𝕜 E] [Module 𝕜₂ F] {σ : 𝕜 →+* 𝕜₂} {f : EF} (h_add : ∀ (x y : E), f (x + y) = f x + f y) (h_smul : ∀ (c : 𝕜) (x : E), f (c x) = σ c f x) {C : } (h_bound : ∀ (x : E), f x C * x) :
      theorem continuous_of_linear_of_bound {𝕜 : Type u_1} {E : Type u_3} {G : Type u_5} [Ring 𝕜] [SeminormedAddCommGroup E] [SeminormedAddCommGroup G] [Module 𝕜 E] [Module 𝕜 G] {f : EG} (h_add : ∀ (x y : E), f (x + y) = f x + f y) (h_smul : ∀ (c : 𝕜) (x : E), f (c x) = c f x) {C : } (h_bound : ∀ (x : E), f x C * x) :
      @[simp]
      theorem LinearMap.mkContinuous_coe {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_3} {F : Type u_4} [Ring 𝕜] [Ring 𝕜₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [Module 𝕜 E] [Module 𝕜₂ F] {σ : 𝕜 →+* 𝕜₂} (f : E →ₛₗ[σ] F) (C : ) (h : ∀ (x : E), f x C * x) :
      @[simp]
      theorem LinearMap.mkContinuous_apply {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_3} {F : Type u_4} [Ring 𝕜] [Ring 𝕜₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [Module 𝕜 E] [Module 𝕜₂ F] {σ : 𝕜 →+* 𝕜₂} (f : E →ₛₗ[σ] F) (C : ) (h : ∀ (x : E), f x C * x) (x : E) :
      ↑(LinearMap.mkContinuous f C h) x = f x
      @[simp]
      theorem LinearMap.mkContinuousOfExistsBound_coe {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_3} {F : Type u_4} [Ring 𝕜] [Ring 𝕜₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [Module 𝕜 E] [Module 𝕜₂ F] {σ : 𝕜 →+* 𝕜₂} (f : E →ₛₗ[σ] F) (h : C, ∀ (x : E), f x C * x) :
      @[simp]
      theorem LinearMap.mkContinuousOfExistsBound_apply {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_3} {F : Type u_4} [Ring 𝕜] [Ring 𝕜₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [Module 𝕜 E] [Module 𝕜₂ F] {σ : 𝕜 →+* 𝕜₂} (f : E →ₛₗ[σ] F) (h : C, ∀ (x : E), f x C * x) (x : E) :
      theorem ContinuousLinearMap.antilipschitz_of_bound {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_3} {F : Type u_4} [Ring 𝕜] [Ring 𝕜₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [Module 𝕜 E] [Module 𝕜₂ F] {σ : 𝕜 →+* 𝕜₂} (f : E →SL[σ] F) {K : NNReal} (h : ∀ (x : E), x K * f x) :
      theorem ContinuousLinearMap.bound_of_antilipschitz {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_3} {F : Type u_4} [Ring 𝕜] [Ring 𝕜₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [Module 𝕜 E] [Module 𝕜₂ F] {σ : 𝕜 →+* 𝕜₂} (f : E →SL[σ] F) {K : NNReal} (h : AntilipschitzWith K f) (x : E) :
      x K * f x
      def LinearEquiv.toContinuousLinearEquivOfBounds {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_3} {F : Type u_4} [Ring 𝕜] [Ring 𝕜₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [Module 𝕜 E] [Module 𝕜₂ F] {σ : 𝕜 →+* 𝕜₂} {σ₂₁ : 𝕜₂ →+* 𝕜} [RingHomInvPair σ σ₂₁] [RingHomInvPair σ₂₁ σ] (e : E ≃ₛₗ[σ] F) (C_to : ) (C_inv : ) (h_to : ∀ (x : E), e x C_to * x) (h_inv : ∀ (x : F), ↑(LinearEquiv.symm e) x C_inv * x) :
      E ≃SL[σ] F

      Construct a continuous linear equivalence from a linear equivalence together with bounds in both directions.

      Equations
      Instances For
        def LinearMap.toContinuousLinearMap₁ {𝕜 : Type u_1} {E : Type u_3} [SeminormedRing 𝕜] [SeminormedAddCommGroup E] [Module 𝕜 E] [BoundedSMul 𝕜 E] (f : 𝕜 →ₗ[𝕜] E) :
        𝕜 →L[𝕜] E

        Reinterpret a linear map 𝕜 →ₗ[𝕜] E as a continuous linear map. This construction is generalized to the case of any finite dimensional domain in LinearMap.toContinuousLinearMap.

        Equations
        Instances For
          @[simp]
          theorem LinearMap.toContinuousLinearMap₁_coe {𝕜 : Type u_1} {E : Type u_3} [SeminormedRing 𝕜] [SeminormedAddCommGroup E] [Module 𝕜 E] [BoundedSMul 𝕜 E] (f : 𝕜 →ₗ[𝕜] E) :
          @[simp]
          theorem LinearMap.toContinuousLinearMap₁_apply {𝕜 : Type u_1} {E : Type u_3} [SeminormedRing 𝕜] [SeminormedAddCommGroup E] [Module 𝕜 E] [BoundedSMul 𝕜 E] (f : 𝕜 →ₗ[𝕜] E) (x : 𝕜) :
          theorem ContinuousLinearMap.uniformEmbedding_of_bound {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_3} {F : Type u_4} [Ring 𝕜] [Ring 𝕜₂] [NormedAddCommGroup E] [NormedAddCommGroup F] [Module 𝕜 E] [Module 𝕜₂ F] {σ : 𝕜 →+* 𝕜₂} (f : E →SL[σ] F) {K : NNReal} (hf : ∀ (x : E), x K * f x) :

          Homotheties #

          def ContinuousLinearMap.ofHomothety {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_3} {F : Type u_4} [Ring 𝕜] [Ring 𝕜₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [Module 𝕜 E] [Module 𝕜₂ F] {σ : 𝕜 →+* 𝕜₂} (f : E →ₛₗ[σ] F) (a : ) (hf : ∀ (x : E), f x = a * x) :
          E →SL[σ] F

          A (semi-)linear map which is a homothety is a continuous linear map. Since the field 𝕜 need not have as a subfield, this theorem is not directly deducible from the corresponding theorem about isometries plus a theorem about scalar multiplication. Likewise for the other theorems about homotheties in this file.

          Equations
          Instances For
            theorem ContinuousLinearEquiv.homothety_inverse {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_3} {F : Type u_4} [Ring 𝕜] [Ring 𝕜₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [Module 𝕜 E] [Module 𝕜₂ F] {σ : 𝕜 →+* 𝕜₂} {σ₂₁ : 𝕜₂ →+* 𝕜} [RingHomInvPair σ σ₂₁] [RingHomInvPair σ₂₁ σ] (a : ) (ha : 0 < a) (f : E ≃ₛₗ[σ] F) :
            (∀ (x : E), f x = a * x) → ∀ (y : F), ↑(LinearEquiv.symm f) y = a⁻¹ * y
            noncomputable def ContinuousLinearEquiv.ofHomothety {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_3} {F : Type u_4} [Ring 𝕜] [Ring 𝕜₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [Module 𝕜 E] [Module 𝕜₂ F] {σ : 𝕜 →+* 𝕜₂} {σ₂₁ : 𝕜₂ →+* 𝕜} [RingHomInvPair σ σ₂₁] [RingHomInvPair σ₂₁ σ] (f : E ≃ₛₗ[σ] F) (a : ) (ha : 0 < a) (hf : ∀ (x : E), f x = a * x) :
            E ≃SL[σ] F

            A linear equivalence which is a homothety is a continuous linear equivalence.

            Equations
            Instances For

              The span of a single vector #

              theorem ContinuousLinearMap.toSpanSingleton_homothety (𝕜 : Type u_1) {E : Type u_3} [NormedDivisionRing 𝕜] [SeminormedAddCommGroup E] [Module 𝕜 E] [BoundedSMul 𝕜 E] (x : E) (c : 𝕜) :
              theorem ContinuousLinearEquiv.toSpanNonzeroSingleton_homothety (𝕜 : Type u_1) {E : Type u_3} [NormedDivisionRing 𝕜] [SeminormedAddCommGroup E] [Module 𝕜 E] [BoundedSMul 𝕜 E] (x : E) (h : x 0) (c : 𝕜) :
              noncomputable def ContinuousLinearEquiv.toSpanNonzeroSingleton (𝕜 : Type u_1) {E : Type u_3} [NormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] (x : E) (h : x 0) :
              𝕜 ≃L[𝕜] { x // x Submodule.span 𝕜 {x} }

              Given a nonzero element x of a normed space E₁ over a field 𝕜, the natural continuous linear equivalence from E₁ to the span of x.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                noncomputable def ContinuousLinearEquiv.coord (𝕜 : Type u_1) {E : Type u_3} [NormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] (x : E) (h : x 0) :
                { x // x Submodule.span 𝕜 {x} } →L[𝕜] 𝕜

                Given a nonzero element x of a normed space E₁ over a field 𝕜, the natural continuous linear map from the span of x to 𝕜.

                Equations
                Instances For
                  @[simp]
                  theorem ContinuousLinearEquiv.coord_toSpanNonzeroSingleton (𝕜 : Type u_1) {E : Type u_3} [NormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {x : E} (h : x 0) (c : 𝕜) :
                  @[simp]
                  theorem ContinuousLinearEquiv.toSpanNonzeroSingleton_coord (𝕜 : Type u_1) {E : Type u_3} [NormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {x : E} (h : x 0) (y : { x // x Submodule.span 𝕜 {x} }) :
                  @[simp]
                  theorem ContinuousLinearEquiv.coord_self (𝕜 : Type u_1) {E : Type u_3} [NormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] (x : E) (h : x 0) :
                  ↑(ContinuousLinearEquiv.coord 𝕜 x h) { val := x, property := (_ : x Submodule.span 𝕜 {x}) } = 1