Real descent for bounded functional calculus

This module exposes the canonical conjugation action on operators over a real Hilbert-space complexification. A conjugation-fixed complex operator descends to a bounded real operator, and real continuous functional calculus preserves the fixed-point subalgebra. These are the reusable seams needed for real infinite-dimensional polar factorization.

Main definitions and results

• TauCeti.RealComplexification.canonicalConjugation: the canonical conjugation of a real complexification, an antilinear isometric involution;
• TauCeti.RealComplexification.conjugateOperator: the induced involution on bounded complex operators, together with its ring, norm and adjoint laws;
• TauCeti.RealComplexification.conjugateOperator_cfc_eq: continuous functional calculus commutes with the conjugation, so the fixed-point subalgebra is preserved; conjugateOperator_cfc is the same statement with the continuity side condition removed;
• TauCeti.RealComplexification.fixed_operator_maps_real_to_real: a conjugation-fixed operator descends to the real subspace;
• TauCeti.RealComplexification.complexify_adjoint and complexify_gram: complexification intertwines adjoints and Gram operators.

Provenance

• Original repository: Davis--Kahan/DKPS formalization (Kitware, Inc.).
• Original module: DavisKahan/SpectralTheory/Complexification/FunctionalCalculus.lean.
• Extraction class: moved, not restated. Its only non-Mathlib import is Complexification/Basic.lean, which is already in ForTauCeti, so it depended on nothing in the paper library.
• The enclosing namespace was TauCeti.DavisKahan.Experimental.ExactSinTheta. RealComplexificationFunctionalCalculus: two paper names, a staging word, and a repetition of the parent. It is now simply TauCeti.RealComplexification, the namespace of the complexify it is about — which is where complexify_adjoint and complexify_gram belonged all along. The scoped instance moved with it, so consumers now write open scoped TauCeti.RealComplexification.
• Original authors / copyright: Jon Crall, OpenAI GPT-5.6 Thinking; Copyright (c) 2026 Kitware, Inc.; Apache 2.0.
• Spectra influence: none.

@[instance_reducible]

noncomputable def TauCeti.RealComplexification.complexOperatorRealAlgebra {E : Type v} [NormedAddCommGroup E] [InnerProductSpace ℝ E] : Algebra ℝ (RealComplexification E →L[ℂ] RealComplexification E)

Scalar restriction of the complex operator algebra to the reals.

scoped, deliberately, and not local or global. Global is the ℝ-algebra diamond that Mathlib declines to install for Algebra.complexToReal, so that door stays shut. local was what this was until 2026-07-30, and it forced three other modules to reinstall a second declaration of the same instance; lemmas stated against one copy then had to be proved defeq against the other, which is what timed out isDefEq when Threshold.lean first tried to import this module's lemmas. A scope gives every consumer the same declaration, so there is nothing to prove. Open it with open scoped RealComplexification.

Equations

• TauCeti.RealComplexification.complexOperatorRealAlgebra = Algebra.complexToReal

theorem TauCeti.RealComplexification.realContinuousFunctionalCalculus {E : Type v} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] : ContinuousFunctionalCalculus ℝ (RealComplexification E →L[ℂ] RealComplexification E) IsSelfAdjoint

Real continuous functional calculus on the complexified operator algebra. scoped for the same reason as complexOperatorRealAlgebra above.

theorem TauCeti.RealComplexification.restrictedReal_smul_operator_eq {E : Type v} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (r : ℝ) (A : RealComplexification E →L[ℂ] RealComplexification E) : SMul.smul r A = r • A

The real scalar action inherited from the complex-operator algebra agrees with the ambient real action on operators. This is the compatibility needed to run real continuous functional calculus inside the complex operator algebra.

Canonical conjugation on the complexification

noncomputable def TauCeti.RealComplexification.canonicalConjugation {E : Type v} [NormedAddCommGroup E] [InnerProductSpace ℝ E] : RealComplexification E ≃ₗᵢ⋆[ℂ] RealComplexification E

Canonical conjugation, bundled as an antiunitary involution.

Equations

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

@[simp]

theorem TauCeti.RealComplexification.canonicalConjugation_apply {E : Type v} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (z : RealComplexification E) : canonicalConjugation z = conjugation z

The canonical conjugation acts pointwise as conjugation.

@[simp]

theorem TauCeti.RealComplexification.canonicalConjugation_symm_apply {E : Type v} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (z : RealComplexification E) : canonicalConjugation.symm z = conjugation z

The canonical conjugation is its own inverse: conjugation is an involution.

