Physlib

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

definition

Unitary operator as a linear partial map

Given a unitary operator u:H≅Hu : H \cong H on a complex Hilbert space HH, this definition represents uu as a linear partial map u:D(u)→Hu : \mathcal{D}(u) \to H where the domain D(u)\mathcal{D}(u) is the entire space HH.

theorem

The domain of a unitary operator as a linear partial map is the entire space HH

For any unitary operator u:H≅Hu : H \cong H on a complex Hilbert space HH, the domain of its representation as a linear partial map is the entire space HH.

theorem

The domain of I−uI - u is HH

Let HH be a complex Hilbert space and u:H→Hu : H \to H be a unitary operator. The domain of the partial linear map I−uI - u, where II is the identity operator, is the entire space HH.

definition

Inverse Cayley transform i(I+u)(I−u)−1i(I + u)(I - u)^{-1}

Let HH be a complex Hilbert space and u:H→Hu: H \to H be a unitary operator. The partial inverse Cayley transform of uu is the partial linear map i(I+u)(I−u)−1i(I + u)(I - u)^{-1}, where II is the identity operator on HH and (I−u)−1(I - u)^{-1} denotes the inverse of the operator I−uI - u defined on its range.

theorem

The domain of the inverse Cayley transform of uu is the range of I−uI - u

Let HH be a complex Hilbert space and u:H→Hu : H \to H be a unitary operator. The domain of the partial inverse Cayley transform of uu, defined as i(I+u)(I−u)−1i(I + u)(I - u)^{-1} (where II is the identity operator), is equal to the range of the operator I−uI - u.

theorem

ker⁡(I−u)={0}\ker(I - u) = \{0\} implies range(I−u)\text{range}(I - u) is dense for unitary uu

Let HH be a complex Hilbert space and u:H→Hu: H \to H be a unitary operator. If the kernel of the operator I−uI - u is trivial (where II is the identity operator), i.e., ker⁡(I−u)={0}\ker(I - u) = \{0\}, then the range of I−uI - u is dense in HH.

theorem

The unitary Cayley transform of a self-adjoint operator TT equals its partial map Cayley transform

Let HH be a complex Hilbert space and TT be a self-adjoint linear partial map on HH. Then the unitary operator resulting from the Cayley transform of TT, when viewed as a linear partial map, is equal to the Cayley transform of TT defined as a partial map.

theorem

ker⁡(I−U)={0}\ker(I - U) = \{0\} for the Cayley transform UU of a self-adjoint operator TT

Let HH be a complex Hilbert space and TT be a self-adjoint partial linear map on HH. Let UU be the unitary operator obtained by the Cayley transform of TT. Then the kernel of the operator I−UI - U is trivial, i.e., ker⁡(I−U)={0}\ker(I - U) = \{0\}.

theorem

range⁡(aQ)=range⁡(Q)\operatorname{range}(a Q) = \operatorname{range}(Q) for a≠0a \neq 0

For any partial linear map QQ on a complex Hilbert space HH and any non-zero scalar a∈C∖{0}a \in \mathbb{C} \setminus \{0\}, the range of the scaled operator aQa Q is equal to the range of QQ, i.e., range⁡(aQ)=range⁡(Q)\operatorname{range}(a Q) = \operatorname{range}(Q).

theorem

Q(Q−1(y))=yQ(Q^{-1}(y)) = y for injective partial linear maps QQ

Let HH be a complex Hilbert space and QQ be a partial linear map on HH. If QQ is injective (that is, its kernel is trivial, ker⁡Q={0}\ker Q = \{0\}), then for any yy in the domain of its inverse Q−1Q^{-1}, applying QQ to Q−1(y)Q^{-1}(y) returns yy.

theorem

dom⁡(inverseCayley⁡(cayley⁡(T)))=dom⁡(T)\operatorname{dom}(\operatorname{inverseCayley}(\operatorname{cayley}(T))) = \operatorname{dom}(T) for self-adjoint TT

Let HH be a complex Hilbert space and TT be a self-adjoint partial linear map on HH. Let uu be the Cayley transform of TT. Then the domain of the inverse Cayley transform of uu is equal to the domain of TT.

theorem

Φ(u)((I−u)a)=i(I+u)a\Phi(u)((I - u)a) = i(I + u)a for the inverse Cayley transform of a unitary uu

