Robust Frame Bounds

Abstract

Weighted finite readouts have sharp spectral frame bounds.

Theorem 1.1 (Weighted readouts have sharp frame bounds).

$$\begin{array}{c}\forall d:\mathbb{N},\mathrm{NeZero}(d),I:Type,\mathrm{Fintype}(I),\\ w:I\to NNReal,E:I\to \mathrm{HermitianSpace}(d),\\ 1<d\Rightarrow \\ \mathrm{let}A:\mathrm{LinearMap}(\mathbb{R},\mathrm{traceZeroHermitian}(d),\mathrm{EuclideanSpace}(\mathbb{R},I)),A(D{)}_i:=\sqrt{w_i}⟨D,E_i{⟩}_{\mathbb{R}},\\ \alpha :=\mathrm{lambdaMin}(A^{\ast }A),\beta :=\mathrm{lambdaMax}(A^{\ast }A),\\ \kappa :=\frac{\mathrm{sigmaMax}(A)}{\mathrm{sigmaMin}(A)},\\ (\forall D:\mathrm{traceZeroHermitian}(d),\alpha {\Vert D\Vert }^2\le {\Vert A(D)\Vert }^2\wedge {\Vert A(D)\Vert }^2\le \beta {\Vert D\Vert }^2)\wedge \\ (\mathrm{Injective}(A)⟺0<\alpha )\wedge \\ \kappa =\sqrt{\frac{\beta }{\alpha }}.\end{array}$$

Proof. Machine-checked in Lean as D5/S3/Observer/Linear/RobustFrameBounds.robust_observer_frame_bounds (✓ std3). ∎

Source. Repository-derived.

Commentary.

Let d exceed one and let a finite index type label nonnegative weights and Hermitian effects. The analysis map sends a real trace-zero Hermitian perturbation to its weighted Hilbert–Schmidt effect coordinates.

The lower and upper constants are the least and greatest eigenvalues of the adjoint Gram operator. Expanding in its ordered orthonormal eigenbasis gives both quadratic frame bounds.

The least endpoint is positive exactly when the analysis map is injective. Squared singular values are the Gram eigenvalues, so the singular-value condition ratio is the square root of the endpoint ratio.

The dimension premise excludes d equal to one, whose trace-zero Hermitian carrier has dimension zero and therefore has no least Gram eigenvalue in the source construction.

References

• Truth anchor: D5/S3/Observer/Linear/RobustFrameBounds.robust_observer_frame_bounds
• Dependency: D5/S3/Quantum/Tomography/InformationalCompletenessEquivalence