Extension of continuous linear maps on Banach spaces

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

• 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.
• LinearMap.extendOfIsometry: Extend a linear map f : E →ₛₗ[𝕜] F between normed spaces to a linear isometry Eₗ →ₗᵢ[𝕜] F between Banach spaces with a dense map e : E →ₗ[𝕜] Eₗ together with the corresponding norm estimate.
• 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.
• LinearIsometry.completion: The linear isometric version of UniformSpace.Completion.extension.
• LinearIsometry.fromCompletion: The linear isometric version of UniformSpace.Completion.map.

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ₗ) : ↥g.range →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 (g.ker.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 e.range.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 LinearMap.extendOfIsometry {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_3} {Eₗ : Type u_4} {F : Type u_5} [NormedDivisionRing 𝕜] [NormedDivisionRing 𝕜₂] [AddCommGroup E] [Module 𝕜 E] [NormedAddCommGroup Eₗ] [Module 𝕜 Eₗ] [IsBoundedSMul 𝕜 Eₗ] [NormedAddCommGroup F] [Module 𝕜₂ F] [IsBoundedSMul 𝕜₂ F] [CompleteSpace F] {σ₁₂ : 𝕜 →+* 𝕜₂} (f : E →ₛₗ[σ₁₂] F) {e : E →ₗ[𝕜] Eₗ} (h_dense : DenseRange ⇑e) (h_norm : ∀ (x : E), ‖f x‖ = ‖e x‖) : Eₗ →ₛₗᵢ[σ₁₂] F

Extend a linear map f : E →ₛₗ[σ₁₂] F to a linear isometry Eₗ →ₛₗᵢ[σ₁₂] F between Banach spaces, using a dense linear map e : E →ₗ[𝕜] Eₗ together with the norm equality ‖f x‖ = ‖e x‖ for all x : E.

Equations

• f.extendOfIsometry h_dense h_norm = { toLinearMap := ↑(f.extendOfNorm e), norm_map' := ⋯ }

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

@[simp]

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

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

theorem LinearMap.extendOfIsometry_unique {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_3} {Eₗ : Type u_4} {F : Type u_5} [NormedDivisionRing 𝕜] [NormedDivisionRing 𝕜₂] [AddCommGroup E] [Module 𝕜 E] [NormedAddCommGroup Eₗ] [Module 𝕜 Eₗ] [IsBoundedSMul 𝕜 Eₗ] [NormedAddCommGroup F] [Module 𝕜₂ F] [IsBoundedSMul 𝕜₂ F] [CompleteSpace F] {σ₁₂ : 𝕜 →+* 𝕜₂} (f : E →ₛₗ[σ₁₂] F) {e : E →ₗ[𝕜] Eₗ} (h_dense : DenseRange ⇑e) (h_norm : ∀ (x : E), ‖f x‖ = ‖e x‖) (g : Eₗ →ₛₗᵢ[σ₁₂] F) (H : g.toLinearMap ∘ₛₗ e = f) : f.extendOfIsometry h_dense h_norm = g

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₂ ⋯), 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)

noncomputable def LinearIsometry.fromCompletion {E : Type u_3} {F : Type u_5} {R : Type u_7} {R₂ : Type u_8} [Semiring R] [Semiring R₂] [SeminormedAddCommGroup E] [Module R E] [IsUniformAddGroup E] [UniformContinuousConstSMul R E] [NormedAddCommGroup F] [Module R₂ F] {σ₁₂ : R →+* R₂} (f : E →ₛₗᵢ[σ₁₂] F) [PseudoMetricSpace R₂] [CompleteSpace F] [IsBoundedSMul R₂ F] : UniformSpace.Completion E →ₛₗᵢ[σ₁₂] F

Extend a linear isometry f : E →ₛₗᵢ[σ₁₂] F to a linear isometry UniformSpace.Completion E →ₛₗᵢ[σ₁₂] F between the completions of E and a complete space F, via the canonical completion embedding. This is the linear isometric version of UniformSpace.Completion.extension.

Equations

