Extension of continuous linear maps

In this file we provide a way to extend a continuous linear map defined on a dense subspace to the entire space.

• ContinuousLinearMap.extend: Extend f : E →SL[σ₁₂] F to a continuous linear map Eₗ →SL[σ₁₂] F, where e : E →ₗ[𝕜] Eₗ is a dense map that is IsUniformInducing.

noncomputable def ContinuousLinearMap.extend {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_3} {F : Type u_4} {Eₗ : 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 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} {F : Type u_4} {Eₗ : 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} {F : Type u_4} {Eₗ : 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 ∘SL e = f) : f.extend e = g

@[simp]

theorem ContinuousLinearMap.extend_zero {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_3} {F : Type u_4} {Eₗ : 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