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,
given an fr : F →ₗ[ℝ] ℝ, we define fc x = fr x - fr (I • x) * I.
Extend fr : F →ₗ[ℝ] ℝ to F →ₗ[ℂ] ℂ in a way that will also be continuous and have its norm
bounded by ∥fr∥ if fr is continuous.
The norm of the extension is bounded by ∥fr∥.
Extend fr : F →L[ℝ] ℝ to F →L[ℂ] ℂ.
Equations
- fr.extend_to_ℂ = fr.to_linear_map.extend_to_ℂ.mk_continuous ∥fr∥ _