The Hilbert-space complexification of a real inner product space

For a real inner product space X, the complexification X_ℂ = X ⊕ i X (TauCeti.Complexification X) carries the complex inner product

⟪x + i y, u + i v⟫ = (⟪x, u⟫ + ⟪y, v⟫) + i (⟪x, v⟫ - ⟪y, u⟫),

whose norm is the L² norm ‖x + i y‖ = √(‖x‖² + ‖y‖²). This is not the Taylor norm that TauCeti.Analysis.Normed.Module.Complexification puts on Complexification X: the two norms are equivalent but differ in general (for orthogonal unit vectors x and y, the Taylor norm of x + i y is 1 and its L² norm is √2). The Hilbert structure therefore lives on the type synonym WithLp 2 (Complexification X), just as Mathlib's L² product of two inner product spaces lives on WithLp 2 (E × F). As a real normed space, X_ℂ is isometric to the L² product WithLp 2 (X × X), so it is complete whenever X is.

A bounded real operator T : X →L[ℝ] Y complexifies to the bounded complex operator T_ℂ (x + i y) = T x + i T y, the WithLp lift of ContinuousLinearMap.complexify. For the L² norm, complexification is isometric and commutes with composition and with adjoints. For a real Hilbert space X, it is therefore an isometric ⋆-algebra embedding of the real C⋆-algebra X →L[ℝ] X into the complex C⋆-algebra X_ℂ →L[ℂ] X_ℂ. This is the standard device for transferring complex spectral theory, such as the continuous functional calculus of a self-adjoint operator, to operators on real Hilbert spaces.

Main declarations

• WithLp.instComplexificationInnerProductSpace: the complex inner product space WithLp 2 (Complexification X), with WithLp.complexification_re_inner and WithLp.complexification_im_inner computing the inner product from real and imaginary parts.
• WithLp.complexification_norm_sq_eq: ‖x + i y‖² = ‖x‖² + ‖y‖².
• WithLp.complexificationEquivProd: the real-linear isometric equivalence WithLp 2 (Complexification X) ≃ₗᵢ[ℝ] WithLp 2 (X × X), and WithLp.instComplexificationCompleteSpace as a consequence.
• ContinuousLinearMap.complexifyL2: the complexification of a bounded real operator, with ContinuousLinearMap.eq_complexifyL2_iff (it is the unique complex-linear extension), ContinuousLinearMap.norm_complexifyL2, ContinuousLinearMap.complexifyL2_comp and ContinuousLinearMap.adjoint_complexifyL2.
• ContinuousLinearMap.complexifyL2ₗᵢ: complexification as a real-linear isometry of operator spaces.
• ContinuousLinearMap.complexifyL2StarAlgHom: complexification of the bounded operators on a real Hilbert space, as a ⋆-algebra homomorphism over ℝ.
• ContinuousLinearMap.isClosedEmbedding_complexifyL2StarAlgHom: complexification of bounded operators is a closed embedding.
• ContinuousLinearMap.isSelfAdjoint_complexifyL2_iff: complexification preserves and reflects self-adjointness.

References

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

Acknowledgements

The Hilbert-space complexification, the complexification of bounded operators and its compatibility with adjoints also appear in ForTauCeti/Analysis/InnerProductSpace/Complexification/ of the AIQ DKPS formalization (Kitware, Inc.; Apache-2.0), on the carrier WithLp 2 (E × E). This file builds the same structure on top of Tau Ceti's algebraic Complexification.

@[instance_reducible]

noncomputable instance WithLp.instComplexificationNormedAddCommGroup {X : Type u_1} [NormedAddCommGroup X] : NormedAddCommGroup (WithLp 2 (TauCeti.Complexification X))

The L² norm ‖x + i y‖ = √(‖x‖² + ‖y‖²) on the complexification, induced from the L² product WithLp 2 (X × X) along the coordinates z ↦ (re z, im z).

theorem WithLp.complexification_norm_eq {X : Type u_1} [NormedAddCommGroup X] (z : WithLp 2 (TauCeti.Complexification X)) : ‖z‖ = ‖toLp 2 (z.ofLp.re, z.ofLp.im)‖

The L² norm of x + i y is the norm of (x, y) in the L² product.

theorem WithLp.complexification_norm_sq_eq {X : Type u_1} [NormedAddCommGroup X] (z : WithLp 2 (TauCeti.Complexification X)) : ‖z‖ ^ 2 = ‖z.ofLp.re‖ ^ 2 + ‖z.ofLp.im‖ ^ 2

The squared L² norm of x + i y is ‖x‖² + ‖y‖².

@[simp]

theorem WithLp.complexification_norm_toLp_ofReal {X : Type u_1} [NormedAddCommGroup X] (x : X) : ‖toLp 2 (TauCeti.Complexification.ofReal x)‖ = ‖x‖

The real embedding x ↦ x + i 0 is isometric for the L² norm.

def WithLp.complexificationEquivProd (X : Type u_1) [NormedAddCommGroup X] [NormedSpace ℝ X] : WithLp 2 (TauCeti.Complexification X) ≃ₗᵢ[ℝ] WithLp 2 (X × X)