theorem TauCeti.RealComplexification.inner_conjugation {E : Type v} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (z w : RealComplexification E) : inner ℂ (conjugation z) (conjugation w) = inner ℂ w z

Conjugation reverses the two slots of the complex inner product.

theorem TauCeti.RealComplexification.inner_conjugation_left {E : Type v} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (z w : RealComplexification E) : inner ℂ (conjugation z) w = inner ℂ (conjugation w) z

Conjugating the left slot exchanges the roles of the two arguments.

theorem TauCeti.RealComplexification.inner_conjugation_right {E : Type v} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (z w : RealComplexification E) : inner ℂ z (conjugation w) = inner ℂ w (conjugation z)

Conjugating the right slot exchanges the roles of the two arguments.

noncomputable def TauCeti.RealComplexification.conjugateOperator {E : Type v} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (A : RealComplexification E →L[ℂ] RealComplexification E) : RealComplexification E →L[ℂ] RealComplexification E

Conjugation of a complexified bounded operator by canonical conjugation.

Equations

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

@[simp]

theorem TauCeti.RealComplexification.conjugateOperator_apply {E : Type v} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (A : RealComplexification E →L[ℂ] RealComplexification E) (z : RealComplexification E) : (conjugateOperator A) z = conjugation (A (conjugation z))

Pointwise formula for the conjugated operator: conjugate the input, apply A, conjugate the output.

@[simp]

theorem TauCeti.RealComplexification.conjugateOperator_zero {E : Type v} [NormedAddCommGroup E] [InnerProductSpace ℝ E] : conjugateOperator 0 = 0

Conjugation fixes the zero operator.

@[simp]

theorem TauCeti.RealComplexification.conjugateOperator_add {E : Type v} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (A B : RealComplexification E →L[ℂ] RealComplexification E) : conjugateOperator (A + B) = conjugateOperator A + conjugateOperator B

Conjugation of operators is additive.

@[simp]

theorem TauCeti.RealComplexification.conjugateOperator_neg {E : Type v} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (A : RealComplexification E →L[ℂ] RealComplexification E) : conjugateOperator (-A) = -conjugateOperator A

Conjugation commutes with negation.

@[simp]

theorem TauCeti.RealComplexification.conjugateOperator_sub {E : Type v} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (A B : RealComplexification E →L[ℂ] RealComplexification E) : conjugateOperator (A - B) = conjugateOperator A - conjugateOperator B

Conjugation commutes with subtraction.

@[simp]

theorem TauCeti.RealComplexification.conjugateOperator_one {E : Type v} [NormedAddCommGroup E] [InnerProductSpace ℝ E] : conjugateOperator 1 = 1

Conjugation fixes the identity operator.

@[simp]

theorem TauCeti.RealComplexification.conjugateOperator_mul {E : Type v} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (A B : RealComplexification E →L[ℂ] RealComplexification E) : conjugateOperator (A * B) = conjugateOperator A * conjugateOperator B

Conjugation is multiplicative, and preserves the order of composition — it is an algebra map, not an anti-map.

@[simp]

theorem TauCeti.RealComplexification.conjugateOperator_real_smul {E : Type v} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (r : ℝ) (A : RealComplexification E →L[ℂ] RealComplexification E) : conjugateOperator (r • A) = r • conjugateOperator A

Conjugation is linear over ℝ. Contrast conjugateOperator_complex_smul, where a complex scalar picks up a conjugate.

theorem TauCeti.RealComplexification.conjugateOperator_complex_smul {E : Type v} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (c : ℂ) (A : RealComplexification E →L[ℂ] RealComplexification E) : conjugateOperator (c • A) = (starRingEnd ℂ) c • conjugateOperator A

Conjugation of operators is conjugate-linear over ℂ.

@[simp]

theorem TauCeti.RealComplexification.conjugateOperator_involutive {E : Type v} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (A : RealComplexification E →L[ℂ] RealComplexification E) : conjugateOperator (conjugateOperator A) = A

Conjugating twice returns the original operator.

theorem TauCeti.RealComplexification.conjugateOperator_adjoint {E : Type v} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (A : RealComplexification E →L[ℂ] RealComplexification E) : conjugateOperator (ContinuousLinearMap.adjoint A) = ContinuousLinearMap.adjoint (conjugateOperator A)

Canonical conjugation commutes with taking adjoints.

theorem TauCeti.RealComplexification.norm_conjugateOperator_le {E : Type v} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (A : RealComplexification E →L[ℂ] RealComplexification E) : ‖conjugateOperator A‖ ≤ ‖A‖

Conjugation does not increase the operator norm. With conjugateOperator_involutive this one-sided bound upgrades to the equality norm_conjugateOperator.

