Preliminary completion lemmas

Structural completion helpers that stay close to completeAtOutcome while keeping only the light projectivity dependencies from SwitchSandwichPrep/Core.lean.

noncomputable def MIPStarRE.LDT.Preliminaries.completeAtOutcomeProj {Outcome : Type u_1} {ι : Type u_2} [Fintype Outcome] [Fintype ι] [DecidableEq ι] (P : ProjSubMeas Outcome ι) (a0 : Outcome) : ProjMeas Outcome ι

Completing a projective submeasurement at a distinguished outcome preserves projectivity. The residual effect 1 - P.total is a projection orthogonal to P.outcome a0, so the completed effect remains idempotent.

Equations

• MIPStarRE.LDT.Preliminaries.completeAtOutcomeProj P a0 = { toMeasurement := MIPStarRE.LDT.Preliminaries.completeAtOutcome P.toSubMeas a0, proj := ⋯ }

@[simp]

theorem MIPStarRE.LDT.Preliminaries.completeAtOutcomeProj_toMeasurement {Outcome : Type u_1} {ι : Type u_2} [Fintype Outcome] [Fintype ι] [DecidableEq ι] (P : ProjSubMeas Outcome ι) (a0 : Outcome) : (completeAtOutcomeProj P a0).toMeasurement = completeAtOutcome P.toSubMeas a0

@[simp]

theorem MIPStarRE.LDT.Preliminaries.completeAtOutcomeProj_toSubMeas {Outcome : Type u_1} {ι : Type u_2} [Fintype Outcome] [Fintype ι] [DecidableEq ι] (P : ProjSubMeas Outcome ι) (a0 : Outcome) : (completeAtOutcomeProj P a0).toSubMeas = (completeAtOutcome P.toSubMeas a0).toSubMeas