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 f : E →SL[σ₁₂] F to a continuous linear map Eₗ →SL[σ₁₂] F, where e : E →ₗ[𝕜] Eₗ is a dense map that is IsUniformInducing.
• LinearMap.extendOfNorm: Extend f : E →ₛₗ[σ₁₂] F to a continuous linear map Eₗ →SL[σ₁₂] F, where e : E →ₗ[𝕜] Eₗ is a dense map and we have the norm estimate ‖f x‖ ≤ C * ‖e x‖ for all x : E.

Moreover, we can extend a linear equivalence:

• LinearEquiv.extend: Extend a linear equivalence between normed spaces to a continuous linear equivalence between Banach spaces with two dense maps e₁ and e₂ and the corresponding norm estimates.
• LinearEquiv.extendOfIsometry: Extend f : E ≃ₗ[𝕜] F to a linear isometry equivalence Eₗ →ₗᵢ[𝕜] Fₗ, where e₁ : E →ₗ[𝕜] Eₗ and e₂ : F →ₗ[𝕜] Fₗ are dense maps into Banach spaces and f preserves the norm.

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 →ₗ[𝕜] 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

noncomputable def LinearEquiv.extend {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_3} {Eₗ : Type u_4} {F : Type u_5} {Fₗ : Type u_6} [NormedDivisionRing 𝕜] [NormedDivisionRing 𝕜₂] [AddCommGroup E] [NormedAddCommGroup Eₗ] [AddCommGroup F] [NormedAddCommGroup Fₗ] [Module 𝕜 E] [Module 𝕜 Eₗ] [IsBoundedSMul 𝕜 Eₗ] [Module 𝕜₂ F] [Module 𝕜₂ Fₗ] [IsBoundedSMul 𝕜₂ Fₗ] [CompleteSpace Eₗ] [CompleteSpace Fₗ] {σ₁₂ : 𝕜 →+* 𝕜₂} {σ₂₁ : 𝕜₂ →+* 𝕜} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] (f : E ≃ₛₗ[σ₁₂] F) (e₁ : E →ₗ[𝕜] Eₗ) (e₂ : F →ₗ[𝕜₂] Fₗ) (h_dense₁ : DenseRange ⇑e₁) (h_norm₁ : ∃ (C : ℝ), ∀ (x : E), ‖e₂ (f x)‖ ≤ C * ‖e₁ x‖) (h_dense₂ : DenseRange ⇑e₂) (h_norm₂ : ∃ (C : ℝ), ∀ (x : F), ‖e₁ (f.symm x)‖ ≤ C * ‖e₂ x‖) : Eₗ ≃SL[σ₁₂] Fₗ

Extension of a linear equivalence f : E ≃ₛₗ[σ₁₂] F to a continuous linear equivalence Eₗ ≃SL[σ₁₂] Fₗ, where E and F are normed spaces and Eₗ and Fₗ are Banach spaces, using dense maps e₁ : E →ₗ[𝕜₁] Eₗ and e₂ : F →ₗ[𝕜₂] F₂ together with bounds ‖e₂ (f x)‖ ≤ C * ‖e₁ x‖ for all x : E and ‖e₁ (f.symm x)‖ ≤ C * ‖e₂ x‖ for all x : F.

Equations

• One or more equations did not get rendered due to their size.

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

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

@[simp]

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

@[simp]

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

theorem LinearEquiv.norm_extend_le {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_3} {Eₗ : Type u_4} {F : Type u_5} {Fₗ : Type u_6} [NormedDivisionRing 𝕜] [NormedDivisionRing 𝕜₂] [AddCommGroup E] [NormedAddCommGroup Eₗ] [AddCommGroup F] [NormedAddCommGroup Fₗ] [Module 𝕜 E] [Module 𝕜 Eₗ] [IsBoundedSMul 𝕜 Eₗ] [Module 𝕜₂ F] [Module 𝕜₂ Fₗ] [IsBoundedSMul 𝕜₂ Fₗ] [CompleteSpace Eₗ] [CompleteSpace Fₗ] {σ₁₂ : 𝕜 →+* 𝕜₂} {σ₂₁ : 𝕜₂ →+* 𝕜} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] (f : E ≃ₛₗ[σ₁₂] F) (e₁ : E →ₗ[𝕜] Eₗ) (e₂ : F →ₗ[𝕜₂] Fₗ) (C : ℝ) (h_dense₁ : DenseRange ⇑e₁) (h_norm₁ : ∀ (x : E), ‖e₂ (f x)‖ ≤ C * ‖e₁ x‖) (h_dense₂ : DenseRange ⇑e₂) (h_norm₂ : ∃ (C : ℝ), ∀ (x : F), ‖e₁ (f.symm x)‖ ≤ C * ‖e₂ x‖) (x : Eₗ) : ‖(f.extend e₁ e₂ h_dense₁ ⋯ h_dense₂ h_norm₂) x‖ ≤ C * ‖x‖