Let HH be a complex Hilbert space and u:H→Hu: H \to H be a unitary operator. Suppose that the operator I−uI - u is injective (i.e., its kernel is trivial), where II denotes the identity operator on HH. For any vector a∈Ha \in H, the inverse Cayley transform Φ(u)=i(I+u)(I−u)−1\Phi(u) = i(I + u)(I - u)^{-1} satisfies: Φ(u)((I−u)a)=i(I+u)a\Phi(u) ((I - u) a) = i(I + u) a where ii is the imaginary unit.

theorem

Inverse Cayley Transform of the Cayley Transform of TT equals TT

Let HH be a complex Hilbert space and TT be a self-adjoint partial linear operator on HH. Let uu be the Cayley transform of TT. Then the inverse Cayley transform of uu recovers the original operator TT: inverseCayleyPMap(u)=T\text{inverseCayleyPMap}(u) = T where the inverse Cayley transform is defined as i(I+u)(I−u)−1i(I + u)(I - u)^{-1}.

theorem

Inner product identity ⟨i(a+ua),b−ub⟩=⟨a−ua,i(b+ub)⟩\langle i(a+ua), b-ub \rangle = \langle a-ua, i(b+ub) \rangle for unitary uu

Let HH be a complex Hilbert space and u:H→Hu: H \to H be a unitary operator. For any vectors a,b∈Ha, b \in H, the following identity holds: ⟨i(a+ua),b−ub⟩=⟨a−ua,i(b+ub)⟩\langle i(a + u a), b - u b \rangle = \langle a - u a, i(b + u b) \rangle where ii is the imaginary unit and ⟨⋅,⋅⟩\langle \cdot, \cdot \rangle denotes the complex inner product.

theorem

Injective I−uI - u implies Symmetry of the Inverse Cayley Transform

Let HH be a complex Hilbert space and u:H→Hu: H \to H be a unitary operator. If the operator I−uI - u is injective (i.e., its kernel is trivial, ker⁡(I−u)={0}\ker(I - u) = \{0\}), then the inverse Cayley transform of uu, defined as the partial operator T=i(I+u)(I−u)−1T = i(I + u)(I - u)^{-1} on the domain ran(I−u)\text{ran}(I - u), is symmetric. That is, for all x,yx, y in the domain of TT, the identity ⟨Tx,y⟩=⟨x,Ty⟩\langle Tx, y \rangle = \langle x, Ty \rangle holds.

theorem

(C−1(u)+iI)x=2ia(C^{-1}(u) + iI)x = 2ia for x=(I−u)ax = (I - u)a

Let HH be a complex Hilbert space and u:H→Hu : H \to H be a unitary operator such that the operator I−uI - u is injective (i.e., its kernel is {0}\{0\}), where II denotes the identity operator. Let C−1(u)=i(I+u)(I−u)−1C^{-1}(u) = i(I + u)(I - u)^{-1} be the inverse Cayley transform of uu. For any vector aa in the domain of I−uI - u, let x=(I−u)ax = (I - u)a be the corresponding element in the domain of C−1(u)C^{-1}(u). Then the following identity holds: C−1(u)x+ix=2iaC^{-1}(u)x + ix = 2ia where ii is the imaginary unit.

theorem

The identity Ax−ix=2iuaAx - ix = 2i u a for the inverse Cayley transform AA

Let HH be a complex Hilbert space and u:H→Hu : H \to H be a unitary operator such that the operator I−uI - u is injective (i.e., its kernel is trivial), where II denotes the identity operator. For any vector a∈Ha \in H, let x=(I−u)ax = (I - u)a be an element in the domain of the inverse Cayley transform A=i(I+u)(I−u)−1A = i(I + u)(I - u)^{-1}. Then the following identity holds: Ax−ix=2iu(a)A x - i x = 2i u(a) where ii is the imaginary unit.

theorem

The inverse Cayley transform has a dense domain if ran(I−u)\text{ran}(I - u) is dense.

Let HH be a complex Hilbert space and u:H→Hu : H \to H be a unitary operator. If the range of the operator I−uI - u is dense in HH (where II denotes the identity operator), then the domain of the inverse Cayley transform of uu, defined as i(I+u)(I−u)−1i(I + u)(I - u)^{-1}, is dense in HH.

