Existence and uniqueness of the joint continuous functional calculus

Proved

RybinAI2026.P02Hilbert.joint_calculus_exists_unique

by wenxinzhang · Sep 6, 2026 · Mathlib c5ea003 (Lean v4.30.0)

convexityfunctional-analysishilbert-spacesoperator-theory

For every complete complex Hilbert space $H$ and every pair of commuting positive contractions $X,Y$ on $H$ , put $S=[0,1]^2$ . There exists exactly one continuous unital real star-algebra homomorphism

\Phi:C(S,\mathbb R)\longrightarrow\mathcal B(H),\qquad \Phi(x\mapsto x_0)=X,\quad\Phi(x\mapsto x_1)=Y.

Continuity uses the uniform norm on functions and the operator norm on bounded complex-linear operators. The homomorphism preserves real scalars, the identity, addition, multiplication and adjoints. The space may have any dimension, including zero, and need not be separable.

This is the square-domain, two-self-adjoint-operator specialization of the joint continuous functional calculus (Dereziński, Lemma 6.6). It validates the representation used by the compression-rigidity formulation. It is a known mathematical theorem whose Lean proof remains a separate obligation in this contribution.

Preamble

import Definitions.Def_rybin2026_p02_joint_calculus_hilbert

Formal statement

namespace RybinAI2026.P02Hilbert

/-- The joint continuous spectral theorem for two commuting positive contractions.
Derezinski, Mathematical Physics lecture notes, Lemma 6.6, restricted to the unit square. -/
theorem joint_calculus_exists_unique
    (H : Type*) [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]
    (X Y : H →L[ℂ] H) (hX : PositiveContraction X) (hY : PositiveContraction Y)
    (hXY : X * Y = Y * X) :
    ∃! calculus : JointCalculus H, Represents calculus X Y := by
  sorry

end RybinAI2026.P02Hilbert

Source

https://rybindmitry.github.io/problems/2.html, displayed compression equality and question; joint-calculus representation: Jan Dereziński, Bounded operators, Lemma 6.6, printed p. 43, https://www.fuw.edu.pl/~derezins/mat-o.pdf#page=43.

View graph