The Cayley transform

This file constructs the bounded Cayley transform of a possibly unbounded self-adjoint operator. The key point is that A + iI, regarded as a map from the domain of A, is bijective. Its inverse can therefore be composed with A - iI, and the resulting everywhere-defined linear map is an isometry, hence continuous.

def plusI {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (A : E →ₗ.[ℂ] E) : ↥A.domain →ₗ[ℂ] E

The map A + iI on the domain of a partial linear operator.

Equations

• plusI A = A.toFun + Complex.I • A.domain.subtype

def minusI {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (A : E →ₗ.[ℂ] E) : ↥A.domain →ₗ[ℂ] E

The map A - iI on the domain of a partial linear operator.

Equations

• minusI A = A.toFun - Complex.I • A.domain.subtype

theorem add_I_surjective_of_isSelfAdjoint {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →ₗ.[ℂ] E) (hA : IsSelfAdjoint A) : Function.Surjective fun (x : ↥A.domain) => ↑A x + Complex.I • ↑x

For a self-adjoint operator, A + iI maps its domain onto the ambient space.

theorem sub_I_surjective_of_isSelfAdjoint {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →ₗ.[ℂ] E) (hA : IsSelfAdjoint A) : Function.Surjective fun (x : ↥A.domain) => ↑A x - Complex.I • ↑x

For a self-adjoint operator, A - iI maps its domain onto the ambient space.

noncomputable def cayleyLinearMap {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →ₗ.[ℂ] E) (hA : IsSelfAdjoint A) : E →ₗ[ℂ] E

The linear map underlying the Cayley transform of a self-adjoint operator.

Equations

• cayleyLinearMap A hA = minusI A ∘ₗ ↑(LinearEquiv.ofBijective (plusI A) ⋯).symm

noncomputable def cayleyTransform {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →ₗ.[ℂ] E) (hA : IsSelfAdjoint A) : E →L[ℂ] E

The Cayley transform (A - iI)(A + iI)⁻¹ of a self-adjoint partial linear map.

Equations

• cayleyTransform A hA = (cayleyLinearMap A hA).mkContinuous 1 ⋯

theorem cayleyTransform_apply_plus {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →ₗ.[ℂ] E) (hA : IsSelfAdjoint A) (x : ↥A.domain) : (cayleyTransform A hA) (↑A x + Complex.I • ↑x) = ↑A x - Complex.I • ↑x

The Cayley transform sends (A + iI)x to (A - iI)x.

theorem norm_cayleyTransform {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →ₗ.[ℂ] E) (hA : IsSelfAdjoint A) (y : E) : ‖(cayleyTransform A hA) y‖ = ‖y‖

The Cayley transform preserves the norm.