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.
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,
fr : F →ₗ[ℝ] ℝ, we define
fc x = fr x - fr (I • x) * I.
fr : F →ₗ[ℝ] ℝ to
F →ₗ[ℂ] ℂ in a way that will also be continuous and have its norm
fr is continuous.