As a real normed space, the L² complexification of X is the L² product X × X, via x + i y ↦ (x, y). Real scalars act on the complexification by restricting the complex ones.

@[simp]

theorem WithLp.complexificationEquivProd_apply {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] (z : WithLp 2 (TauCeti.Complexification X)) : (complexificationEquivProd X) z = toLp 2 (z.ofLp.re, z.ofLp.im)

@[simp]

theorem WithLp.complexificationEquivProd_symm_apply {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] (p : WithLp 2 (X × X)) : (complexificationEquivProd X).symm p = toLp 2 { re := p.ofLp.1, im := p.ofLp.2 }

instance WithLp.instComplexificationCompleteSpace {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] : CompleteSpace (WithLp 2 (TauCeti.Complexification X))

The L² complexification of a real Banach space is complete.

theorem WithLp.complexification_norm_smul {X : Type u_1} [NormedAddCommGroup X] [InnerProductSpace ℝ X] (c : ℂ) (z : WithLp 2 (TauCeti.Complexification X)) : ‖c • z‖ = ‖c‖ * ‖z‖

Complex scaling multiplies the L² norm of the complexification by the modulus.

@[instance_reducible]

noncomputable instance WithLp.instComplexificationInnerProductSpace {X : Type u_1} [NormedAddCommGroup X] [InnerProductSpace ℝ X] : InnerProductSpace ℂ (WithLp 2 (TauCeti.Complexification X))

The complex inner product ⟪x + i y, u + i v⟫ = (⟪x, u⟫ + ⟪y, v⟫) + i (⟪x, v⟫ - ⟪y, u⟫) on the complexification of a real inner product space, whose norm is the L² norm.

@[simp]

theorem WithLp.complexification_re_inner {X : Type u_1} [NormedAddCommGroup X] [InnerProductSpace ℝ X] (z w : WithLp 2 (TauCeti.Complexification X)) : (inner ℂ z w).re = inner ℝ z.ofLp.re w.ofLp.re + inner ℝ z.ofLp.im w.ofLp.im

The real part of the inner product on the complexification.

@[simp]

theorem WithLp.complexification_im_inner {X : Type u_1} [NormedAddCommGroup X] [InnerProductSpace ℝ X] (z w : WithLp 2 (TauCeti.Complexification X)) : (inner ℂ z w).im = inner ℝ z.ofLp.re w.ofLp.im - inner ℝ z.ofLp.im w.ofLp.re

The imaginary part of the inner product on the complexification.