theorem TauCeti.RealComplexification.norm_conjugateOperator {E : Type v} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (A : RealComplexification E →L[ℂ] RealComplexification E) : ‖conjugateOperator A‖ = ‖A‖

Conjugation preserves the operator norm.

theorem TauCeti.RealComplexification.isometry_conjugateOperator {E : Type v} [NormedAddCommGroup E] [InnerProductSpace ℝ E] : Isometry conjugateOperator

Conjugation is an isometry of the operator algebra. It is only conjugate-linear over ℂ, so this is a metric statement rather than a linear-isometry one.

noncomputable def TauCeti.RealComplexification.conjugateOperatorHom {E : Type v} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] : (RealComplexification E →L[ℂ] RealComplexification E) →⋆ₐ[ℝ] RealComplexification E →L[ℂ] RealComplexification E

Canonical conjugation is a continuous real star-algebra automorphism of bounded operators on the complexification.

Equations

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

theorem TauCeti.RealComplexification.continuous_conjugateOperatorHom {E : Type v} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] : Continuous ⇑conjugateOperatorHom

The conjugation star-algebra map is continuous, being an isometry.

theorem TauCeti.RealComplexification.conjugateOperator_complexify {E : Type v} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (A : E →L[ℝ] E) : conjugateOperator (complexify A) = complexify A

Every complexified real operator is fixed by canonical conjugation.

theorem TauCeti.RealComplexification.conjugateOperator_cfcHom {E : Type v} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (C : RealComplexification E →L[ℂ] RealComplexification E) (hC : IsSelfAdjoint C) (hfix : conjugateOperator C = C) (g : C(↑(spectrum ℝ C), ℝ)) : conjugateOperator ((cfcHom hC) g) = (cfcHom hC) g

The bundled functional calculus of a conjugation-fixed self-adjoint operator lands in the fixed-point subalgebra. Stated for cfcHom, the ⋆-algebra homomorphism itself, rather than for a single symbol: this is what a descent of the calculus needs, and the symbol-level statements conjugateOperator_cfc_eq and conjugateOperator_cfc below are corollaries.

The proof is the uniqueness of the calculus: conjugateOperatorHom.comp (cfcHom hC) is another continuous real ⋆-algebra homomorphism sending the restricted identity to C.

theorem TauCeti.RealComplexification.conjugateOperator_cfc_eq {E : Type v} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (C : RealComplexification E →L[ℂ] RealComplexification E) (hC : IsSelfAdjoint C) (hfix : conjugateOperator C = C) (f : ℝ → ℝ) (hf : ContinuousOn f (spectrum ℝ C)) : conjugateOperator (cfc f C) = cfc f C

Continuous real functional calculus of a conjugation-fixed self-adjoint operator remains conjugation-fixed.

Descent of conjugation-fixed operators

theorem TauCeti.RealComplexification.fixed_operator_maps_real_to_real {E : Type v} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {A : RealComplexification E →L[ℂ] RealComplexification E} (hfix : conjugateOperator A = A) (x : E) : (A (ofReal x)).im = 0

A conjugation-fixed operator maps the real copy into itself: the imaginary coordinate of A (ofReal x) vanishes.

theorem TauCeti.RealComplexification.fixed_operator_on_ofReal {E : Type v} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {A : RealComplexification E →L[ℂ] RealComplexification E} (hfix : conjugateOperator A = A) (x : E) : A (ofReal x) = ofReal ((realPartOperator A) x)

On the real copy, a conjugation-fixed operator is determined by its real restriction.

theorem TauCeti.RealComplexification.complexify_realPartOperator {E : Type v} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {A : RealComplexification E →L[ℂ] RealComplexification E} (hfix : conjugateOperator A = A) : complexify (realPartOperator A) = A

A conjugation-fixed complex operator is exactly the complexification of its restriction to the real copy.

Complexification and the Gram operator

theorem TauCeti.RealComplexification.complexify_adjoint {E : Type v} {F : Type vF} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] [NormedAddCommGroup F] [InnerProductSpace ℝ F] [CompleteSpace F] (T : E →L[ℝ] F) : complexify (ContinuousLinearMap.adjoint T) = ContinuousLinearMap.adjoint (complexify T)

Complexification commutes with the Hilbert-space adjoint.

theorem TauCeti.RealComplexification.complexify_gram {E : Type v} {F : Type vF} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] [NormedAddCommGroup F] [InnerProductSpace ℝ F] [CompleteSpace F] (T : E →L[ℝ] F) : complexify (ContinuousLinearMap.adjoint T ∘SL T) = ContinuousLinearMap.adjoint (complexify T) ∘SL complexify T

