Complexification of a real inner product space

Why this file is needed: the spectral projection is built with the continuous functional calculus, which is only available over ℂ. To obtain it over ℝ (and uniformly over any RCLike field), RealProjection/Representation complexify the space, run the ℂ construction, and restrict back — and this file supplies the complexification with its complex inner product (a piece Mathlib does not yet have).

Given a real inner product space H, this file builds its complexification Complexification H: the complex inner product space whose elements are thought of as formal sums x + i·y with x, y ∈ H.

Concretely we model Complexification H as the pair type H × H (the pair (x, y) standing for x + i·y), equip it with

• the complex scalar multiplication (a + b·i) • (x, y) = (a·x - b·y, a·y + b·x), and
• the Hermitian inner product ⟪(x₁,y₁), (x₂,y₂)⟫ = (⟪x₁,x₂⟫ + ⟪y₁,y₂⟫) + i·(⟪x₁,y₂⟫ - ⟪y₁,x₂⟫),

and prove that this makes Complexification H a complex inner product space (InnerProductSpace ℂ). The canonical real-linear isometric embedding x ↦ x + i·0 is provided as Complexification.ofRealLi.

Note. Mathlib has base change of modules (ℂ ⊗[ℝ] M is a Module ℂ) but no construction equipping the complexification of a real inner product space with its complex inner product. This file constructs it, kept deliberately elementary and self-contained.

def Complexification (H : Type u_2) : Type u_2

The complexification of a real inner product space H, modelled as the pair type H × H; the pair (x, y) represents the formal sum x + i·y.

Equations

• Complexification H = (H × H)

@[instance_reducible]

instance Complexification.instAddCommGroup {H : Type u_1} [NormedAddCommGroup H] : AddCommGroup (Complexification H)

The underlying additive group is that of H × H.

Equations

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

def Complexification.mk {H : Type u_1} (x y : H) : Complexification H

The element x + i·y of the complexification.

This is the pair (x, y), but wrapped in a name. Writing a bare pair (x, y) at type Complexification H is only type-correct after unfolding Complexification, which simp and rw refuse to do; going through mk together with the projection lemmas mk_fst/mk_snd below keeps every goal in this file stated in terms the simp set can act on.

Equations

• Complexification.mk x y = (x, y)

@[simp]

theorem Complexification.mk_fst {H : Type u_1} (x y : H) : (mk x y).1 = x

@[simp]

theorem Complexification.mk_snd {H : Type u_1} (x y : H) : (mk x y).2 = y

@[instance_reducible]

instance Complexification.instSMulComplex {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℝ H] : SMul ℂ (Complexification H)

Complex scalar multiplication: (a + b·i) • (x, y) = (a·x - b·y, a·y + b·x).

Equations

• Complexification.instSMulComplex = { smul := fun (c : ℂ) (u : Complexification H) => Complexification.mk (c.re • u.1 - c.im • u.2) (c.re • u.2 + c.im • u.1) }

@[simp]

theorem Complexification.smul_fst {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℝ H] (c : ℂ) (u : Complexification H) : (c • u).1 = c.re • u.1 - c.im • u.2

@[simp]

theorem Complexification.smul_snd {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℝ H] (c : ℂ) (u : Complexification H) : (c • u).2 = c.re • u.2 + c.im • u.1

@[simp]

theorem Complexification.add_fst {H : Type u_1} [NormedAddCommGroup H] (u v : Complexification H) : (u + v).1 = u.1 + v.1

@[simp]

theorem Complexification.add_snd {H : Type u_1} [NormedAddCommGroup H] (u v : Complexification H) : (u + v).2 = u.2 + v.2

@[simp]

theorem Complexification.zero_fst {H : Type u_1} [NormedAddCommGroup H] : 0.1 = 0

@[simp]

theorem Complexification.zero_snd {H : Type u_1} [NormedAddCommGroup H] : 0.2 = 0

@[simp]

theorem Complexification.sub_fst {H : Type u_1} [NormedAddCommGroup H] (u v : Complexification H) : (u - v).1 = u.1 - v.1

@[simp]

theorem Complexification.sub_snd {H : Type u_1} [NormedAddCommGroup H] (u v : Complexification H) : (u - v).2 = u.2 - v.2

@[instance_reducible]

instance Complexification.instModuleComplex {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℝ H] : Module ℂ (Complexification H)

Equations

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

@[instance_reducible]

instance Complexification.instInnerComplex {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℝ H] : Inner ℂ (Complexification H)

The Hermitian inner product: ⟪(x₁,y₁), (x₂,y₂)⟫ = (⟪x₁,x₂⟫ + ⟪y₁,y₂⟫) + i·(⟪x₁,y₂⟫ - ⟪y₁,x₂⟫).

