mathlib3 documentation

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 #

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.

source
noncomputable def linear_map.extend_to_π•œ' {π•œ : Type u_1} [is_R_or_C π•œ] {F : Type u_2} [seminormed_add_comm_group F] [normed_space π•œ F] [module ℝ F] [is_scalar_tower ℝ π•œ 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
source
theorem linear_map.extend_to_π•œ'_apply {π•œ : Type u_1} [is_R_or_C π•œ] {F : Type u_2} [seminormed_add_comm_group F] [normed_space π•œ F] [module ℝ F] [is_scalar_tower ℝ π•œ F] (fr : F β†’β‚—[ℝ] ℝ) (x : F) :
⇑(fr.extend_to_π•œ') x = ↑(⇑fr x) - is_R_or_C.I * ↑(⇑fr (is_R_or_C.I β€’ x))
source
@[simp]
theorem linear_map.extend_to_π•œ'_apply_re {π•œ : Type u_1} [is_R_or_C π•œ] {F : Type u_2} [seminormed_add_comm_group F] [normed_space π•œ F] [module ℝ F] [is_scalar_tower ℝ π•œ F] (fr : F β†’β‚—[ℝ] ℝ) (x : F) :
⇑is_R_or_C.re (⇑(fr.extend_to_π•œ') x) = ⇑fr x
source
theorem linear_map.norm_extend_to_π•œ'_apply_sq {π•œ : Type u_1} [is_R_or_C π•œ] {F : Type u_2} [seminormed_add_comm_group F] [normed_space π•œ F] [module ℝ F] [is_scalar_tower ℝ π•œ F] (f : F β†’β‚—[ℝ] ℝ) (x : F) :
‖⇑(f.extend_to_π•œ') xβ€– ^ 2 = ⇑f (⇑(star_ring_end π•œ) (⇑(f.extend_to_π•œ') x) β€’ x)
source
theorem continuous_linear_map.norm_extend_to_π•œ'_bound {π•œ : Type u_1} [is_R_or_C π•œ] {F : Type u_2} [seminormed_add_comm_group F] [normed_space π•œ F] [normed_space ℝ F] [is_scalar_tower ℝ π•œ F] (fr : F β†’L[ℝ] ℝ) (x : F) :
‖⇑(fr.to_linear_map.extend_to_π•œ') xβ€– ≀ β€–frβ€– * β€–xβ€–

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

source
noncomputable def continuous_linear_map.extend_to_π•œ' {π•œ : Type u_1} [is_R_or_C π•œ] {F : Type u_2} [seminormed_add_comm_group F] [normed_space π•œ F] [normed_space ℝ F] [is_scalar_tower ℝ π•œ F] (fr : F β†’L[ℝ] ℝ) :
F β†’L[π•œ] π•œ

Extend fr : F β†’L[ℝ] ℝ to F β†’L[π•œ] π•œ.

Equations
source
theorem continuous_linear_map.extend_to_π•œ'_apply {π•œ : Type u_1} [is_R_or_C π•œ] {F : Type u_2} [seminormed_add_comm_group F] [normed_space π•œ F] [normed_space ℝ F] [is_scalar_tower ℝ π•œ F] (fr : F β†’L[ℝ] ℝ) (x : F) :
⇑(fr.extend_to_π•œ') x = ↑(⇑fr x) - is_R_or_C.I * ↑(⇑fr (is_R_or_C.I β€’ x))
source
@[simp]
theorem continuous_linear_map.norm_extend_to_π•œ' {π•œ : Type u_1} [is_R_or_C π•œ] {F : Type u_2} [seminormed_add_comm_group F] [normed_space π•œ F] [normed_space ℝ F] [is_scalar_tower ℝ π•œ F] (fr : F β†’L[ℝ] ℝ) :
β€–fr.extend_to_π•œ'β€– = β€–frβ€–
source
noncomputable def linear_map.extend_to_π•œ {π•œ : Type u_1} [is_R_or_C π•œ] {F : Type u_2} [seminormed_add_comm_group F] [normed_space π•œ F] (fr : restrict_scalars ℝ π•œ F β†’β‚—[ℝ] ℝ) :
F β†’β‚—[π•œ] π•œ

Extend fr : restrict_scalars ℝ π•œ F β†’β‚—[ℝ] ℝ to F β†’β‚—[π•œ] π•œ.

Equations
source
theorem linear_map.extend_to_π•œ_apply {π•œ : Type u_1} [is_R_or_C π•œ] {F : Type u_2} [seminormed_add_comm_group F] [normed_space π•œ F] (fr : restrict_scalars ℝ π•œ F β†’β‚—[ℝ] ℝ) (x : F) :
⇑(fr.extend_to_π•œ) x = ↑(⇑fr x) - is_R_or_C.I * ↑(⇑fr (is_R_or_C.I β€’ x))
source
noncomputable def continuous_linear_map.extend_to_π•œ {π•œ : Type u_1} [is_R_or_C π•œ] {F : Type u_2} [seminormed_add_comm_group F] [normed_space π•œ F] (fr : restrict_scalars ℝ π•œ F β†’L[ℝ] ℝ) :
F β†’L[π•œ] π•œ

Extend fr : restrict_scalars ℝ π•œ F β†’L[ℝ] ℝ to F β†’L[π•œ] π•œ.

Equations
source
theorem continuous_linear_map.extend_to_π•œ_apply {π•œ : Type u_1} [is_R_or_C π•œ] {F : Type u_2} [seminormed_add_comm_group F] [normed_space π•œ F] (fr : restrict_scalars ℝ π•œ F β†’L[ℝ] ℝ) (x : F) :
⇑(fr.extend_to_π•œ) x = ↑(⇑fr x) - is_R_or_C.I * ↑(⇑fr (is_R_or_C.I β€’ x))
source
@[simp]
theorem continuous_linear_map.norm_extend_to_π•œ {π•œ : Type u_1} [is_R_or_C π•œ] {F : Type u_2} [seminormed_add_comm_group F] [normed_space π•œ F] (fr : restrict_scalars ℝ π•œ F β†’L[ℝ] ℝ) :
β€–fr.extend_to_π•œβ€– = β€–frβ€–