Unitarity of the Cayley transform

This file proves the Cayley transform of a self-adjoint operator is surjective, and combines this with its isometry (from Spectral.Cayley.Basic) to show it is unitary.

theorem cayleyTransform_unitary {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →ₗ.[ℂ] E) (hA : IsSelfAdjoint A) : cayleyTransform A hA ∈ unitary (E →L[ℂ] E)

theorem one_not_mem_eigenvalues_cayleyTransform {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →ₗ.[ℂ] E) (hA : IsSelfAdjoint A) (x : E) : (cayleyTransform A hA) x = x → x = 0

theorem dense_range_one_sub_cayleyTransform {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →ₗ.[ℂ] E) (hA : IsSelfAdjoint A) : DenseRange fun (x : E) => x - (cayleyTransform A hA) x