Extending an ℝ-linear functional to a 𝕜-linear functional

In this file we provide a way to extend a (optionally, 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.

In Analysis/Normed/Module/RCLike/Extend.lean we show that this extension is isometric. This is separate to avoid importing material about the operator norm into files about more elementary properties, like locally convex spaces.

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 : Module.Dual ℝ F) : Module.Dual 𝕜 F

Extend fr : Dual ℝ F to Dual 𝕜 F in a way that will also be continuous and have its norm (as a continuous linear map) equal to ‖fr‖ when fr is itself continuous on a normed space.

Equations

• LinearMap.extendTo𝕜' fr = { 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 : Module.Dual ℝ F) (x : F) : (extendTo𝕜' fr) 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 : Module.Dual ℝ F) (x : F) : RCLike.re ((extendTo𝕜' fr) 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 : Module.Dual ℝ F) (x : F) : ‖(extendTo𝕜' fr) x‖ ^ 2 = fr ((starRingEnd 𝕜) ((extendTo𝕜' fr) x) • x)

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

Equations

• LinearMap.instNormedSpaceRestrictScalarsReal = inferInstanceAs (NormedSpace 𝕜 F)

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

Extend fr : Dual ℝ (RestrictScalars ℝ 𝕜 F) to Dual 𝕜 F.

Equations

• LinearMap.extendTo𝕜 fr = LinearMap.extendTo𝕜' fr

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] [NormedSpace ℝ F] [IsScalarTower ℝ 𝕜 F] (fr : StrongDual ℝ F) : StrongDual 𝕜 F

Extend fr : StrongDual ℝ F to StrongDual 𝕜 F.

It would be possible to use LinearMap.mkContinuous here, but we would need to know that the continuity of fr implies it has bounded norm and we want to avoid that dependency here.

Norm properties of this extension can be found in Mathlib/Analysis/Normed/Module/RCLike/Extend.lean.

Equations

• ContinuousLinearMap.extendTo𝕜' fr = { toLinearMap := (↑fr).extendTo𝕜', cont := ⋯ }

theorem ContinuousLinearMap.extendTo𝕜'_apply {𝕜 : Type u_1} [RCLike 𝕜] {F : Type u_2} [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedSpace ℝ F] [IsScalarTower ℝ 𝕜 F] (fr : StrongDual ℝ F) (x : F) : (extendTo𝕜' fr) 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 : StrongDual ℝ (RestrictScalars ℝ 𝕜 F)) : StrongDual 𝕜 F

Extend fr : StrongDual ℝ (RestrictScalars ℝ 𝕜 F) to StrongDual 𝕜 F.

Equations

• ContinuousLinearMap.extendTo𝕜 fr = ContinuousLinearMap.extendTo𝕜' fr

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