The complexification of a real seminormed space

For a real normed space X, the complexification X_ℂ = X ⊕ i X is the complex vector space of formal sums x + i y with x y : X, where (a + b i) • (x + i y) = (a x - b y) + i (b x + a y). It is the standard device for applying complex-analytic spectral theory to operators on a real Banach space: a bounded real operator T extends to the complex-linear operator T_ℂ (x + i y) = T x + i T y.

There are many equivalent complex norms on X_ℂ; this file uses the Taylor norm

‖z‖ = ⨆ w ∈ 𝕋, ‖Re (w • z)‖,

that is, ‖x + i y‖ = sup_θ ‖cos θ • x - sin θ • y‖. With this norm the passage from X to X_ℂ loses no constants:

• the embedding x ↦ x + i 0 is an isometry (TauCeti.Complexification.norm_ofReal);
• the real and imaginary parts are bounded by the norm, and the norm by their sum (norm_re_le, norm_im_le, norm_le_norm_re_add_norm_im), so X_ℂ carries the product topology and is complete whenever X is;
• the complexification of a bounded operator has the same operator norm (ContinuousLinearMap.norm_complexify).

Together with ContinuousLinearMap.complexify_comp, the last point means that an operator-norm estimate for real operators, such as a growth bound ‖S t‖ ≤ M e^{ω t} for a family of operators or a bound ‖Rⁿ‖ ≤ C on the powers of one operator, holds verbatim for their complexifications. (On a real Hilbert space the Taylor norm is in general not the Hilbert norm √(‖x‖² + ‖y‖²); the two are equivalent.)

The construction, estimates, product equivalence, and extension of bounded operators also work for real seminormed spaces, giving a Taylor seminorm. Definiteness is needed only to obtain the NormedAddCommGroup instance from this seminormed structure.

Main declarations

• TauCeti.Complexification: the complexification of a real vector space, with its complex module structure.
• TauCeti.Complexification.ofReal, TauCeti.Complexification.re_add_I_smul_im: the real embedding, and the decomposition z = re z + i im z.
• TauCeti.Complexification.norm_le_iff: the characterization of the Taylor seminorm by bounds on the real parts of rotations.
• TauCeti.Complexification.instNormedSpace, TauCeti.Complexification.instCompleteSpace: the complex seminormed space structure, complete when X is.
• TauCeti.Complexification.equivProd: X_ℂ is real-linearly homeomorphic to X × X.
• ContinuousLinearMap.complexify: the complex-linear extension of a bounded real operator, with ContinuousLinearMap.norm_complexify and the bundled ContinuousLinearMap.complexifyAlgHom.
• TauCeti.Complexification.ext_ofReal: complex-linear maps out of X_ℂ are determined on X, so T.complexify is the unique complex-linear extension of T.

References

• G. A. Muñoz, Y. Sarantopoulos, A. Tonge, Complexifications of real Banach spaces, polynomials and multilinear maps, Studia Math. 134 (1999), 1–33.

structure TauCeti.Complexification (X : Type u_1) : Type u_1

The complexification X ⊕ i X of a real vector space X: an element with real part re and imaginary part im stands for the formal sum re + i im.

• re : X

  The real part of an element of the complexification.

• im : X

  The imaginary part of an element of the complexification.

theorem TauCeti.Complexification.ext_iff {X : Type u_1} {x y : Complexification X} : x = y ↔ x.re = y.re ∧ x.im = y.im

theorem TauCeti.Complexification.ext {X : Type u_1} {x y : Complexification X} (re : x.re = y.re) (im : x.im = y.im) : x = y

@[instance_reducible]

instance TauCeti.Complexification.instZero {X : Type u_1} [Zero X] : Zero (Complexification X)

Equations

• TauCeti.Complexification.instZero = { zero := { re := 0, im := 0 } }

@[instance_reducible]

instance TauCeti.Complexification.instAdd {X : Type u_1} [Add X] : Add (Complexification X)

Equations

• TauCeti.Complexification.instAdd = { add := fun (z w : TauCeti.Complexification X) => { re := z.re + w.re, im := z.im + w.im } }

@[instance_reducible]

instance TauCeti.Complexification.instNeg {X : Type u_1} [Neg X] : Neg (Complexification X)

Equations

• TauCeti.Complexification.instNeg = { neg := fun (z : TauCeti.Complexification X) => { re := -z.re, im := -z.im } }

@[instance_reducible]

instance TauCeti.Complexification.instSub {X : Type u_1} [Sub X] : Sub (Complexification X)

Equations

• TauCeti.Complexification.instSub = { sub := fun (z w : TauCeti.Complexification X) => { re := z.re - w.re, im := z.im - w.im } }

