Complexification of real Hilbert spaces

This file supplies the concrete complexification foundation needed to reuse the complex operator-angle and spectral calculus for real Hilbert spaces.

For a real Hilbert space E, its complexification is the L2 product E × E. The pair (x, y) represents x + i y, with complex scalar multiplication

(a + i b) • (x + i y) = (a x - b y) + i (b x + a y).

The complex inner product is

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

The construction includes:

• the canonical isometric real-linear embedding ofReal;
• complex conjugation as a real-linear isometric involution;
• complexification of bounded real-linear operators;
• preservation of zero, identity, addition, subtraction, scalar multiplication, and composition;
• exact preservation of operator norm;
• reflection of equality and transport of symmetry.

No unbounded-operator, spectral-cutoff, or Ky Fan file depends on this module.

def TauCeti.RealComplexification (E : Type u_1) : Type u_1

The complexification of a real normed space, represented by its real and imaginary coordinates with the L2 product norm.

Equations

• TauCeti.RealComplexification E = WithLp 2 (E × E)

@[instance_reducible]

instance TauCeti.RealComplexification.instAddCommGroup {E : Type u_1} [AddCommGroup E] : AddCommGroup (RealComplexification E)

Additive structure, inherited from the underlying WithLp 2 (E × E).

Equations

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

@[instance_reducible]

noncomputable instance TauCeti.RealComplexification.instNormedAddCommGroup {E : Type u_1} [NormedAddCommGroup E] : NormedAddCommGroup (RealComplexification E)

The L² product norm, inherited from WithLp 2 (E × E). This is the choice that makes the complexification an inner-product space rather than merely a normed one.

Equations

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

instance TauCeti.RealComplexification.instCompleteSpace {E : Type u_1} [NormedAddCommGroup E] [CompleteSpace E] : CompleteSpace (RealComplexification E)

Completeness is inherited from E.

@[instance_reducible]

instance TauCeti.RealComplexification.instSMulReal {E : Type u_1} [SMul ℝ E] : SMul ℝ (RealComplexification E)

Real scalar action, coordinatewise.

Equations

• TauCeti.RealComplexification.instSMulReal = { smul := TauCeti.RealComplexification.instSMulReal._aux_1 }

@[instance_reducible]

instance TauCeti.RealComplexification.instModuleReal {E : Type u_1} [AddCommGroup E] [Module ℝ E] : Module ℝ (RealComplexification E)

Real module structure, inherited from the product.

Equations

• TauCeti.RealComplexification.instModuleReal = { toSMul := TauCeti.RealComplexification.instSMulReal, mul_smul := ⋯, one_smul := ⋯, smul_zero := ⋯, smul_add := ⋯, add_smul := ⋯, zero_smul := ⋯ }

@[instance_reducible]

instance TauCeti.RealComplexification.instNormedSpaceReal {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] : NormedSpace ℝ (RealComplexification E)

The L² norm is compatible with real scaling.

Equations

• TauCeti.RealComplexification.instNormedSpaceReal = { toModule := TauCeti.RealComplexification.instModuleReal, norm_smul_le := ⋯ }

def TauCeti.RealComplexification.mk {E : Type u_1} (x y : E) : RealComplexification E

Construct a complexified vector from its real and imaginary coordinates.

Equations

• TauCeti.RealComplexification.mk x y = WithLp.toLp 2 (x, y)

def TauCeti.RealComplexification.re {E : Type u_1} (z : RealComplexification E) : E

The real coordinate of a complexified vector.

Equations

• z.re = z.ofLp.1

def TauCeti.RealComplexification.im {E : Type u_1} (z : RealComplexification E) : E

The imaginary coordinate of a complexified vector.

Equations

• z.im = z.ofLp.2

@[simp]

theorem TauCeti.RealComplexification.re_mk {E : Type u_1} (x y : E) : (mk x y).re = x

The real part of a vector built from coordinates.

@[simp]

theorem TauCeti.RealComplexification.im_mk {E : Type u_1} (x y : E) : (mk x y).im = y

The imaginary part of a vector built from coordinates.

@[simp]

theorem TauCeti.RealComplexification.mk_re_im {E : Type u_1} (z : RealComplexification E) : mk z.re z.im = z

Rebuilding a vector from its own coordinates is the identity.

theorem TauCeti.RealComplexification.ext {E : Type u_1} {z w : RealComplexification E} (hre : z.re = w.re) (him : z.im = w.im) : z = w

