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.

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ₗᵢ_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

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

@[deprecated StrongDual.norm_extendRCLike_bound (since := "2026-02-24")]

theorem ContinuousLinearMap.norm_extendTo𝕜'_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‖

Alias of StrongDual.norm_extendRCLike_bound.

---

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

@[deprecated StrongDual.norm_extendRCLike (since := "2026-02-24")]

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

Alias of StrongDual.norm_extendRCLike.

@[deprecated StrongDual.norm_extendRCLike (since := "2026-02-24")]

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

Alias of StrongDual.norm_extendRCLike.