Complexification commutes with forming the Gram operator Tᵃ ∘ T.

Complexification as a real ⋆-algebra homomorphism

Complexification/Basic.lean supplies the additive and composition laws; complexify_comp and complexify_id are the ring laws once ContinuousLinearMap.mul_def is unfolded. Adding complexify_adjoint bundles complexify into a unital ⋆-algebra map over ℝ, which is the form the real spectral theory needs.

The ⋆-algebra structure maps are not re-exported as separate lemmas here. Three DavisKahan modules already declare complexify_mul, complexify_one and complexify_star in three different namespaces, and several of their consumers use the bare names under an open of this namespace; a fourth copy here would make those uses ambiguous. Use map_mul complexifyStarAlgHom, map_one, map_star instead, and see the note in RealContinuousFunctionalCalculus.lean on consolidating the three.

theorem TauCeti.RealComplexification.complexify_algebraMapComplex {E : Type v} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (r : ℝ) : complexify ((algebraMap ℝ (E →L[ℝ] E)) r) = (algebraMap ℂ (RealComplexification E →L[ℂ] RealComplexification E)) ↑r

Complexification intertwines the real algebra map of E →L[ℝ] E with the complex algebra map of the complexified operator algebra, along ℝ → ℂ.

Stated against algebraMap ℂ rather than algebraMap ℝ because the complexified operator algebra carries two real algebra structures: ContinuousLinearMap.algebra, which is global and sends r to the ambient r • 1, and the scoped complexOperatorRealAlgebra, which sends r to (r : ℂ) • 1. They are propositionally but not definitionally equal. The complex algebra map is unambiguous, so it is the one to phrase transport against.

theorem TauCeti.RealComplexification.algebraMap_complexOperator {E : Type v} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (r : ℝ) : (algebraMap ℝ (RealComplexification E →L[ℂ] RealComplexification E)) r = (algebraMap ℂ (RealComplexification E →L[ℂ] RealComplexification E)) ↑r

The scoped real algebra structure on the complexified operator algebra factors the complex one through ℝ → ℂ; this holds by definition of Algebra.complexToReal. It is what makes spectrum ℝ on that algebra the real trace of spectrum ℂ.

theorem TauCeti.RealComplexification.complexify_algebraMapReal {E : Type v} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (r : ℝ) : complexify ((algebraMap ℝ (E →L[ℝ] E)) r) = (algebraMap ℝ (RealComplexification E →L[ℂ] RealComplexification E)) r

Complexification intertwines the two real algebra maps, for the scoped real structure on the target.

noncomputable def TauCeti.RealComplexification.complexifyStarAlgHom {E : Type v} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] : (E →L[ℝ] E) →⋆ₐ[ℝ] RealComplexification E →L[ℂ] RealComplexification E

Complexification bundled as a unital real ⋆-algebra homomorphism. Its target carries the scoped real algebra structure complexOperatorRealAlgebra, so a consumer needs open scoped TauCeti.RealComplexification.

Equations

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

@[simp]

theorem TauCeti.RealComplexification.complexifyStarAlgHom_apply {E : Type v} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (A : E →L[ℝ] E) : complexifyStarAlgHom A = complexify A

complexifyStarAlgHom acts by complexify.

The fixed-point subalgebra is closed under the whole spectral calculus

conjugateOperator_cfc_eq above needs the symbol to be continuous on the spectrum. The result below removes that side condition. Modulus transport is kept downstream in ForTauCeti.Analysis.InnerProductSpace.ModulusTransport, so this functional-calculus foundation does not depend on the modulus built from it.

theorem TauCeti.RealComplexification.conjugateOperator_cfc {E : Type v} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (C : RealComplexification E →L[ℂ] RealComplexification E) (hC : IsSelfAdjoint C) (hfix : conjugateOperator C = C) (f : ℝ → ℝ) : conjugateOperator (cfc f C) = cfc f C

The continuous functional calculus of a conjugation-fixed self-adjoint operator is conjugation-fixed, with no continuity hypothesis on the symbol: off the continuous symbols the calculus is zero, which is fixed as well.

theorem TauCeti.RealComplexification.conjugateOperator_nonneg {E : Type v} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {A : RealComplexification E →L[ℂ] RealComplexification E} (hA : 0 ≤ A) : 0 ≤ conjugateOperator A

Canonical conjugation preserves positivity of an operator. It is an ℝ-linear ⋆-algebra automorphism, so it preserves both halves of the definition; the quadratic form is transported by conjugating the argument.