The inverse Cayley transform

This file shows the Cayley transform of a self-adjoint operator is surjective onto 1 - U's complement, giving the inverse construction used to recover the self-adjoint operator from its unitary Cayley transform.

def oneSub {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (U : E →L[ℂ] E) : E →ₗ[ℂ] E

The linear map I - U associated to a continuous linear operator.

Equations

• oneSub U = LinearMap.id - ↑U

def oneAdd {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (U : E →L[ℂ] E) : E →ₗ[ℂ] E

The linear map I + U associated to a continuous linear operator.

Equations

• oneAdd U = LinearMap.id + ↑U

noncomputable def inverseCayley {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (U : E →L[ℂ] E) (_hU : U ∈ unitary (E →L[ℂ] E)) (hInj : ∀ (x : E), U x = x → x = 0) (_hDense : DenseRange fun (x : E) => x - U x) : E →ₗ.[ℂ] E

The inverse Cayley transform i(I + U)(I - U)⁻¹, with domain ran(I - U).

Equations

• inverseCayley U _hU hInj _hDense = { domain := (oneSub U).range, toFun := Complex.I • oneAdd U ∘ₗ ↑(LinearEquiv.ofInjective (oneSub U) ⋯).symm }

theorem inverseCayley_cayleyTransform {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →ₗ.[ℂ] E) (hA : IsSelfAdjoint A) : inverseCayley (cayleyTransform A hA) ⋯ ⋯ ⋯ = A

Applying the inverse Cayley transform to the Cayley transform recovers the original operator.