The continuous functional calculus on real and RCLike Hilbert spaces

Mathlib's continuous functional calculus for bounded self-adjoint operators comes from the complex C⋆-algebra structure of E →L[ℂ] E, so it is available only on complex Hilbert spaces. This file supplies the instance

ContinuousFunctionalCalculus ℝ (E →L[𝕜] E) IsSelfAdjoint

for every Hilbert space E over RCLike 𝕜, in any dimension, for every real algebra structure on E →L[𝕜] E compatible with the 𝕜-action (IsScalarTower ℝ 𝕜 (E →L[𝕜] E)), and with it Mathlib's star order (ContinuousLinearMap.instStarOrderedRingRCLike). Hence cfc f T and the positive square root CFC.sqrt T of a positive operator are available on Hilbert spaces over every RCLike 𝕜, as is the absolute value CFC.abs T = √(T† T) of every bounded operator. Over an abstract RCLike field, the real algebra structure is ContinuousLinearMap.realAlgebra, obtained by restricting scalars along ℝ → 𝕜; at 𝕜 = ℝ and 𝕜 = ℂ it is Mathlib's own, and any two compatible real algebra structures coincide by Algebra.restrictScalars_eq.

The real calculus is pulled back from the complexification. Complexification T ↦ T_ℂ (ContinuousLinearMap.complexifyL2StarAlgHom) is an isometric unital ⋆-homomorphism from X →L[ℝ] X into the complex C⋆-algebra X_ℂ →L[ℂ] X_ℂ, so it is a closed embedding, and StarAlgHom.continuousFunctionalCalculus_of_isClosedEmbedding applies. Consequently complexification preserves the spectrum of a self-adjoint operator (ContinuousLinearMap.spectrum_complexifyL2) and intertwines the two calculi (ContinuousLinearMap.complexifyL2_cfc): (f(T))_ℂ = f(T_ℂ). Since the calculus of the complex C⋆-algebra is isometric, so is the real one.

The calculus over RCLike 𝕜 is in turn pulled back from the real one along realification. A Hilbert space E over 𝕜 is a real Hilbert space for the inner product re ⟪x, y⟫ (InnerProductSpace.rclikeToReal), and restricting scalars T ↦ T.restrictScalars ℝ is an isometric unital ⋆-homomorphism from E →L[𝕜] E into the real operators on E (ContinuousLinearMap.restrictScalarsStarAlgHom): the adjoint for re ⟪·, ·⟫ of the restriction of T is the restriction of T† (ContinuousLinearMap.adjoint_restrictScalars). Consequently realification preserves the spectrum of a self-adjoint operator (ContinuousLinearMap.spectrum_restrictScalars) and intertwines the two calculi (ContinuousLinearMap.restrictScalars_cfc).

Main declarations

• ContinuousLinearMap.instContinuousFunctionalCalculusRealIsSelfAdjoint: the continuous functional calculus for bounded self-adjoint operators on a real Hilbert space.
• ContinuousLinearMap.instContinuousFunctionalCalculusRCLikeIsSelfAdjoint: the continuous functional calculus for bounded self-adjoint operators on a Hilbert space over RCLike 𝕜.
• ContinuousLinearMap.instStarOrderedRingRCLike: Mathlib's star order on bounded operators, registered here as an instance.
• ContinuousLinearMap.instIsometricContinuousFunctionalCalculusRealIsSelfAdjoint: the real calculus is isometric, hence continuous in the operator.
• ContinuousLinearMap.spectrum_complexifyL2: complexification preserves the spectrum of a self-adjoint operator.
• ContinuousLinearMap.complexifyL2_cfc: complexification commutes with the continuous functional calculus.
• ContinuousLinearMap.restrictScalarsStarAlgHom: realification of the bounded operators on a Hilbert space over RCLike 𝕜, as a ⋆-algebra homomorphism over ℝ.
• ContinuousLinearMap.spectrum_restrictScalars: realification preserves the spectrum of a self-adjoint operator.
• ContinuousLinearMap.restrictScalars_cfc: realification commutes with the continuous functional calculus.
• LinearIsometryEquiv.cfcₙ_conjStarAlgEquiv, LinearIsometryEquiv.posPart_conjStarAlgEquiv, LinearIsometryEquiv.negPart_conjStarAlgEquiv: isometric conjugation commutes with the non-unital continuous functional calculus and with positive and negative parts.

