Real continuous functional calculus at an arbitrary RCLike field

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

for every RCLike 𝕜 and every 𝕜-Hilbert space E, at unrestricted dimension.

Mathlib registers this at 𝕜 = ℂ, through the C⋆-algebra structure of E →L[ℂ] E; ForTauCeti/Analysis/InnerProductSpace/RealContinuousFunctionalCalculus.lean registers it at 𝕜 = ℝ, by descending the complex calculus along the complexification. Every RCLike field is isomorphic to one of those two, so the general case is a transport — of the calculus itself, not of an existential witness.

What this removes

Scalar-generic operator modules are stated over an arbitrary RCLike field but built on real functional calculus, and historically carried

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

in every signature. None of those is a mathematical hypothesis of any theorem that carries them: the first two are restriction of scalars (ContinuousLinearMap.realAlgebra), and the third is this file. A caller of a scalar-generic theorem should supply [RCLike 𝕜] and the mathematics, and nothing else.

The shape of the argument

ScalarTransport e E is E with the 𝕂-structure induced through a field isomorphism e : RCLikeIso 𝕜 𝕂, and ScalarTransport.clm carries operators across. It is a bijection that preserves composition, the adjoint and the norm, so it is an isometric ℝ-⋆-algebra isomorphism (E →L[𝕜] E) ≃⋆ₐ[ℝ] (ScalarTransport e E →L[𝕂] ScalarTransport e E), and ContinuousFunctionalCalculus.of_starAlgEquiv moves the calculus back along it.

RCLike.I_eq_zero_or_im_I_eq_one supplies the isomorphism, to ℝ or to ℂ. This is the same two-case dispatch that ContinuousLinearMap.hasMinMaxLowerBoundEverywhere and TauCeti.DavisKahan.Sylvester.hasUnboundedSylvesterKyFan already use, and it lands in the same place: an instance, discharged once, invisible to every caller.

Provenance

• Original repository: Davis--Kahan/DKPS formalization (Kitware, Inc.).
• Original module: none. Written directly here, 2026-09-03.
• Extraction class: new. It depends on RCLike/ScalarTransport.lean, InnerProductSpace/RealContinuousFunctionalCalculus.lean and CStarAlgebra/ContinuousFunctionalCalculusTransport.lean, all of which are in ForTauCeti.
• Namespace: TauCeti.ScalarTransport for the isomorphism, ContinuousLinearMap for the instance, matching the objects they are about.
• Original authors / copyright: Jon Crall, Claude Opus 5; Copyright (c) 2026 Kitware, Inc.; Apache 2.0.
• Spectra influence: none.

@[simp]