theorem LinearEquiv.norm_extend_symm_le {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_3} {Eₗ : Type u_4} {F : Type u_5} {Fₗ : Type u_6} [NormedDivisionRing 𝕜] [NormedDivisionRing 𝕜₂] [AddCommGroup E] [NormedAddCommGroup Eₗ] [AddCommGroup F] [NormedAddCommGroup Fₗ] [Module 𝕜 E] [Module 𝕜 Eₗ] [IsBoundedSMul 𝕜 Eₗ] [Module 𝕜₂ F] [Module 𝕜₂ Fₗ] [IsBoundedSMul 𝕜₂ Fₗ] [CompleteSpace Eₗ] [CompleteSpace Fₗ] {σ₁₂ : 𝕜 →+* 𝕜₂} {σ₂₁ : 𝕜₂ →+* 𝕜} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] (f : E ≃ₛₗ[σ₁₂] F) (e₁ : E →ₗ[𝕜] Eₗ) (e₂ : F →ₗ[𝕜₂] Fₗ) (C : ℝ) (h_dense₁ : DenseRange ⇑e₁) (h_norm₁ : ∃ (C : ℝ), ∀ (x : E), ‖e₂ (f x)‖ ≤ C * ‖e₁ x‖) (h_dense₂ : DenseRange ⇑e₂) (h_norm₂ : ∀ (x : F), ‖e₁ (f.symm x)‖ ≤ C * ‖e₂ x‖) (x : Fₗ) : ‖(f.extend e₁ e₂ h_dense₁ h_norm₁ h_dense₂ ⋯).symm x‖ ≤ C * ‖x‖

noncomputable def LinearEquiv.extendOfIsometry {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_3} {Eₗ : Type u_4} {F : Type u_5} {Fₗ : Type u_6} [NormedField 𝕜] [NormedField 𝕜₂] [AddCommGroup E] [Module 𝕜 E] [AddCommGroup F] [Module 𝕜₂ F] [NormedAddCommGroup Eₗ] [NormedSpace 𝕜 Eₗ] [CompleteSpace Eₗ] [NormedAddCommGroup Fₗ] [NormedSpace 𝕜₂ Fₗ] [CompleteSpace Fₗ] {σ₁₂ : 𝕜 →+* 𝕜₂} {σ₂₁ : 𝕜₂ →+* 𝕜} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] (f : E ≃ₛₗ[σ₁₂] F) (e₁ : E →ₗ[𝕜] Eₗ) (e₂ : F →ₗ[𝕜₂] Fₗ) (h_dense₁ : DenseRange ⇑e₁) (h_dense₂ : DenseRange ⇑e₂) (h_norm : ∀ (x : E), ‖e₂ (f x)‖ = ‖e₁ x‖) : Eₗ ≃ₛₗᵢ[σ₁₂] Fₗ

Extend a densely defined operator that preserves the norm to a linear isometry equivalence.

Equations

• f.extendOfIsometry e₁ e₂ h_dense₁ h_dense₂ h_norm = { toLinearEquiv := (f.extend e₁ e₂ h_dense₁ ⋯ h_dense₂ ⋯).toLinearEquiv, norm_map' := ⋯ }

theorem LinearEquiv.extendOfIsometry_apply {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_3} {Eₗ : Type u_4} {F : Type u_5} {Fₗ : Type u_6} [NormedField 𝕜] [NormedField 𝕜₂] [AddCommGroup E] [Module 𝕜 E] [AddCommGroup F] [Module 𝕜₂ F] [NormedAddCommGroup Eₗ] [NormedSpace 𝕜 Eₗ] [CompleteSpace Eₗ] [NormedAddCommGroup Fₗ] [NormedSpace 𝕜₂ Fₗ] [CompleteSpace Fₗ] {σ₁₂ : 𝕜 →+* 𝕜₂} {σ₂₁ : 𝕜₂ →+* 𝕜} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] (f : E ≃ₛₗ[σ₁₂] F) (e₁ : E →ₗ[𝕜] Eₗ) (e₂ : F →ₗ[𝕜₂] Fₗ) (h_dense₁ : DenseRange ⇑e₁) (h_dense₂ : DenseRange ⇑e₂) (h_norm : ∀ (x : E), ‖e₂ (f x)‖ = ‖e₁ x‖) (x : Eₗ) : (f.extendOfIsometry e₁ e₂ h_dense₁ h_dense₂ h_norm) x = ((e₂ ∘ₛₗ ↑f).extendOfNorm e₁) x