@[instance_reducible]

instance TauCeti.Complexification.instSMulNat {X : Type u_1} [SMul ℕ X] : SMul ℕ (Complexification X)

Equations

• TauCeti.Complexification.instSMulNat = { smul := fun (n : ℕ) (z : TauCeti.Complexification X) => { re := n • z.re, im := n • z.im } }

@[instance_reducible]

instance TauCeti.Complexification.instSMulInt {X : Type u_1} [SMul ℤ X] : SMul ℤ (Complexification X)

Equations

• TauCeti.Complexification.instSMulInt = { smul := fun (n : ℤ) (z : TauCeti.Complexification X) => { re := n • z.re, im := n • z.im } }

@[simp]

theorem TauCeti.Complexification.zero_re {X : Type u_1} [Zero X] : re 0 = 0

@[simp]

theorem TauCeti.Complexification.zero_im {X : Type u_1} [Zero X] : im 0 = 0

@[simp]

theorem TauCeti.Complexification.add_re {X : Type u_1} [Add X] (z w : Complexification X) : (z + w).re = z.re + w.re

@[simp]

theorem TauCeti.Complexification.add_im {X : Type u_1} [Add X] (z w : Complexification X) : (z + w).im = z.im + w.im

@[simp]

theorem TauCeti.Complexification.neg_re {X : Type u_1} [Neg X] (z : Complexification X) : (-z).re = -z.re

@[simp]

theorem TauCeti.Complexification.neg_im {X : Type u_1} [Neg X] (z : Complexification X) : (-z).im = -z.im

@[simp]

theorem TauCeti.Complexification.sub_re {X : Type u_1} [Sub X] (z w : Complexification X) : (z - w).re = z.re - w.re

@[simp]

theorem TauCeti.Complexification.sub_im {X : Type u_1} [Sub X] (z w : Complexification X) : (z - w).im = z.im - w.im

@[instance_reducible]

instance TauCeti.Complexification.instAddCommGroup {X : Type u_1} [AddCommGroup X] : AddCommGroup (Complexification X)

Equations

• TauCeti.Complexification.instAddCommGroup = Function.Injective.addCommGroup (fun (z : TauCeti.Complexification X) => (z.re, z.im)) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

def TauCeti.Complexification.ofReal {X : Type u_1} [Zero X] (x : X) : Complexification X

The embedding x ↦ x + i 0 of a real vector space into its complexification.

Equations

• TauCeti.Complexification.ofReal x = { re := x, im := 0 }

@[simp]

theorem TauCeti.Complexification.ofReal_re {X : Type u_1} [Zero X] (x : X) : (ofReal x).re = x

@[simp]

theorem TauCeti.Complexification.ofReal_im {X : Type u_1} [Zero X] (x : X) : (ofReal x).im = 0

@[instance_reducible]

instance TauCeti.Complexification.instSMulComplex {X : Type u_1} [AddCommGroup X] [Module ℝ X] : SMul ℂ (Complexification X)

Complex scalars act by (a + b i) • (x + i y) = (a x - b y) + i (b x + a y).

Equations

• TauCeti.Complexification.instSMulComplex = { smul := fun (c : ℂ) (z : TauCeti.Complexification X) => { re := c.re • z.re - c.im • z.im, im := c.im • z.re + c.re • z.im } }

@[simp]

theorem TauCeti.Complexification.smul_re {X : Type u_1} [AddCommGroup X] [Module ℝ X] (c : ℂ) (z : Complexification X) : (c • z).re = c.re • z.re - c.im • z.im

@[simp]

theorem TauCeti.Complexification.smul_im {X : Type u_1} [AddCommGroup X] [Module ℝ X] (c : ℂ) (z : Complexification X) : (c • z).im = c.im • z.re + c.re • z.im

@[instance_reducible]

instance TauCeti.Complexification.instModuleComplex {X : Type u_1} [AddCommGroup X] [Module ℝ X] : Module ℂ (Complexification X)

Equations

• TauCeti.Complexification.instModuleComplex = { toSMul := TauCeti.Complexification.instSMulComplex, mul_smul := ⋯, one_smul := ⋯, smul_zero := ⋯, smul_add := ⋯, add_smul := ⋯, zero_smul := ⋯ }

@[simp]

theorem TauCeti.Complexification.real_smul_re {X : Type u_1} [AddCommGroup X] [Module ℝ X] (r : ℝ) (z : Complexification X) : (r • z).re = r • z.re

Real scalars act componentwise.

@[simp]

