The pair shift and a self-adjointness criterion

Over ℂ the classical self-adjointness criterion of von Neumann asks that the deficiency operators B ± i μ of a symmetric operator be surjective. To treat real and complex scalars uniformly we use their real form instead. For a partial linear map B and μ : ℝ, the pair shift is

B.pairShift μ (x, y) = (μ • x - B y, B x + μ • y),

which is the operator μ + i B on the complexification E ⊕ i E written in real coordinates, so it makes sense over every RCLike field. For symmetric B it satisfies

‖μ • x - B y‖² + ‖B x + μ • y‖² = μ² (‖x‖² + ‖y‖²) + ‖B x‖² + ‖B y‖²,

and for μ ≠ 0 it characterizes self-adjointness: a symmetric B is self-adjoint exactly when B.pairShift μ is surjective (LinearPMap.IsFormalAdjoint.isSelfAdjoint_iff_surjective_pairShift). Surjectivity of the pair shift of a self-adjoint A comes from the orthogonal decomposition of the L² product along the closed graph of A.

Main declarations

• LinearPMap.pairShift: the pair shift (x, y) ↦ (μ • x - B y, B x + μ • y).
• LinearPMap.IsFormalAdjoint.norm_smul_sub_sq_add_norm_add_smul_sq: its norm identity.
• LinearPMap.IsFormalAdjoint.re_inner_pairShift: its real-part identity re (⟪x, (B.pairShift μ (x, y)).1⟫ + ⟪y, (B.pairShift μ (x, y)).2⟫) = μ (‖x‖² + ‖y‖²).
• LinearPMap.IsFormalAdjoint.dense_domain_of_surjective_pairShift: a symmetric map with a surjective pair shift is densely defined.
• LinearPMap.IsFormalAdjoint.isSelfAdjoint_of_surjective_pairShift and IsSelfAdjoint.surjective_pairShift: the self-adjointness criterion and its converse, combined in LinearPMap.IsFormalAdjoint.isSelfAdjoint_iff_surjective_pairShift.

References

• M. Reed and B. Simon, Methods of Modern Mathematical Physics I: Functional Analysis, Academic Press (1980), Theorem VIII.3 (the basic criterion for self-adjointness).

def LinearPMap.pairShift {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (B : E →ₗ.[𝕜] E) (μ : ℝ) : ↥B.domain × ↥B.domain →ₗ[𝕜] E × E

The pair shift (x, y) ↦ (μ • x - B y, B x + μ • y) of a partial linear map B, defined on pairs of vectors in the domain of B. It is the operator μ + i B on the complexification of E, written in real coordinates.

@[simp]

theorem LinearPMap.pairShift_apply {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (B : E →ₗ.[𝕜] E) (μ : ℝ) (z : ↥B.domain × ↥B.domain) : (B.pairShift μ) z = (↑μ • ↑z.1 - ↑B z.2, ↑B z.1 + ↑μ • ↑z.2)

theorem LinearPMap.IsFormalAdjoint.norm_smul_sub_sq_add_norm_add_smul_sq {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {B : E →ₗ.[𝕜] E} (hB : B.IsFormalAdjoint B) (μ : ℝ) (x y : ↥B.domain) : ‖↑μ • ↑x - ↑B y‖ ^ 2 + ‖↑B x + ↑μ • ↑y‖ ^ 2 = μ ^ 2 * (‖↑x‖ ^ 2 + ‖↑y‖ ^ 2) + (‖↑B x‖ ^ 2 + ‖↑B y‖ ^ 2)

The norm identity of the pair shift of a symmetric partial linear map: ‖μ • x - B y‖² + ‖B x + μ • y‖² = μ² (‖x‖² + ‖y‖²) + ‖B x‖² + ‖B y‖².

theorem LinearPMap.IsFormalAdjoint.re_inner_pairShift {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {B : E →ₗ.[𝕜] E} (hB : B.IsFormalAdjoint B) (μ : ℝ) (x y : ↥B.domain) : RCLike.re (inner 𝕜 (↑x) ((B.pairShift μ) (x, y)).1 + inner 𝕜 (↑y) ((B.pairShift μ) (x, y)).2) = μ * (‖↑x‖ ^ 2 + ‖↑y‖ ^ 2)

The real-part identity of the pair shift of a symmetric partial linear map: re (⟪x, μ • x - B y⟫ + ⟪y, B x + μ • y⟫) = μ (‖x‖² + ‖y‖²).

theorem LinearPMap.IsFormalAdjoint.dense_domain_of_surjective_pairShift {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {B : E →ₗ.[𝕜] E} [CompleteSpace E] (hB : B.IsFormalAdjoint B) {μ : ℝ} (hμ : μ ≠ 0) (h : Function.Surjective ⇑(B.pairShift μ)) : Dense ↑B.domain

A symmetric partial linear map whose pair shift is surjective, for some μ ≠ 0, is densely defined.

theorem LinearPMap.IsFormalAdjoint.isSelfAdjoint_of_surjective_pairShift {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {B : E →ₗ.[𝕜] E} [CompleteSpace E] (hB : B.IsFormalAdjoint B) {μ : ℝ} (hμ : μ ≠ 0) (h : Function.Surjective ⇑(B.pairShift μ)) : IsSelfAdjoint B

A self-adjointness criterion. A symmetric partial linear map on a Hilbert space whose pair shift is surjective for some μ ≠ 0 is self-adjoint. This is the real form of von Neumann's criterion that B ± i μ be surjective.

theorem IsSelfAdjoint.surjective_pairShift {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] {A : E →ₗ.[𝕜] E} (hA : IsSelfAdjoint A) {μ : ℝ} (hμ : μ ≠ 0) : Function.Surjective ⇑(A.pairShift μ)

The pair shift of a self-adjoint partial linear map is surjective for every μ ≠ 0.

theorem LinearPMap.IsFormalAdjoint.isSelfAdjoint_iff_surjective_pairShift {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] {B : E →ₗ.[𝕜] E} (hB : B.IsFormalAdjoint B) {μ : ℝ} (hμ : μ ≠ 0) : IsSelfAdjoint B ↔ Function.Surjective ⇑(B.pairShift μ)

Self-adjointness through the pair shift. For μ ≠ 0, a symmetric partial linear map on a Hilbert space is self-adjoint exactly when its pair shift is surjective.