Continuous functional calculus over ℝ for a real Hilbert space #
ContinuousLinearMap.instContinuousFunctionalCalculusRealIsSelfAdjoint registers
ContinuousFunctionalCalculus ℝ (E →L[ℝ] E) IsSelfAdjoint
for every real Hilbert space E, at unrestricted dimension.
Why this is not in Mathlib #
Mathlib's only unital real calculus for operators,
IsSelfAdjoint.instContinuousFunctionalCalculus, descends by spectrum restriction from a
calculus over ℂ for star-normal elements, and CStarAlgebra (E →L[𝕜] E) is registered only
at 𝕜 = ℂ. Matrix n n 𝕜 escapes this through a separate spectral-theorem construction in
Analysis/Matrix/HermitianFunctionalCalculus.lean, so a real matrix calculus exists while the
operator one does not. Mathlib records the gap in prose: Analysis/InnerProductSpace/
StarOrder.lean proves ContinuousLinearMap.instStarOrderedRingRCLike for a general RCLike
field and declines to register it, because it takes exactly this calculus as an argument and
"for the moment we only have this for 𝕜 := ℂ". Registering the instance below supplies the
missing input to ContinuousLinearMap.instStarOrderedRingRCLike. The modulus and polar
factorization consume it downstream rather than being dependencies of this foundational file.
This real instance is the concrete-field base case used by the RCLike-generic continuous
functional calculus in ScalarTransportFunctionalCalculus.lean.
The construction #
Complexification, as a proof technique rather than as architecture: the missing ingredient is
genuinely complex-only, so the smallest necessary portion is transported and the actual
mathematical object -- cfcHom itself -- is descended, not an existential witness.
For a : E →L[ℝ] E self-adjoint:
complexify ais a self-adjoint operator on the complexification, and the complexified algebra already carries a real calculus (realContinuousFunctionalCalculus);spectrum_complexifyidentifies the two spectra, so the symbol algebras agree (spectrumComplexifyMap) andcomplexifiedCfcHomis a real⋆-algebra mapC(spectrum ℝ a, ℝ) →⋆ₐ[ℝ] (Eℂ →L[ℂ] Eℂ);- its whole image is fixed by the canonical conjugation
(
conjugateOperator_complexifiedCfcHom, fromconjugateOperator_cfcHom), and a conjugation-fixed operator is a complexification (complexify_realPartOperator), so the map descends torealCfcHom : C(spectrum ℝ a, ℝ) →⋆ₐ[ℝ] (E →L[ℝ] E); - every field of the calculus is then read off through
complexify, which is an injective isometric unital⋆-algebra map (complexifyStarAlgHom,isometry_complexify).
Main results #
TauCeti.RealComplexification.realCfcHom: the descended calculus;ContinuousLinearMap.instContinuousFunctionalCalculusRealIsSelfAdjoint: the real-field instance;TauCeti.RealComplexification.complexify_cfc: naturality of the calculus under complexification.
A duplication this file does not resolve #
complexify_mul, complexify_one and complexify_star are each declared in two or three
DavisKahan modules, in different namespaces, and several consumers use the bare names under an
open of TauCeti.RealComplexification. Adding canonical copies here would make those uses
ambiguous, so this file routes through complexifyStarAlgHom and map_mul / map_one /
map_star instead. Consolidating the three copies into Complexification/Basic.lean is a
separate, mechanical piece of work.
Transporting the symbol algebra #
The identity, read as a map from the spectrum of complexify a to the spectrum of a.
It is a bijection, by spectrum_complexify.
Equations
- TauCeti.RealComplexification.spectrumComplexifyMap a = { toFun := Set.inclusion ⋯, continuous_toFun := ⋯ }
Instances For
spectrumComplexifyMap does not move points: it is the identity on underlying reals.
spectrumComplexifyMap is surjective, the two spectra being equal. This is what makes
precomposition with it injective on symbols, and what turns Set.range (f ∘ _) into
Set.range f.
The calculus of a, computed in the complexification #
The real continuous functional calculus of a, taken in the complexified operator
algebra: a symbol on spectrum ℝ a is read as a symbol on spectrum ℝ (complexify a) and fed
to the calculus that Complexification/FunctionalCalculus.lean already registers there.
Equations
Instances For
complexifiedCfcHom unfolded: reindex the symbol, then apply the complex-algebra
calculus.
complexifiedCfcHom is continuous: cfcHom is, and reindexing symbols is.
complexifiedCfcHom is injective: cfcHom is, and reindexing along a surjection is.
complexifiedCfcHom sends the restricted identity symbol to complexify a.
The spectral mapping theorem for complexifiedCfcHom.
complexifiedCfcHom produces self-adjoint operators, real symbols being self-adjoint.
The calculus of complexify a stays in the fixed-point subalgebra of the canonical
conjugation. This is the descent step: by complexify_realPartOperator a conjugation-fixed
operator is the complexification of a bounded real operator.
The descended calculus #
The real continuous functional calculus of a self-adjoint a : E →L[ℝ] E, as a function on
symbols: complexifiedCfcHom followed by the descent of a conjugation-fixed operator to the
real copy. complexifyStarAlgHom_realCfcFun says the descent is exact.
Equations
Instances For
The defining property of the descended calculus. Every algebraic law below is this
identity plus injectivity of complexify.
complexifyStarAlgHom is injective; this is complexify_injective under the bundling.
The real continuous functional calculus of a self-adjoint bounded operator on a real
Hilbert space, bundled as a ⋆-algebra homomorphism over ℝ.
Equations
- TauCeti.RealComplexification.realCfcHom ha = { toFun := TauCeti.RealComplexification.realCfcFun ha, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯, commutes' := ⋯, map_star' := ⋯ }
Instances For
realCfcHom acts by realCfcFun.
The descent identity for the bundled calculus: complexifying realCfcHom recovers the
calculus computed in the complexification. Every property of realCfcHom below is transported
through this equation.
realCfcHom is continuous. Continuity transports backwards along complexify because
it is an isometric embedding, not merely norm-preserving; this is what isometry_complexify
is for.
realCfcHom is injective.
realCfcHom sends the restricted identity symbol to a; with continuity and
multiplicativity this is what pins the calculus down uniquely.
The spectral mapping theorem over ℝ: the spectrum of f applied to a is the range
of f on the spectrum of a.
realCfcHom produces self-adjoint operators, so the calculus is closed on its own
predicate.
Nontriviality #
A nontrivial bounded operator algebra forces a nontrivial space.
The instance #
The continuous functional calculus over ℝ for self-adjoint bounded operators on a real
Hilbert space, in unrestricted dimension.
Naturality of the calculus along the complexification #
The instance above makes cfc f a meaningful for a real self-adjoint a, but leaves it
opaque: cfcHom is a choose against exists_cfc_of_predicate, so nothing yet connects it
to realCfcHom, which is the map the instance actually supplied. Uniqueness closes that gap
(ContinuousMap.UniqueHom ℝ holds for every T2 real topological ⋆-algebra), and with it the
calculus commutes with complexify.
This is the interface a consumer wants. A statement proved over ℂ for complexify a
transfers to a itself, and — in the other direction — a real object defined by descent from
the complexification is recognized as a genuine real functional calculus.
cfcHom, for a self-adjoint operator on a real Hilbert space, is the descended
calculus realCfcHom. Both are continuous ⋆-algebra maps sending the identity symbol to
a, and ContinuousMap.UniqueHom ℝ says there is only one such.
The continuous functional calculus commutes with complexification.
The complexification is an injective isometric unital ⋆-algebra map that preserves spectra,
so this is the naturality one expects; the content is that the real calculus on E →L[ℝ] E
that this file registers is the one descended from the complex side, which is
cfcHom_eq_realCfcHom.
The hypotheses are the ones cfc itself requires: without them both sides are 0 by
cfc_apply_of_not_predicate, so the statement is not vacuous but is uninteresting.
The reverse reading of complexify_cfc: a real functional calculus may be computed in the
complexification. This is the form the angle operators of the Davis--Kahan development use,
where the real object is defined by descent and has to be recognized as cfc.
Positivity #
complexify preserves and reflects the order, because it preserves self-adjointness and the
real spectrum, and in a C⋆-algebra nonnegativity is exactly a self-adjoint element with
nonnegative spectrum. Modulus naturality is downstream in
ForTauCeti.Analysis.InnerProductSpace.ModulusTransport.
Complexification preserves and reflects nonnegativity.