# 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 #

source
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

- f.mkContinuous C h = { toLinearMap := f, cont := ⋯ }

Instances For

source
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

- f.mkContinuousOfExistsBound h = { toLinearMap := f, cont := ⋯ }

Instances For

source
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 : E → F} (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‖) :
Continuous f
source
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 : E → G} (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‖) :
Continuous f
source
@[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‖) :
↑(f.mkContinuous C h) = f
source
@[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) :
(f.mkContinuous C h) x = f x
source
@[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‖) :
↑(f.mkContinuousOfExistsBound h) = f
source
@[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) :
(f.mkContinuousOfExistsBound h) x = f x
source
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‖) :
AntilipschitzWith K ⇑f
source
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‖
source
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), ‖e.symm x‖ ≤ C_inv * ‖x‖) :
E ≃SL[σ] F

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

Equations

- e.toContinuousLinearEquivOfBounds C_to C_inv h_to h_inv = { toLinearEquiv := e, continuous_toFun := ⋯, continuous_invFun := ⋯ }

Instances For

source
def LinearMap.toContinuousLinearMap₁ {𝕜 : Type u_1} {E : Type u_3} [SeminormedRing 𝕜] [SeminormedAddCommGroup E] [Module 𝕜 E] [IsBoundedSMul 𝕜 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

- f.toContinuousLinearMap₁ = f.mkContinuous ‖f 1‖ ⋯

Instances For

source
@[simp]
theorem LinearMap.toContinuousLinearMap₁_coe {𝕜 : Type u_1} {E : Type u_3} [SeminormedRing 𝕜] [SeminormedAddCommGroup E] [Module 𝕜 E] [IsBoundedSMul 𝕜 E] (f : 𝕜 →ₗ[𝕜] E) :
↑f.toContinuousLinearMap₁ = f
source
@[simp]
theorem LinearMap.toContinuousLinearMap₁_apply {𝕜 : Type u_1} {E : Type u_3} [SeminormedRing 𝕜] [SeminormedAddCommGroup E] [Module 𝕜 E] [IsBoundedSMul 𝕜 E] (f : 𝕜 →ₗ[𝕜] E) (x : 𝕜) :
f.toContinuousLinearMap₁ x = f x
source
theorem ContinuousLinearMap.isUniformEmbedding_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‖) :
IsUniformEmbedding ⇑f

## Homotheties #

source
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

- ContinuousLinearMap.ofHomothety f a hf = f.mkContinuous a ⋯

Instances For

source
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), ‖f.symm y‖ = a⁻¹ * ‖y‖
source
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

- ContinuousLinearEquiv.ofHomothety f a ha hf = f.toContinuousLinearEquivOfBounds a a⁻¹ ⋯ ⋯

Instances For