def Submodule.complexifyL2 {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (S : Submodule ℝ E) : Submodule ℂ (WithLp 2 (TauCeti.Complexification E))

The complex subspace whose real and imaginary parts lie in a given real subspace, on the Hilbert-norm complexification.

@[simp]

theorem Submodule.mem_complexifyL2 {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (S : Submodule ℝ E) (z : WithLp 2 (TauCeti.Complexification E)) : z ∈ S.complexifyL2 ↔ z.ofLp.re ∈ S ∧ z.ofLp.im ∈ S

@[simp]

theorem Submodule.dense_complexifyL2_iff {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (S : Submodule ℝ E) : Dense ↑S.complexifyL2 ↔ Dense ↑S

Complexifying a real subspace preserves and reflects density.

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

The complexification T_ℂ (x + i y) = T x + i T y of a bounded real operator, as a bounded complex-linear operator between the L² complexifications.

@[simp]

theorem ContinuousLinearMap.ofLp_complexifyL2_apply {X : Type u_1} {Y : Type u_2} [NormedAddCommGroup X] [NormedSpace ℝ X] [NormedAddCommGroup Y] [NormedSpace ℝ Y] (T : X →L[ℝ] Y) (z : WithLp 2 (TauCeti.Complexification X)) : (T.complexifyL2 z).ofLp = T.complexify z.ofLp

The complexification acts on the underlying vector of WithLp 2 (Complexification X) by ContinuousLinearMap.complexify.

@[simp]

theorem ContinuousLinearMap.complexifyL2_toLp_ofReal {X : Type u_1} {Y : Type u_2} [NormedAddCommGroup X] [NormedSpace ℝ X] [NormedAddCommGroup Y] [NormedSpace ℝ Y] (T : X →L[ℝ] Y) (x : X) : T.complexifyL2 (WithLp.toLp 2 (TauCeti.Complexification.ofReal x)) = WithLp.toLp 2 (TauCeti.Complexification.ofReal (T x))

The complexification agrees with T on real vectors.

theorem ContinuousLinearMap.eq_complexifyL2_iff {X : Type u_1} {Y : Type u_2} [NormedAddCommGroup X] [NormedSpace ℝ X] [NormedAddCommGroup Y] [NormedSpace ℝ Y] (T : X →L[ℝ] Y) (S : WithLp 2 (TauCeti.Complexification X) →L[ℂ] WithLp 2 (TauCeti.Complexification Y)) : S = T.complexifyL2 ↔ ∀ (x : X), S (WithLp.toLp 2 (TauCeti.Complexification.ofReal x)) = WithLp.toLp 2 (TauCeti.Complexification.ofReal (T x))

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

@[simp]

theorem ContinuousLinearMap.complexifyL2_zero {X : Type u_1} {Y : Type u_2} [NormedAddCommGroup X] [NormedSpace ℝ X] [NormedAddCommGroup Y] [NormedSpace ℝ Y] : complexifyL2 0 = 0

Complexification sends the zero operator to zero.

@[simp]

theorem ContinuousLinearMap.complexifyL2_add {X : Type u_1} {Y : Type u_2} [NormedAddCommGroup X] [NormedSpace ℝ X] [NormedAddCommGroup Y] [NormedSpace ℝ Y] (S T : X →L[ℝ] Y) : (S + T).complexifyL2 = S.complexifyL2 + T.complexifyL2

Complexification is additive.

@[simp]

theorem ContinuousLinearMap.complexifyL2_id {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] : (ContinuousLinearMap.id ℝ X).complexifyL2 = ContinuousLinearMap.id ℂ (WithLp 2 (TauCeti.Complexification X))

Complexification preserves identity maps.

@[simp]

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

Complexification preserves composition of bounded operators.

@[simp]

theorem ContinuousLinearMap.norm_complexifyL2 {X : Type u_1} {Y : Type u_2} [NormedAddCommGroup X] [InnerProductSpace ℝ X] [NormedAddCommGroup Y] [InnerProductSpace ℝ Y] (T : X →L[ℝ] Y) : ‖T.complexifyL2‖ = ‖T‖

Complexification preserves the operator norm.

@[simp]

theorem ContinuousLinearMap.adjoint_complexifyL2 {X : Type u_1} {Y : Type u_2} [NormedAddCommGroup X] [InnerProductSpace ℝ X] [NormedAddCommGroup Y] [InnerProductSpace ℝ Y] [CompleteSpace X] [CompleteSpace Y] (T : X →L[ℝ] Y) : adjoint T.complexifyL2 = (adjoint T).complexifyL2

The adjoint of a complexification is the complexification of the adjoint.

@[simp]

theorem ContinuousLinearMap.complexifyL2_smul {X : Type u_1} {Y : Type u_2} [NormedAddCommGroup X] [InnerProductSpace ℝ X] [NormedAddCommGroup Y] [InnerProductSpace ℝ Y] (r : ℝ) (T : X →L[ℝ] Y) : (r • T).complexifyL2 = r • T.complexifyL2

Complexification is real-homogeneous.

noncomputable def ContinuousLinearMap.complexifyL2ₗᵢ (X : Type u_1) (Y : Type u_2) [NormedAddCommGroup X] [InnerProductSpace ℝ X] [NormedAddCommGroup Y] [InnerProductSpace ℝ Y] : (X →L[ℝ] Y) →ₗᵢ[ℝ] WithLp 2 (TauCeti.Complexification X) →L[ℂ] WithLp 2 (TauCeti.Complexification Y)

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

noncomputable def ContinuousLinearMap.complexifyL2StarAlgHom (X : Type u_1) [NormedAddCommGroup X] [InnerProductSpace ℝ X] [CompleteSpace X] : (X →L[ℝ] X) →⋆ₐ[ℝ] WithLp 2 (TauCeti.Complexification X) →L[ℂ] WithLp 2 (TauCeti.Complexification X)

Complexification of the bounded operators on a real Hilbert space, as a homomorphism of real ⋆-algebras.

@[simp]

theorem ContinuousLinearMap.complexifyL2ₗᵢ_apply {X : Type u_1} {Y : Type u_2} [NormedAddCommGroup X] [InnerProductSpace ℝ X] [NormedAddCommGroup Y] [InnerProductSpace ℝ Y] (T : X →L[ℝ] Y) : (complexifyL2ₗᵢ X Y) T = T.complexifyL2

@[simp]

theorem ContinuousLinearMap.complexifyL2StarAlgHom_apply {X : Type u_1} [NormedAddCommGroup X] [InnerProductSpace ℝ X] [CompleteSpace X] (T : X →L[ℝ] X) : (complexifyL2StarAlgHom X) T = T.complexifyL2

theorem ContinuousLinearMap.isClosedEmbedding_complexifyL2StarAlgHom (X : Type u_1) [NormedAddCommGroup X] [InnerProductSpace ℝ X] [CompleteSpace X] : Topology.IsClosedEmbedding ⇑(complexifyL2StarAlgHom X)

Complexification of the bounded operators on a real Hilbert space is a closed embedding.

@[simp]

theorem ContinuousLinearMap.isSelfAdjoint_complexifyL2_iff {X : Type u_1} [NormedAddCommGroup X] [InnerProductSpace ℝ X] [CompleteSpace X] {T : X →L[ℝ] X} : IsSelfAdjoint T.complexifyL2 ↔ IsSelfAdjoint T

A bounded operator on a real Hilbert space is self-adjoint exactly when its complexification is.