Equations

• Complexification.instInnerComplex = { inner := fun (u v : Complexification H) => { re := inner ℝ u.1 v.1 + inner ℝ u.2 v.2, im := inner ℝ u.1 v.2 - inner ℝ u.2 v.1 } }

@[simp]

theorem Complexification.inner_re {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℝ H] (u v : Complexification H) : (inner ℂ u v).re = inner ℝ u.1 v.1 + inner ℝ u.2 v.2

@[simp]

theorem Complexification.inner_im {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℝ H] (u v : Complexification H) : (inner ℂ u v).im = inner ℝ u.1 v.2 - inner ℝ u.2 v.1

@[reducible]

def Complexification.core {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℝ H] : InnerProductSpace.Core ℂ (Complexification H)

The InnerProductSpace.Core packaging all the axioms of the complex inner product on the complexification.

Equations

• Complexification.core = { inner := fun (u v : Complexification H) => inner ℂ u v, conj_inner_symm := ⋯, re_inner_nonneg := ⋯, add_left := ⋯, smul_left := ⋯, definite := ⋯ }

@[instance_reducible]

noncomputable instance Complexification.instNormedAddCommGroup {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℝ H] : NormedAddCommGroup (Complexification H)

The norm coming from the complex inner product.

Equations

• Complexification.instNormedAddCommGroup = InnerProductSpace.Core.toNormedAddCommGroup

@[instance_reducible]

noncomputable instance Complexification.instInnerProductSpaceComplex {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℝ H] : InnerProductSpace ℂ (Complexification H)

The complexification of a real inner product space is a complex inner product space.

Equations

• Complexification.instInnerProductSpaceComplex = InnerProductSpace.ofCore inferInstance

instance Complexification.instNontrivial {H : Type u_1} [Nontrivial H] : Nontrivial (Complexification H)

@[simp]

theorem Complexification.rsmul_fst {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℝ H] (r : ℝ) (u : Complexification H) : (r • u).1 = r • u.1

The real scalar action (the restriction of the complex one) is component-wise.

@[simp]

theorem Complexification.rsmul_snd {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℝ H] (r : ℝ) (u : Complexification H) : (r • u).2 = r • u.2

def Complexification.ofReal {H : Type u_1} [NormedAddCommGroup H] (x : H) : Complexification H

The canonical embedding x ↦ x + i·0 of H into its complexification.

Equations

• Complexification.ofReal x = Complexification.mk x 0

@[simp]

theorem Complexification.ofReal_fst {H : Type u_1} [NormedAddCommGroup H] (x : H) : (ofReal x).1 = x

@[simp]

theorem Complexification.ofReal_snd {H : Type u_1} [NormedAddCommGroup H] (x : H) : (ofReal x).2 = 0

@[simp]

theorem Complexification.ofReal_add {H : Type u_1} [NormedAddCommGroup H] (x y : H) : ofReal (x + y) = ofReal x + ofReal y

@[simp]

theorem Complexification.ofReal_sub {H : Type u_1} [NormedAddCommGroup H] (x y : H) : ofReal (x - y) = ofReal x - ofReal y

@[simp]

theorem Complexification.norm_ofReal {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℝ H] (x : H) : ‖ofReal x‖ = ‖x‖

The embedding ofReal preserves norms: ‖x + i·0‖ = ‖x‖.

def Complexification.ofRealLi {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℝ H] : H →ₗᵢ[ℝ] Complexification H

The embedding ofReal as a real-linear isometry H →ₗᵢ[ℝ] Complexification H.

Equations

