Documentation

MIPRE.Background.LIDT.Co.Preliminaries.Completion

Preliminary completion lemmas #

Structural completion helpers that stay close to completeAtOutcome while keeping only the light projectivity dependencies from SwitchSandwichPrep/Core.lean: the counterpart of MIPRE/Background/LIDT/MIPStarRE/LDT/Preliminaries/Completion.lean in the port of planning/c6b-plan.md (milestone M3, section "Port conventions").

The vendored declarations are about matrices Op ι and mention no state; here they are stated for any C*-algebra R with its order (local operators in 𝔓, joint ones in K →L[ℂ] K), the setting of the projective lemmas ProjSubMeas.outcome_mul_total_eq_outcome and ProjSubMeas.total_proj (Co/Basic/SubMeasurementCore.lean). The self-adjointness of a positive element is IsSelfAdjoint.of_nonneg, in place of the vendored positive semidefiniteness of matrices.

Not ported #

Every declaration of the vendored file has a counterpart here.

source
noncomputable def MIPRE.LIDT.Co.Preliminaries.completeAtOutcomeProj {R : Type u_1} [CStarAlgebra R] [PartialOrder R] [StarOrderedRing R] {Outcome : Type u_2} [Fintype Outcome] (P : ProjSubMeas Outcome R) (a0 : Outcome) :
ProjMeas Outcome R

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
Instances For
    source
    @[simp]
    theorem MIPRE.LIDT.Co.Preliminaries.completeAtOutcomeProj_toMeasurement {R : Type u_1} [CStarAlgebra R] [PartialOrder R] [StarOrderedRing R] {Outcome : Type u_2} [Fintype Outcome] (P : ProjSubMeas Outcome R) (a0 : Outcome) :
    (completeAtOutcomeProj P a0).toMeasurement = completeAtOutcome P.toSubMeas a0

    The underlying measurement of completeAtOutcomeProj P a0 is completeAtOutcome.

    source
    @[simp]
    theorem MIPRE.LIDT.Co.Preliminaries.completeAtOutcomeProj_toSubMeas {R : Type u_1} [CStarAlgebra R] [PartialOrder R] [StarOrderedRing R] {Outcome : Type u_2} [Fintype Outcome] (P : ProjSubMeas Outcome R) (a0 : Outcome) :
    (completeAtOutcomeProj P a0).toSubMeas = (completeAtOutcome P.toSubMeas a0).toSubMeas

    The underlying submeasurement of completeAtOutcomeProj P a0 is that of completeAtOutcome.