Compressed Power Defect

Abstract

A coisometric compression has a quadratic power defect controlled by its two-step leakage.

Theorem 1.1 (Compressed powers have a binomial leakage bound).

$$\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),b:\mathbb{R},\\ F\circ F^{\ast }=I\Rightarrow \mathrm{IsSelfAdjoint}(S)\Rightarrow \Vert S\Vert \le b\Rightarrow \\ P:=F^{\ast }\circ F,Q:=I-P,\\ A:=F\circ S\circ F^{\ast },delta:=\Vert F\circ S\circ Q\circ S\circ F^{\ast }\Vert ,\\ (F\circ S^2\circ F^{\ast }-A^2=F\circ S\circ Q\circ S\circ F^{\ast })\wedge \\ (\forall n:\mathrm{Nat},2\le n\Rightarrow \Vert F\circ S^n\circ F^{\ast }-A^n\Vert \le \mathrm{choose}(n,2)\cdot b^{n-2}\cdot delta).\end{array}$$

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

Source. Repository-derived.

Commentary.

Let F be a coisometry between finite-dimensional real or complex inner-product spaces, and let S be a self-adjoint operator bounded in norm by b. The operator P = F*F is the visible projection and Q = I-P is its orthogonal complement.

The quadratic compression defect is exactly the path that leaves the visible subspace through Q and returns after the second application of S.

For every higher power, a commutator expansion controls hidden leakage at each possible crossing time. Iterating the resulting defect recursion sums these contributions to the binomial coefficient n choose 2.

References

• Truth anchor: D5/S3/Quantum/Dynamics/CompressedPowerDefect.compressed_power_defect
• Dependency: D5/S3/Observer/HiddenFlow/ProjectionCommutatorIdentity