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 map into the domain together with 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ₗ) : 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 = if h : DenseRange ⇑e ∧ IsUniformInducing ⇑e then have cont := ⋯; have eq := ⋯; { toFun := ⋯.extend ⇑f, map_add' := ⋯, map_smul' := ⋯, cont := cont } else 0

@[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) (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 = 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 = 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ₗ} {N : NNReal} [RingHomIsometric σ₁₂] (h_dense : DenseRange ⇑e) (h_e : ∀ (x : E), ‖x‖ ≤ ↑N * ‖e x‖) : ‖f.extend e‖ ≤ ↑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‖.

noncomputable def LinearMap.compLeftInverse {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_3} {Eₗ : Type u_4} {F : Type u_5} [DivisionRing 𝕜] [DivisionRing 𝕜₂] {σ₁₂ : 𝕜 →+* 𝕜₂} [AddCommGroup E] [NormedAddCommGroup F] [SeminormedAddCommGroup Eₗ] [Module 𝕜 E] [Module 𝕜₂ F] [Module 𝕜 Eₗ] (f : E →ₛₗ[σ₁₂] F) (g : E →ₗ[𝕜] Eₗ) : ↥(range g) →SL[σ₁₂] F

Composition of a semilinear map f with the left inverse of a linear map g as a continuous linear map provided that the norm estimate ‖f x‖ ≤ C * ‖g x‖ holds for all x : E.

Equations

• f.compLeftInverse g = if h : ∃ (C : ℝ), ∀ (x : E), ‖f x‖ ≤ C * ‖g x‖ then ((LinearMap.ker g).liftQ f ⋯ ∘ₛₗ ↑g.quotKerEquivRange.symm).mkContinuousOfExistsBound ⋯ else 0

theorem LinearMap.compLeftInverse_apply_of_bdd {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_3} {Eₗ : Type u_4} {F : Type u_5} [DivisionRing 𝕜] [DivisionRing 𝕜₂] {σ₁₂ : 𝕜 →+* 𝕜₂} [AddCommGroup E] [NormedAddCommGroup F] [SeminormedAddCommGroup Eₗ] [Module 𝕜 E] [Module 𝕜₂ F] [Module 𝕜 Eₗ] (f : E →ₛₗ[σ₁₂] F) (g : E →ₗ[𝕜] Eₗ) (h_norm : ∃ (C : ℝ), ∀ (x : E), ‖f x‖ ≤ C * ‖g x‖) (x : E) (y : Eₗ) (hx : g x = y) : (f.compLeftInverse g) ⟨y, ⋯⟩ = f x

noncomputable def LinearMap.extendOfNorm {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_3} {Eₗ : Type u_4} {F : Type u_5} [NormedDivisionRing 𝕜] [NormedDivisionRing 𝕜₂] {σ₁₂ : 𝕜 →+* 𝕜₂} [AddCommGroup E] [SeminormedAddCommGroup Eₗ] [NormedAddCommGroup F] [Module 𝕜 E] [Module 𝕜₂ F] [IsBoundedSMul 𝕜₂ F] [Module 𝕜 Eₗ] [IsBoundedSMul 𝕜 Eₗ] [CompleteSpace F] (f : E →ₛₗ[σ₁₂] F) (e : E →ₗ[𝕜] Eₗ) : Eₗ →SL[σ₁₂] F

Extension of a linear map f : E →ₛₗ[σ₁₂] F to a continuous linear map Eₗ →SL[σ₁₂] F, where E is a normed space and F a complete normed space, using a dense map e : E →L[𝕜] Eₗ together with a bound ‖f x‖ ≤ C * ‖e x‖ for all x : E.

Equations

• f.extendOfNorm e = (f.compLeftInverse e).extend (LinearMap.range e).subtypeL

theorem LinearMap.extendOfNorm_eq {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_3} {Eₗ : Type u_4} {F : Type u_5} [NormedDivisionRing 𝕜] [NormedDivisionRing 𝕜₂] {σ₁₂ : 𝕜 →+* 𝕜₂} [AddCommGroup E] [SeminormedAddCommGroup Eₗ] [NormedAddCommGroup F] [Module 𝕜 E] [Module 𝕜₂ F] [IsBoundedSMul 𝕜₂ F] [Module 𝕜 Eₗ] [IsBoundedSMul 𝕜 Eₗ] [CompleteSpace F] {f : E →ₛₗ[σ₁₂] F} {e : E →ₗ[𝕜] Eₗ} (h_dense : DenseRange ⇑e) (h_norm : ∃ (C : ℝ), ∀ (x : E), ‖f x‖ ≤ C * ‖e x‖) (x : E) : (f.extendOfNorm e) (e x) = f x

theorem LinearMap.norm_extendOfNorm_apply_le {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_3} {Eₗ : Type u_4} {F : Type u_5} [NormedDivisionRing 𝕜] [NormedDivisionRing 𝕜₂] {σ₁₂ : 𝕜 →+* 𝕜₂} [AddCommGroup E] [SeminormedAddCommGroup Eₗ] [NormedAddCommGroup F] [Module 𝕜 E] [Module 𝕜₂ F] [IsBoundedSMul 𝕜₂ F] [Module 𝕜 Eₗ] [IsBoundedSMul 𝕜 Eₗ] [CompleteSpace F] {f : E →ₛₗ[σ₁₂] F} {e : E →ₗ[𝕜] Eₗ} (h_dense : DenseRange ⇑e) (C : ℝ) (h_norm : ∀ (x : E), ‖f x‖ ≤ C * ‖e x‖) (x : Eₗ) : ‖(f.extendOfNorm e) x‖ ≤ C * ‖x‖

theorem LinearMap.extendOfNorm_unique {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_3} {Eₗ : Type u_4} {F : Type u_5} [NormedDivisionRing 𝕜] [NormedDivisionRing 𝕜₂] {σ₁₂ : 𝕜 →+* 𝕜₂} [AddCommGroup E] [SeminormedAddCommGroup Eₗ] [NormedAddCommGroup F] [Module 𝕜 E] [Module 𝕜₂ F] [IsBoundedSMul 𝕜₂ F] [Module 𝕜 Eₗ] [IsBoundedSMul 𝕜 Eₗ] [CompleteSpace F] {f : E →ₛₗ[σ₁₂] F} {e : E →ₗ[𝕜] Eₗ} (h_dense : DenseRange ⇑e) (C : ℝ) (h_norm : ∀ (x : E), ‖f x‖ ≤ C * ‖e x‖) (g : Eₗ →SL[σ₁₂] F) (H : ↑g ∘ₛₗ e = f) : f.extendOfNorm e = g

theorem LinearMap.opNorm_extendOfNorm_le {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_3} {Eₗ : Type u_4} {F : Type u_5} [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] {σ₁₂ : 𝕜 →+* 𝕜₂} [NormedAddCommGroup F] [SeminormedAddCommGroup Eₗ] [NormedSpace 𝕜₂ F] [NormedSpace 𝕜 Eₗ] [AddCommGroup E] [Module 𝕜 E] [CompleteSpace F] {f : E →ₛₗ[σ₁₂] F} {e : E →ₗ[𝕜] Eₗ} (h_dense : DenseRange ⇑e) {C : ℝ} (hC : 0 ≤ C) (h_norm : ∀ (x : E), ‖f x‖ ≤ C * ‖e x‖) : ‖f.extendOfNorm e‖ ≤ C