Documentation

MIPRE.Background.LIDT.MIPStarRE.LDT.MakingMeasurementsProjective.Orthonormalization.RestrictSome

Section 5 — restriction of completed projective submeasurements #

This file contains the elementary order algebra used after applying the orthonormalization theorem to the option completion of a submeasurement.

source
noncomputable def MIPStarRE.LDT.MakingMeasurementsProjective.restrictSomeProjSubMeas {Outcome : Type u_1} {ι : Type u_2} [Fintype Outcome] [Fintype ι] [DecidableEq ι] (P : ProjSubMeas (Option Outcome) ι) :
ProjSubMeas Outcome ι

Discard the fresh none outcome from an option-indexed projective submeasurement. The remaining some a outcomes still form a projective submeasurement.

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