Acknowledgements

A real continuous functional calculus for bounded operators, also obtained from the complexification, appears in ForTauCeti/Analysis/InnerProductSpace/RealContinuousFunctionalCalculus.lean of the AIQ DKPS formalization (Kitware, Inc.; Apache-2.0). There the calculus is descended through the conjugation of the complexification; here it is restricted to the closed range of the complexification map. The normal-operator half-plane bound ContinuousLinearMap.nonneg_add_star_sub_smul_of_spectrum_re is adapted from DavisKahan/InfiniteDimensional/TanTwoTheta/QuarterAcuteFormGap.lean, Kitware DKPS (Jon Crall, OpenAI GPT-5.6 Thinking and Claude Opus 5; Apache-2.0). It turns a lower bound a on real parts of the spectrum into W + W† ≥ 2 a I.

instance ContinuousLinearMap.instContinuousFunctionalCalculusRealIsSelfAdjoint {X : Type u_1} [NormedAddCommGroup X] [InnerProductSpace ℝ X] [CompleteSpace X] : ContinuousFunctionalCalculus ℝ (X →L[ℝ] X) IsSelfAdjoint

The continuous functional calculus for bounded self-adjoint operators on a real Hilbert space, pulled back from the complexification.

theorem ContinuousLinearMap.spectrum_complexifyL2 {X : Type u_1} [NormedAddCommGroup X] [InnerProductSpace ℝ X] [CompleteSpace X] {T : X →L[ℝ] X} (hT : IsSelfAdjoint T) : spectrum ℝ T.complexifyL2 = spectrum ℝ T

Complexification preserves the spectrum of a self-adjoint operator on a real Hilbert space.

theorem ContinuousLinearMap.complexifyL2_cfc {X : Type u_1} [NormedAddCommGroup X] [InnerProductSpace ℝ X] [CompleteSpace X] (f : ℝ → ℝ) (T : X →L[ℝ] X) (hf : ContinuousOn f (spectrum ℝ T) := by cfc_cont_tac) (hT : IsSelfAdjoint T := by cfc_tac) : (cfc f T).complexifyL2 = cfc f T.complexifyL2

Complexification commutes with the continuous functional calculus: for a self-adjoint operator T on a real Hilbert space and f continuous on its spectrum, (f(T))_ℂ = f(T_ℂ).

instance ContinuousLinearMap.instIsometricContinuousFunctionalCalculusRealIsSelfAdjoint {X : Type u_1} [NormedAddCommGroup X] [InnerProductSpace ℝ X] [CompleteSpace X] : IsometricContinuousFunctionalCalculus ℝ (X →L[ℝ] X) IsSelfAdjoint

The continuous functional calculus for bounded self-adjoint operators on a real Hilbert space is isometric: ‖f(T)‖ is the supremum of |f| on the spectrum of T. This is what makes the calculus continuous in the operator, as in CFC.continuousOn_rpow and CFC.continuousOn_sqrt.

@[simp]

theorem ContinuousLinearMap.adjoint_restrictScalars {𝕜 : Type u_2} {E : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] {F : Type u_4} [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] (T : E →L[𝕜] F) : adjoint (restrictScalars ℝ T) = restrictScalars ℝ (adjoint T)

For the real inner product re ⟪x, y⟫, the adjoint of the realification of a bounded operator is the realification of its adjoint.

@[simp]

theorem ContinuousLinearMap.isSelfAdjoint_restrictScalars_iff {𝕜 : Type u_2} {E : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] {T : E →L[𝕜] E} : IsSelfAdjoint (restrictScalars ℝ T) ↔ IsSelfAdjoint T

