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 StrongDual.norm_extendRCLike_bound {𝕜 : Type u_1} {F : Type u_2} [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_2} [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_2} [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_2} [RCLike 𝕜] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedSpace ℝ F] [IsScalarTower ℝ 𝕜 F] (f : StrongDual 𝕜 F) : extendRCLikeₗᵢ.symm f = ContinuousLinearMap.comp RCLike.reCLM (ContinuousLinearMap.restrictScalars ℝ f)

theorem StrongDual.extendRCLikeₗᵢ_apply {𝕜 : Type u_1} {F : Type u_2} [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_2} [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_2} [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_2} [RCLike 𝕜] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedSpace ℝ F] [IsScalarTower ℝ 𝕜 F] (fr : StrongDual ℝ F) : ‖fr.extendRCLike‖ = ‖fr‖

Alias of StrongDual.norm_extendRCLike.