Documentation

Mathlib.Analysis.Normed.Module.RCLike.Extend

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

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

source
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.

source
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
Instances For
    source
    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
    source
    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
    source
    @[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ₗ
    source
    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.

    source
    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‖.

    source
    @[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‖
    source
    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
    Instances For
      source
      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
      source
      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
      source
      @[simp]
      theorem StrongDual.toLinearEquiv_extendRCLikeₗᵢ {𝕜 : Type u_1} {F : Type u_3} [RCLike 𝕜] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedSpace ℝ F] [IsScalarTower ℝ 𝕜 F] :
      extendRCLikeₗᵢ.toLinearEquiv = extendRCLikeₗ
      source
      @[simp]
      theorem StrongDual.toContinuousLinearEquiv_extendRCLikeₗᵢ {𝕜 : Type u_1} {F : Type u_3} [RCLike 𝕜] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedSpace ℝ F] [IsScalarTower ℝ 𝕜 F] :
      ↑extendRCLikeₗᵢ = extendRCLikeL
      source
      @[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‖.

      source
      @[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.

      source
      @[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.