Joint continuous functional calculus on arbitrary complex Hilbert spaces
Definitionrybin2026_p02_joint_calculus_hilbertLet and let be an arbitrary complete complex Hilbert space. The two coordinate functions on are continuous real functions. A joint calculus is a unital real star-algebra homomorphism from to the bounded complex-linear operators on . It represents when it is continuous in the uniform and operator-norm topologies and sends the coordinates to .
A positive contraction is specified by , for every , and . Restriction of to requires continuity only on .
Formalization Note. The joint evaluation chooses one representing homomorphism if one exists, and is zero for every input function if none exists. Existence and uniqueness for commuting positive contractions are the separate standard joint-calculus theorem. The definition does not assume the compression-rigidity conclusion. No finite-dimensional, separability or nonzero-space restriction is imposed.
import Mathlib
namespace RybinAI2026.P02Hilbert
/-- The compact joint spectral box for two positive contractions. -/
def unitSquare : Set (Fin 2 → ℝ) := Set.Icc 0 1
abbrev Square := ↥unitSquare
/-- The two real coordinate functions on the joint spectral box. -/
def coordinate (i : Fin 2) : C(Square, ℝ) :=
⟨fun x => x.1 i, (continuous_apply i).comp continuous_subtype_val⟩
/-- Restriction of a continuous-on-the-square function, without requiring continuity outside. -/
def restrictFunction (f : (Fin 2 → ℝ) → ℝ) (hf : ContinuousOn f unitSquare) :
C(Square, ℝ) := ⟨fun x => f x.1, hf.restrict⟩
/-- A joint continuous functional calculus, represented by its continuous unital star homomorphism.
The coordinate images are the two commuting positive contractions; no eigenbasis is assumed. -/
abbrev JointCalculus (H : Type*) [NormedAddCommGroup H] [InnerProductSpace ℂ H]
[CompleteSpace H] := C(Square, ℝ) →⋆ₐ[ℝ] (H →L[ℂ] H)
variable {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]
/-- Explicit positivity and contraction conditions for a bounded operator. -/
def PositiveContraction (X : H →L[ℂ] H) : Prop :=
star X = X ∧ (∀ v : H, 0 ≤ (inner ℂ v (X v)).re) ∧ ‖X‖ ≤ 1
/-- The actual continuous joint functional-calculus representation of a given pair. -/
def Represents (calculus : JointCalculus H) (X Y : H →L[ℂ] H) : Prop :=
Continuous calculus ∧ calculus (coordinate 0) = X ∧ calculus (coordinate 1) = Y
/-- Joint functional calculus chosen from its defining representation property. Existence and
uniqueness for commuting positive contractions are a separate standard spectral-theorem target.
The zero fallback is used only for pairs for which no such representation exists. -/
noncomputable def jointCFC (X Y : H →L[ℂ] H) (g : C(Square, ℝ)) : H →L[ℂ] H := by
classical
exact if h : ∃ calculus : JointCalculus H, Represents calculus X Y then
(Classical.choose h) g
else 0
end RybinAI2026.P02Hilbert