# 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 `Mathlib/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.

source
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' := ⋯ }

Instances For

source
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))
source
@[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
source
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)
source
instance LinearMap.instNormedSpaceRestrictScalarsReal {𝕜 : Type u_1} [RCLike 𝕜] {F : Type u_2} [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] :
NormedSpace 𝕜 (RestrictScalars ℝ 𝕜 F)
Equations

- LinearMap.instNormedSpaceRestrictScalarsReal = inferInstanceAs (NormedSpace 𝕜 F)

source
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

Instances For

source
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))
source
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 := ⋯ }

Instances For

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

Instances For

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