Compressions of operators

For bounded operators A : E → E and X : F → E between Hilbert spaces, the compression of A along X is the operator X† A X on F, ContinuousLinearMap.compression A X. When X is an isometry it is A cut down to the subspace range X, read in the coordinates of F. This file records its basic algebra: it is additive and homogeneous in A, commutes with adjoints, preserves symmetry, and compressing in two steps is compressing along the composite. Compressing to the orthogonal complement of an eigenvector creates no new eigenvalues (ContinuousLinearMap.hasEigenvalue_of_hasEigenvalue_compression_orthogonal_span_singleton).

Compressions model operators on a trial subspace in the Rayleigh–Ritz procedure, and compress representations to invariant subspaces.

noncomputable def ContinuousLinearMap.compression {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] (A : E →L[𝕜] E) (X : F →L[𝕜] E) : F →L[𝕜] F

The compression X† A X of an operator A on E along an operator X : F →L[𝕜] E. When X is an isometry, it is A cut down to the trial subspace range X, in the coordinates of F.

theorem ContinuousLinearMap.compression_def {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] (A : E →L[𝕜] E) (X : F →L[𝕜] E) : A.compression X = adjoint X ∘SL A ∘SL X

@[simp]

theorem ContinuousLinearMap.compression_apply {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] (A : E →L[𝕜] E) (X : F →L[𝕜] E) (x : F) : (A.compression X) x = (adjoint X) (A (X x))

@[simp]

theorem ContinuousLinearMap.compression_zero {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] (X : F →L[𝕜] E) : compression 0 X = 0

Compression sends the zero operator to zero.

@[simp]

theorem ContinuousLinearMap.compression_add {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] (A : E →L[𝕜] E) (X : F →L[𝕜] E) (B : E →L[𝕜] E) : (A + B).compression X = A.compression X + B.compression X

Compression preserves addition in the operator argument.

@[simp]

theorem ContinuousLinearMap.compression_sub {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] (A : E →L[𝕜] E) (X : F →L[𝕜] E) (B : E →L[𝕜] E) : (A - B).compression X = A.compression X - B.compression X

Compression preserves subtraction in the operator argument.

@[simp]

theorem ContinuousLinearMap.compression_smul {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] (A : E →L[𝕜] E) (X : F →L[𝕜] E) (c : 𝕜) : (c • A).compression X = c • A.compression X

Compression preserves scalar multiplication in the operator argument.

theorem ContinuousLinearMap.inner_compression_apply {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] (A : E →L[𝕜] E) (X : F →L[𝕜] E) (x y : F) : inner 𝕜 x ((A.compression X) y) = inner 𝕜 (X x) (A (X y))

The matrix coefficients of the compression are those of A on the images under X.

@[simp]

theorem ContinuousLinearMap.compression_id {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] (A : E →L[𝕜] E) : A.compression (ContinuousLinearMap.id 𝕜 E) = A

theorem ContinuousLinearMap.compression_comp {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] (A : E →L[𝕜] E) (X : F →L[𝕜] E) {G : Type u_4} [NormedAddCommGroup G] [InnerProductSpace 𝕜 G] [CompleteSpace G] (Y : G →L[𝕜] F) : A.compression (X ∘SL Y) = (A.compression X).compression Y

Compressing in two steps is compressing along the composite.

@[simp]

theorem ContinuousLinearMap.adjoint_compression {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] (A : E →L[𝕜] E) (X : F →L[𝕜] E) : adjoint (A.compression X) = (adjoint A).compression X

The adjoint of the compression is the compression of the adjoint.

theorem ContinuousLinearMap.isSymmetric_compression {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] (X : F →L[𝕜] E) {A : E →L[𝕜] E} (hA : (↑A).IsSymmetric) : (↑(A.compression X)).IsSymmetric

The compression of a symmetric operator is symmetric.

theorem ContinuousLinearMap.hasEigenvalue_of_hasEigenvalue_compression_orthogonal_span_singleton {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] {A : E →L[𝕜] E} {u : E} {lam μ : 𝕜} (hu : u ≠ 0) (hAu : A u = lam • u) (hμ : Module.End.HasEigenvalue (↑(A.compression (𝕜 ∙ u)ᗮ.subtypeL)) μ) : Module.End.HasEigenvalue (↑A) μ

If u is an eigenvector of A, with eigenvalue λ, then A is block upper triangular along E = 𝕜 u ⊕ u^⊥, so every eigenvalue of the compression of A to u^⊥ is an eigenvalue of A. An eigenvector k ∈ u^⊥ of the compression, with eigenvalue μ, gives the eigenvector u of A if μ = λ, and the eigenvector k + ⟪u, A k⟫ / (‖u‖² (μ - λ)) • u of A otherwise.