A bounded operator on a Hilbert space over RCLike 𝕜 is self-adjoint exactly when its realification is, for the real inner product re ⟪x, y⟫.

noncomputable def ContinuousLinearMap.restrictScalarsStarAlgHom (𝕜 : Type u_2) (E : Type u_3) [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] [Algebra ℝ (E →L[𝕜] E)] [IsScalarTower ℝ 𝕜 (E →L[𝕜] E)] : (E →L[𝕜] E) →⋆ₐ[ℝ] E →L[ℝ] E

Realification T ↦ T.restrictScalars ℝ of the bounded operators on a Hilbert space over RCLike 𝕜, as a ⋆-algebra homomorphism over ℝ into the bounded operators on the underlying real Hilbert space, for any real algebra structure compatible with the 𝕜-action.

@[simp]

theorem ContinuousLinearMap.restrictScalarsStarAlgHom_apply {𝕜 : Type u_2} {E : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] [Algebra ℝ (E →L[𝕜] E)] [IsScalarTower ℝ 𝕜 (E →L[𝕜] E)] (T : E →L[𝕜] E) : (restrictScalarsStarAlgHom 𝕜 E) T = restrictScalars ℝ T

theorem ContinuousLinearMap.isometry_restrictScalarsStarAlgHom (𝕜 : Type u_2) (E : Type u_3) [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] [Algebra ℝ (E →L[𝕜] E)] [IsScalarTower ℝ 𝕜 (E →L[𝕜] E)] : Isometry ⇑(restrictScalarsStarAlgHom 𝕜 E)

Realification of the bounded operators on a Hilbert space over RCLike 𝕜 is an isometry.

theorem ContinuousLinearMap.isClosedEmbedding_restrictScalarsStarAlgHom (𝕜 : Type u_2) (E : Type u_3) [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] [Algebra ℝ (E →L[𝕜] E)] [IsScalarTower ℝ 𝕜 (E →L[𝕜] E)] : Topology.IsClosedEmbedding ⇑(restrictScalarsStarAlgHom 𝕜 E)

Realification of the bounded operators on a Hilbert space over RCLike 𝕜 is a closed embedding.

instance ContinuousLinearMap.instContinuousFunctionalCalculusRCLikeIsSelfAdjoint {𝕜 : Type u_2} {E : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] [Algebra ℝ (E →L[𝕜] E)] [IsScalarTower ℝ 𝕜 (E →L[𝕜] E)] : ContinuousFunctionalCalculus ℝ (E →L[𝕜] E) IsSelfAdjoint

The continuous functional calculus for bounded self-adjoint operators on a Hilbert space over RCLike 𝕜, for any real algebra structure on the operators compatible with the 𝕜-action, pulled back from the real calculus along realification.

theorem ContinuousLinearMap.spectrum_restrictScalars {𝕜 : Type u_2} {E : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] [Algebra ℝ (E →L[𝕜] E)] [IsScalarTower ℝ 𝕜 (E →L[𝕜] E)] {T : E →L[𝕜] E} (hT : IsSelfAdjoint T) : spectrum ℝ (restrictScalars ℝ T) = spectrum ℝ T

Realification preserves the spectrum of a self-adjoint operator on a Hilbert space over RCLike 𝕜.

theorem ContinuousLinearMap.restrictScalars_cfc {𝕜 : Type u_2} {E : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] [Algebra ℝ (E →L[𝕜] E)] [IsScalarTower ℝ 𝕜 (E →L[𝕜] E)] (f : ℝ → ℝ) (T : E →L[𝕜] E) (hf : ContinuousOn f (spectrum ℝ T) := by cfc_cont_tac) (hT : IsSelfAdjoint T := by cfc_tac) : restrictScalars ℝ (cfc f T) = cfc f (restrictScalars ℝ T)

Realification commutes with the continuous functional calculus: for a self-adjoint operator T on a Hilbert space over RCLike 𝕜 and f continuous on its spectrum, (f(T)).restrictScalars ℝ = f(T.restrictScalars ℝ).

