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 #
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.
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
- fr.extend_to_π' = let fc : F β π := Ξ» (x : F), β(βfr x) - is_R_or_C.I * β(βfr (is_R_or_C.I β’ x)) in {to_fun := fc, map_add' := _, map_smul' := _}
The norm of the extension is bounded by β₯frβ₯
.
Extend fr : F βL[β] β
to F βL[π] π
.
Equations
Extend fr : restrict_scalars β π F ββ[β] β
to F ββ[π] π
.
Equations
- fr.extend_to_π = fr.extend_to_π'
Extend fr : restrict_scalars β π F βL[β] β
to F βL[π] π
.
Equations
- fr.extend_to_π = fr.extend_to_π'