• Complexification.ofRealLi = { toFun := Complexification.ofReal, map_add' := ⋯, map_smul' := ⋯, norm_map' := ⋯ }

Completeness

The norm ‖(x, y)‖ = √(‖x‖² + ‖y‖²) controls each component (‖x‖, ‖y‖ ≤ ‖(x,y)‖) and is in turn controlled by them (‖(x,y)‖ ≤ ‖x‖ + ‖y‖). Hence a Cauchy sequence in Complexification H has Cauchy components, and converges componentwise; so the complexification of a complete real inner product space is itself complete — a complex Hilbert space.

theorem Complexification.re_inner_self {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℝ H] (u : Complexification H) : (inner ℂ u u).re = ‖u.1‖ ^ 2 + ‖u.2‖ ^ 2

The squared norm is the sum of the squared component norms.

theorem Complexification.norm_sq_eq {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℝ H] (u : Complexification H) : ‖u‖ ^ 2 = ‖u.1‖ ^ 2 + ‖u.2‖ ^ 2

theorem Complexification.norm_fst_le {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℝ H] (u : Complexification H) : ‖u.1‖ ≤ ‖u‖

theorem Complexification.norm_snd_le {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℝ H] (u : Complexification H) : ‖u.2‖ ≤ ‖u‖

theorem Complexification.norm_le_add {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℝ H] (u : Complexification H) : ‖u‖ ≤ ‖u.1‖ + ‖u.2‖

def Complexification.fstₗ {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℝ H] : Complexification H →ₗ[ℝ] H

The real-part projection (x, y) ↦ x as an ℝ-linear map.

Equations

• Complexification.fstₗ = { toFun := fun (u : Complexification H) => u.1, map_add' := ⋯, map_smul' := ⋯ }

noncomputable def Complexification.fstL {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℝ H] : Complexification H →L[ℝ] H

The real-part projection (x, y) ↦ x as a continuous ℝ-linear map.

Equations

• Complexification.fstL = Complexification.fstₗ.mkContinuous 1 ⋯

@[simp]

theorem Complexification.fstL_apply {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℝ H] (u : Complexification H) : fstL u = u.1

instance Complexification.instCompleteSpace {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] : CompleteSpace (Complexification H)

Conjugation

Complex conjugation x + i·y ↦ x - i·y is the canonical conjugate-linear isometric involution of the complexification. Its set of fixed points is exactly the image of ofReal, i.e. the "real" elements — the fact that lets one detect when a complex object descends to the real space.

def Complexification.conj {H : Type u_1} [NormedAddCommGroup H] (u : Complexification H) : Complexification H

Complex conjugation on the complexification: (x, y) ↦ (x, -y).

Equations

• u.conj = Complexification.mk u.1 (-u.2)

@[simp]

theorem Complexification.conj_fst {H : Type u_1} [NormedAddCommGroup H] (u : Complexification H) : u.conj.1 = u.1

@[simp]

theorem Complexification.conj_snd {H : Type u_1} [NormedAddCommGroup H] (u : Complexification H) : u.conj.2 = -u.2

@[simp]

theorem Complexification.conj_conj {H : Type u_1} [NormedAddCommGroup H] (u : Complexification H) : u.conj.conj = u

@[simp]

theorem Complexification.conj_ofReal {H : Type u_1} [NormedAddCommGroup H] (x : H) : (ofReal x).conj = ofReal x

theorem Complexification.conj_add {H : Type u_1} [NormedAddCommGroup H] (u v : Complexification H) : (u + v).conj = u.conj + v.conj

theorem Complexification.conj_smul {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℝ H] (c : ℂ) (u : Complexification H) : (c • u).conj = (starRingEnd ℂ) c • u.conj

Conjugation is conjugate-linear: conj (c • u) = conj c • conj u.

@[simp]

theorem Complexification.norm_conj {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℝ H] (u : Complexification H) : ‖u.conj‖ = ‖u‖

def Complexification.conjLi {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℝ H] : Complexification H →ₗᵢ[ℝ] Complexification H

Conjugation as a real-linear isometry.

Equations

• Complexification.conjLi = { toFun := Complexification.conj, map_add' := ⋯, map_smul' := ⋯, norm_map' := ⋯ }

noncomputable def Complexification.conjL {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℝ H] : Complexification H →L[ℝ] Complexification H

Conjugation as a continuous ℝ-linear map.

Equations

• Complexification.conjL = Complexification.conjLi.toContinuousLinearMap

@[simp]

theorem Complexification.conjL_apply {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℝ H] (u : Complexification H) : conjL u = u.conj

theorem Complexification.conj_eq_self_iff {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℝ H] (u : Complexification H) : u.conj = u ↔ ∃ (x : H), u = ofReal x

The elements fixed by conjugation are exactly the "real" ones, x + i·0.

Complexification of operators

A real bounded operator S : H₁ →L[ℝ] H₂ extends to a complex bounded operator Sℂ : Complexification H₁ →L[ℂ] Complexification H₂, (x, y) ↦ (S x, S y), with the same operator norm. It commutes with conjugation and is compatible with the real embedding — the precise senses in which Sℂ "is" S viewed complex-linearly.

def Complexification.complexifyₗ {H₁ : Type u_2} {H₂ : Type u_3} [NormedAddCommGroup H₁] [InnerProductSpace ℝ H₁] [NormedAddCommGroup H₂] [InnerProductSpace ℝ H₂] (S : H₁ →L[ℝ] H₂) : Complexification H₁ →ₗ[ℂ] Complexification H₂

The complexification of S as a ℂ-linear map, (x, y) ↦ (S x, S y).

Equations

• Complexification.complexifyₗ S = { toFun := fun (u : Complexification H₁) => Complexification.mk (S u.1) (S u.2), map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem Complexification.complexifyₗ_fst {H₁ : Type u_2} {H₂ : Type u_3} [NormedAddCommGroup H₁] [InnerProductSpace ℝ H₁] [NormedAddCommGroup H₂] [InnerProductSpace ℝ H₂] (S : H₁ →L[ℝ] H₂) (u : Complexification H₁) : ((complexifyₗ S) u).1 = S u.1

@[simp]

theorem Complexification.complexifyₗ_snd {H₁ : Type u_2} {H₂ : Type u_3} [NormedAddCommGroup H₁] [InnerProductSpace ℝ H₁] [NormedAddCommGroup H₂] [InnerProductSpace ℝ H₂] (S : H₁ →L[ℝ] H₂) (u : Complexification H₁) : ((complexifyₗ S) u).2 = S u.2

theorem Complexification.norm_complexifyₗ_le {H₁ : Type u_2} {H₂ : Type u_3} [NormedAddCommGroup H₁] [InnerProductSpace ℝ H₁] [NormedAddCommGroup H₂] [InnerProductSpace ℝ H₂] (S : H₁ →L[ℝ] H₂) (u : Complexification H₁) : ‖(complexifyₗ S) u‖ ≤ ‖S‖ * ‖u‖

noncomputable def Complexification.complexify {H₁ : Type u_2} {H₂ : Type u_3} [NormedAddCommGroup H₁] [InnerProductSpace ℝ H₁] [NormedAddCommGroup H₂] [InnerProductSpace ℝ H₂] (S : H₁ →L[ℝ] H₂) : Complexification H₁ →L[ℂ] Complexification H₂

The complexification of a real bounded operator S, as a ℂ-linear bounded operator (x, y) ↦ (S x, S y).

Equations

• Complexification.complexify S = (Complexification.complexifyₗ S).mkContinuous ‖S‖ ⋯

@[simp]

theorem Complexification.complexify_fst {H₁ : Type u_2} {H₂ : Type u_3} [NormedAddCommGroup H₁] [InnerProductSpace ℝ H₁] [NormedAddCommGroup H₂] [InnerProductSpace ℝ H₂] (S : H₁ →L[ℝ] H₂) (u : Complexification H₁) : ((complexify S) u).1 = S u.1

@[simp]

theorem Complexification.complexify_snd {H₁ : Type u_2} {H₂ : Type u_3} [NormedAddCommGroup H₁] [InnerProductSpace ℝ H₁] [NormedAddCommGroup H₂] [InnerProductSpace ℝ H₂] (S : H₁ →L[ℝ] H₂) (u : Complexification H₁) : ((complexify S) u).2 = S u.2

@[simp]

theorem Complexification.complexify_ofReal {H₁ : Type u_2} {H₂ : Type u_3} [NormedAddCommGroup H₁] [InnerProductSpace ℝ H₁] [NormedAddCommGroup H₂] [InnerProductSpace ℝ H₂] (S : H₁ →L[ℝ] H₂) (x : H₁) : (complexify S) (ofReal x) = ofReal (S x)

Sℂ agrees with S on the real subspace: Sℂ (x + i·0) = (S x) + i·0.

@[simp]

theorem Complexification.complexify_conj {H₁ : Type u_2} {H₂ : Type u_3} [NormedAddCommGroup H₁] [InnerProductSpace ℝ H₁] [NormedAddCommGroup H₂] [InnerProductSpace ℝ H₂] (S : H₁ →L[ℝ] H₂) (u : Complexification H₁) : (complexify S) u.conj = ((complexify S) u).conj

Sℂ commutes with conjugation (this is what it means for Sℂ to be "real").

@[simp]

theorem Complexification.norm_complexify {H₁ : Type u_2} {H₂ : Type u_3} [NormedAddCommGroup H₁] [InnerProductSpace ℝ H₁] [NormedAddCommGroup H₂] [InnerProductSpace ℝ H₂] (S : H₁ →L[ℝ] H₂) : ‖complexify S‖ = ‖S‖

The complexification preserves the operator norm.

@[simp]

theorem Complexification.adjoint_complexify {H₁ : Type u_2} {H₂ : Type u_3} [NormedAddCommGroup H₁] [InnerProductSpace ℝ H₁] [NormedAddCommGroup H₂] [InnerProductSpace ℝ H₂] [CompleteSpace H₁] [CompleteSpace H₂] (S : H₁ →L[ℝ] H₂) : ContinuousLinearMap.adjoint (complexify S) = complexify (ContinuousLinearMap.adjoint S)

Complexification commutes with taking adjoints: (Sℂ)* = (S*)ℂ.