PhyslibAlpha.AlgebraicFramework.HilbertSpace.Unbounded.Cayley.Inverse
The inverse Cayley operator
This file contains the reusable operator-side converse to `Cayley/Basic.lean`'s Cayley transform. A unitary operator `u` has a possible missing point at `1`; its inverse Cayley transform is therefore the partial operator
`i (1 + u) (1 - u)⁻¹`.
The inverse is defined on the range of `1 - u`. The no-fixed-vector hypothesis in `CayleyUnitaryData` makes the inverse unambiguous. For a unitary, the same hypothesis also forces the range of `1 - u` to be dense; that fact is proved here using orthogonal complements and the Hilbert-space adjoint theorem. The range calculations at `± i` then prove self-adjointness directly from the symmetric-operator criterion already available for `LinearPMap`.
No model-specific completeness theorem is used here: this is the general layer that a concrete Hamiltonian can use after producing its Cayley unitary.
- `inverseCayleyPMap` : the partial inverse Cayley transform of a unitary operator. - `inverseCayleyPMap_isSelfAdjoint` : the inverse Cayley transform of a unitary with `1` not a fixed vector, and with `1 - u` having dense range, is self-adjoint. - `CayleyUnitaryData` : the standard hypotheses for taking an inverse Cayley transform. - `cayleyContinuousLinearMap_inverseCayleyPMap_eq` : the inverse Cayley transform of `u`'s Cayley transform recovers `u` itself.
A. The partial inverse Cayley transform
B. Density of the range of `1 - u`
C. Self-adjointness of the inverse Cayley transform
D. Round trip with the forward Cayley transform
25 declarations
Unitary operator as a linear partial map
Given a unitary operator on a complex Hilbert space , this definition represents as a linear partial map where the domain is the entire space .
The domain of a unitary operator as a linear partial map is the entire space
For any unitary operator on a complex Hilbert space , the domain of its representation as a linear partial map is the entire space .
The domain of is
Let be a complex Hilbert space and be a unitary operator. The domain of the partial linear map , where is the identity operator, is the entire space .
Inverse Cayley transform
Let be a complex Hilbert space and be a unitary operator. The partial inverse Cayley transform of is the partial linear map , where is the identity operator on and denotes the inverse of the operator defined on its range.
The domain of the inverse Cayley transform of is the range of
Let be a complex Hilbert space and be a unitary operator. The domain of the partial inverse Cayley transform of , defined as (where is the identity operator), is equal to the range of the operator .
implies is dense for unitary
Let be a complex Hilbert space and be a unitary operator. If the kernel of the operator is trivial (where is the identity operator), i.e., , then the range of is dense in .
The unitary Cayley transform of a self-adjoint operator equals its partial map Cayley transform
Let be a complex Hilbert space and be a self-adjoint linear partial map on . Then the unitary operator resulting from the Cayley transform of , when viewed as a linear partial map, is equal to the Cayley transform of defined as a partial map.
for the Cayley transform of a self-adjoint operator
Let be a complex Hilbert space and be a self-adjoint partial linear map on . Let be the unitary operator obtained by the Cayley transform of . Then the kernel of the operator is trivial, i.e., .
for
For any partial linear map on a complex Hilbert space and any non-zero scalar , the range of the scaled operator is equal to the range of , i.e., .
for injective partial linear maps
Let be a complex Hilbert space and be a partial linear map on . If is injective (that is, its kernel is trivial, ), then for any in the domain of its inverse , applying to returns .
for self-adjoint
Let be a complex Hilbert space and be a self-adjoint partial linear map on . Let be the Cayley transform of . Then the domain of the inverse Cayley transform of is equal to the domain of .
for the inverse Cayley transform of a unitary
Let be a complex Hilbert space and be a unitary operator. Suppose that the operator is injective (i.e., its kernel is trivial), where denotes the identity operator on . For any vector , the inverse Cayley transform satisfies: where is the imaginary unit.
Inverse Cayley Transform of the Cayley Transform of equals
Let be a complex Hilbert space and be a self-adjoint partial linear operator on . Let be the Cayley transform of . Then the inverse Cayley transform of recovers the original operator : where the inverse Cayley transform is defined as .
Inner product identity for unitary
Let be a complex Hilbert space and be a unitary operator. For any vectors , the following identity holds: where is the imaginary unit and denotes the complex inner product.
Injective implies Symmetry of the Inverse Cayley Transform
Let be a complex Hilbert space and be a unitary operator. If the operator is injective (i.e., its kernel is trivial, ), then the inverse Cayley transform of , defined as the partial operator on the domain , is symmetric. That is, for all in the domain of , the identity holds.
for
Let be a complex Hilbert space and be a unitary operator such that the operator is injective (i.e., its kernel is ), where denotes the identity operator. Let be the inverse Cayley transform of . For any vector in the domain of , let be the corresponding element in the domain of . Then the following identity holds: where is the imaginary unit.
The identity for the inverse Cayley transform
Let be a complex Hilbert space and be a unitary operator such that the operator is injective (i.e., its kernel is trivial), where denotes the identity operator. For any vector , let be an element in the domain of the inverse Cayley transform . Then the following identity holds: where is the imaginary unit.
The inverse Cayley transform has a dense domain if is dense.
Let be a complex Hilbert space and be a unitary operator. If the range of the operator is dense in (where denotes the identity operator), then the domain of the inverse Cayley transform of , defined as , is dense in .
The range of is
Let be a complex Hilbert space and be a unitary operator. If the kernel of the operator is trivial (i.e., is not an eigenvalue of ), then the range of the partial linear map is the entire space , where denotes the identity operator and is the imaginary unit.
Range of
Let be a complex Hilbert space and be a unitary operator. Suppose that the kernel of the operator is trivial (i.e., ), where denotes the identity operator. Let be the partial inverse Cayley transform of . Then the range of the operator is the entire space .
The Inverse Cayley Transform of a Unitary is Self-Adjoint
Let be a complex Hilbert space and be a unitary operator. Suppose that the kernel of the operator is trivial (i.e., ) and that the range of is dense in . Then the partial inverse Cayley transform of , defined as , is a self-adjoint operator.
for unitary operators
Let be a complex Hilbert space and be a unitary operator. Suppose that the kernel of is trivial (i.e., ) and that the range of is dense in . Let be the partial inverse Cayley transform of . Then for any , applying the Cayley transform to yields .
The Cayley transform of the inverse Cayley transform of equals
Let be a complex Hilbert space and be a unitary operator. Suppose that the kernel of the operator is trivial, i.e., , and that the range of is dense in . Let be the inverse Cayley transform of . Then the Cayley transform of , defined as (where is the identity operator and is the imaginary unit), is equal to the original operator .
The inverse Cayley transform of a unitary operator is self-adjoint if
Let be a complex Hilbert space and be a unitary operator. If the kernel of the operator is trivial (i.e., ), then the inverse Cayley transform of , defined as the partial linear map , is self-adjoint.
The inverse Cayley transform is self-adjoint
Let be a complex Hilbert space and be a unitary operator. Suppose satisfies the conditions of `CayleyUnitaryData`, which include that is not a fixed vector of (i.e., ) and that the range of the operator is dense in . Then the inverse Cayley transform of , defined as the partial linear map , is a self-adjoint operator.