theorem TauCeti.Complexification.real_smul_im {X : Type u_1} [AddCommGroup X] [Module ℝ X] (r : ℝ) (z : Complexification X) : (r • z).im = r • z.im

Real scalars act componentwise.

theorem TauCeti.Complexification.re_add_I_smul_im {X : Type u_1} [AddCommGroup X] [Module ℝ X] (z : Complexification X) : ofReal z.re + Complex.I • ofReal z.im = z

Every element of the complexification is re + i im.

theorem TauCeti.Complexification.ext_ofReal {X : Type u_1} [AddCommGroup X] [Module ℝ X] {E : Type u_2} [AddCommGroup E] [Module ℂ E] {f g : Complexification X →ₗ[ℂ] E} (h : ∀ (x : X), f (ofReal x) = g (ofReal x)) : f = g

Complex-linear maps out of the complexification agree once they agree on real vectors.

@[instance_reducible]

noncomputable instance TauCeti.Complexification.instNorm {X : Type u_1} [SeminormedAddCommGroup X] [NormedSpace ℝ X] : Norm (Complexification X)

The Taylor seminorm ‖z‖ = ⨆ w ∈ 𝕋, ‖Re (w • z)‖ on the complexification.

Equations

• TauCeti.Complexification.instNorm = { norm := fun (z : TauCeti.Complexification X) => ⨆ (w : Circle), ‖(↑w • z).re‖ }

theorem TauCeti.Complexification.norm_def {X : Type u_1} [SeminormedAddCommGroup X] [NormedSpace ℝ X] (z : Complexification X) : ‖z‖ = ⨆ (w : Circle), ‖(↑w • z).re‖

theorem TauCeti.Complexification.norm_circle_smul_re_le {X : Type u_1} [SeminormedAddCommGroup X] [NormedSpace ℝ X] (w : Circle) (z : Complexification X) : ‖(↑w • z).re‖ ≤ ‖z‖

The seminorm of the real part of every rotation is bounded by the Taylor seminorm.

theorem TauCeti.Complexification.norm_le_iff {X : Type u_1} [SeminormedAddCommGroup X] [NormedSpace ℝ X] {z : Complexification X} {r : ℝ} : ‖z‖ ≤ r ↔ ∀ (w : Circle), ‖(↑w • z).re‖ ≤ r

The Taylor seminorm is the least bound on the real parts of all rotations.

theorem TauCeti.Complexification.norm_re_le {X : Type u_1} [SeminormedAddCommGroup X] [NormedSpace ℝ X] (z : Complexification X) : ‖z.re‖ ≤ ‖z‖

The seminorm of the real part is at most the Taylor seminorm.

theorem TauCeti.Complexification.norm_im_le {X : Type u_1} [SeminormedAddCommGroup X] [NormedSpace ℝ X] (z : Complexification X) : ‖z.im‖ ≤ ‖z‖

The seminorm of the imaginary part is at most the Taylor seminorm.

theorem TauCeti.Complexification.norm_le_norm_re_add_norm_im {X : Type u_1} [SeminormedAddCommGroup X] [NormedSpace ℝ X] (z : Complexification X) : ‖z‖ ≤ ‖z.re‖ + ‖z.im‖

The Taylor seminorm is at most the sum of the seminorms of the two components.

theorem TauCeti.Complexification.norm_smul_re_le {X : Type u_1} [SeminormedAddCommGroup X] [NormedSpace ℝ X] (c : ℂ) (z : Complexification X) : ‖(c • z).re‖ ≤ ‖c‖ * ‖z‖

The seminorm of the real part of a complex multiple is bounded by the scalar norm times the Taylor seminorm.

@[simp]

theorem TauCeti.Complexification.norm_ofReal {X : Type u_1} [SeminormedAddCommGroup X] [NormedSpace ℝ X] (x : X) : ‖ofReal x‖ = ‖x‖

theorem TauCeti.Complexification.seminormedSpaceCore {X : Type u_1} [SeminormedAddCommGroup X] [NormedSpace ℝ X] : SeminormedSpace.Core ℂ (Complexification X)

The Taylor seminorm satisfies the axioms of a complex seminormed space.

@[instance_reducible]

noncomputable instance TauCeti.Complexification.instSeminormedAddCommGroup {X : Type u_1} [SeminormedAddCommGroup X] [NormedSpace ℝ X] : SeminormedAddCommGroup (Complexification X)

Equations

• TauCeti.Complexification.instSeminormedAddCommGroup = SeminormedAddCommGroup.ofCore ⋯

@[instance_reducible]

instance TauCeti.Complexification.instNormedSpace {X : Type u_1} [SeminormedAddCommGroup X] [NormedSpace ℝ X] : NormedSpace ℂ (Complexification X)

