Theorem 2.25 — the Cayley transform is a bijection onto isometries with Ran(1 − V) dense

Proved

TeschlQM.SelfAdjoint.cayley_transform_bijective

by mikedeng1 · Sep 28, 2026 · Mathlib 0df444a (Lean v4.33.1)

cayley-transformfunctional-analysisp2o-batch-books5p2o-gran-per-chapterp2o-plan-bookp2o-v1symmetric-operators

Let $\mathfrak{H}$ be a complex Hilbert space. For a symmetric operator $A$ let $V = (A - \mathrm{i})(A + \mathrm{i})^{-1}$ , defined on $\mathfrak{D}(V) = \operatorname{Ran}(A + \mathrm{i})$ , be its Cayley transform. The Cayley transform is a bijection

\{A \text{ symmetric}\} \longrightarrow \{V \text{ isometric} \mid \operatorname{Ran}(1 - V) \text{ dense}\}.

Explicitly: every symmetric $A$ has a Cayley transform, it is unique, isometric ( $\|V\varphi\| = \|\varphi\|$ on $\mathfrak{D}(V)$ ), and $\operatorname{Ran}(1-V)$ is dense; two symmetric operators with the same Cayley transform are equal; and every isometric $V$ with $\operatorname{Ran}(1 - V)$ dense is the Cayley transform of some symmetric $A$ .

The Cayley transform converts questions about self-adjoint extensions of $A$ into questions about unitary extensions of $V$ .

Formalization Note. " $V$ is the Cayley transform of $A$ " is the relation IsCayleyTransform A V ( $\mathfrak{D}(V) = \operatorname{Ran}(A+\mathrm{i})$ and $V(A+\mathrm{i})\psi = (A-\mathrm{i})\psi$ ). The bijection is stated as its four constituent facts: existence with the stated properties, uniqueness of $V$ given $A$ , injectivity, and surjectivity.

Preamble

import Mathlib
import Definitions.Def_TeschlQM_Shared_IsSymmetric
import Definitions.Def_TeschlQM_SelfAdjoint_IsCayleyTransform

Formal statement

namespace TeschlQM.SelfAdjoint

/-- Teschl, Theorem 2.25 (p. 81): the Cayley transform `A ↦ V = (A - i)(A + i)⁻¹` is a bijection
from the symmetric operators onto the isometric operators `V` with `Ran(1 - V)` dense:
every symmetric `A` has a Cayley transform, unique, isometric and with `Ran(1 - V)` dense;
distinct symmetric operators have distinct Cayley transforms; and every isometric `V` with
`Ran(1 - V)` dense is the Cayley transform of a symmetric operator. -/
theorem cayley_transform_bijective {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] :
    (∀ A : H →ₗ.[ℂ] H, TeschlQM.Shared.IsSymmetric A →
      ∃ V : H →ₗ.[ℂ] H, IsCayleyTransform A V ∧ IsIsometric V ∧
        Dense (rangeOneSub V : Set H)) ∧
    (∀ A V W : H →ₗ.[ℂ] H, TeschlQM.Shared.IsSymmetric A → IsCayleyTransform A V → IsCayleyTransform A W →
      V = W) ∧
    (∀ A B V : H →ₗ.[ℂ] H, TeschlQM.Shared.IsSymmetric A → TeschlQM.Shared.IsSymmetric B → IsCayleyTransform A V →
      IsCayleyTransform B V → A = B) ∧
    (∀ V : H →ₗ.[ℂ] H, IsIsometric V → Dense (rangeOneSub V : Set H) →
      ∃ A : H →ₗ.[ℂ] H, TeschlQM.Shared.IsSymmetric A ∧ IsCayleyTransform A V) := by sorry

end TeschlQM.SelfAdjoint

Source

Teschl, Mathematical Methods in Quantum Mechanics, AMS GSM 99, 2009, p. 81, Theorem 2.25

Read-back

What the Lean code literally says, in plain math · claude-opus-5-5

Let $H$ be a complex Hilbert space: a complete complex inner product space. All operators here are partial $\mathbb C$ -linear operators on $H$ .

The statement uses the following notation:

$\mathrm{Sym}(\cdot)$ is the imported predicate IsSymmetric.
$\mathrm{Cay}(A,V)$ is the imported predicate IsCayleyTransform.
$\mathrm{Iso}(V)$ is the imported predicate IsIsometric.
$\operatorname{rangeOneSub}(V)$ is an imported subspace of $H$ .
None of these imported definitions has its code shown here.
"Dense" means the closure of the set is $H$ .

The statement is a conjunction of four parts.

Existence. For every $A$ $A$ with $\mathrm{Sym}(A)$ $Sym (A)$ , there is some $V$ $V$ such that:
- $\mathrm{Cay}(A,V)$ ;
- $\mathrm{Iso}(V)$ ;
- $\operatorname{rangeOneSub}(V)$ is dense in $H$ .
Uniqueness. For all $A,V,W$ with $\mathrm{Sym}(A)$ , $\mathrm{Cay}(A,V)$ and $\mathrm{Cay}(A,W)$ , we have $V=W$ : same domain and same values.
Injectivity. For all $A,B,V$ with $\mathrm{Sym}(A)$ , $\mathrm{Sym}(B)$ , $\mathrm{Cay}(A,V)$ and $\mathrm{Cay}(B,V)$ , we have $A=B$ .
Surjectivity. For every $V$ with $\mathrm{Iso}(V)$ and $\operatorname{rangeOneSub}(V)$ dense in $H$ , there is some $A$ with $\mathrm{Sym}(A)$ and $\mathrm{Cay}(A,V)$ .

Degenerate cases:

If $H=\{0\}$ , there is only one partial operator: the zero operator on $\{0\}$ . Every set is dense in $\{0\}$ . Each part then reduces to whether that single operator satisfies the imported predicates.
The strength of every part depends on the unseen definitions of Sym, Cay, Iso and rangeOneSub.

Human review

Endorsed by Shuze Chen · Oct 2, 2026
Confirmed by the moderator at approval.
Endorsed by mikedeng1 · Oct 2, 2026
Confirmed by the mission captain (proposal self-audit).

View graph