theorem TauCeti.ScalarTransport.clm_mul {𝕜 : Type u} {𝕂 : Type w} [RCLike 𝕜] [RCLike 𝕂] {e : RCLikeIso 𝕜 𝕂} {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (S T : E →L[𝕜] E) : clm (S * T) = clm S * clm T

The transport preserves composition: it does not move the underlying functions.

@[simp]

theorem TauCeti.ScalarTransport.clm_one {𝕜 : Type u} {𝕂 : Type w} [RCLike 𝕜] [RCLike 𝕂] {e : RCLikeIso 𝕜 𝕂} {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] : clm 1 = 1

The transport preserves the identity operator.

@[simp]

theorem TauCeti.ScalarTransport.clm_add {𝕜 : Type u} {𝕂 : Type w} [RCLike 𝕜] [RCLike 𝕂] {e : RCLikeIso 𝕜 𝕂} {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (S T : E →L[𝕜] E) : clm (S + T) = clm S + clm T

The transport is additive.

@[simp]

theorem TauCeti.ScalarTransport.clm_smul {𝕜 : Type u} {𝕂 : Type w} [RCLike 𝕜] [RCLike 𝕂] {e : RCLikeIso 𝕜 𝕂} {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (c : 𝕜) (T : E →L[𝕜] E) : clm (c • T) = e.toRingEquiv c • clm T

The transport is semilinear along e: a 𝕜-scalar becomes its image.

@[simp]

theorem TauCeti.ScalarTransport.clm_real_smul {𝕜 : Type u} {𝕂 : Type w} [RCLike 𝕜] [RCLike 𝕂] {e : RCLikeIso 𝕜 𝕂} {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (r : ℝ) (T : E →L[𝕜] E) : clm (r • T) = r • clm T

The transport is ℝ-homogeneous. Both sides act by restriction of scalars along their own algebraMap from ℝ, and e fixes the reals.

@[simp]

theorem TauCeti.ScalarTransport.clm_star {𝕜 : Type u} {𝕂 : Type w} [RCLike 𝕜] [RCLike 𝕂] {e : RCLikeIso 𝕜 𝕂} {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] (T : E →L[𝕜] E) : clm (star T) = star (clm T)

The transport is a ⋆-map: star on a Hilbert-space operator algebra is the adjoint, and adjoint_clm is exactly that statement.

noncomputable def TauCeti.ScalarTransport.clmStarAlgEquiv {𝕜 : Type u} {𝕂 : Type w} [RCLike 𝕜] [RCLike 𝕂] (e : RCLikeIso 𝕜 𝕂) (E : Type v) [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] : (E →L[𝕜] E) ≃⋆ₐ[ℝ] ScalarTransport e E →L[𝕂] ScalarTransport e E

The scalar transport of operators is an ℝ-⋆-algebra isomorphism.

Composition, the adjoint and the norm are all preserved because the transport changes no function and no metric; only the field the scalars are named in moves.

Equations

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

@[simp]

theorem TauCeti.ScalarTransport.clmStarAlgEquiv_apply {𝕜 : Type u} {𝕂 : Type w} [RCLike 𝕜] [RCLike 𝕂] {e : RCLikeIso 𝕜 𝕂} {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] (T : E →L[𝕜] E) : (clmStarAlgEquiv e E) T = clm T

The star-algebra equivalence acts by the operator transport clm.

theorem TauCeti.ScalarTransport.continuous_clmStarAlgEquiv {𝕜 : Type u} {𝕂 : Type w} [RCLike 𝕜] [RCLike 𝕂] {e : RCLikeIso 𝕜 𝕂} {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] : Continuous ⇑(clmStarAlgEquiv e E)

The transport preserves the operator norm, so it is continuous.

theorem TauCeti.ScalarTransport.continuous_clmStarAlgEquiv_symm {𝕜 : Type u} {𝕂 : Type w} [RCLike 𝕜] [RCLike 𝕂] {e : RCLikeIso 𝕜 𝕂} {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] : Continuous ⇑(clmStarAlgEquiv e E).symm

The transport preserves the operator norm, so its inverse is continuous. This is the one analytic input ContinuousFunctionalCalculus.of_starAlgEquiv asks for.

theorem ContinuousLinearMap.continuousFunctionalCalculusReal {𝕜 : Type u} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] : ContinuousFunctionalCalculus ℝ (E →L[𝕜] E) IsSelfAdjoint

The continuous functional calculus over ℝ for self-adjoint bounded operators on a Hilbert space over an arbitrary RCLike field, in unrestricted dimension.

Proved by transport: the field is isomorphic to ℝ or to ℂ, and the calculus is already registered at both.

Not an instance, for the reason ContinuousLinearMap.realAlgebra is not: its statement mentions that real algebra structure, so it can only be activated together with it. A consumer writes

attribute [local instance 100] ContinuousLinearMap.realAlgebra
  ContinuousLinearMap.realIsScalarTower ContinuousLinearMap.continuousFunctionalCalculusReal

and a definition elaborated under those carries them in its body.

What the transport does to the calculus

With the instance in place on both sides, clm commutes with the functional calculus. Modulus naturality is downstream in ForTauCeti.Analysis.InnerProductSpace.ModulusTransport, which keeps this file usable by the modulus definition without an import cycle.

@[simp]

theorem TauCeti.ScalarTransport.spectrum_clm {𝕜 : Type u} {𝕂 : Type w} [RCLike 𝕜] [RCLike 𝕂] {e : RCLikeIso 𝕜 𝕂} {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] (T : E →L[𝕜] E) : spectrum ℝ (clm T) = spectrum ℝ T

The transport preserves the real spectrum: it is an ℝ-algebra isomorphism.

@[simp]

theorem TauCeti.ScalarTransport.nonneg_clm_iff {𝕜 : Type u} {𝕂 : Type w} [RCLike 𝕜] [RCLike 𝕂] {e : RCLikeIso 𝕜 𝕂} {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] {T : E →L[𝕜] E} : 0 ≤ clm T ↔ 0 ≤ T

The transport preserves and reflects nonnegativity.

theorem TauCeti.ScalarTransport.clm_cfc {𝕜 : Type u} {𝕂 : Type w} [RCLike 𝕜] [RCLike 𝕂] {e : RCLikeIso 𝕜 𝕂} {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] (f : ℝ → ℝ) {T : E →L[𝕜] E} (hT : IsSelfAdjoint T) (hf : ContinuousOn f (spectrum ℝ T)) : clm (cfc f T) = cfc f (clm T)

The transport commutes with the continuous functional calculus.

Reflections and reflected subspaces

The reflection in a subspace is 2 P - 1, so the transport carries it, and hence carries the image of one subspace under the reflection in another. That image is the object the Davis--Kahan double-angle statements are about.

@[simp]

theorem TauCeti.ScalarTransport.reflectionOperator_clm {𝕜 : Type u} {𝕂 : Type w} [RCLike 𝕜] [RCLike 𝕂] {e : RCLikeIso 𝕜 𝕂} {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (S : Submodule 𝕜 E) [S.HasOrthogonalProjection] : (submodule S).reflectionOperator = clm S.reflectionOperator

The transport carries the reflection operator of a subspace.