# mathlib3documentation

analysis.normed_space.extend

# Extending a continuous β-linear map to a continuous π-linear map #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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} [normed_space π 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} [normed_space π F] [ F] [ π F] (fr : F ββ[β] β) (x : F) :
@[simp]
theorem linear_map.extend_to_π'_apply_re {π : Type u_1} [is_R_or_C π] {F : Type u_2} [normed_space π F] [ F] [ π F] (fr : F ββ[β] β) (x : F) :
theorem linear_map.norm_extend_to_π'_apply_sq {π : Type u_1} [is_R_or_C π] {F : Type u_2} [normed_space π F] [ F] [ π F] (f : F ββ[β] β) (x : F) :
theorem continuous_linear_map.norm_extend_to_π'_bound {π : Type u_1} [is_R_or_C π] {F : Type u_2} [normed_space π 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} [normed_space π 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} [normed_space π F] [ F] [ π F] (fr : F βL[β] β) (x : F) :
@[simp]
theorem continuous_linear_map.norm_extend_to_π' {π : Type u_1} [is_R_or_C π] {F : Type u_2} [normed_space π F] [ F] [ π F] (fr : F βL[β] β) :
noncomputable def linear_map.extend_to_π {π : Type u_1} [is_R_or_C π] {F : Type u_2} [normed_space π F] (fr : π F ββ[β] β) :
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} [normed_space π F] (fr : π F ββ[β] β) (x : F) :
noncomputable def continuous_linear_map.extend_to_π {π : Type u_1} [is_R_or_C π] {F : Type u_2} [normed_space π F] (fr : π F β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} [normed_space π F] (fr : π F βL[β] β) (x : F) :
@[simp]
theorem continuous_linear_map.norm_extend_to_π {π : Type u_1} [is_R_or_C π] {F : Type u_2} [normed_space π F] (fr : π F βL[β] β) :