theorem LinearEquiv.extendOfIsometry_symm_apply {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_3} {Eₗ : Type u_4} {F : Type u_5} {Fₗ : Type u_6} [NormedField 𝕜] [NormedField 𝕜₂] [AddCommGroup E] [Module 𝕜 E] [AddCommGroup F] [Module 𝕜₂ F] [NormedAddCommGroup Eₗ] [NormedSpace 𝕜 Eₗ] [CompleteSpace Eₗ] [NormedAddCommGroup Fₗ] [NormedSpace 𝕜₂ Fₗ] [CompleteSpace Fₗ] {σ₁₂ : 𝕜 →+* 𝕜₂} {σ₂₁ : 𝕜₂ →+* 𝕜} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] (f : E ≃ₛₗ[σ₁₂] F) (e₁ : E →ₗ[𝕜] Eₗ) (e₂ : F →ₗ[𝕜₂] Fₗ) (h_dense₁ : DenseRange ⇑e₁) (h_dense₂ : DenseRange ⇑e₂) (h_norm : ∀ (x : E), ‖e₂ (f x)‖ = ‖e₁ x‖) (x : Fₗ) : (f.extendOfIsometry e₁ e₂ h_dense₁ h_dense₂ h_norm).symm x = ((e₁ ∘ₛₗ ↑f.symm).extendOfNorm e₂) x

@[simp]

theorem LinearEquiv.extendOfIsometry_eq {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_3} {Eₗ : Type u_4} {F : Type u_5} {Fₗ : Type u_6} [NormedField 𝕜] [NormedField 𝕜₂] [AddCommGroup E] [Module 𝕜 E] [AddCommGroup F] [Module 𝕜₂ F] [NormedAddCommGroup Eₗ] [NormedSpace 𝕜 Eₗ] [CompleteSpace Eₗ] [NormedAddCommGroup Fₗ] [NormedSpace 𝕜₂ Fₗ] [CompleteSpace Fₗ] {σ₁₂ : 𝕜 →+* 𝕜₂} {σ₂₁ : 𝕜₂ →+* 𝕜} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] (f : E ≃ₛₗ[σ₁₂] F) (e₁ : E →ₗ[𝕜] Eₗ) (e₂ : F →ₗ[𝕜₂] Fₗ) (h_dense₁ : DenseRange ⇑e₁) (h_dense₂ : DenseRange ⇑e₂) (h_norm : ∀ (x : E), ‖e₂ (f x)‖ = ‖e₁ x‖) (x : E) : (f.extendOfIsometry e₁ e₂ h_dense₁ h_dense₂ h_norm) (e₁ x) = e₂ (f x)

@[simp]

theorem LinearEquiv.extendOfIsometry_symm_eq {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_3} {Eₗ : Type u_4} {F : Type u_5} {Fₗ : Type u_6} [NormedField 𝕜] [NormedField 𝕜₂] [AddCommGroup E] [Module 𝕜 E] [AddCommGroup F] [Module 𝕜₂ F] [NormedAddCommGroup Eₗ] [NormedSpace 𝕜 Eₗ] [CompleteSpace Eₗ] [NormedAddCommGroup Fₗ] [NormedSpace 𝕜₂ Fₗ] [CompleteSpace Fₗ] {σ₁₂ : 𝕜 →+* 𝕜₂} {σ₂₁ : 𝕜₂ →+* 𝕜} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] (f : E ≃ₛₗ[σ₁₂] F) (e₁ : E →ₗ[𝕜] Eₗ) (e₂ : F →ₗ[𝕜₂] Fₗ) (h_dense₁ : DenseRange ⇑e₁) (h_dense₂ : DenseRange ⇑e₂) (h_norm : ∀ (x : E), ‖e₂ (f x)‖ = ‖e₁ x‖) (x : F) : (f.extendOfIsometry e₁ e₂ h_dense₁ h_dense₂ h_norm).symm (e₂ x) = e₁ (f.symm x)