Two complexified vectors are equal when their real and imaginary coordinates agree. Tagged @[ext], so ext splits any goal about them into two real goals.

theorem TauCeti.RealComplexification.ext_iff {E : Type u_1} {z w : RealComplexification E} : z = w ↔ z.re = w.re ∧ z.im = w.im

@[simp]

theorem TauCeti.RealComplexification.re_zero {E : Type u_1} [AddCommGroup E] : re 0 = 0

Zero has zero real part.

@[simp]

theorem TauCeti.RealComplexification.im_zero {E : Type u_1} [AddCommGroup E] : im 0 = 0

Zero has zero imaginary part.

@[simp]

theorem TauCeti.RealComplexification.re_add {E : Type u_1} [AddCommGroup E] (z w : RealComplexification E) : (z + w).re = z.re + w.re

Addition is coordinatewise on real parts.

@[simp]

theorem TauCeti.RealComplexification.im_add {E : Type u_1} [AddCommGroup E] (z w : RealComplexification E) : (z + w).im = z.im + w.im

Addition is coordinatewise on imaginary parts.

@[simp]

theorem TauCeti.RealComplexification.re_neg {E : Type u_1} [AddCommGroup E] (z : RealComplexification E) : (-z).re = -z.re

Negation on real parts.

@[simp]

theorem TauCeti.RealComplexification.im_neg {E : Type u_1} [AddCommGroup E] (z : RealComplexification E) : (-z).im = -z.im

Negation on imaginary parts.

@[simp]

theorem TauCeti.RealComplexification.re_sub {E : Type u_1} [AddCommGroup E] (z w : RealComplexification E) : (z - w).re = z.re - w.re

Subtraction on real parts.

@[simp]

theorem TauCeti.RealComplexification.im_sub {E : Type u_1} [AddCommGroup E] (z w : RealComplexification E) : (z - w).im = z.im - w.im

Subtraction on imaginary parts.

@[simp]

theorem TauCeti.RealComplexification.re_real_smul {E : Type u_1} [AddCommGroup E] [Module ℝ E] (r : ℝ) (z : RealComplexification E) : (r • z).re = r • z.re

Real scaling acts on the real part.

@[simp]

theorem TauCeti.RealComplexification.im_real_smul {E : Type u_1} [AddCommGroup E] [Module ℝ E] (r : ℝ) (z : RealComplexification E) : (r • z).im = r • z.im

Real scaling acts on the imaginary part.

@[instance_reducible]

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

Complex scalar multiplication on the real L2 product.

Equations

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

@[simp]

theorem TauCeti.RealComplexification.re_complex_smul {E : Type u_1} [AddCommGroup E] [Module ℝ E] (c : ℂ) (z : RealComplexification E) : (c • z).re = c.re • z.re - c.im • z.im

Real part of a complex scaling: re (c • z) = c.re • re z - c.im • im z, the real half of complex multiplication.

@[simp]

theorem TauCeti.RealComplexification.im_complex_smul {E : Type u_1} [AddCommGroup E] [Module ℝ E] (c : ℂ) (z : RealComplexification E) : (c • z).im = c.im • z.re + c.re • z.im

Imaginary part of a complex scaling: im (c • z) = c.im • re z + c.re • im z.

@[instance_reducible]

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

The complex module structure, where the complexification earns its name: i acts by (x, y) ↦ (-y, x). Built from minimal axioms because the four laws are exactly the four real identities that have to be checked coordinatewise.

Equations

• TauCeti.RealComplexification.instModuleComplex = Module.ofMinimalAxioms ⋯ ⋯ ⋯ ⋯

instance TauCeti.RealComplexification.instIsScalarTower {E : Type u_1} [AddCommGroup E] [Module ℝ E] : IsScalarTower ℝ ℂ (RealComplexification E)

Real and complex scalar actions are compatible, so ℝ-linear statements can be read inside ℂ-linear ones without transport.

theorem TauCeti.RealComplexification.norm_sq {E : Type u_1} [NormedAddCommGroup E] (z : RealComplexification E) : ‖z‖ ^ 2 = ‖z.re‖ ^ 2 + ‖z.im‖ ^ 2

The squared L2 norm is the sum of the squared coordinate norms.