• f.fromCompletion = { toLinearMap := ↑f.toContinuousLinearMap.fromCompletion, norm_map' := ⋯ }

theorem LinearIsometry.fromCompletion_apply_coe {E : Type u_3} {F : Type u_5} {R : Type u_7} {R₂ : Type u_8} [Semiring R] [Semiring R₂] [SeminormedAddCommGroup E] [Module R E] [IsUniformAddGroup E] [UniformContinuousConstSMul R E] [NormedAddCommGroup F] [Module R₂ F] {σ₁₂ : R →+* R₂} (f : E →ₛₗᵢ[σ₁₂] F) [PseudoMetricSpace R₂] [CompleteSpace F] [IsBoundedSMul R₂ F] (x : E) : f.fromCompletion ↑x = f x

@[simp]

theorem LinearIsometry.coe_fromCompletion {E : Type u_3} {F : Type u_5} {R : Type u_7} {R₂ : Type u_8} [Semiring R] [Semiring R₂] [SeminormedAddCommGroup E] [Module R E] [IsUniformAddGroup E] [UniformContinuousConstSMul R E] [NormedAddCommGroup F] [Module R₂ F] {σ₁₂ : R →+* R₂} (f : E →ₛₗᵢ[σ₁₂] F) [PseudoMetricSpace R₂] [CompleteSpace F] [IsBoundedSMul R₂ F] : ⇑f.fromCompletion = UniformSpace.Completion.extension ⇑f

@[simp]

theorem LinearIsometry.toContinuousLinearMap_fromCompletion {E : Type u_3} {F : Type u_5} {R : Type u_7} {R₂ : Type u_8} [Semiring R] [Semiring R₂] [SeminormedAddCommGroup E] [Module R E] [IsUniformAddGroup E] [UniformContinuousConstSMul R E] [NormedAddCommGroup F] [Module R₂ F] {σ₁₂ : R →+* R₂} (f : E →ₛₗᵢ[σ₁₂] F) [PseudoMetricSpace R₂] [CompleteSpace F] [IsBoundedSMul R₂ F] : f.fromCompletion.toContinuousLinearMap = f.toContinuousLinearMap.fromCompletion

@[simp]

theorem LinearIsometry.toAddMonoidHom_fromCompletion {E : Type u_3} {F : Type u_5} {R : Type u_7} {R₂ : Type u_8} [Semiring R] [Semiring R₂] [SeminormedAddCommGroup E] [Module R E] [IsUniformAddGroup E] [UniformContinuousConstSMul R E] [NormedAddCommGroup F] [Module R₂ F] {σ₁₂ : R →+* R₂} [PseudoMetricSpace R₂] [CompleteSpace F] [IsBoundedSMul R₂ F] (f : E →ₛₗᵢ[σ₁₂] F) : f.fromCompletion.toAddMonoidHom = f.toAddMonoidHom.extension ⋯

noncomputable def LinearIsometry.completion {E : Type u_3} {F : Type u_5} {R : Type u_7} {R₂ : Type u_8} [Semiring R] [Semiring R₂] [SeminormedAddCommGroup E] [Module R E] [IsUniformAddGroup E] [UniformContinuousConstSMul R E] [NormedAddCommGroup F] [Module R₂ F] {σ₁₂ : R →+* R₂} (f : E →ₛₗᵢ[σ₁₂] F) [UniformContinuousConstSMul R₂ F] : UniformSpace.Completion E →ₛₗᵢ[σ₁₂] UniformSpace.Completion F

Extend a linear isometry f : E →ₛₗᵢ[σ₁₂] F to a linear isometry UniformSpace.Completion E →ₛₗᵢ[σ₁₂] UniformSpace.Completion F between the completions of E and F, via the canonical completion embeddings. This is the linear isometric version of UniformSpace.Completion.map.

Equations

• f.completion = { toLinearMap := ↑f.toContinuousLinearMap.completion, norm_map' := ⋯ }

theorem LinearIsometry.completion_apply_coe {E : Type u_3} {F : Type u_5} {R : Type u_7} {R₂ : Type u_8} [Semiring R] [Semiring R₂] [SeminormedAddCommGroup E] [Module R E] [IsUniformAddGroup E] [UniformContinuousConstSMul R E] [NormedAddCommGroup F] [Module R₂ F] {σ₁₂ : R →+* R₂} (f : E →ₛₗᵢ[σ₁₂] F) [UniformContinuousConstSMul R₂ F] (x : E) : f.completion ↑x = ↑(f x)

@[simp]

theorem LinearIsometry.coe_completion {E : Type u_3} {F : Type u_5} {R : Type u_7} {R₂ : Type u_8} [Semiring R] [Semiring R₂] [SeminormedAddCommGroup E] [Module R E] [IsUniformAddGroup E] [UniformContinuousConstSMul R E] [NormedAddCommGroup F] [Module R₂ F] {σ₁₂ : R →+* R₂} (f : E →ₛₗᵢ[σ₁₂] F) [UniformContinuousConstSMul R₂ F] : ⇑f.completion = UniformSpace.Completion.map ⇑f

@[simp]

theorem LinearIsometry.toContinuousLinearMap_completion {E : Type u_3} {F : Type u_5} {R : Type u_7} {R₂ : Type u_8} [Semiring R] [Semiring R₂] [SeminormedAddCommGroup E] [Module R E] [IsUniformAddGroup E] [UniformContinuousConstSMul R E] [NormedAddCommGroup F] [Module R₂ F] {σ₁₂ : R →+* R₂} (f : E →ₛₗᵢ[σ₁₂] F) [UniformContinuousConstSMul R₂ F] : f.completion.toContinuousLinearMap = f.toContinuousLinearMap.completion

@[simp]

theorem LinearIsometry.toAddMonoidHom_completion {E : Type u_3} {F : Type u_5} {R : Type u_7} {R₂ : Type u_8} [Semiring R] [Semiring R₂] [SeminormedAddCommGroup E] [Module R E] [IsUniformAddGroup E] [UniformContinuousConstSMul R E] [NormedAddCommGroup F] [Module R₂ F] {σ₁₂ : R →+* R₂} (f : E →ₛₗᵢ[σ₁₂] F) [UniformContinuousConstSMul R₂ F] : f.completion.toAddMonoidHom = f.toAddMonoidHom.completion ⋯