Extending a continuous ℝ-linear map to a continuous 𝕜-linear map

In this file we provide a way to extend a continuous ℝ-linear map to a continuous 𝕜-linear map in a way that bounds the norm by the norm of the original map, when 𝕜 is either ℝ (the extension is trivial) or ℂ. We formulate the extension uniformly, by assuming RCLike 𝕜.

We motivate the form of the extension as follows. Note that fc : F →ₗ[𝕜] 𝕜 is determined fully by re fc: for all x : F, fc (I • x) = I * fc x, so im (fc x) = -re (fc (I • x)). Therefore, given an fr : F →ₗ[ℝ] ℝ, we define fc x = fr x - fr (I • x) * I.

Main definitions

• LinearMap.extendTo𝕜
• ContinuousLinearMap.extendTo𝕜

Implementation details

For convenience, the main definitions above operate in terms of RestrictScalars ℝ 𝕜 F. Alternate forms which operate on [IsScalarTower ℝ 𝕜 F] instead are provided with a primed name.

noncomputable def LinearMap.extendTo𝕜' {𝕜 : Type u_1} [RCLike 𝕜] {F : Type u_2} [AddCommGroup F] [Module ℝ F] [Module 𝕜 F] [IsScalarTower ℝ 𝕜 F] (fr : F →ₗ[ℝ] ℝ) : F →ₗ[𝕜] 𝕜

Extend fr : F →ₗ[ℝ] ℝ to F →ₗ[𝕜] 𝕜 in a way that will also be continuous and have its norm bounded by ‖fr‖ if fr is continuous.

Equations

• fr.extendTo𝕜' = { toFun := fun (x : F) => ↑(fr x) - RCLike.I * ↑(fr (RCLike.I • x)), map_add' := ⋯, map_smul' := ⋯ }

theorem LinearMap.extendTo𝕜'_apply {𝕜 : Type u_1} [RCLike 𝕜] {F : Type u_2} [AddCommGroup F] [Module ℝ F] [Module 𝕜 F] [IsScalarTower ℝ 𝕜 F] (fr : F →ₗ[ℝ] ℝ) (x : F) : fr.extendTo𝕜' x = ↑(fr x) - RCLike.I * ↑(fr (RCLike.I • x))

@[simp]

theorem LinearMap.extendTo𝕜'_apply_re {𝕜 : Type u_1} [RCLike 𝕜] {F : Type u_2} [AddCommGroup F] [Module ℝ F] [Module 𝕜 F] [IsScalarTower ℝ 𝕜 F] (fr : F →ₗ[ℝ] ℝ) (x : F) : RCLike.re (fr.extendTo𝕜' x) = fr x

theorem LinearMap.norm_extendTo𝕜'_apply_sq {𝕜 : Type u_1} [RCLike 𝕜] {F : Type u_2} [AddCommGroup F] [Module ℝ F] [Module 𝕜 F] [IsScalarTower ℝ 𝕜 F] (fr : F →ₗ[ℝ] ℝ) (x : F) : ‖fr.extendTo𝕜' x‖ ^ 2 = fr ((starRingEnd 𝕜) (fr.extendTo𝕜' x) • x)

theorem ContinuousLinearMap.norm_extendTo𝕜'_bound {𝕜 : Type u_1} [RCLike 𝕜] {F : Type u_2} [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedSpace ℝ F] [IsScalarTower ℝ 𝕜 F] (fr : F →L[ℝ] ℝ) (x : F) : ‖(↑fr).extendTo𝕜' x‖ ≤ ‖fr‖ * ‖x‖

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

noncomputable def ContinuousLinearMap.extendTo𝕜' {𝕜 : Type u_1} [RCLike 𝕜] {F : Type u_2} [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedSpace ℝ F] [IsScalarTower ℝ 𝕜 F] (fr : F →L[ℝ] ℝ) : F →L[𝕜] 𝕜

Extend fr : F →L[ℝ] ℝ to F →L[𝕜] 𝕜.

Equations

• fr.extendTo𝕜' = (↑fr).extendTo𝕜'.mkContinuous ‖fr‖ ⋯

theorem ContinuousLinearMap.extendTo𝕜'_apply {𝕜 : Type u_1} [RCLike 𝕜] {F : Type u_2} [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedSpace ℝ F] [IsScalarTower ℝ 𝕜 F] (fr : F →L[ℝ] ℝ) (x : F) : fr.extendTo𝕜' x = ↑(fr x) - RCLike.I * ↑(fr (RCLike.I • x))

@[simp]

theorem ContinuousLinearMap.norm_extendTo𝕜' {𝕜 : Type u_1} [RCLike 𝕜] {F : Type u_2} [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedSpace ℝ F] [IsScalarTower ℝ 𝕜 F] (fr : F →L[ℝ] ℝ) : ‖fr.extendTo𝕜'‖ = ‖fr‖

instance instNormedSpaceRestrictScalarsReal {𝕜 : Type u_1} [RCLike 𝕜] {F : Type u_2} [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] : NormedSpace 𝕜 (RestrictScalars ℝ 𝕜 F)

Equations

• instNormedSpaceRestrictScalarsReal = id inferInstance

noncomputable def LinearMap.extendTo𝕜 {𝕜 : Type u_1} [RCLike 𝕜] {F : Type u_2} [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] (fr : RestrictScalars ℝ 𝕜 F →ₗ[ℝ] ℝ) : F →ₗ[𝕜] 𝕜

Extend fr : RestrictScalars ℝ 𝕜 F →ₗ[ℝ] ℝ to F →ₗ[𝕜] 𝕜.

Equations

• fr.extendTo𝕜 = fr.extendTo𝕜'

theorem LinearMap.extendTo𝕜_apply {𝕜 : Type u_1} [RCLike 𝕜] {F : Type u_2} [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] (fr : RestrictScalars ℝ 𝕜 F →ₗ[ℝ] ℝ) (x : F) : fr.extendTo𝕜 x = ↑(fr x) - RCLike.I * ↑(fr (RCLike.I • x))

noncomputable def ContinuousLinearMap.extendTo𝕜 {𝕜 : Type u_1} [RCLike 𝕜] {F : Type u_2} [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] (fr : RestrictScalars ℝ 𝕜 F →L[ℝ] ℝ) : F →L[𝕜] 𝕜

Extend fr : RestrictScalars ℝ 𝕜 F →L[ℝ] ℝ to F →L[𝕜] 𝕜.

Equations

• fr.extendTo𝕜 = fr.extendTo𝕜'

theorem ContinuousLinearMap.extendTo𝕜_apply {𝕜 : Type u_1} [RCLike 𝕜] {F : Type u_2} [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] (fr : RestrictScalars ℝ 𝕜 F →L[ℝ] ℝ) (x : F) : fr.extendTo𝕜 x = ↑(fr x) - RCLike.I * ↑(fr (RCLike.I • x))

@[simp]

theorem ContinuousLinearMap.norm_extendTo𝕜 {𝕜 : Type u_1} [RCLike 𝕜] {F : Type u_2} [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] (fr : RestrictScalars ℝ 𝕜 F →L[ℝ] ℝ) : ‖fr.extendTo𝕜‖ = ‖fr‖