The complexification carries the complex seminormed space structure from its Taylor seminorm.

Equations

• TauCeti.Complexification.instNormedSpace = { toModule := TauCeti.Complexification.instModuleComplex, norm_smul_le := ⋯ }

noncomputable def TauCeti.Complexification.reCLM (X : Type u_1) [SeminormedAddCommGroup X] [NormedSpace ℝ X] : Complexification X →L[ℝ] X

The real part, as a bounded real-linear map of norm at most one.

Equations

• TauCeti.Complexification.reCLM X = { toFun := TauCeti.Complexification.re, map_add' := ⋯, map_smul' := ⋯ }.mkContinuous 1 ⋯

noncomputable def TauCeti.Complexification.imCLM (X : Type u_1) [SeminormedAddCommGroup X] [NormedSpace ℝ X] : Complexification X →L[ℝ] X

The imaginary part, as a bounded real-linear map of norm at most one.

Equations

• TauCeti.Complexification.imCLM X = { toFun := TauCeti.Complexification.im, map_add' := ⋯, map_smul' := ⋯ }.mkContinuous 1 ⋯

def TauCeti.Complexification.ofRealLI (X : Type u_1) [SeminormedAddCommGroup X] [NormedSpace ℝ X] : X →ₗᵢ[ℝ] Complexification X

The real embedding, as a real-linear isometry.

Equations

