Fisher information and the qubit rank alternative

Abstract

Spectral SLD information bounds measurement Fisher information and controls the rank-one branch.

The first statement allows arbitrary finite matrix and outcome index sets n and J, including empty sets; Jm in the second is Fin m. PSD means positive semidefinite, 1n is the identity matrix, and all derivatives are real derivatives. C1(I) means continuously differentiable on I. spectralQFI is the spectral SLD information defined in ActualPureQubitGeometry; the displayed cost uses positivity at zero supplied by the hypotheses. The real rank is the dimension of the range of the real linear map effectReadout. Open refers to the ordinary topology of the real line.

Theorem 1.1 (Measurement Fisher lower bound).

$$\begin{array}{rl}& \forall n,J\mathrm{finite},N:J\to {\mathbb{C}}^{n\times n},\rho :\mathbb{R}\to {\mathbb{C}}^{n\times n},p,v:J\to \mathbb{R},\\ & (\forall j\in J,\mathrm{PSD}(N_j))\wedge \sum _{j\in J}{N}_j=1_n\wedge (\forall j\in J,0<p_j)\wedge \mathrm{DifferentiableAt}(\rho ,0)\\ & \wedge (\exists \delta >0,\forall u\in \mathbb{R},|u|<\delta ⟶\mathrm{PSD}(\rho (u)))\\ & \wedge (\exists {\delta }_2>0,\forall u\in \mathbb{R},|u|<{\delta }_2⟶\forall j\in J,\mathrm{Re}\mathrm{tr}(N_j\rho (u))=p_j+u{v}_j)\\ & ⟶\sum _{j\in J}\frac{v_j^2}{p_j}\le \mathrm{spectralQFI}(\rho (0),{\rho }^{\prime }(0))\end{array}$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Information/ActualPureQubitFisherRank.actual_fisher (✓ std3). ∎

Source. Repository-derived.

Commentary.

The two neighborhood hypotheses are two-sided at zero. The lower bound applies to the spectral information of the differentiable positive curve with the stated exact real-part readout.

Theorem 1.2 (Rank alternative and binary cost gap).

$$\begin{array}{rl}& \forall m\in \mathbb{N},N:J_m\to {\mathbb{C}}^{2\times 2},\rho :\mathbb{R}\to {\mathbb{C}}^{2\times 2},p,v:J_m\to \mathbb{R},I\subseteq \mathbb{R},\ell ,h\in J_m,\\ & \mathrm{Open}(I)\wedge 0\in I\wedge v\ne 0\wedge (\forall j\in J_m,0<p_j)\wedge (\forall j\in J_m,\mathrm{PSD}(N_j))\wedge \rho \in C^1(I)\\ & \wedge (\forall u\in I,\mathrm{PSD}(\rho (u))\wedge \mathrm{tr}(\rho (u))=1\wedge \rho (u{)}^2=\rho (u))\\ & \wedge (\forall u\in I,\forall j\in J_m,\mathrm{Re}\mathrm{tr}(N_j\rho (u))=p_j+u{v}_j)\wedge \frac{v_{\ell }}{p_{\ell }}<0\wedge 0<\frac{v_h}{p_h}\\ & ⟶{\mathrm{rank}}_{\mathbb{R}}(\mathrm{effectReadout}(N))=2\vee -\frac{v_{\ell }}{p_{\ell }}\frac{v_h}{p_h}\le \mathrm{spectralQFI}(\rho (0),{\rho }^{\prime }(0))\end{array}$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Information/ActualPureQubitFisherRank.actual_rank_alternative (✓ std3). ∎

Source. Repository-derived.

Commentary.

For every chosen negative-score index and positive-score index, the conclusion is the displayed disjunction. The hypotheses require positive effects but do not require their sum to be the identity or I to be preconnected.

References

• Truth anchor: D5/S3/Quantum/Information/ActualPureQubitFisherRank.actual_fisher
• Truth anchor: D5/S3/Quantum/Information/ActualPureQubitFisherRank.actual_rank_alternative
• Dependency: D5/S3/Quantum/Information/ActualPureQubitGeometry