theorem TauCeti.RealComplexification.norm_complex_smul {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (c : ℂ) (z : RealComplexification E) : ‖c • z‖ = ‖c‖ * ‖z‖

Complex scalar multiplication scales the L2 norm exactly.

@[instance_reducible]

instance TauCeti.RealComplexification.instNormedSpaceComplex {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] : NormedSpace ℂ (RealComplexification E)

The L² norm is compatible with complex scaling. This is the non-formal instance of the group: it needs ‖c • z‖ = ‖c‖ ‖z‖ for complex c, which is the Pythagorean computation above and not a consequence of the real case.

Equations

• TauCeti.RealComplexification.instNormedSpaceComplex = { toModule := TauCeti.RealComplexification.instModuleComplex, norm_smul_le := ⋯ }

@[instance_reducible]

instance TauCeti.RealComplexification.instInnerProductSpaceComplex {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] : InnerProductSpace ℂ (RealComplexification E)

The canonical complex inner product on a real Hilbert-space complexification.

Equations

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

@[simp]

theorem TauCeti.RealComplexification.inner_apply {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (z w : RealComplexification E) : inner ℂ z w = { re := inner ℝ z.re w.re + inner ℝ z.im w.im, im := inner ℝ z.re w.im - inner ℝ z.im w.re }

The complex inner product in coordinates: real part ⟪re z, re w⟫ + ⟪im z, im w⟫, imaginary part ⟪re z, im w⟫ - ⟪im z, re w⟫. True by rfl, and the form every computation unfolds to.

def TauCeti.RealComplexification.ofReal {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] : E →ₗᵢ[ℝ] RealComplexification E

The canonical embedding of a real Hilbert space into its complexification.

Equations

• TauCeti.RealComplexification.ofReal = { toFun := fun (x : E) => TauCeti.RealComplexification.mk x 0, map_add' := ⋯, map_smul' := ⋯, norm_map' := ⋯ }

@[simp]

theorem TauCeti.RealComplexification.re_ofReal {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (x : E) : (ofReal x).re = x

The real part of a real vector is itself.

@[simp]

theorem TauCeti.RealComplexification.im_ofReal {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (x : E) : (ofReal x).im = 0

A real vector has zero imaginary part.

theorem TauCeti.RealComplexification.inner_ofReal {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (x y : E) : inner ℂ (ofReal x) (ofReal y) = ↑(inner ℝ x y)

The complex inner product of two real vectors is the real one, coerced -- so the embedding E → RealComplexification E is isometric.

@[simp]

theorem TauCeti.RealComplexification.I_smul_ofReal {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (x : E) : Complex.I • ofReal x = mk 0 x

Multiplication by i sends the real copy to the imaginary copy.

def TauCeti.RealComplexification.conjugation {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] : RealComplexification E →ₗᵢ[ℝ] RealComplexification E

Complex conjugation on the complexification.

Equations

• TauCeti.RealComplexification.conjugation = { toFun := fun (z : TauCeti.RealComplexification E) => TauCeti.RealComplexification.mk z.re (-z.im), map_add' := ⋯, map_smul' := ⋯, norm_map' := ⋯ }

@[simp]

theorem TauCeti.RealComplexification.re_conj {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (z : RealComplexification E) : (conjugation z).re = z.re

Conjugation fixes the real part.

@[simp]

theorem TauCeti.RealComplexification.im_conj {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (z : RealComplexification E) : (conjugation z).im = -z.im

Conjugation negates the imaginary part.

@[simp]

theorem TauCeti.RealComplexification.conjugation_involutive {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (z : RealComplexification E) : conjugation (conjugation z) = z

Conjugation is an involution.

@[simp]

theorem TauCeti.RealComplexification.conjugation_ofReal {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (x : E) : conjugation (ofReal x) = ofReal x

Conjugation fixes real vectors, which characterises the real subspace.

@[simp]

theorem TauCeti.RealComplexification.conjugation_complex_smul {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (c : ℂ) (z : RealComplexification E) : conjugation (c • z) = (starRingEnd ℂ) c • conjugation z

Conjugation is conjugate-linear, not linear: the scalar comes out starred.

noncomputable def TauCeti.RealComplexification.complexify {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup F] [InnerProductSpace ℝ F] (T : E →L[ℝ] F) : RealComplexification E →L[ℂ] RealComplexification F

Coordinatewise extension of a bounded real-linear operator.

Equations

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

@[simp]

theorem TauCeti.RealComplexification.re_complexify {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup F] [InnerProductSpace ℝ F] (T : E →L[ℝ] F) (z : RealComplexification E) : ((complexify T) z).re = T z.re

The complexified operator acts on real parts by the original operator.

@[simp]

theorem TauCeti.RealComplexification.im_complexify {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup F] [InnerProductSpace ℝ F] (T : E →L[ℝ] F) (z : RealComplexification E) : ((complexify T) z).im = T z.im

The complexified operator acts on imaginary parts by the original operator.

@[simp]

theorem TauCeti.RealComplexification.complexify_ofReal {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup F] [InnerProductSpace ℝ F] (T : E →L[ℝ] F) (x : E) : (complexify T) (ofReal x) = ofReal (T x)

Complexification agrees with the original operator on real vectors.

@[simp]

theorem TauCeti.RealComplexification.complexify_zero {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup F] [InnerProductSpace ℝ F] : complexify 0 = 0

The complexification of the zero operator is zero.

@[simp]

theorem TauCeti.RealComplexification.complexify_id {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] : complexify (ContinuousLinearMap.id ℝ E) = ContinuousLinearMap.id ℂ (RealComplexification E)

The complexification of the identity is the identity.

@[simp]

theorem TauCeti.RealComplexification.complexify_add {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup F] [InnerProductSpace ℝ F] (S T : E →L[ℝ] F) : complexify (S + T) = complexify S + complexify T

Complexification is additive.

@[simp]

theorem TauCeti.RealComplexification.complexify_neg {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup F] [InnerProductSpace ℝ F] (T : E →L[ℝ] F) : complexify (-T) = -complexify T

Complexification commutes with negation.

@[simp]

theorem TauCeti.RealComplexification.complexify_sub {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup F] [InnerProductSpace ℝ F] (S T : E →L[ℝ] F) : complexify (S - T) = complexify S - complexify T

Complexification commutes with subtraction.

@[simp]

theorem TauCeti.RealComplexification.complexify_real_smul {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup F] [InnerProductSpace ℝ F] (r : ℝ) (T : E →L[ℝ] F) : complexify (r • T) = ↑r • complexify T

Complexification is real-homogeneous. It is not complex-homogeneous -- the complexified operator is ℂ-linear, but complexify itself only transports real scalars.

@[simp]

theorem TauCeti.RealComplexification.complexify_comp {E : Type u_1} {F : Type u_2} {G : Type u_3} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup F] [InnerProductSpace ℝ F] [NormedAddCommGroup G] [InnerProductSpace ℝ G] (S : F →L[ℝ] G) (T : E →L[ℝ] F) : complexify (S ∘SL T) = complexify S ∘SL complexify T

Complexification is functorial: it commutes with composition.

theorem TauCeti.RealComplexification.norm_complexify {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup F] [InnerProductSpace ℝ F] (T : E →L[ℝ] F) : ‖complexify T‖ = ‖T‖

Complexification preserves operator norm exactly.

theorem TauCeti.RealComplexification.isometry_complexify {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup F] [InnerProductSpace ℝ F] : Isometry complexify

Complexification is an isometry of operator spaces, not merely norm-preserving on each operator: it is additive, so norm_complexify upgrades to a statement about distances. This is the form needed to transport a topological property back from the complexification, where norm_complexify alone only transports one forward.

theorem TauCeti.RealComplexification.complexify_injective {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup F] [InnerProductSpace ℝ F] : Function.Injective complexify

Complexification reflects equality of bounded real operators.

theorem TauCeti.RealComplexification.coe_real_smul {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (r : ℝ) (z : RealComplexification E) : ↑r • z = r • z

A real scalar acts through its complex coercion.

theorem TauCeti.RealComplexification.norm_re_le {E : Type u_1} [NormedAddCommGroup E] (z : RealComplexification E) : ‖z.re‖ ≤ ‖z‖

A coordinate of a vector is no longer than the vector. The single statement of ‖re z‖ ≤ ‖z‖ in this repository, and the earliest in import order, so every consumer can reach it.

It was private until 2026-07-30, guarded by a note saying a public copy would make unqualified uses ambiguous in Sources/DavisKahan1970/Ideals/HilbertSchmidtRealDescent.lean, which opens two of the namespaces that had a copy. That was true, and it was the wrong conclusion: the ambiguity came from the other three copies, not from this one being visible.

Getting there took a broken tree first, and the sequence is worth keeping. edward (aiq-gpu) deleted the PartialMapComplexification sibling in 4dacc008 and pointed that module here; separately this one was still private. Each fix is right alone and they are fatal together — with the sibling gone and this one private, no public copy was reachable from PartialMap/Complexification.lean and the build stopped. Lane {lane:CPLX-DEDUP-1} then deleted the remaining copies and made this one public, which is the state described above.

noncomputable def TauCeti.RealComplexification.realPartOperator {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup F] [InnerProductSpace ℝ F] (T : RealComplexification E →L[ℂ] RealComplexification F) : E →L[ℝ] F

Restrict a complex operator to the real copy and take its real coordinate. No invariance assumption is needed to define this: the map is x ↦ re (T (ofReal x)) for any bounded T, and it is bounded by ‖T‖ because neither coordinate projection nor the real embedding changes a norm.

Stated rectangularly, between two different spaces. Three copies of this definition existed until 2026-07-30 and they were not three copies of one thing: Sources/DavisKahan1970/Ideals/HilbertSchmidtRealDescent.lean had the rectangular one while Complexification/FunctionalCalculus.lean and OperatorIdeal/ApproximationNumbers/Real/Threshold.lean had the square case, which is this at F = E. This module is the only one all three consumers import, so it is where the general form belongs.

Equations

• TauCeti.RealComplexification.realPartOperator T = { toFun := fun (x : E) => (T (TauCeti.RealComplexification.ofReal x)).re, map_add' := ⋯, map_smul' := ⋯ }.mkContinuous ‖T‖ ⋯

@[simp]

theorem TauCeti.RealComplexification.realPartOperator_apply {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup F] [InnerProductSpace ℝ F] (T : RealComplexification E →L[ℂ] RealComplexification F) (x : E) : (realPartOperator T) x = (T (ofReal x)).re

Pointwise formula for the real restriction: embed, apply, take the real coordinate.

theorem TauCeti.RealComplexification.eq_ofReal_add_I_smul_ofReal {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (z : RealComplexification E) : z = ofReal z.re + Complex.I • ofReal z.im

Every vector is its real part plus i times its imaginary part.

theorem TauCeti.RealComplexification.im_apply_ofReal_eq_zero {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup F] [InnerProductSpace ℝ F] {T : RealComplexification E →L[ℂ] RealComplexification F} (hT : ∀ (z : RealComplexification E), T (conjugation z) = conjugation (T z)) (x : E) : (T (ofReal x)).im = 0

An operator commuting with conjugation maps the real copy into the real copy: the imaginary part of T (ofReal x) vanishes.

This is the whole content of the conjugation condition, and it is what makes realify below a two-sided inverse of complexify.

noncomputable def TauCeti.RealComplexification.realify {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup F] [InnerProductSpace ℝ F] (T : RealComplexification E →L[ℂ] RealComplexification F) : E →L[ℝ] F

The real operator underlying a ℂ-linear operator: read off the action on the real copy.

Paired with complexify_realify this says complexify is a bijection onto the operators commuting with conjugation — the surjectivity half that complexify_injective leaves open.

Equations

• TauCeti.RealComplexification.realify T = { toFun := fun (x : E) => (T (TauCeti.RealComplexification.ofReal x)).re, map_add' := ⋯, map_smul' := ⋯ }.mkContinuous ‖T‖ ⋯

@[simp]

theorem TauCeti.RealComplexification.realify_apply {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup F] [InnerProductSpace ℝ F] (T : RealComplexification E →L[ℂ] RealComplexification F) (x : E) : (realify T) x = (T (ofReal x)).re

realify T acts by reading the real part of T on the real copy.

theorem TauCeti.RealComplexification.complexify_realify {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup F] [InnerProductSpace ℝ F] {T : RealComplexification E →L[ℂ] RealComplexification F} (hT : ∀ (z : RealComplexification E), T (conjugation z) = conjugation (T z)) : complexify (realify T) = T

complexify is onto the conjugation-commuting operators. Together with complexify_injective, complexification identifies E →L[ℝ] F with exactly those ℂ-linear operators that commute with conjugation.

theorem TauCeti.RealComplexification.complexify_conjugation {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup F] [InnerProductSpace ℝ F] (T : E →L[ℝ] F) (z : RealComplexification E) : (complexify T) (conjugation z) = conjugation ((complexify T) z)

The complexification of a real operator commutes with conjugation.

theorem TauCeti.RealComplexification.complexify_isSymmetric_iff {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (T : E →L[ℝ] E) : (↑(complexify T)).IsSymmetric ↔ (↑T).IsSymmetric

Symmetry of a real operator is equivalent to symmetry of its complexification.

theorem TauCeti.RealComplexification.complexify_isSelfAdjoint_iff {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (T : E →L[ℝ] E) : IsSelfAdjoint (complexify T) ↔ IsSelfAdjoint T

Self-adjointness is preserved and reflected by complexification.