Section 5 — restriction of completed projective submeasurements

The elementary order algebra used after applying the orthonormalization theorem to the option completion of a submeasurement: the counterpart of MIPRE/Background/LIDT/MIPStarRE/LDT/MakingMeasurementsProjective/Orthonormalization/RestrictSome.lean in the port of planning/c6b-plan.md (milestone M8, section "Port conventions").

The restriction mentions no state and is generic over an ordered ⋆-ring. It was written in milestone M2 for Theorem G (Co/Doubling/Orthonormalization.lean) and lives here, its vendored home. Unlike the vendored file, this one does not import Statements.lean: the restriction needs only the submeasurement structures.

Not ported

Every declaration of the vendored file has a counterpart here.

def MIPRE.LIDT.Co.MakingMeasurementsProjective.restrictSomeProjSubMeas {R : Type u_1} [Ring R] [StarRing R] [PartialOrder R] [StarOrderedRing R] {Outcome : Type u_2} [Fintype Outcome] (P : ProjSubMeas (Option Outcome) R) : ProjSubMeas Outcome R

The outcomes some a of a projective submeasurement on Option Outcome, a projective submeasurement (the vendored restrictSomeProjSubMeas): the fresh outcome none is discarded.

Equations

• One or more equations did not get rendered due to their size.