Section 5 — Q/X/XHat/P almost-projectivity

Almost-projective estimates for the rank-reduced Q family.

theorem MIPStarRE.LDT.MakingMeasurementsProjective.qAlmostProjective {Outcome : Type u_1} {ι : Type u_2} [Fintype ι] [DecidableEq ι] [Fintype Outcome] (ψ : QuantumState ι) (A : Measurement Outcome ι) (ζ : Error) (data : QLayerData Outcome ι) (hζ : 0 ≤ ζ) (hζ_small : ζ ≤ 1 / 4) : RankReductionWitness ψ A ζ data → ∑ a : Outcome, (Qa data a * QTotal data * Qa data a - Qa data a) ≤ (↑4 * ↑(spectralTruncationError ζ)) • 1

Q is almost projective (lem:q-almost-projective).

The rank-reduced family satisfies the operator inequality ∑_a (Q_a Q Q_a - Q_a) ≤ 4√ζ · I.