theorem

The range of i(I+u)(I−u)−1+iIi(I + u)(I - u)^{-1} + iI is HH

Let HH be a complex Hilbert space and u:H→Hu : H \to H be a unitary operator. If the kernel of the operator I−uI - u is trivial (i.e., 11 is not an eigenvalue of uu), then the range of the partial linear map i(I+u)(I−u)−1+iIi(I + u)(I - u)^{-1} + iI is the entire space HH, where II denotes the identity operator and ii is the imaginary unit.

theorem

Range of i(I+u)(I−u)−1−iI=Hi(I + u)(I - u)^{-1} - iI = H

Let HH be a complex Hilbert space and u:H→Hu : H \to H be a unitary operator. Suppose that the kernel of the operator I−uI - u is trivial (i.e., ker⁡(I−u)={0}\ker(I - u) = \{0\}), where II denotes the identity operator. Let C(u)=i(I+u)(I−u)−1C(u) = i(I + u)(I - u)^{-1} be the partial inverse Cayley transform of uu. Then the range of the operator C(u)−iIC(u) - iI is the entire space HH.

theorem

The Inverse Cayley Transform of a Unitary is Self-Adjoint

Let HH be a complex Hilbert space and u:H→Hu : H \to H be a unitary operator. Suppose that the kernel of the operator I−uI - u is trivial (i.e., ker⁡(I−u)={0}\ker(I - u) = \{0\}) and that the range of I−uI - u is dense in HH. Then the partial inverse Cayley transform of uu, defined as i(I+u)(I−u)−1i(I + u)(I - u)^{-1}, is a self-adjoint operator.

theorem

C(C−1(u))x=u(x)C(C^{-1}(u))x = u(x) for unitary operators uu

Let HH be a complex Hilbert space and u:H→Hu : H \to H be a unitary operator. Suppose that the kernel of I−uI - u is trivial (i.e., ker⁡(I−u)={0}\ker(I - u) = \{0\}) and that the range of I−uI - u is dense in HH. Let T=i(I+u)(I−u)−1T = i(I + u)(I - u)^{-1} be the partial inverse Cayley transform of uu. Then for any x∈Hx \in H, applying the Cayley transform C(T)=I−2i(T+iI)−1C(T) = I - 2i(T + iI)^{-1} to xx yields u(x)u(x).

theorem

The Cayley transform of the inverse Cayley transform of uu equals uu

Let HH be a complex Hilbert space and u:H→Hu: H \to H be a unitary operator. Suppose that the kernel of the operator I−uI - u is trivial, i.e., ker⁡(I−u)={0}\ker(I - u) = \{0\}, and that the range of I−uI - u is dense in HH. Let T=i(I+u)(I−u)−1T = i(I + u)(I - u)^{-1} be the inverse Cayley transform of uu. Then the Cayley transform of TT, defined as C(T)=I−2i(T+iI)−1C(T) = I - 2i(T + iI)^{-1} (where II is the identity operator and ii is the imaginary unit), is equal to the original operator uu.

theorem

The inverse Cayley transform of a unitary operator uu is self-adjoint if ker⁡(I−u)={0}\ker(I - u) = \{0\}

Let HH be a complex Hilbert space and u:H→Hu : H \to H be a unitary operator. If the kernel of the operator I−uI - u is trivial (i.e., ker⁡(I−u)={0}\ker(I - u) = \{0\}), then the inverse Cayley transform of uu, defined as the partial linear map i(I+u)(I−u)−1i(I + u)(I - u)^{-1}, is self-adjoint.

theorem

The inverse Cayley transform i(I+u)(I−u)−1i(I + u)(I - u)^{-1} is self-adjoint

Let HH be a complex Hilbert space and u:H→Hu: H \to H be a unitary operator. Suppose uu satisfies the conditions of `CayleyUnitaryData`, which include that 11 is not a fixed vector of uu (i.e., ker⁡(I−u)={0}\ker(I - u) = \{0\}) and that the range of the operator I−uI - u is dense in HH. Then the inverse Cayley transform of uu, defined as the partial linear map i(I+u)(I−u)−1i(I + u)(I - u)^{-1}, is a self-adjoint operator.