# mathlibdocumentation

analysis.normed_space.extend

# 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 is_R_or_C 𝕜.

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 #

• linear_map.extend_to_𝕜
• continuous_linear_map.extend_to_𝕜

## Implementation details #

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

noncomputable def linear_map.extend_to_𝕜' {𝕜 : Type u_1} [is_R_or_C 𝕜] {F : Type u_2} [ F] [ F] [ 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
theorem linear_map.extend_to_𝕜'_apply {𝕜 : Type u_1} [is_R_or_C 𝕜] {F : Type u_2} [ F] [ F] [ F] (fr : F →ₗ[] ) (x : F) :
theorem norm_bound {𝕜 : Type u_1} [is_R_or_C 𝕜] {F : Type u_2} [ F] [ F] [ F] (fr : F →L[] ) (x : F) :

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

noncomputable def continuous_linear_map.extend_to_𝕜' {𝕜 : Type u_1} [is_R_or_C 𝕜] {F : Type u_2} [ F] [ F] [ F] (fr : F →L[] ) :
F →L[𝕜] 𝕜

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

Equations
theorem continuous_linear_map.extend_to_𝕜'_apply {𝕜 : Type u_1} [is_R_or_C 𝕜] {F : Type u_2} [ F] [ F] [ F] (fr : F →L[] ) (x : F) :
noncomputable def linear_map.extend_to_𝕜 {𝕜 : Type u_1} [is_R_or_C 𝕜] {F : Type u_2} [ F] (fr : →ₗ[] ) :
F →ₗ[𝕜] 𝕜

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

Equations
theorem linear_map.extend_to_𝕜_apply {𝕜 : Type u_1} [is_R_or_C 𝕜] {F : Type u_2} [ F] (fr : →ₗ[] ) (x : F) :
noncomputable def continuous_linear_map.extend_to_𝕜 {𝕜 : Type u_1} [is_R_or_C 𝕜] {F : Type u_2} [ F] (fr : →L[] ) :
F →L[𝕜] 𝕜

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

Equations
theorem continuous_linear_map.extend_to_𝕜_apply {𝕜 : Type u_1} [is_R_or_C 𝕜] {F : Type u_2} [ F] (fr : →L[] ) (x : F) :