Compressed Resolvent Remainder

Abstract

A coisometric compression has a positive second-order resolvent remainder with a cubic gap bound.

Theorem 1.1 (The compressed resolvent has a positive cubic remainder).

$$\begin{array}{c}\forall K,R,E:\mathrm{Type},\\ [\mathrm{RCLike}(K)],[\mathrm{NormedAddCommGroup}(R)],[\mathrm{InnerProductSpace}(K,R)],[\mathrm{FiniteDimensional}(K,R)],\\ [\mathrm{NormedAddCommGroup}(E)],[\mathrm{InnerProductSpace}(K,E)],[\mathrm{FiniteDimensional}(K,E)],\\ F:\mathrm{ContinuousLinearMap}(K,R,E),S:\mathrm{ContinuousLinearMap}(K,R,R),a:\mathbb{R},u:\mathbb{R},\\ (F\circ F^{\ast }=I_E)\Rightarrow (\mathrm{IsSelfAdjoint}(S))\Rightarrow (0<a)\Rightarrow \\ (a\cdot I_R\le S)\Rightarrow (0\le u)\Rightarrow \\ P:=F^{\ast }\circ F,Q:=I_R-P,\\ A:=F\circ S\circ F^{\ast },delta:=\Vert F\circ S\circ Q\circ S\circ F^{\ast }\Vert ,\\ S_0:=P\circ S\circ P+Q\circ S\circ Q,V:=S-S_0,\\ R_u:=(S+u\cdot I_R{)}^{-1},R_u^0:=(S_0+u\cdot I_R{)}^{-1},\\ D_u:=F\circ R_u\circ F^{\ast }-(A+u\cdot I_E{)}^{-1},\\ (R_u-R_u^0=-((R_u^0\circ V\circ R_u^0))+R_u^0\circ V\circ R_u\circ V\circ R_u^0)\wedge \\ (D_u=(A+u\cdot I_E{)}^{-1}\circ F\circ S\circ Q\circ R_u\circ Q\circ S\circ F^{\ast }\circ (A+u\cdot I_E{)}^{-1})\wedge \\ (0\le D_u)\wedge \\ (\Vert D_u\Vert \le \frac{delta}{(a+u{)}^3}).\end{array}$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Dynamics/CompressedResolventRemainder.compressed_resolvent_remainder (✓ std3). ∎

Source. Repository-derived.

Commentary.

Let F be a coisometry between finite-dimensional real or complex inner-product spaces. Let S be self-adjoint with spectral floor a, where a is positive, and let the resolvent parameter u be nonnegative.

The block-diagonal part S0 is formed with the visible projection P and its orthogonal complement Q. Substituting the two inverse-difference identities into one another isolates the displayed second-order term.

Compression removes the first-order cross-block term. The remaining expression is an adjoint sandwich of the positive resolvent, while the two leakage factors and three inverse factors give the stated cubic estimate.

References

• Truth anchor: D5/S3/Quantum/Dynamics/CompressedResolventRemainder.compressed_resolvent_remainder
• Dependency: D5/S3/Observer/BlockStructure/FourBlockDecomposition