Norm properties of the extension of continuous ℝ-linear functionals to 𝕜-linear functionals

This file shows that StrongDual.extendRCLike preserves the norm of the functional.

theorem Module.Dual.norm_extendRCLike_le_seminorm {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [AddCommGroup E] [Module 𝕜 E] [Module ℝ E] [IsScalarTower ℝ 𝕜 E] (fr : Dual ℝ E) {p : Seminorm 𝕜 E} (hp : ∀ (x : E), |fr x| ≤ p x) (x : E) : ‖fr.extendRCLike x‖ ≤ p x

If a real-linear functional is bounded by a 𝕜-seminorm, then its 𝕜-linear extension is bounded by the same seminorm.

noncomputable def StrongDual.extendRCLikeL {𝕜 : Type u_4} {F : Type u_5} [RCLike 𝕜] [TopologicalSpace F] [AddCommGroup F] [Module 𝕜 F] [ContinuousSMul 𝕜 F] [Module ℝ F] [IsScalarTower ℝ 𝕜 F] : StrongDual ℝ F ≃L[ℝ] StrongDual 𝕜 F

The extension StrongDual.extendRCLike as a continuous linear equivalence between the strong duals when scalar multiplication (by 𝕜) is jointly continuous.

Equations

• StrongDual.extendRCLikeL = { toLinearEquiv := StrongDual.extendRCLikeₗ, continuous_toFun := ⋯, continuous_invFun := ⋯ }

theorem StrongDual.extendRCLikeL_symm_apply {𝕜 : Type u_4} {F : Type u_5} [RCLike 𝕜] [TopologicalSpace F] [AddCommGroup F] [Module 𝕜 F] [ContinuousSMul 𝕜 F] [Module ℝ F] [IsScalarTower ℝ 𝕜 F] (f : StrongDual 𝕜 F) : extendRCLikeL.symm f = RCLike.reCLM ∘SL ContinuousLinearMap.restrictScalars ℝ f

theorem StrongDual.extendRCLikeL_apply {𝕜 : Type u_4} {F : Type u_5} [RCLike 𝕜] [TopologicalSpace F] [AddCommGroup F] [Module 𝕜 F] [ContinuousSMul 𝕜 F] [Module ℝ F] [IsScalarTower ℝ 𝕜 F] (fr : StrongDual ℝ F) : extendRCLikeL fr = fr.extendRCLike

@[simp]

theorem StrongDual.toLinearEquiv_extendRCLikeL {𝕜 : Type u_4} {F : Type u_5} [RCLike 𝕜] [TopologicalSpace F] [AddCommGroup F] [Module 𝕜 F] [ContinuousSMul 𝕜 F] [Module ℝ F] [IsScalarTower ℝ 𝕜 F] : ↑extendRCLikeL = extendRCLikeₗ

theorem StrongDual.norm_extendRCLike_le_seminorm {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [AddCommGroup E] [Module 𝕜 E] [Module ℝ E] [IsScalarTower ℝ 𝕜 E] [TopologicalSpace E] [ContinuousConstSMul 𝕜 E] (fr : StrongDual ℝ E) {p : Seminorm 𝕜 E} (hp : ∀ (x : E), |fr x| ≤ p x) (x : E) : ‖fr.extendRCLike x‖ ≤ p x

If a continuous real-linear functional is bounded by a 𝕜-seminorm, then its 𝕜-linear extension is bounded by the same seminorm.

theorem StrongDual.norm_extendRCLike_bound {𝕜 : Type u_1} {F : Type u_3} [RCLike 𝕜] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedSpace ℝ F] [IsScalarTower ℝ 𝕜 F] (fr : StrongDual ℝ F) (x : F) : ‖fr.extendRCLike x‖ ≤ ‖fr‖ * ‖x‖

The norm of the extension is bounded by ‖fr‖.

@[simp]

theorem StrongDual.norm_extendRCLike {𝕜 : Type u_1} {F : Type u_3} [RCLike 𝕜] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedSpace ℝ F] [IsScalarTower ℝ 𝕜 F] (fr : StrongDual ℝ F) : ‖fr.extendRCLike‖ = ‖fr‖

noncomputable def StrongDual.extendRCLikeₗᵢ {𝕜 : Type u_1} {F : Type u_3} [RCLike 𝕜] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedSpace ℝ F] [IsScalarTower ℝ 𝕜 F] : StrongDual ℝ F ≃ₗᵢ[ℝ] StrongDual 𝕜 F

StrongDual.extendRCLike bundled into a linear isometry equivalence.

Equations

• StrongDual.extendRCLikeₗᵢ = { toLinearEquiv := StrongDual.extendRCLikeₗ, norm_map' := ⋯ }

theorem StrongDual.extendRCLikeₗᵢ_apply {𝕜 : Type u_1} {F : Type u_3} [RCLike 𝕜] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedSpace ℝ F] [IsScalarTower ℝ 𝕜 F] (fr : StrongDual ℝ F) : extendRCLikeₗᵢ fr = fr.extendRCLike

theorem StrongDual.extendRCLikeₗᵢ_symm_apply {𝕜 : Type u_1} {F : Type u_3} [RCLike 𝕜] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedSpace ℝ F] [IsScalarTower ℝ 𝕜 F] (f : StrongDual 𝕜 F) : extendRCLikeₗᵢ.symm f = RCLike.reCLM ∘SL ContinuousLinearMap.restrictScalars ℝ f

@[simp]

theorem StrongDual.toLinearEquiv_extendRCLikeₗᵢ {𝕜 : Type u_1} {F : Type u_3} [RCLike 𝕜] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedSpace ℝ F] [IsScalarTower ℝ 𝕜 F] : extendRCLikeₗᵢ.toLinearEquiv = extendRCLikeₗ

@[simp]

theorem StrongDual.toContinuousLinearEquiv_extendRCLikeₗᵢ {𝕜 : Type u_1} {F : Type u_3} [RCLike 𝕜] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedSpace ℝ F] [IsScalarTower ℝ 𝕜 F] : ↑extendRCLikeₗᵢ = extendRCLikeL