Conditioning Trace-Distance Constant

Abstract

Positive conditioning filters have sharp trace-distance constant equal to the spectral condition number.

Definition 1.1 (The normalized conditioned state).

$$\mathrm{conditionedState}(h_d,R,h_R,\rho ):\mathrm{DensityState}(\mathrm{Fin}(d)):=\frac{((\mathrm{sqrt}(R)\cdot CStarMatrix.ofMatrix.symm(\mathrm{val}(\rho )))\cdot \mathrm{sqrt}(R))}{(\mathrm{Re}(\mathrm{Tr}(R\cdot CStarMatrix.ofMatrix.symm(\mathrm{val}(\rho )))))}.$$

Formalization. D5/S3/Quantum/Measurement/ConditioningTraceDistanceConstant.conditionedState (✓ std3).

Source. Repository-derived.

Commentary.

The bundled definition applies the positive filter on both sides, normalizes by its real trace, and returns a DensityState.

Theorem 1.2 (Conditioning has sharp constant equal to the condition number).

$$\forall d:\mathbb{N},h_d:2\le d,R:\mathrm{Matrix}(\mathrm{Fin}(d),\mathrm{Fin}(d),\mathbb{C}),h_R:\mathrm{PosDef}(R),\mathrm{let}(h_0:0<d)(\forall \rho :\mathrm{DensityState}(\mathrm{Fin}(d)),(\forall \sigma :\mathrm{DensityState}(\mathrm{Fin}(d)),(((\mathrm{inv}(\frac{\mathrm{greatestEigenvalue}(R,h_R)}{\mathrm{leastEigenvalue}(R,h_R)})\cdot \mathrm{traceDistance}(\rho ,\sigma ))\le \mathrm{traceDistance}(\mathrm{conditionedState}(h_0,R,h_R,\rho ),\mathrm{conditionedState}(h_0,R,h_R,\sigma ))\wedge \mathrm{traceDistance}(\mathrm{conditionedState}(h_0,R,h_R,\rho ),\mathrm{conditionedState}(h_0,R,h_R,\sigma ))\le (\frac{\mathrm{greatestEigenvalue}(R,h_R)}{\mathrm{leastEigenvalue}(R,h_R)}\cdot \mathrm{traceDistance}(\rho ,\sigma )))))\wedge (\forall \rho :\mathrm{DensityState}(\mathrm{Fin}(d)),((\mathrm{leastEigenvalue}(R,h_R)=\mathrm{greatestEigenvalue}(R,h_R)\Rightarrow \mathrm{conditionedState}(h_0,R,h_R,\rho )=\rho ))\wedge \mathrm{IsLUB}(\{x\mid \exists \rho :\mathrm{DensityState}(\mathrm{Fin}(d)),(\exists \sigma :\mathrm{DensityState}(\mathrm{Fin}(d)),((\rho \ne \sigma \wedge x=(\frac{\mathrm{traceDistance}(\mathrm{conditionedState}(h_0,R,h_R,\rho ),\mathrm{conditionedState}(h_0,R,h_R,\sigma ))}{\mathrm{traceDistance}(\rho ,\sigma )}))))\},\frac{\mathrm{greatestEigenvalue}(R,h_R)}{\mathrm{leastEigenvalue}(R,h_R)}))).$$

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

Source. Repository-derived.

Commentary.

For a positive definite filter in dimension at least two, canonical density states obey the two-sided trace-distance bound.

Equal extreme eigenvalues make the bundled conditioned state equal to the input, and the condition number is the least upper bound of all nontrivial conditioned-to-unconditioned ratios.

The scoped hypothesis h_0 : 0 < d is derived from h_d : 2 <= d and supplies every positivity proof argument in the displayed statement.

Here Fin d models the source support space H_P; the construction of H_P and R from a general instrument (Convention 26.1), and the exact values along the sharpness family, are not part of the statement.

References

• Truth anchor: D5/S3/Quantum/Measurement/ConditioningTraceDistanceConstant.conditionedState
• Truth anchor: D5/S3/Quantum/Measurement/ConditioningTraceDistanceConstant.conditioning_trace_distance_constant
• Dependency: D5/S3/Quantum/Measurement/BranchConditionedTraceDistance
• Dependency: D5/S3/Quantum/Measurement/ExactConditionalPreparationCost