Extension of continuous linear maps on Banach spaces

In this file we provide two different ways to extend a continuous linear map defined on a dense subspace to the entire Banach space.

• ContinuousLinearMap.extend: Extend from a dense subspace using IsUniformInducing
• ContinuousLinearMap.extendOfNorm: Extend from a continuous linear map that is a dense injection into the domain and using a norm estimate.

noncomputable def ContinuousLinearMap.extend {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_3} {Eₗ : Type u_4} {F : Type u_5} [AddCommGroup E] [UniformSpace E] [IsUniformAddGroup E] [AddCommGroup F] [UniformSpace F] [IsUniformAddGroup F] [T0Space F] [AddCommMonoid Eₗ] [UniformSpace Eₗ] [ContinuousAdd Eₗ] [Semiring 𝕜] [Semiring 𝕜₂] [Module 𝕜 E] [Module 𝕜₂ F] [Module 𝕜 Eₗ] [ContinuousConstSMul 𝕜 Eₗ] [ContinuousConstSMul 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} (f : E →SL[σ₁₂] F) [CompleteSpace F] (e : E →L[𝕜] Eₗ) (h_dense : DenseRange ⇑e) (h_e : IsUniformInducing ⇑e) : Eₗ →SL[σ₁₂] F

Extension of a continuous linear map f : E →SL[σ₁₂] F, with E a normed space and F a complete normed space, along a uniform and dense embedding e : E →L[𝕜] Eₗ.

Equations

• f.extend e h_dense h_e = { toFun := ⋯.extend ⇑f, map_add' := ⋯, map_smul' := ⋯, cont := ⋯ }

@[simp]

theorem ContinuousLinearMap.extend_eq {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_3} {Eₗ : Type u_4} {F : Type u_5} [AddCommGroup E] [UniformSpace E] [IsUniformAddGroup E] [AddCommGroup F] [UniformSpace F] [IsUniformAddGroup F] [T0Space F] [AddCommMonoid Eₗ] [UniformSpace Eₗ] [ContinuousAdd Eₗ] [Semiring 𝕜] [Semiring 𝕜₂] [Module 𝕜 E] [Module 𝕜₂ F] [Module 𝕜 Eₗ] [ContinuousConstSMul 𝕜 Eₗ] [ContinuousConstSMul 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} (f : E →SL[σ₁₂] F) [CompleteSpace F] (e : E →L[𝕜] Eₗ) (h_dense : DenseRange ⇑e) (h_e : IsUniformInducing ⇑e) (x : E) : (f.extend e h_dense h_e) (e x) = f x

theorem ContinuousLinearMap.extend_unique {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_3} {Eₗ : Type u_4} {F : Type u_5} [AddCommGroup E] [UniformSpace E] [IsUniformAddGroup E] [AddCommGroup F] [UniformSpace F] [IsUniformAddGroup F] [T0Space F] [AddCommMonoid Eₗ] [UniformSpace Eₗ] [ContinuousAdd Eₗ] [Semiring 𝕜] [Semiring 𝕜₂] [Module 𝕜 E] [Module 𝕜₂ F] [Module 𝕜 Eₗ] [ContinuousConstSMul 𝕜 Eₗ] [ContinuousConstSMul 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} (f : E →SL[σ₁₂] F) [CompleteSpace F] (e : E →L[𝕜] Eₗ) (h_dense : DenseRange ⇑e) (h_e : IsUniformInducing ⇑e) (g : Eₗ →SL[σ₁₂] F) (H : g.comp e = f) : f.extend e h_dense h_e = g

@[simp]

theorem ContinuousLinearMap.extend_zero {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_3} {Eₗ : Type u_4} {F : Type u_5} [AddCommGroup E] [UniformSpace E] [IsUniformAddGroup E] [AddCommGroup F] [UniformSpace F] [IsUniformAddGroup F] [T0Space F] [AddCommMonoid Eₗ] [UniformSpace Eₗ] [ContinuousAdd Eₗ] [Semiring 𝕜] [Semiring 𝕜₂] [Module 𝕜 E] [Module 𝕜₂ F] [Module 𝕜 Eₗ] [ContinuousConstSMul 𝕜 Eₗ] [ContinuousConstSMul 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [CompleteSpace F] (e : E →L[𝕜] Eₗ) (h_dense : DenseRange ⇑e) (h_e : IsUniformInducing ⇑e) : extend 0 e h_dense h_e = 0

theorem ContinuousLinearMap.opNorm_extend_le {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_3} {Eₗ : Type u_4} {F : Type u_5} [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] {σ₁₂ : 𝕜 →+* 𝕜₂} [NormedAddCommGroup E] [NormedAddCommGroup Eₗ] [NormedAddCommGroup F] [NormedSpace 𝕜 E] [NormedSpace 𝕜 Eₗ] [NormedSpace 𝕜₂ F] [CompleteSpace F] (f : E →SL[σ₁₂] F) (e : E →L[𝕜] Eₗ) (h_dense : DenseRange ⇑e) {N : NNReal} (h_e : ∀ (x : E), ‖x‖ ≤ ↑N * ‖e x‖) [RingHomIsometric σ₁₂] : ‖f.extend e h_dense ⋯‖ ≤ ↑N * ‖f‖

If a dense embedding e : E →L[𝕜] G expands the norm by a constant factor N⁻¹, then the norm of the extension of f along e is bounded by N * ‖f‖.