Residual Tail Contraction for General Instruments

Abstract

The residual above the maximal fixed survival effect contracts geometrically, has a summable tail, and determines a unique dominated solution of the residual Poisson equation.

Theorem 1.1 (Geometric contraction and the residual Poisson solution).

$$\begin{gathered} \forall d:\mathbb{N},\alpha :\mathrm{Type},\iota :\mathrm{Type},[\mathrm{Fintype}(\alpha )],[\mathrm{Fintype}(\iota )], \\ Q:\alpha \to \mathrm{Matrix}(\mathrm{Fin}(d),\mathrm{Fin}(d),\mathbb{C}),L:\iota \to \mathrm{Matrix}(\mathrm{Fin}(d),\mathrm{Fin}(d),\mathbb{C}),F:\mathrm{Matrix}(\mathrm{Fin}(d),\mathrm{Fin}(d),\mathbb{C}), \\ \sum _{a\in \alpha }{Q}_a^{\ast }{Q}_a+\sum _{i\in \iota }{L}_i^{\ast }{L}_i=I\Rightarrow \underset{n\to \infty }{\lim }{S}_n=F\Rightarrow \\ (\forall n\in \mathbb{N},((S_n-F)={\mathcal{A}}^n((I-F)))\wedge (0\le (S_n-F)\le (I-F)))\wedge \\ (\exists M\in \mathbb{N},(1\le M)\wedge \exists q\in \mathbb{R},(0<q<1)\wedge \\ ((S_M-F)\le q(I-F))\wedge (\forall n\in \mathbb{N},(S_n-F)\le q^{\lfloor \frac{n}{M}\rfloor }(I-F))\wedge (\mathrm{Summable}(n\mapsto (S_n-F)))\wedge \\ \mathrm{let}(T:=\sum _{n=0}^{\infty }(S_n-F))((0\le T)\wedge (T\le \frac{M}{(1-q)}(I-F))\wedge (T-\mathcal{A}(T)=(I-F))\wedge \\ (\forall \rho :\mathrm{Matrix}(\mathrm{Fin}(d),\mathrm{Fin}(d),\mathbb{C}),(\mathrm{PosSemidef}(\rho ))\Rightarrow (\mathrm{Tr}(\rho )=1)\Rightarrow \mathrm{let}(r_{\rho }:=\mathrm{Re}\mathrm{Tr}(\rho (I-F)))(0<r_{\rho })\Rightarrow \frac{\mathrm{Re}\mathrm{Tr}(\rho T)}{r_{\rho }}\le \frac{M}{(1-q)})\wedge (\forall k\in \mathbb{N},(0\le (T-\sum _{n<kM}(S_n-F)))\wedge ((T-\sum _{n<kM}(S_n-F))\le \frac{(M{q}^k)}{(1-q)}(I-F)))\wedge \\ (\forall \rho :\mathrm{Matrix}(\mathrm{Fin}(d),\mathrm{Fin}(d),\mathbb{C}),(\mathrm{PosSemidef}(\rho ))\Rightarrow (\mathrm{Tr}(\rho )=1)\Rightarrow \mathrm{let}(r_{\rho }:=\mathrm{Re}\mathrm{Tr}(\rho (I-F)))(0<r_{\rho })\Rightarrow (\forall k\in \mathbb{N},0\le \frac{\mathrm{Re}\mathrm{Tr}(\rho (T-{\sum }_{n<kM}(S_n-F)))}{r_{\rho }}\le \frac{(M{q}^k)}{(1-q)}))\wedge (\forall X:\mathrm{Matrix}(\mathrm{Fin}(d),\mathrm{Fin}(d),\mathbb{C}),c:\mathbb{R},(X-\mathcal{A}(X)=(I-F))\Rightarrow (0\le X)\Rightarrow (X\le c(I-F))\Rightarrow X=T))). \end{gathered}$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Measurement/GeneralInstrumentResidualTailContraction.residual_tail_contraction (✓ std3). ∎

Source. Repository-derived.

Commentary.

Let A be the dual no-click map, let S_n be its n-fold action on the identity, and let F be the limiting survival effect. Write R = I - F and R_n = S_n - F. The residuals are positive, decrease in the Loewner order, and equal A^n(R).

When R is nonzero, finite-dimensional spectral comparison gives a block length M for which R_M is at most one strict scalar multiple of R. Positivity and monotonicity propagate this estimate to every residual, so the residual series is summable and its block tails obey a geometric bound. When R is zero, all residuals and their sum vanish, and M = 1 and q = 1/2 give the same conclusions.

The sum T of the residuals is positive, is bounded by the corresponding geometric majorant, and satisfies T - A(T) = R. Iterating the same equation shows that any positive solution dominated by a scalar multiple of R has a remainder tending to zero, and therefore equals T.

For every positive trace-one matrix whose residual weight is positive, taking the trace against the operator bounds gives the normalized bound for T and the normalized geometric bound for every truncated tail.

References

• Truth anchor: D5/S3/Quantum/Measurement/GeneralInstrumentResidualTailContraction.residual_tail_contraction
• Dependency: D5/S3/Quantum/Measurement/GeneralInstrumentSurvivalLimit