theorem ContinuousLinearMap.inner_sqrt_apply_sqrt_apply_eq_inner {X : Type u_1} [NormedAddCommGroup X] [InnerProductSpace ℝ X] [CompleteSpace X] {T : X →L[ℝ] X} (hT : 0 ≤ T) (u v : X) : inner ℝ ((CFC.sqrt T) u) ((CFC.sqrt T) v) = inner ℝ (T u) v

The inner product of two images under a positive operator's square root.

theorem ContinuousLinearMap.norm_rpow_le_one_of_one_le_of_nonpos {X : Type u_1} [NormedAddCommGroup X] [InnerProductSpace ℝ X] [CompleteSpace X] (P : X →L[ℝ] X) (hP : 1 ≤ P) {s : ℝ} (hs : s ≤ 0) : ‖P ^ s‖ ≤ 1

Negative real powers of a positive real Hilbert space operator above the identity are contractions in operator norm.

theorem ContinuousLinearMap.norm_rpow_apply_le_of_one_le_of_nonpos {X : Type u_1} [NormedAddCommGroup X] [InnerProductSpace ℝ X] [CompleteSpace X] (P : X →L[ℝ] X) (hP : 1 ≤ P) {s : ℝ} (hs : s ≤ 0) (y : X) : ‖(P ^ s) y‖ ≤ ‖y‖

Nonpositive real powers of an operator above the identity do not increase vector norms.

theorem ContinuousLinearMap.nonneg_add_star_sub_smul_of_spectrum_re {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (W : E →L[ℂ] E) [IsStarNormal W] {a : ℝ} (hspec : ∀ z ∈ spectrum ℂ W, a ≤ z.re) : 0 ≤ W + star W - ↑(2 * a) • 1

A spectral half-plane bound for a normal operator is an order bound for its Hermitian part.

theorem LinearIsometryEquiv.continuous_conjStarAlgEquiv {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] (e : E ≃ₗᵢ[𝕜] F) : Continuous ⇑e.conjStarAlgEquiv

Conjugation of bounded operators by a linear isometric equivalence is continuous.

theorem LinearIsometryEquiv.cfcₙ_conjStarAlgEquiv {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] [Algebra ℝ (E →L[𝕜] E)] [IsScalarTower ℝ 𝕜 (E →L[𝕜] E)] [Algebra ℝ (F →L[𝕜] F)] [IsScalarTower ℝ 𝕜 (F →L[𝕜] F)] (e : E ≃ₗᵢ[𝕜] F) (f : ℝ → ℝ) (A : E →L[𝕜] E) : cfcₙ f (e.conjStarAlgEquiv A) = e.conjStarAlgEquiv (cfcₙ f A)

Conjugation by a linear isometric equivalence commutes with the non-unital continuous functional calculus.

@[simp]

theorem LinearIsometryEquiv.posPart_conjStarAlgEquiv {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] [Algebra ℝ (E →L[𝕜] E)] [IsScalarTower ℝ 𝕜 (E →L[𝕜] E)] [Algebra ℝ (F →L[𝕜] F)] [IsScalarTower ℝ 𝕜 (F →L[𝕜] F)] (e : E ≃ₗᵢ[𝕜] F) (A : E →L[𝕜] E) : (e.conjStarAlgEquiv A)⁺ = e.conjStarAlgEquiv A⁺

Conjugation by a linear isometric equivalence commutes with the positive part of a bounded operator.

@[simp]

theorem LinearIsometryEquiv.negPart_conjStarAlgEquiv {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] [Algebra ℝ (E →L[𝕜] E)] [IsScalarTower ℝ 𝕜 (E →L[𝕜] E)] [Algebra ℝ (F →L[𝕜] F)] [IsScalarTower ℝ 𝕜 (F →L[𝕜] F)] (e : E ≃ₗᵢ[𝕜] F) (A : E →L[𝕜] E) : (e.conjStarAlgEquiv A)⁻ = e.conjStarAlgEquiv A⁻

Conjugation by a linear isometric equivalence commutes with the negative part of a bounded operator.