# 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} [NormedSpace đť•ś F] [] [IsScalarTower â„ť đť•ś F] (fr : ) :
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
• One or more equations did not get rendered due to their size.
Instances For
theorem LinearMap.extendTođť•ś'_apply {đť•ś : Type u_1} [RCLike đť•ś] {F : Type u_2} [NormedSpace đť•ś F] [] [IsScalarTower â„ť đť•ś F] (fr : ) (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} [NormedSpace đť•ś F] [] [IsScalarTower â„ť đť•ś F] (fr : ) (x : F) :
RCLike.re (fr.extendTođť•ś' x) = fr x
theorem LinearMap.norm_extendTođť•ś'_apply_sq {đť•ś : Type u_1} [RCLike đť•ś] {F : Type u_2} [NormedSpace đť•ś F] [] [IsScalarTower â„ť đť•ś F] (fr : ) (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} [NormedSpace đť•ś F] [] [IsScalarTower â„ť đť•ś F] (fr : ) (x : F) :
â€–fr.extendTođť•ś' xâ€– â‰¤

The norm of the extension is bounded by â€–frâ€–.

noncomputable def ContinuousLinearMap.extendTođť•ś' {đť•ś : Type u_1} [RCLike đť•ś] {F : Type u_2} [NormedSpace đť•ś F] [] [IsScalarTower â„ť đť•ś F] (fr : ) :
F â†’L[đť•ś] đť•ś

Extend fr : F â†’L[â„ť] â„ť to F â†’L[đť•ś] đť•ś.

Equations
• fr.extendTođť•ś' = fr.extendTođť•ś'.mkContinuous â€–frâ€– â‹Ż
Instances For
theorem ContinuousLinearMap.extendTođť•ś'_apply {đť•ś : Type u_1} [RCLike đť•ś] {F : Type u_2} [NormedSpace đť•ś F] [] [IsScalarTower â„ť đť•ś F] (fr : ) (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} [NormedSpace đť•ś F] [] [IsScalarTower â„ť đť•ś F] (fr : ) :
â€–fr.extendTođť•ś'â€– = â€–frâ€–
instance instNormedSpaceRestrictScalarsReal {đť•ś : Type u_1} [RCLike đť•ś] {F : Type u_2} [NormedSpace đť•ś F] :
NormedSpace đť•ś (RestrictScalars â„ť đť•ś F)
Equations
• instNormedSpaceRestrictScalarsReal = id inferInstance
noncomputable def LinearMap.extendTođť•ś {đť•ś : Type u_1} [RCLike đť•ś] {F : Type u_2} [NormedSpace đť•ś F] (fr : RestrictScalars â„ť đť•ś F â†’â‚—[â„ť] â„ť) :
F â†’â‚—[đť•ś] đť•ś

Extend fr : RestrictScalars â„ť đť•ś F â†’â‚—[â„ť] â„ť to F â†’â‚—[đť•ś] đť•ś.

Equations
• fr.extendTođť•ś = fr.extendTođť•ś'
Instances For
theorem LinearMap.extendTođť•ś_apply {đť•ś : Type u_1} [RCLike đť•ś] {F : Type u_2} [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} [NormedSpace đť•ś F] (fr : RestrictScalars â„ť đť•ś F â†’L[â„ť] â„ť) :
F â†’L[đť•ś] đť•ś

Extend fr : RestrictScalars â„ť đť•ś F â†’L[â„ť] â„ť to F â†’L[đť•ś] đť•ś.

Equations
• fr.extendTođť•ś = fr.extendTođť•ś'
Instances For
theorem ContinuousLinearMap.extendTođť•ś_apply {đť•ś : Type u_1} [RCLike đť•ś] {F : Type u_2} [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} [NormedSpace đť•ś F] (fr : RestrictScalars â„ť đť•ś F â†’L[â„ť] â„ť) :
â€–fr.extendTođť•śâ€– = â€–frâ€–