• TauCeti.Complexification.ofRealLI X = { toFun := TauCeti.Complexification.ofReal, map_add' := ⋯, map_smul' := ⋯, norm_map' := ⋯ }

@[simp]

theorem TauCeti.Complexification.reCLM_apply {X : Type u_1} [SeminormedAddCommGroup X] [NormedSpace ℝ X] (z : Complexification X) : (reCLM X) z = z.re

@[simp]

theorem TauCeti.Complexification.imCLM_apply {X : Type u_1} [SeminormedAddCommGroup X] [NormedSpace ℝ X] (z : Complexification X) : (imCLM X) z = z.im

@[simp]

theorem TauCeti.Complexification.ofRealLI_apply {X : Type u_1} [SeminormedAddCommGroup X] [NormedSpace ℝ X] (x : X) : (ofRealLI X) x = ofReal x

noncomputable def TauCeti.Complexification.equivProd (X : Type u_1) [SeminormedAddCommGroup X] [NormedSpace ℝ X] : Complexification X ≃L[ℝ] X × X

The complexification is real-linearly homeomorphic to X × X via z ↦ (re z, im z).

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.Complexification.equivProd_apply {X : Type u_1} [SeminormedAddCommGroup X] [NormedSpace ℝ X] (z : Complexification X) : (equivProd X) z = (z.re, z.im)

@[simp]

theorem TauCeti.Complexification.equivProd_symm_apply {X : Type u_1} [SeminormedAddCommGroup X] [NormedSpace ℝ X] (p : X × X) : (equivProd X).symm p = { re := p.1, im := p.2 }

instance TauCeti.Complexification.instCompleteSpace {X : Type u_1} [SeminormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] : CompleteSpace (Complexification X)

The complexification is complete whenever the original real seminormed space is complete.

@[instance_reducible]

noncomputable instance TauCeti.Complexification.instNormedAddCommGroup {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] : NormedAddCommGroup (Complexification X)

The Taylor seminorm is a norm when the original real seminorm is a norm.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def ContinuousLinearMap.complexify {X : Type u_1} {Y : Type u_2} [SeminormedAddCommGroup X] [NormedSpace ℝ X] [SeminormedAddCommGroup Y] [NormedSpace ℝ Y] (T : X →L[ℝ] Y) : TauCeti.Complexification X →L[ℂ] TauCeti.Complexification Y

The complexification T_ℂ (x + i y) = T x + i T y of a bounded real operator, a bounded complex-linear operator.

Equations

• T.complexify = { toFun := fun (z : TauCeti.Complexification X) => { re := T z.re, im := T z.im }, map_add' := ⋯, map_smul' := ⋯ }.mkContinuous ‖T‖ ⋯

@[simp]

theorem ContinuousLinearMap.complexify_apply_re {X : Type u_1} {Y : Type u_2} [SeminormedAddCommGroup X] [NormedSpace ℝ X] [SeminormedAddCommGroup Y] [NormedSpace ℝ Y] (T : X →L[ℝ] Y) (z : TauCeti.Complexification X) : (T.complexify z).re = T z.re

@[simp]

theorem ContinuousLinearMap.complexify_apply_im {X : Type u_1} {Y : Type u_2} [SeminormedAddCommGroup X] [NormedSpace ℝ X] [SeminormedAddCommGroup Y] [NormedSpace ℝ Y] (T : X →L[ℝ] Y) (z : TauCeti.Complexification X) : (T.complexify z).im = T z.im

@[simp]

theorem ContinuousLinearMap.complexify_ofReal {X : Type u_1} {Y : Type u_2} [SeminormedAddCommGroup X] [NormedSpace ℝ X] [SeminormedAddCommGroup Y] [NormedSpace ℝ Y] (T : X →L[ℝ] Y) (x : X) : T.complexify (TauCeti.Complexification.ofReal x) = TauCeti.Complexification.ofReal (T x)

theorem ContinuousLinearMap.eq_complexify_iff {X : Type u_1} {Y : Type u_2} [SeminormedAddCommGroup X] [NormedSpace ℝ X] [SeminormedAddCommGroup Y] [NormedSpace ℝ Y] (T : X →L[ℝ] Y) (S : TauCeti.Complexification X →L[ℂ] TauCeti.Complexification Y) : S = T.complexify ↔ ∀ (x : X), S (TauCeti.Complexification.ofReal x) = TauCeti.Complexification.ofReal (T x)

The complexification is the unique complex-linear extension of T.

@[simp]

theorem ContinuousLinearMap.norm_complexify {X : Type u_1} {Y : Type u_2} [SeminormedAddCommGroup X] [NormedSpace ℝ X] [SeminormedAddCommGroup Y] [NormedSpace ℝ Y] (T : X →L[ℝ] Y) : ‖T.complexify‖ = ‖T‖

Complexification preserves the operator norm.

@[simp]

theorem ContinuousLinearMap.complexify_id {X : Type u_1} [SeminormedAddCommGroup X] [NormedSpace ℝ X] : (ContinuousLinearMap.id ℝ X).complexify = ContinuousLinearMap.id ℂ (TauCeti.Complexification X)

Complexification preserves identity maps.

@[simp]

theorem ContinuousLinearMap.complexify_comp {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [SeminormedAddCommGroup X] [NormedSpace ℝ X] [SeminormedAddCommGroup Y] [NormedSpace ℝ Y] [SeminormedAddCommGroup Z] [NormedSpace ℝ Z] (T : Y →L[ℝ] Z) (S : X →L[ℝ] Y) : (T ∘SL S).complexify = T.complexify ∘SL S.complexify

Complexification preserves composition of bounded operators.

noncomputable def ContinuousLinearMap.complexifyₗᵢ (X : Type u_1) (Y : Type u_2) [SeminormedAddCommGroup X] [NormedSpace ℝ X] [SeminormedAddCommGroup Y] [NormedSpace ℝ Y] : (X →L[ℝ] Y) →ₗᵢ[ℝ] TauCeti.Complexification X →L[ℂ] TauCeti.Complexification Y

Complexification of bounded operators, as a real-linear isometry.

Equations

• ContinuousLinearMap.complexifyₗᵢ X Y = { toFun := ContinuousLinearMap.complexify, map_add' := ⋯, map_smul' := ⋯, norm_map' := ⋯ }

noncomputable def ContinuousLinearMap.complexifyAlgHom (X : Type u_1) [SeminormedAddCommGroup X] [NormedSpace ℝ X] : (X →L[ℝ] X) →ₐ[ℝ] TauCeti.Complexification X →L[ℂ] TauCeti.Complexification X

Complexification of bounded endomorphisms, as a homomorphism of real algebras.

Equations

• ContinuousLinearMap.complexifyAlgHom X = { toFun := ContinuousLinearMap.complexify, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯, commutes' := ⋯ }

@[simp]

theorem ContinuousLinearMap.complexifyₗᵢ_apply {X : Type u_1} {Y : Type u_2} [SeminormedAddCommGroup X] [NormedSpace ℝ X] [SeminormedAddCommGroup Y] [NormedSpace ℝ Y] (T : X →L[ℝ] Y) : (complexifyₗᵢ X Y) T = T.complexify

@[simp]

theorem ContinuousLinearMap.complexifyAlgHom_apply {X : Type u_1} [SeminormedAddCommGroup X] [NormedSpace ℝ X] (T : X →L[ℝ] X) : (complexifyAlgHom X) T = T.complexify

@[simp]

theorem ContinuousLinearMap.complexify_pow {X : Type u_1} [SeminormedAddCommGroup X] [NormedSpace ℝ X] (T : X →L[ℝ] X) (n : ℕ) : (T ^ n).complexify = T.complexify ^ n

Complexification preserves natural powers of bounded endomorphisms.